1 files changed, 0 insertions, 84 deletions
diff --git a/src/AST/Bindings.hs b/src/AST/Bindings.hs
deleted file mode 100644
index 463586a..0000000
--- a/src/AST/Bindings.hs
+++ /dev/null
@@ -1,84 +0,0 @@
-{-# 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 AST.Env
-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`
-
-bpush :: Bindings (Expr x) env binds -> Expr x (Append binds env) t -> Bindings (Expr x) env (t : binds)
-bpush b e = b `BPush` (typeOf e, e)
-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')
-
-weakenBindingsE :: env1 :> env2
-                -> Bindings (Expr x) env1 binds
-                -> (Bindings (Expr x) env2 binds, Append binds env1 :> Append binds env2)
-weakenBindingsE = weakenBindings weakenExpr
-
-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 :: forall env' env binds f. 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
-
-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