{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedRecordUpdate #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ImplicitPrelude #-}
{-# OPTIONS_GHC -Wall -Wno-unused-imports 
    -fno-show-error-context -fprint-explicit-kinds #-}

module Corecords where

import Data.Bool (bool)
import Data.Coerce (coerce)
import Data.Kind (Constraint, Type)
import Data.SOP (NP (..), Proxy (Proxy))
import GHC.TypeLits (Symbol)

-- The following machinery makes this possible:
--
-- named arguments to a "normal" function using recordupdate syntax
--
-- >>> ex
-- 65.7
ex :: Double
ex = exp' {base = 3, exponent = 2, coefficient = 7.3}

exp' :: Double :# "coefficient" -> Double :# "base" -> Int :# "exponent" -> Double
exp' a b x = unTag a * (unTag b ^ unTag x)

-- It can also pick out arguments that are named from the function
namedPlus3 :: Int -> Int :# "arg1" -> String -> Bool :# "arg2" -> Int :# "arg3" -> Int
namedPlus3 d a a' b c = fromIntegral $ unTag a + bool 42 69 (unTag b) - unTag c + length a' + d

np3 :: Int :# "arg1" -> Int -> [Char] -> Int
np3 = namedPlus3 {arg3 = 4, arg2 = True}

type (:#) :: Type -> Symbol -> Type
newtype t :# s = Tag {unTag :: t}
  deriving stock (Eq, Ord, Show)

type NamedArgs :: Type -> [(Type, Symbol)]
type family NamedArgs f where
  -- we care about the arguents that have an annotation
  NamedArgs (typ :# s -> r) = '(typ, s) : NamedArgs r
  -- we don't care about the rest of the function
  NamedArgs (typ -> r) = NamedArgs r
  -- we have reached the tail which is not a function
  NamedArgs r = '[]

type RestOfFunction :: Type -> Type
type family RestOfFunction f where
  -- discard the named arg
  RestOfFunction (typ :# s -> r) = RestOfFunction r
  -- keep the unnamed args
  RestOfFunction (typ -> r) = typ -> RestOfFunction r
  -- reached the end
  RestOfFunction r = r

type Snd :: (a, b) -> b
type family Snd tup where
  Snd '(a, b) = b

type Fst :: (a, b) -> a
type family Fst tup where
  Fst '(a, b) = a

type Named :: (Type, Symbol) -> Type
newtype Named tup = MkNamed {unNamed :: Fst tup}

class RewriteToCurried a where
  collectNamedArgs :: a -> NP Named (NamedArgs a) -> RestOfFunction a

instance (RewriteToCurried r) => RewriteToCurried (typ :# s -> r) where
  collectNamedArgs f (x :* xs) = collectNamedArgs (f (coerce x)) xs

instance
  {-# OVERLAPPABLE #-}
  ( RewriteToCurried r
  , RestOfFunction (s -> r) ~ (s -> RestOfFunction r)
  , NamedArgs (s -> r) ~ NamedArgs r
  )
  => RewriteToCurried (s -> r)
  where
  collectNamedArgs f xs x = collectNamedArgs @r (f x) xs

instance
  {-# OVERLAPPABLE #-}
  ( NamedArgs r ~ '[] -- this is kinda suspicious, we don't need the fact that we're matching on Nil
  , RestOfFunction r ~ r
  )
  => RewriteToCurried r
  where
  collectNamedArgs f _ = f

type SetField :: Symbol -> Type -> [(Type, Symbol)] -> Constraint
class SetField name a xs | xs -> a name where
  setField' :: forall r. (NP Named xs -> r) -> a -> NP Named (Removed name a xs) -> r

type Removed :: Symbol -> Type -> [(Type, Symbol)] -> [(Type, Symbol)]
type family Removed name a xs where
  Removed name a '[] = '[]
  Removed name a ('(b, name) : xs) = xs
  Removed name a ('(b, other) : xs) = ('(b, other) : Removed name a xs)

instance {-# OVERLAPPING #-} (a ~ b) => SetField name a ('(b, name) : xs) where
  setField' f a xs = f (MkNamed a :* xs)

instance (SetField name a xs, Removed name a ('(b, other) : xs) ~ '(b, other) : Removed name a xs) => SetField name a ('(b, other) : xs) where
  setField' f a = \case
    (x :* xs) -> setField' @name @a @xs (\ys -> f (x :* ys)) a xs

class ExpandArgs xs r where
  type Expanded xs r :: Type
  expandArgs :: (NP Named xs -> r) -> Expanded xs r

instance ExpandArgs '[] r where
  type Expanded '[] r = r
  expandArgs f = f Nil

instance (ExpandArgs xs r) => ExpandArgs ('(typ, name) : xs) r where
  type Expanded ('(typ, name) : xs) r = typ :# name -> Expanded xs r
  expandArgs f n = expandArgs @xs @r \xs -> f (coerce n :* xs)

getField :: a
getField = undefined

setField
  :: forall name infn field
   . ( ExpandArgs (Removed name field (NamedArgs infn)) (RestOfFunction infn)
     , SetField name field (NamedArgs infn)
     , RewriteToCurried infn
     )
  => infn
  -> field
  -> Expanded (Removed name field (NamedArgs infn)) (RestOfFunction infn)
setField fn a = expandArgs (setField' @name (collectNamedArgs fn) a)

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE BlockArguments #-}
module ScopedCont2 where

import System.IO qualified
import Control.Monad.Codensity
import UnliftIO (MonadIO, IOMode (WriteMode), liftIO)
import Data.Kind
import Control.Monad.Trans (MonadTrans, lift)

newtype SCod s (m :: k -> Type) a = MkSCod {unSCod :: forall b. (a -> m b) -> m b}
  deriving (Functor, Applicative, Monad) via (Codensity m)
  deriving MonadTrans via Codensity

instance MonadIO m => MonadIO (SCod s m) where 
  liftIO = lift . liftIO


runSCod :: (Applicative m) => (forall s. SCod s m r) -> m r
runSCod k = unSCod k pure

data Handle s = MkHandle {handleName :: String, unsafeGetHandle :: System.IO.Handle}

withFile :: FilePath -> System.IO.IOMode -> SCod s IO (Handle s)
withFile fp md = MkSCod (\k -> putStrLn ("allocating " <> fp) *> System.IO.withFile fp md (k . MkHandle fp) <* putStrLn ("deallocated " <> fp))

hPutStrLn :: Handle s -> String -> SCod s IO ()
hPutStrLn (MkHandle fp hdl) s = liftIO $ putStrLn ("writing to handle " <> fp) *> System.IO.hPutStrLn hdl s <* putStrLn ("wrote to handle " <> fp)

scoped :: Monad m => (forall s. SCod s m r) -> SCod s' m r
scoped act = lift (runSCod act)

x :: IO ()
x = runSCod do
  bla <- withFile "bla" WriteMode
  hPutStrLn bla "test"
  scoped do 
    foo <- withFile "foo" WriteMode
    hPutStrLn foo "woop"
  blup <- withFile "blup" WriteMode
  hPutStrLn blup "test2"

-- z :: IO (String -> IO ())
-- z = runSCod do 
--   hdl <- withFile "bla" WriteMode
--   pure (hPutStrLn hdl)


{-
allocating bla
writing to handle bla
wrote to handle bla
allocating foo
writing to handle foo
wrote to handle foo
deallocated foo
allocating blup
writing to handle blup
wrote to handle blup
deallocated blup
deallocated bla
-}

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE BlockArguments #-}
module ScopedCont where

import System.IO qualified
import Control.Monad.Codensity
import UnliftIO (MonadIO, IOMode (WriteMode), liftIO)
import Data.Kind
import Control.Monad.Trans (MonadTrans, lift)

newtype SCod s (m :: k -> Type) a = MkSCod {unSCod :: forall b. (a -> m b) -> m b}
  deriving (Functor, Applicative, Monad) via (Codensity m)
  deriving MonadTrans via Codensity

instance MonadIO m => MonadIO (SCod s m) where 
  liftIO = lift . liftIO


runSCod :: (Applicative m) => (forall s. SCod s m r) -> m r
runSCod k = unSCod k pure

data Handle s = MkHandle {handleName :: String, unsafeGetHandle :: System.IO.Handle}

withFile :: FilePath -> System.IO.IOMode -> SCod s IO (Handle s)
withFile fp md = MkSCod (\k -> putStrLn ("allocating " <> fp) *> System.IO.withFile fp md (k . MkHandle fp) <* putStrLn ("deallocated " <> fp))

hPutStrLn :: Handle s -> String -> IO ()
hPutStrLn (MkHandle fp hdl) s = putStrLn ("writing to handle " <> fp) *> System.IO.hPutStrLn hdl s <* putStrLn ("wrote to handle " <> fp)

scoped :: Monad m => (forall s. SCod s m r) -> SCod s' m r
scoped act = lift (runSCod act)

x :: IO ()
x = runSCod do
  bla <- withFile "bla" WriteMode
  liftIO $ hPutStrLn bla "test"
  scoped do 
    foo <- withFile "foo" WriteMode
    liftIO $ hPutStrLn bla "test3!"
    liftIO $ hPutStrLn foo "woop"
  blup <- withFile "blup" WriteMode
  liftIO $ hPutStrLn blup "test2"

{-
allocating bla
writing to handle bla
wrote to handle bla
allocating foo
writing to handle bla
wrote to handle bla
writing to handle foo
wrote to handle foo
deallocated foo
allocating blup
writing to handle blup
wrote to handle blup
deallocated blup
deallocated bla
-}

{-# HLINT ignore "Unused LANGUAGE pragma" #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE TypeAbstractions #-}
{-# HLINT ignore "Unused LANGUAGE pragma" #-}
{-# LANGUAGE TypeData #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wall -Wno-unrecognised-pragmas -fno-show-error-context #-}

module PatternCinnamons where

import Data.Char
import Data.Dynamic

type data N = Z | S N

data SN (n :: N) where SZ :: SN Z; SN :: SN n -> SN (S n)

data V (n :: N) a where
  Nil :: V Z a
  (:::) :: a -> V n a -> V (S n) a

pattern SV :: forall n a. forall. n ~ S Z => a -> V n a
pattern SV a <- a ::: Nil
  where
    SV a = a ::: Nil

x :: V n a -> SN n
x = \case
  Nil -> SZ
  SV _ -> (SN SZ)
  (_ ::: xs) -> SN (x xs)

pattern TypeIs :: forall b. Typeable b => forall a. a ~ b => a -> Dynamic
pattern TypeIs x <- (fromDynamic -> Just x)
  where
    TypeIs a = toDyn a

-- >>> y (toDyn False)
-- 0
-- >>> y (TypeIs (4 :: Int))
-- 4
-- >>> y (toDyn (Just 'x'))
-- 120
-- >>> y (toDyn (Nothing :: Maybe Char))
-- 9
-- >>> y (toDyn True)
-- 2
y :: Dynamic -> Int
y = \case
  TypeIs @Int a -> a
  TypeIs @Bool True -> 2
  TypeIs @(Maybe Char) (Just c) -> ord c
  TypeIs @(Maybe Char) Nothing -> 9
  _ -> 0

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}

module Main where

import UnliftIO
import UnliftIO.Concurrent

-- | @'pooledConcurrentlyCatchN' n jobs@ enqueues @n@ jobs at a time and returns a (potentially unordered) list of
-- results of these jobs running to end
pooledConcurrentlyCatchN :: (MonadUnliftIO m) => Int -> [m a] -> m [Either SomeException a]
pooledConcurrentlyCatchN n jobs = do
  sem <- newQSem n
  go sem [] jobs
 where
  go _ acc [] = traverse waitCatch acc
  go sem acc (job : jobs) = do
    as <- do
      waitQSem sem
      async do
        job `finally` signalQSem sem
    go sem (as : acc) jobs

-- | like 'pooledConcurrentlyCatchN' but rethrows the first exception to occur after running all jobs to end
pooledConcurrentlyN :: (MonadUnliftIO m) => Int -> [m a] -> m [a]
pooledConcurrentlyN n jobs =
  pooledConcurrentlyCatchN n jobs >>= traverse \case
    Left ex -> throwIO ex
    Right a -> pure a

-- | like 'pooledConcurrentlyCatchN' but uses exactly the amount of available capabilities
pooledConcurrentlyCatch :: (MonadUnliftIO m) => [m a] -> m [Either SomeException a]
pooledConcurrentlyCatch jobs = do
  caps <- getNumCapabilities
  pooledConcurrentlyCatchN caps jobs

-- | like 'pooledConcurrentlyN' but uses exactly the amount of available capabilities
pooledConcurrently :: (MonadUnliftIO m) => [m a] -> m [a]
pooledConcurrently jobs = do
  caps <- getNumCapabilities
  pooledConcurrentlyN caps jobs

-- example
main :: IO ()
main = do
  setNumCapabilities 2
  print =<< getNumCapabilities
  print =<< pooledConcurrentlyCatch (threads [n ^ 2 | n <- [10, 5, 1]])
 where
  threads = map \n -> do
    tid <- myThreadId
    let m = n * 100_000
    putStrLn (show tid <> ": sleeping " <> show m)
    threadDelay m
    putStrLn (show tid <> ": waking up")
    pure n

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedRecordDot #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}

import Control.Algebra
import Control.Carrier.Reader
import Control.Monad (void)
import Control.Monad.IO.Class
import Data.Foldable (for_)
import Data.Kind
import UnliftIO

newtype LHEnv p = LHEnv {lhHandlers :: [p -> IO ()]}

data Log p m k where
  WithLogEnv :: (LHEnv p -> LHEnv p) -> m a -> Log p m a
  WriteLog :: p -> Log p m ()

withLogEnv :: (Has (Log p) sig m) => (LHEnv p -> LHEnv p) -> m a -> m a
withLogEnv f act = send (WithLogEnv f act)

writeLog :: (Has (Log p) sig m) => p -> m ()
writeLog i = send (WriteLog i)

newtype LogConcurrentlyC p m (a :: Type) = MkLogConcurrentlyC {runLogConcurrentlyC :: LHEnv p -> m a}
  deriving (Functor, Applicative, Monad, MonadIO, MonadUnliftIO) via ReaderC (LHEnv p) m

runLogConcurrently :: LHEnv p -> LogConcurrentlyC p m a -> m a
runLogConcurrently = flip runLogConcurrentlyC

instance (Algebra sig m, MonadIO m) => Algebra (Log p :+: sig) (LogConcurrentlyC p m) where
  alg hdl sig ctx = MkLogConcurrentlyC \env -> case sig of
    L (WithLogEnv f m) -> runLogConcurrently (f env) (hdl (m <$ ctx))
    L (WriteLog x) ->
      ctx <$ liftIO do
        void $ async $ forConcurrently_ env.lhHandlers \logger ->
          logger x
    R other -> alg (runLogConcurrently env . hdl) other ctx

newtype LogSyncC p m (a :: Type) = MkLogSyncC {runLogSyncC :: LHEnv p -> m a}
  deriving (Functor, Applicative, Monad, MonadIO, MonadUnliftIO) via ReaderC (LHEnv p) m

runLogSync :: LHEnv p -> LogSyncC p m a -> m a
runLogSync = flip runLogSyncC

instance (Algebra sig m, MonadIO m) => Algebra (Log p :+: sig) (LogSyncC p m) where
  alg hdl sig ctx = MkLogSyncC \env -> case sig of
    L (WithLogEnv f m) -> runLogSync (f env) (hdl (m <$ ctx))
    L (WriteLog x) ->
      ctx <$ liftIO do
        for_ env.lhHandlers \logger ->
          logger x
    R other -> alg (runLogSync env . hdl) other ctx

newtype LogRefC p m (a :: Type) = MkLogRefC {runLogRefC :: IORef [p] -> m a}
  deriving (Functor, Applicative, Monad, MonadIO, MonadUnliftIO) via ReaderC (IORef [p]) m

runLogRef :: (MonadIO m) => LogRefC p m a -> m ([p], a)
runLogRef act = do
  ref <- newIORef []
  res <- runLogRefC act ref
  logs <- reverse <$> readIORef ref
  pure (logs, res)

instance (Algebra sig m, MonadIO m) => Algebra (Log p :+: sig) (LogRefC p m) where
  alg hdl sig ctx = MkLogRefC \ref -> case sig of
    L (WithLogEnv _f m) -> runLogRefC (hdl (m <$ ctx)) ref
    L (WriteLog x) ->
      ctx <$ liftIO do modifyIORef ref (x :)
    R other -> alg (flip runLogRefC ref . hdl) other ctx

{-# LANGUAGE BlockArguments #-}

module Parse where

import Options.Applicative

main :: IO ()
main = do
  parsed :: Either () () <- execParser do
    let p = pure (Left ()) <|> subparser do command "bla" (info (pure (Right ())) briefDesc)
    info p briefDesc
  case parsed of
    Left _ -> putStrLn "no arg"
    Right _ -> putStrLn "had arg"

programs.neovim.package = pkgs.neovim-unwrapped.overrideAttrs (old: {
  patches = old.patches or [] ++ [
    (pkgs.fetchpatch {
      name = "strip-consecutive-white-spaces.patch"; 
      url = "https://github.com/mangoiv/neovim/commit/ea0a9163cb37e8444465b81abbed82c54134c12e.patch"; 
      hash = "sha256-LQwS+yJucin5AlXTPa3O95Zwjw4RerniPtNT8ctw0AU=";
    })
  ];
});

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverloadedRecordUpdate #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}

module RecordUpdate where

import Data.Kind (Type)
import Data.Type.Bool (type (||))
import GHC.Generics
import GHC.TypeError (ErrorMessage (..), TypeError)
import GHC.TypeLits (Symbol)
import Prelude

class GHasField (name :: k) (recordRep :: Type -> Type) (field :: Type) | name recordRep -> field where
  gGetField :: recordRep a -> field
  gSetField :: recordRep a -> field -> recordRep a

--------------------------------------------------------------------------------
-- threading through constructors and type names
--------------------------------------------------------------------------------
instance (GHasField n k f) => GHasField n (C1 m k) f where
  gGetField = gGetField @_ @n . unM1
  gSetField x a = M1 $ gSetField @_ @n (unM1 x) a

instance (GHasField n k f) => GHasField n (D1 m k) f where
  gGetField = gGetField @_ @n . unM1
  gSetField x a = M1 $ gSetField @_ @n (unM1 x) a

--------------------------------------------------------------------------------
-- threading through sum and product
--------------------------------------------------------------------------------

-- this seems a bit wonky, perhaps could be improved
type IsInRemaining :: Symbol -> (Type -> Type) -> Bool
type family IsInRemaining n f where
  IsInRemaining n (k1 :*: k2) = CheckField n k1 || IsInRemaining n k2
  IsInRemaining n (M1 s m k) = CheckField n (M1 s m k)
  IsInRemaining n f = TypeError (Text "unexpected type " :<>: ShowType f :<>: Text "on lhs of IsInRemaining")

type CheckField :: Symbol -> (Type -> Type) -> Bool
type family CheckField n f where
  CheckField n (S1 (MetaSel (Just n) su ss l) a) = 'True
  CheckField n (S1 (MetaSel (Just n') su ss l) a) = 'False

class GHasField' b n t f | b n t -> f where
  gGetField' :: t a -> f
  gSetField' :: t a -> f -> t a

instance (GHasField n t f) => GHasField' False n (t :*: r) f where
  gGetField' (l :*: _r) = gGetField @_ @n l
  gSetField' (l :*: r) f = gSetField @_ @n l f :*: r

instance (GHasField n r f) => GHasField' True n (t :*: r) f where
  gGetField' (_l :*: r) = gGetField @_ @n r
  gSetField' (l :*: r) f = l :*: gSetField @_ @n r f

instance (GHasField' (IsInRemaining n r) n (t :*: r) f) => GHasField n (t :*: r) f where
  gGetField = gGetField' @(IsInRemaining n r) @n
  gSetField = gSetField' @(IsInRemaining n r) @n

--------------------------------------------------------------------------------
-- we want a nice error message if that didn't work out
--------------------------------------------------------------------------------
instance GHasField n (S1 (MetaSel (Just n) su ss l) (K1 i f)) f where
  gGetField = unK1 . unM1
  gSetField _x a = M1 $ K1 a

--------------------------------------------------------------------------------
-- the actual definitions
--------------------------------------------------------------------------------
getField :: forall {k} (name :: k) (record :: Type) (field :: Type). (Generic record, GHasField name (Rep record) field) => record -> field
getField rec = gGetField @k @name @(Rep record) @field (from @record rec)

setField :: forall {k} (name :: k) (record :: Type) (field :: Type). (Generic record, GHasField name (Rep record) field) => record -> field -> record
setField r = to . gSetField @k @name @(Rep record) @field (from r)

data A = MkA {b :: Bool, a :: Int}
  deriving stock (Eq, Ord, Show, Generic)

data B = MkB {b :: Bool, c :: Int, a :: Int}
  deriving stock (Eq, Ord, Show, Generic)

u :: B -> Int -> B
u a i = a {a = i}

{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module GCurry where

import Data.Kind (Type)
import Generics.SOP
import Prelude hiding (curry)

-- >>> curry (\(x, y, z) -> x + y + z) 5 6 7
-- 18
curry :: forall a xs b. (Generic a, Code a ~ '[xs]) => (a -> b) -> Curry xs b
curry f = mk (f . to . SOP . Z)
 where
  mk :: forall ys. (All Top ys) => (NP I ys -> b) -> Curry ys b
  mk g = case sList @ys of
    SNil -> g Nil
    SCons -> \x -> mk \rest -> g (I x :* rest)

type family Curry xs b where
  Curry '[] b = b
  Curry (x : xs) b = x -> Curry xs b

module CheckInitialized where

import Data.IORef
import System.IO.Unsafe (unsafePerformIO)

doInit :: IO ()
doInit = putStrLn "initializing"

{-# NOINLINE initStatus #-}
initStatus :: IORef Bool
initStatus = unsafePerformIO (newIORef False)

checkInit :: IO ()
checkInit = do
  initialized <- readIORef initStatus
  if initialized
    then putStrLn "already initialized"
    else doInit *> writeIORef initStatus True

-- this is some function in libsodium-bindings
fn :: IO ()
fn = do
  checkInit
  -- do something else

-- this is some downstream program using the bindings
main :: IO () 
main = do 
  fn 
  fn 
  fn