diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-12-06 19:54:05 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-12-06 19:54:05 +0100 |
| commit | 4c96a1ab3d2bd862dde977aae705a5c731d239d2 (patch) | |
| tree | 5dcf2d08242e00057abb80daaa9395505c218a52 | |
| parent | 0ccd55fc7b3d5511935111d0e2712f452da035f4 (diff) | |
Simplify: Some forgotten 'acted'
| -rw-r--r-- | src/Simplify.hs | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/src/Simplify.hs b/src/Simplify.hs index 0dfa107..1646213 100644 --- a/src/Simplify.hs +++ b/src/Simplify.hs @@ -60,19 +60,23 @@ simplify' = \case weakenExpr (WCopy WSink) (snd (simplify' b)) -- beta rules for products - EFst _ (EPair _ e e') | not (hasAdds e') -> simplify' e - ESnd _ (EPair _ e' e) | not (hasAdds e') -> simplify' e + EFst _ (EPair _ e e') | not (hasAdds e') -> acted $ simplify' e + ESnd _ (EPair _ e' e) | not (hasAdds e') -> acted $ simplify' e -- beta rules for coproducts - ECase _ (EInl _ _ e) rhs _ -> simplify' (ELet ext e rhs) - ECase _ (EInr _ _ e) _ rhs -> simplify' (ELet ext e rhs) + ECase _ (EInl _ _ e) rhs _ -> acted $ simplify' (ELet ext e rhs) + ECase _ (EInr _ _ e) _ rhs -> acted $ simplify' (ELet ext e rhs) + + -- beta rules for maybe + EMaybe _ e1 _ ENothing{} -> acted $ simplify' e1 + EMaybe _ _ e1 (EJust _ e2) -> acted $ simplify' $ ELet ext e2 e1 -- let floating to facilitate beta reduction - EFst _ (ELet _ rhs body) -> simplify' (ELet ext rhs (EFst ext body)) - ESnd _ (ELet _ rhs body) -> simplify' (ELet ext rhs (ESnd ext body)) - ECase _ (ELet _ rhs body) e1 e2 -> simplify' (ELet ext rhs (ECase ext body (weakenExpr (WCopy WSink) e1) (weakenExpr (WCopy WSink) e2))) - EIdx0 _ (ELet _ rhs body) -> simplify' (ELet ext rhs (EIdx0 ext body)) - EIdx1 _ (ELet _ rhs body) e -> simplify' (ELet ext rhs (EIdx1 ext body (weakenExpr WSink e))) + EFst _ (ELet _ rhs body) -> acted $ simplify' (ELet ext rhs (EFst ext body)) + ESnd _ (ELet _ rhs body) -> acted $ simplify' (ELet ext rhs (ESnd ext body)) + ECase _ (ELet _ rhs body) e1 e2 -> acted $ simplify' (ELet ext rhs (ECase ext body (weakenExpr (WCopy WSink) e1) (weakenExpr (WCopy WSink) e2))) + EIdx0 _ (ELet _ rhs body) -> acted $ simplify' (ELet ext rhs (EIdx0 ext body)) + EIdx1 _ (ELet _ rhs body) e -> acted $ simplify' (ELet ext rhs (EIdx1 ext body (weakenExpr WSink e))) -- projection down-commuting EFst _ (ECase _ e1 (EPair _ e2 _) (EPair _ e3 _)) -> |