diff options
Diffstat (limited to 'src/CHAD/AST')
| -rw-r--r-- | src/CHAD/AST/Env.hs | 16 | ||||
| -rw-r--r-- | src/CHAD/AST/Weaken.hs | 22 |
2 files changed, 38 insertions, 0 deletions
diff --git a/src/CHAD/AST/Env.hs b/src/CHAD/AST/Env.hs index 8e6b745..8eb4f77 100644 --- a/src/CHAD/AST/Env.hs +++ b/src/CHAD/AST/Env.hs @@ -89,6 +89,22 @@ subenvMap _ SNil SETop = SETop subenvMap f (t `SCons` l) (SEYes s sub) = SEYes (f t s) (subenvMap f l sub) subenvMap f (_ `SCons` l) (SENo sub) = SENo (subenvMap f l sub) +subenvUnion :: Subenv env env1 -> Subenv env env2 + -> (forall env3. Subenv env env3 -> Subenv env3 env1 -> Subenv env3 env2 -> r) -> r +subenvUnion SETop SETop k = k SETop SETop SETop +subenvUnion (SEYesR sub1) (SEYesR sub2) k = + subenvUnion sub1 sub2 $ \sub3 sub31 sub32 -> + k (SEYesR sub3) (SEYesR sub31) (SEYesR sub32) +subenvUnion (SEYesR sub1) (SENo sub2) k = + subenvUnion sub1 sub2 $ \sub3 sub31 sub32 -> + k (SEYesR sub3) (SEYesR sub31) (SENo sub32) +subenvUnion (SENo sub1) (SEYes Refl sub2) k = + subenvUnion sub1 sub2 $ \sub3 sub31 sub32 -> + k (SEYesR sub3) (SENo sub31) (SEYesR sub32) +subenvUnion (SENo sub1) (SENo sub2) k = + subenvUnion sub1 sub2 $ \sub3 sub31 sub32 -> + k (SENo sub3) sub31 sub32 + subenvD2E :: Subenv env env' -> Subenv (D2E env) (D2E env') subenvD2E SETop = SETop subenvD2E (SEYesR sub) = SEYesR (subenvD2E sub) diff --git a/src/CHAD/AST/Weaken.hs b/src/CHAD/AST/Weaken.hs index ac0d152..16403dd 100644 --- a/src/CHAD/AST/Weaken.hs +++ b/src/CHAD/AST/Weaken.hs @@ -109,6 +109,25 @@ infixr 3 .> (.>) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3 (.>) = flip WThen +unweakenList :: as :> bs -> SList f bs -> SList f as +unweakenList WId l = l +unweakenList WSink (SCons _ l) = l +unweakenList (WCopy w) (SCons x l) = SCons x (unweakenList w l) +unweakenList (WPop w) l = let SCons _ l' = unweakenList w l in l' +unweakenList (WThen w1 w2) l = unweakenList w1 (unweakenList w2 l) +unweakenList WClosed _ = SNil +unweakenList (WIdx i) l = SCons (slistIdx l i) l +unweakenList (WPick @_ @_ @_ @env' pre w) (SCons x l) = + let (l1, l2) = sunappend @env' pre l + in sappend l1 (SCons x (unweakenList w l2)) +unweakenList (WSwap @env @as as bs) l = + let (l1, l23) = sunappend @(Append as env) bs l + (l2, l3) = sunappend @env as l23 + in sappend l2 (sappend l1 l3) +unweakenList (WStack @_ @env2 _ bs wab w12) l = + let (l1, l2) = sunappend @env2 bs l + in sappend (unweakenList wab l1) (unweakenList w12 l2) + class KnownListSpine list where knownListSpine :: SList (Const ()) list instance KnownListSpine '[] where knownListSpine = SNil instance KnownListSpine list => KnownListSpine (t : list) where knownListSpine = SCons (Const ()) knownListSpine @@ -133,6 +152,9 @@ wRaiseAbove :: SList f env1 -> proxy env -> env1 :> Append env1 env wRaiseAbove SNil _ = WClosed wRaiseAbove (SCons _ s) env = WCopy (wRaiseAbove s env) +wUnder :: SList f as -> as :> bs -> Append as env :> Append bs env +wUnder as w = WStack (slistMap (\_ -> Const ()) as) (subList) w WId + wPops :: SList f bs -> Append bs env1 :> env2 -> env1 :> env2 wPops SNil w = w wPops (_ `SCons` bs) w = wPops bs (WPop w) |