1 files changed, 64 insertions, 0 deletions
diff --git a/src/AST/Bindings.hs b/src/AST/Bindings.hs
new file mode 100644
index 0000000..2e63b42
--- /dev/null
+++ b/src/AST/Bindings.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+
+-- I want to bring various type variables in scope using type annotations in
+-- patterns, but I don't want to have to mention all the other type parameters
+-- of the types in question as well then. Partial type signatures (with '_') are
+-- useful here.
+{-# LANGUAGE PartialTypeSignatures #-}
+{-# OPTIONS -Wno-partial-type-signatures #-}
+module AST.Bindings where
+
+import AST
+import Data
+import Lemmas
+
+
+-- binding lists: a let stack without a body. The stack lives in 'env' and defines 'binds'.
+data Bindings f env binds where
+  BTop :: Bindings f env '[]
+  BPush :: Bindings f env binds -> (STy t, f (Append binds env) t) -> Bindings f env (t : binds)
+deriving instance (forall e t. Show (f e t)) => Show (Bindings f env env')
+infixl `BPush`
+
+mapBindings :: (forall env' t'. f env' t' -> g env' t')
+            -> Bindings f env binds -> Bindings g env binds
+mapBindings _ BTop = BTop
+mapBindings f (BPush b (t, e)) = BPush (mapBindings f b) (t, f e)
+
+weakenBindings :: (forall e1 e2 t. e1 :> e2 -> f e1 t -> f e2 t)
+               -> env1 :> env2
+               -> Bindings f env1 binds
+               -> (Bindings f env2 binds, Append binds env1 :> Append binds env2)
+weakenBindings _ w BTop = (BTop, w)
+weakenBindings wf w (BPush b (t, x)) =
+  let (b', w') = weakenBindings wf w b
+  in (BPush b' (t, wf w' x), WCopy w')
+
+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 BTop = WId
+sinkWithBindings (BPush b _) = WSink .> sinkWithBindings b
+
+bconcat :: forall f env binds1 binds2. Bindings f env binds1 -> Bindings f (Append binds1 env) binds2 -> Bindings f env (Append binds2 binds1)
+bconcat b1 BTop = b1
+bconcat b1 (BPush (b2 :: Bindings _ (Append binds1 env) binds2C) (t, x))
+  | Refl <- lemAppendAssoc @binds2C @binds1 @env
+  = BPush (bconcat b1 b2) (t, x)
+
+bindingsBinds :: Bindings f env binds -> SList STy binds
+bindingsBinds BTop = SNil
+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