ERecompute

1 files changed, 11 insertions, 0 deletions

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