diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2026-02-22 12:59:40 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2026-02-22 12:59:40 +0100 |
| commit | eb25e315ac8bd1e75498cc92c7f3326fa582171a (patch) | |
| tree | 71df3e761c127ad3ca301a0645ae7760099088ae /src/CHAD/AST/Env.hs | |
| parent | f5b1b405fa4ba63bdffe0f2998f655f0b06534bf (diff) | |
WIP: Store subset of D1 Gamma for recompute at binding sitesrecompute-primalstores
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) |