diff options
Diffstat (limited to 'src/CHAD/AST/Sparse.hs')
| -rw-r--r-- | src/CHAD/AST/Sparse.hs | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/src/CHAD/AST/Sparse.hs b/src/CHAD/AST/Sparse.hs index 85f2882..8b7c085 100644 --- a/src/CHAD/AST/Sparse.hs +++ b/src/CHAD/AST/Sparse.hs @@ -13,38 +13,6 @@ import CHAD.AST.Sparse.Types import CHAD.Data (SBool(..)) -sparsePlus :: SMTy t -> Sparse t t' -> Ex env t' -> Ex env t' -> Ex env t' -sparsePlus _ SpAbsent e1 e2 = use e1 $ use e2 $ ENil ext -sparsePlus t sp e1 e2 | Just Refl <- isDense t sp = EPlus ext t e1 e2 -sparsePlus t (SpSparse sp) e1 e2 = sparsePlus (SMTMaybe t) (SpMaybe sp) e1 e2 -- heh -sparsePlus (SMTPair t1 t2) (SpPair sp1 sp2) e1 e2 = - eunPair e1 $ \w1 e1a e1b -> - eunPair (weakenExpr w1 e2) $ \w2 e2a e2b -> - EPair ext (sparsePlus t1 sp1 (weakenExpr w2 e1a) e2a) - (sparsePlus t2 sp2 (weakenExpr w2 e1b) e2b) -sparsePlus (SMTLEither t1 t2) (SpLEither sp1 sp2) e1 e2 = - elet e2 $ - elcase (weakenExpr WSink e1) - (evar IZ) - (elcase (evar (IS IZ)) - (ELInl ext (applySparse sp2 (fromSMTy t2)) (evar IZ)) - (ELInl ext (applySparse sp2 (fromSMTy t2)) (sparsePlus t1 sp1 (evar (IS IZ)) (evar IZ))) - (EError ext (fromSMTy (applySparse (SpLEither sp1 sp2) (SMTLEither t1 t2))) "splus ll+lr")) - (elcase (evar (IS IZ)) - (ELInr ext (applySparse sp1 (fromSMTy t1)) (evar IZ)) - (EError ext (fromSMTy (applySparse (SpLEither sp1 sp2) (SMTLEither t1 t2))) "splus lr+ll") - (ELInr ext (applySparse sp1 (fromSMTy t1)) (sparsePlus t2 sp2 (evar (IS IZ)) (evar IZ)))) -sparsePlus (SMTMaybe t) (SpMaybe sp) e1 e2 = - elet e2 $ - emaybe (weakenExpr WSink e1) - (evar IZ) - (emaybe (evar (IS IZ)) - (EJust ext (evar IZ)) - (EJust ext (sparsePlus t sp (evar (IS IZ)) (evar IZ)))) -sparsePlus (SMTArr _ t) (SpArr sp) e1 e2 = ezipWith (sparsePlus t sp (evar (IS IZ)) (evar IZ)) e1 e2 -sparsePlus t@SMTScal{} SpScal e1 e2 = EPlus ext t e1 e2 - - cheapZero :: SMTy t -> Maybe (forall env. Ex env t) cheapZero SMTNil = Just (ENil ext) cheapZero (SMTPair t1 t2) |