diff options
| -rw-r--r-- | src/Simplify.hs | 21 |
1 files changed, 21 insertions, 0 deletions
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 |