{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Control.Static.Closure where
import Data.Constraint (Dict (..))
import Data.Functor (($>))
import Data.Kind (Constraint)
import Data.Singletons.Prelude
import Data.Singletons.TH (genDefunSymbols)
import Control.Static.Common
import Control.Static.Serialise
import Control.Static.Static
type ClosureFunc cxt env arg res = CxtW cxt (env -> arg -> res)
type ClosureApply g = SKeyedExt g
applyClosure
:: RepVal g arg k
=> SKeyed k (CxtW cxt (env -> arg -> res))
-> arg
-> ClosureApply g
applyClosure (SKeyed k cl) arg = toSKeyedExt (SKeyed k arg)
envTabCons
:: SKeyed k (CxtW cxt (env -> arg -> res))
-> env
-> TTab kk vv
-> TTab (k ': kk) (env ': vv)
envTabCons cl env = skeyedCons (cl $> env)
envTabNil :: TTab '[] '[]
envTabNil = TCNil @NullC2Sym0
class Closure (Part pcl) => PreClosure pcl where
type Cxt pcl :: Constraint
type Env pcl
type Part pcl
applyPre :: Cxt pcl => pcl -> Env pcl -> Part pcl
instance PreClosure (CxtW c (e -> v -> r)) where
type Cxt (CxtW c (e -> v -> r)) = c
type Env (CxtW c (e -> v -> r)) = e
type Part (CxtW c (e -> v -> r)) = v -> r
applyPre (CxtW pcl) = pcl
class Closure cl where
type Arg cl
type Res cl
apply :: cl -> Arg cl -> Res cl
instance Closure (v -> r) where
type Arg (v -> r) = v
type Res (v -> r) = r
apply = ($)
class PostClosure x f where
type Pre f
applyPost :: f -> Pre f -> x
instance PostClosure x (r -> x) where
type Pre (r -> x) = r
applyPost = ($)
genDefunSymbols [''Cxt, ''Env, ''Part, ''Arg, ''Res, ''Pre]
type ResCont x = TyContSym1 x .@#@$$$ ResSym0
applyClosureTabPre
:: forall c1 kk vv
. ConstrainList (Fmap CxtSym0 vv)
=> TCTab' PreClosure kk vv
-> TCTab c1 kk (Fmap EnvSym0 vv)
-> TCTab' Closure kk (Fmap PartSym0 vv)
applyClosureTabPre tab env =
zipWith3TC @_ @_ @_ @_ @_ @(DictOf CxtSym0) @EnvSym0 @PartSym0 tab cxt env
$ \_ cl _ Dict _ e -> (applyPre cl e, Dict)
where cxt = toTCDict @_ @_ @CxtSym0 tab
applyClosureTab
:: forall c1 kk vv
. TCTab' Closure kk vv
-> TCTab c1 kk (Fmap ArgSym0 vv)
-> TTab kk (Fmap ResSym0 vv)
applyClosureTab tab arg =
zipWithTC @_ @_ @_ @_ @ArgSym0 @ResSym0 tab arg $ \_ cl _ a -> (apply cl a, Dict)
applyClosureTabPost
:: forall c0 kk rr x
. TCTab c0 kk rr
-> TCTab' (PostClosure x) kk (Fmap (TyContSym1 x) rr)
-> TTab kk (Fmap (ConstSym1 x) rr)
applyClosureTabPost res post =
zipWithTC @_ @_ @_ @_ @(TyContSym1 x) @(ConstSym1 x) res post
$ \_ r _ p -> (applyPost p r, Dict)
evalClosureTab
:: forall (kk :: [Symbol]) vv x
. TCTab' Closure kk vv
-> TTab kk (Fmap ArgSym0 vv)
-> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv)
-> TTab kk (Fmap (ConstSym1 x) vv)
evalClosureTab tab arg post =
zipWith3TC @_ @_ @_ @_ @_ @ArgSym0 @(ResCont x) @(ConstSym1 x) tab arg post
$ \_ cl _ a _ p -> (applyPost p (apply cl a), Dict)
mkClosureTab
:: forall c1 kk vv
. ConstrainList (Fmap CxtSym0 vv)
=> ConstrainList (ZipWith (ConstSym1 (TyCon1 PreClosure)) kk vv)
=> TTab kk vv
-> TCTab c1 kk (Fmap EnvSym0 vv)
-> TCTab' Closure kk (Fmap PartSym0 vv)
mkClosureTab = applyClosureTabPre . strengthenTC0
type RepClosure c g
= RepExtSym3
(AndC2 (ConstSym1 (TyCon1 Closure)) (FlipSym2 (.@#@$) ResSym0 .@#@$$$ c))
g
ArgSym0
type RepClosure' r g = RepClosure (ConstSym1 (TyCon1 ((~) r))) g
repClosureTab
:: forall c g (kk :: [Symbol]) vv
. ConstrainList (ZipWith (FlipSym2 (.@#@$) ResSym0 .@#@$$$ c) kk vv)
=> ConstrainList
(ZipWith (FlipSym1 (TyCon2 (RepVal g) .@#@$$$ ApplySym1 ArgSym0)) kk vv)
=> TCTab' Closure kk vv
-> TCTab (RepClosure c g) kk vv
repClosureTab = strengthenTC . strengthenTC
withEvalClosureCts
:: forall c g (k :: Symbol) (kk :: [Symbol]) vv x
. TCTab (RepClosure c g) kk vv
-> SKeyed k g
-> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv)
-> Either SKeyedError x
withEvalClosureCts tab val post = gwithStatic @_ @_ @(ResCont x) tab val post
$ \_ cont cl -> applyPost cont . apply cl
withEvalSomeClosureCts
:: forall c g (kk :: [Symbol]) vv x
. TCTab (RepClosure c g) kk vv
-> ClosureApply g
-> TCTab' (PostClosure x) kk (Fmap (ResCont x) vv)
-> Either SKeyedError x
withEvalSomeClosureCts tab ext post =
withSKeyedExt ext $ \val -> withEvalClosureCts tab val post
withEvalClosureCxt
:: forall c f g (k :: Symbol) (kk :: [Symbol]) vv r
. TCTab (RepClosure c g) kk vv
-> SKeyed k g
-> ( forall k' v
. 'Just '(k', v) ~ LookupKV k kk vv
=> ProofLookupKV f k kk vv
=> (c @@ k' @@ Res v) => Sing k' -> Res v -> r
)
-> Either SKeyedError r
withEvalClosureCxt tab val go =
withStaticCxt @_ @f tab val $ \k' cl a -> go k' (apply cl a)
withEvalSomeClosureCxt
:: forall c f g (kk :: [Symbol]) vv r
. TCTab (RepClosure c g) kk vv
-> ClosureApply g
-> ( forall k k' v
. 'Just '(k', v) ~ LookupKV k kk vv
=> ProofLookupKV f k kk vv
=> (c @@ k' @@ Res v) => Sing k' -> Res v -> r
)
-> Either SKeyedError r
withEvalSomeClosureCxt tab ext go = withSKeyedExt ext
$ \(val :: SKeyed k g) -> withEvalClosureCxt @_ @f tab val (go @k)
evalClosure
:: forall g (k :: Symbol) (kk :: [Symbol]) vv r
. TCTab (RepClosure' r g) kk vv
-> SKeyed k g
-> Either SKeyedError r
evalClosure tab val = withEvalClosureCxt tab val $ const id
evalSomeClosure
:: forall g (kk :: [Symbol]) vv r
. TCTab (RepClosure' r g) kk vv
-> ClosureApply g
-> Either SKeyedError r
evalSomeClosure tab ext = withSKeyedExt ext $ evalClosure tab