diff options
| author | Tom Smeding <t.j.smeding@uu.nl> | 2025-04-21 21:57:24 +0200 |
|---|---|---|
| committer | Tom Smeding <t.j.smeding@uu.nl> | 2025-04-21 21:57:24 +0200 |
| commit | b1a41a3e7b796f9bde7642fc4d7de70a7cdadc71 (patch) | |
| tree | 62c0d3a96bf5875434812f3fe8276949d3457492 | |
| parent | c586e7d2343fa735a9b27e0b1a201dd2cb2bc68e (diff) | |
Let peeling (let x = Just e in e' ~> let x = e in e'[Just x/x])
| -rw-r--r-- | src/AST.hs | 12 | ||||
| -rw-r--r-- | src/Simplify.hs | 12 |
2 files changed, 18 insertions, 6 deletions
@@ -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 diff --git a/src/Simplify.hs b/src/Simplify.hs index cb835aa..e0ab37b 100644 --- a/src/Simplify.hs +++ b/src/Simplify.hs @@ -61,14 +61,14 @@ simplify' = \case -- inlining ELet _ rhs body | cheapExpr rhs - -> acted $ simplify' (subst1 rhs body) + -> acted $ simplify' (substInline rhs body) | Occ lexOcc runOcc <- occCount IZ body , ((not ?accumInScope || not (hasAdds rhs)) && lexOcc <= One && runOcc <= One) -- without effects, normal rules apply || (lexOcc == One && runOcc == One) -- with effects, linear inlining is still allowed, but weakening is not - -> acted $ simplify' (subst1 rhs body) + -> acted $ simplify' (substInline rhs body) - -- let splitting + -- let splitting / let peeling ELet _ (EPair _ a b) body -> acted $ simplify' $ ELet ext a $ @@ -76,6 +76,12 @@ simplify' = \case subst (\_ t -> \case IZ -> EPair ext (EVar ext (typeOf a) (IS IZ)) (EVar ext (typeOf b) IZ) IS i -> EVar ext t (IS (IS i))) body + ELet _ (EJust _ a) body -> + acted $ simplify' $ ELet ext a $ subst0 (EJust ext (EVar ext (typeOf a) IZ)) body + ELet _ (EInl _ t2 a) body -> + acted $ simplify' $ ELet ext a $ subst0 (EInl ext t2 (EVar ext (typeOf a) IZ)) body + ELet _ (EInr _ t1 a) body -> + acted $ simplify' $ ELet ext a $ subst0 (EInr ext t1 (EVar ext (typeOf a) IZ)) body -- let rotation ELet _ (ELet _ rhs a) b -> |