aboutsummaryrefslogtreecommitdiff
path: root/src/CHAD/Accum.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/CHAD/Accum.hs')
-rw-r--r--src/CHAD/Accum.hs72
1 files changed, 0 insertions, 72 deletions
diff --git a/src/CHAD/Accum.hs b/src/CHAD/Accum.hs
deleted file mode 100644
index a7bc53f..0000000
--- a/src/CHAD/Accum.hs
+++ /dev/null
@@ -1,72 +0,0 @@
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE TypeOperators #-}
--- | TODO this module is a grab-bag of random utility functions that are shared
--- between CHAD and CHAD.Top.
-module CHAD.Accum where
-
-import AST
-import CHAD.Types
-import Data
-import AST.Env
-
-
-d2zeroInfo :: STy t -> Ex env (D1 t) -> Ex env (ZeroInfo (D2 t))
-d2zeroInfo STNil _ = ENil ext
-d2zeroInfo (STPair a b) e =
- eunPair e $ \_ e1 e2 ->
- EPair ext (d2zeroInfo a e1) (d2zeroInfo b e2)
-d2zeroInfo STEither{} _ = ENil ext
-d2zeroInfo STLEither{} _ = ENil ext
-d2zeroInfo STMaybe{} _ = ENil ext
-d2zeroInfo (STArr _ t) e = emap (d2zeroInfo t (EVar ext (d1 t) IZ)) e
-d2zeroInfo (STScal t) _ | Refl <- lemZeroInfoScal t = ENil ext
-d2zeroInfo STAccum{} _ = error "accumulators not allowed in source program"
-
-d2deepZeroInfo :: STy t -> Ex env (D1 t) -> Ex env (DeepZeroInfo (D2 t))
-d2deepZeroInfo STNil _ = ENil ext
-d2deepZeroInfo (STPair a b) e =
- eunPair e $ \_ e1 e2 ->
- EPair ext (d2deepZeroInfo a e1) (d2deepZeroInfo b e2)
-d2deepZeroInfo (STEither a b) e =
- ECase ext e
- (ELInl ext (tDeepZeroInfo (d2M b)) (d2deepZeroInfo a (EVar ext (d1 a) IZ)))
- (ELInr ext (tDeepZeroInfo (d2M a)) (d2deepZeroInfo b (EVar ext (d1 b) IZ)))
-d2deepZeroInfo (STLEither a b) e =
- elcase e
- (ELNil ext (tDeepZeroInfo (d2M a)) (tDeepZeroInfo (d2M b)))
- (ELInl ext (tDeepZeroInfo (d2M b)) (d2deepZeroInfo a (EVar ext (d1 a) IZ)))
- (ELInr ext (tDeepZeroInfo (d2M a)) (d2deepZeroInfo b (EVar ext (d1 b) IZ)))
-d2deepZeroInfo (STMaybe a) e =
- emaybe e
- (ENothing ext (tDeepZeroInfo (d2M a)))
- (EJust ext (d2deepZeroInfo a (EVar ext (d1 a) IZ)))
-d2deepZeroInfo (STArr _ t) e = emap (d2deepZeroInfo t (EVar ext (d1 t) IZ)) e
-d2deepZeroInfo (STScal t) _ | Refl <- lemDeepZeroInfoScal t = ENil ext
-d2deepZeroInfo STAccum{} _ = error "accumulators not allowed in source program"
-
--- The weakening is necessary because we need to initialise the created
--- accumulators with zeros. Those zeros are deep and need full primals. This
--- means, in the end, that primals corresponding to environment entries
--- promoted to an accumulator with accumPromote in CHAD need to be stored for
--- the dual.
-makeAccumulators :: D1E envPro :> env -> SList STy envPro -> Ex (Append (D2AcE envPro) env) t -> Ex env (InvTup t (D2E envPro))
-makeAccumulators _ SNil e = e
-makeAccumulators w (t `SCons` envpro) e =
- makeAccumulators (WPop w) envpro $
- EWith ext (d2M t) (EDeepZero ext (d2M t) (d2deepZeroInfo t (EVar ext (d1 t) (wSinks (d2ace envpro) .> w @> IZ)))) 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))))
-
-subenvD1E :: Subenv env env' -> Subenv (D1E env) (D1E env')
-subenvD1E SETop = SETop
-subenvD1E (SEYesR sub) = SEYesR (subenvD1E sub)
-subenvD1E (SENo sub) = SENo (subenvD1E sub)