From b1a41a3e7b796f9bde7642fc4d7de70a7cdadc71 Mon Sep 17 00:00:00 2001
From: Tom Smeding <t.j.smeding@uu.nl>
Date: Mon, 21 Apr 2025 21:57:24 +0200
Subject: Let peeling (let x = Just e in e' ~> let x = e in e'[Just x/x])

---
 src/AST.hs | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

(limited to 'src/AST.hs')

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
-- 
cgit v1.2.3-70-g09d2