Let peeling (let x = Just e in e' ~> let x = e in e'[Just x/x])

1 files changed, 9 insertions, 3 deletions

diff --git a/src/AST.hs b/src/AST.hs
index 9161956..fb5a45e 100644
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -285,9 +285,15 @@ mapExt f = \case
   EOneHot x t p a b -> EOneHot (f x) t p (mapExt f a) (mapExt f b)
   EError x t s -> EError (f x) t s
 
-subst1 :: Expr x env a -> Expr x (a : env) t -> Expr x env t
-subst1 repl = subst $ \x t -> \case IZ -> repl
-                                    IS i -> EVar x t i
+substInline :: Expr x env a -> Expr x (a : env) t -> Expr x env t
+substInline repl =
+  subst $ \x t -> \case IZ -> repl
+                        IS i -> EVar x t i
+
+subst0 :: Ex (b : env) a -> Ex (a : env) t -> Ex (b : env) t
+subst0 repl =
+  subst $ \_ t -> \case IZ -> repl
+                        IS i -> EVar ext t (IS i)
 
 subst :: (forall a. x a -> STy a -> Idx env a -> Expr x env' a)
       -> Expr x env t -> Expr x env' t