1 files changed, 12 insertions, 1 deletions
diff --git a/src/AST/Bindings.hs b/src/AST/Bindings.hs
index 2e63b42..2310f4b 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
 
@@ -45,7 +46,7 @@ weakenOver :: SList STy ts -> env :> env' -> Append ts env :> Append ts env'
 weakenOver SNil w = w
 weakenOver (SCons _ ts) w = WCopy (weakenOver ts w)
 
-sinkWithBindings :: Bindings f env binds -> env' :> Append binds env'
+sinkWithBindings :: forall env' env binds f. Bindings f env binds -> env' :> Append binds env'
 sinkWithBindings BTop = WId
 sinkWithBindings (BPush b _) = WSink .> sinkWithBindings b
 
@@ -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 (SEYesR 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