diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-11-06 23:52:28 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-11-06 23:52:28 +0100 |
| commit | 401e74939fe2a717852acc4b7a452b222d82274a (patch) | |
| tree | 689492e33018eff4815839c7b5ca882872c2b46b | |
| parent | a76ec3bcbdea7beaf9066e4ce0b8c5868f571cdb (diff) | |
Some simplification rules
| -rw-r--r-- | src/Data.hs | 4 | ||||
| -rw-r--r-- | src/Simplify.hs | 17 |
2 files changed, 20 insertions, 1 deletions
diff --git a/src/Data.hs b/src/Data.hs index c5d6219..1371902 100644 --- a/src/Data.hs +++ b/src/Data.hs @@ -80,6 +80,10 @@ type family n + m where Z + m = m S n + m = S (n + m) +snatAdd :: SNat n -> SNat m -> SNat (n + m) +snatAdd SZ m = m +snatAdd (SS n) m = SS (snatAdd n m) + lemPlusSuccRight :: n + S m :~: S (n + m) lemPlusSuccRight = unsafeCoerceRefl diff --git a/src/Simplify.hs b/src/Simplify.hs index 0ce5594..f8b4b63 100644 --- a/src/Simplify.hs +++ b/src/Simplify.hs @@ -74,13 +74,28 @@ simplify' = \case 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))) + -- projection down-commuting + EFst _ (ECase _ e1 (EPair _ e2 _) (EPair _ e3 _)) -> + acted $ simplify' $ + ECase ext e1 e2 e3 + ESnd _ (ECase _ e1 (EPair _ _ e2) (EPair _ _ e3)) -> + acted $ simplify' $ + ECase ext e1 e2 e3 + -- TODO: array indexing (index of build, index of fold) -- TODO: beta rules for maybe -- TODO: constant folding for operations - -- TODO: accum of zero, plus of zero + -- TODO: properly concatenate accum/onehot + EAccum SZ _ (EOneHot _ i idx val) acc -> + acted $ simplify' $ + EAccum i idx val acc + EAccum _ _ (EZero _) _ -> (Any True, ENil ext) + EPlus _ (EZero _) e -> acted $ simplify' e + EPlus _ e (EZero _) -> acted $ simplify' e + EOneHot _ SZ _ e -> acted $ simplify' e EVar _ t i -> pure $ EVar ext t i ELet _ a b -> ELet ext <$> simplify' a <*> simplify' b |