From eb25e315ac8bd1e75498cc92c7f3326fa582171a Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Sun, 22 Feb 2026 12:59:40 +0100 Subject: WIP: Store subset of D1 Gamma for recompute at binding sites --- src/CHAD/AST/Env.hs | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'src/CHAD/AST/Env.hs') 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) -- cgit v1.2.3-70-g09d2