diff options
Diffstat (limited to 'src/AST/Env.hs')
| -rw-r--r-- | src/AST/Env.hs | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/src/AST/Env.hs b/src/AST/Env.hs index c33bad3..4f34166 100644 --- a/src/AST/Env.hs +++ b/src/AST/Env.hs @@ -1,5 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} +{-# LANGUAGE ExplicitForAll #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE StandaloneDeriving #-} @@ -14,8 +15,8 @@ import Data -- @env'@ ('SEYes') or not included in @env'@ ('SENo'). data Subenv env env' where SETop :: Subenv '[] '[] - SEYes :: Subenv env env' -> Subenv (t : env) (t : env') - SENo :: Subenv env env' -> Subenv (t : env) env' + SEYes :: forall t env env'. Subenv env env' -> Subenv (t : env) (t : env') + SENo :: forall t env env'. Subenv env env' -> Subenv (t : env) env' deriving instance Show (Subenv env env') subList :: SList f env -> Subenv env env' -> SList f env' @@ -41,3 +42,18 @@ subenvCompose SETop SETop = SETop subenvCompose (SEYes sub1) (SEYes sub2) = SEYes (subenvCompose sub1 sub2) subenvCompose (SEYes sub1) (SENo sub2) = SENo (subenvCompose sub1 sub2) subenvCompose (SENo sub1) sub2 = SENo (subenvCompose sub1 sub2) + +subenvConcat :: Subenv env1 env1' -> Subenv env2 env2' -> Subenv (Append env2 env1) (Append env2' env1') +subenvConcat sub1 SETop = sub1 +subenvConcat sub1 (SEYes sub2) = SEYes (subenvConcat sub1 sub2) +subenvConcat sub1 (SENo sub2) = SENo (subenvConcat sub1 sub2) + +sinkWithSubenv :: Subenv env env' -> env0 :> Append env' env0 +sinkWithSubenv SETop = WId +sinkWithSubenv (SEYes sub) = WSink .> sinkWithSubenv sub +sinkWithSubenv (SENo sub) = sinkWithSubenv sub + +wUndoSubenv :: Subenv env env' -> env' :> env +wUndoSubenv SETop = WId +wUndoSubenv (SEYes sub) = WCopy (wUndoSubenv sub) +wUndoSubenv (SENo sub) = WSink .> wUndoSubenv sub |