From 40a0abca1cedcdd930bb33d1874b7922443e5a8c Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Fri, 6 Dec 2024 19:54:23 +0100
Subject: Simplify: Reduce plus of literals

---
 src/Simplify.hs | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/src/Simplify.hs b/src/Simplify.hs
index 1646213..6303716 100644
--- a/src/Simplify.hs
+++ b/src/Simplify.hs
@@ -101,6 +101,27 @@ simplify' = \case
   EPlus _ e (EZero _) -> acted $ simplify' e
   EOneHot _ SZ _ e -> acted $ simplify' e
 
+  -- equations for plus
+  EPlus STNil _ _ -> (Any True, ENil ext)
+
+  EPlus (STPair t1 t2) (EJust _ (EPair _ a1 b1)) (EJust _ (EPair _ a2 b2)) ->
+    acted $ simplify' $ EJust ext (EPair ext (EPlus t1 a1 a2) (EPlus t2 b1 b2))
+  EPlus STPair{} ENothing{} e -> acted $ simplify' e
+  EPlus STPair{} e ENothing{} -> acted $ simplify' e
+
+  EPlus (STEither t1 _) (EJust _ (EInl _ dt2 a1)) (EJust _ (EInl _ _ a2)) ->
+    acted $ simplify' $ EJust ext (EInl ext dt2 (EPlus t1 a1 a2))
+  EPlus (STEither _ t2) (EJust _ (EInr _ dt1 b1)) (EJust _ (EInr _ _ b2)) ->
+    acted $ simplify' $ EJust ext (EInr ext dt1 (EPlus t2 b1 b2))
+  EPlus STEither{} ENothing{} e -> acted $ simplify' e
+  EPlus STEither{} e ENothing{} -> acted $ simplify' e
+
+  EPlus (STMaybe t) (EJust _ e1) (EJust _ e2) ->
+    acted $ simplify' $ EJust ext (EPlus t e1 e2)
+  EPlus STMaybe{} ENothing{} e -> acted $ simplify' e
+  EPlus STMaybe{} e ENothing{} -> acted $ simplify' e
+
+  -- fallback recursion
   EVar _ t i -> pure $ EVar ext t i
   ELet _ a b -> ELet ext <$> simplify' a <*> simplify' b
   EPair _ a b -> EPair ext <$> simplify' a <*> simplify' b
-- 
cgit v1.2.3-70-g09d2