{-# 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