aboutsummaryrefslogtreecommitdiff
path: root/src/AST/Env.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/AST/Env.hs')
-rw-r--r--src/AST/Env.hs59
1 files changed, 0 insertions, 59 deletions
diff --git a/src/AST/Env.hs b/src/AST/Env.hs
deleted file mode 100644
index 4f34166..0000000
--- a/src/AST/Env.hs
+++ /dev/null
@@ -1,59 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE EmptyCase #-}
-{-# LANGUAGE ExplicitForAll #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE StandaloneDeriving #-}
-{-# LANGUAGE TypeOperators #-}
-module AST.Env where
-
-import AST.Weaken
-import Data
-
-
--- | @env'@ is a subset of @env@: each element of @env@ is either included in
--- @env'@ ('SEYes') or not included in @env'@ ('SENo').
-data Subenv env env' where
- SETop :: Subenv '[] '[]
- 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'
-subList SNil SETop = SNil
-subList (SCons x xs) (SEYes sub) = SCons x (subList xs sub)
-subList (SCons _ xs) (SENo sub) = subList xs sub
-
-subenvAll :: SList f env -> Subenv env env
-subenvAll SNil = SETop
-subenvAll (SCons _ env) = SEYes (subenvAll env)
-
-subenvNone :: SList f env -> Subenv env '[]
-subenvNone SNil = SETop
-subenvNone (SCons _ env) = SENo (subenvNone env)
-
-subenvOnehot :: SList f env -> Idx env t -> Subenv env '[t]
-subenvOnehot (SCons _ env) IZ = SEYes (subenvNone env)
-subenvOnehot (SCons _ env) (IS i) = SENo (subenvOnehot env i)
-subenvOnehot SNil i = case i of {}
-
-subenvCompose :: Subenv env1 env2 -> Subenv env2 env3 -> Subenv env1 env3
-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