blob: 4f3416693452c74849bd2c3b5b5762ed221ee5e6 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
{-# 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
|
