summaryrefslogtreecommitdiff
path: root/src/CHAD/Accum.hs
diff options
context:
space:
mode:
authorTom Smeding <tom@tomsmeding.com>2025-06-06 22:50:06 +0200
committerTom Smeding <tom@tomsmeding.com>2025-06-06 22:50:06 +0200
commit56056c98b2e3dce65a0e42bce0410c083fd1f8be (patch)
tree8db2d1be037f8f980c3d1bf76ff9078048f33d63 /src/CHAD/Accum.hs
parent7bd37711ffecb7a0e202ecfd717e3a4cbbe6074f (diff)
WIP mixed static/dynamic sparsitysparse
Diffstat (limited to 'src/CHAD/Accum.hs')
-rw-r--r--src/CHAD/Accum.hs27
1 files changed, 0 insertions, 27 deletions
diff --git a/src/CHAD/Accum.hs b/src/CHAD/Accum.hs
deleted file mode 100644
index d8a71b5..0000000
--- a/src/CHAD/Accum.hs
+++ /dev/null
@@ -1,27 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-module CHAD.Accum where
-
-import AST
-import CHAD.Types
-import Data
-
-
-
-makeAccumulators :: SList STy envPro -> Ex (Append (D2AcE envPro) env) t -> Ex env (InvTup t (D2E envPro))
-makeAccumulators SNil e = e
-makeAccumulators (t `SCons` envpro) e | Refl <- lemZeroInfoD2 t =
- makeAccumulators envpro $
- EWith ext (d2M t) (EZero ext (d2M t) (ENil ext)) e
-
-uninvertTup :: SList STy list -> STy core -> Ex env (InvTup core list) -> Ex env (TPair core (Tup list))
-uninvertTup SNil _ e = EPair ext e (ENil ext)
-uninvertTup (t `SCons` list) tcore e =
- ELet ext (uninvertTup list (STPair tcore t) e) $
- let recT = STPair (STPair tcore t) (tTup list) -- type of the RHS of that let binding
- in EPair ext
- (EFst ext (EFst ext (EVar ext recT IZ)))
- (EPair ext
- (ESnd ext (EVar ext recT IZ))
- (ESnd ext (EFst ext (EVar ext recT IZ))))
-