From c36849cb6247f957b4e6b093e16d04421c8cea3d Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Sun, 25 May 2025 23:35:31 +0200 Subject: ERecompute --- src/AST/Bindings.hs | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'src/AST/Bindings.hs') diff --git a/src/AST/Bindings.hs b/src/AST/Bindings.hs index 3d99afe..745a93b 100644 --- a/src/AST/Bindings.hs +++ b/src/AST/Bindings.hs @@ -16,6 +16,7 @@ module AST.Bindings where import AST +import AST.Env import Data import Lemmas @@ -62,3 +63,13 @@ bindingsBinds (BPush binds (t, _)) = SCons t (bindingsBinds binds) letBinds :: Bindings Ex env binds -> Ex (Append binds env) t -> Ex env t letBinds BTop = id letBinds (BPush b (_, rhs)) = letBinds b . ELet ext rhs + +collectBindings :: SList STy env -> Subenv env env' -> Bindings Ex env env' +collectBindings = \env -> fst . go env WId + where + go :: SList STy env -> env :> env0 -> Subenv env env' -> (Bindings Ex env0 env', env0 :> Append env' env0) + go _ _ SETop = (BTop, WId) + go (ty `SCons` env) w (SEYes sub) = + let (bs, w') = go env (WPop w) sub + in (BPush bs (ty, EVar ext ty (w' .> w @> IZ)), WSink .> w') + go (_ `SCons` env) w (SENo sub) = go env (WPop w) sub -- cgit v1.2.3-70-g09d2