diff options
Diffstat (limited to 'src/CHAD/AST/Env.hs')
| -rw-r--r-- | src/CHAD/AST/Env.hs | 16 |
1 files changed, 16 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) |