summaryrefslogtreecommitdiff
path: root/src/CHAD.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/CHAD.hs')
-rw-r--r--src/CHAD.hs131
1 files changed, 0 insertions, 131 deletions
diff --git a/src/CHAD.hs b/src/CHAD.hs
index ffbdcac..8080ec0 100644
--- a/src/CHAD.hs
+++ b/src/CHAD.hs
@@ -192,57 +192,6 @@ reconstructBindings binds tape =
,sreverse (stapeUnfoldings binds))
---------------------------------- VECTORISATION --------------------------------
--- Currently only used in D[build1], should be removed.
-
-{-
-type family Vectorise n list where
- Vectorise _ '[] = '[]
- Vectorise n (t : ts) = TArr n t : Vectorise n ts
-
-vectoriseEnv :: SNat n -> SList STy env -> SList STy (Vectorise n env)
-vectoriseEnv _ SNil = SNil
-vectoriseEnv n (t `SCons` env) = STArr n t `SCons` vectoriseEnv n env
-
-vectoriseIdx :: Idx binds t -> Idx (Vectorise n binds) (TArr n t)
-vectoriseIdx IZ = IZ
-vectoriseIdx (IS i) = IS (vectoriseIdx i)
-
-vectoriseExpr :: forall prefix binds env t f.
- SList f prefix
- -> SList STy binds
- -> SList f env
- -> Ex (Append prefix (Append binds env)) t
- -> Ex (TIx : Append prefix (Append (Vectorise (S Z) binds) env)) t
-vectoriseExpr prefix binds env =
- let wTarget :: Layout True ['("ix", '[TIx]), '("pre", prefix), '("vbinds", Vectorise (S Z) binds), '("env", env)] e
- -> e :> TIx : Append prefix (Append (Vectorise (S Z) binds) env)
- wTarget layout =
- autoWeak (#ix (auto1 @TIx) &. #pre prefix &. #vbinds (vectoriseEnv (SS SZ) binds) &. #env env)
- layout
- (#ix :++: #pre :++: #vbinds :++: #env)
- in
- subst $ \_ t i ->
- case splitIdx @(Append binds env) prefix i of
- Left iPre -> EVar ext t (wTarget #pre @> iPre)
- Right i' ->
- case splitIdx @env binds i' of
- Left iBinds ->
- EIdx0 ext $
- EIdx1 ext (EVar ext (STArr (SS SZ) t) (wTarget #vbinds @> vectoriseIdx iBinds))
- (EVar ext tIx IZ)
- Right iEnv -> EVar ext t (wTarget #env @> iEnv)
-
-vectorise1Binds :: forall env binds. SList STy env -> Idx env TIx -> Bindings Ex env binds -> Bindings Ex env (Vectorise (S Z) binds)
-vectorise1Binds _ _ BTop = BTop
-vectorise1Binds env n (bs `BPush` (t, e)) =
- let bs' = vectorise1Binds env n bs
- e' = EBuild1 ext (EVar ext tIx (sinkWithBindings bs' @> n))
- (vectoriseExpr SNil (bindingsBinds bs) env e)
- in bs' `BPush` (STArr (SS SZ) t, e')
--}
-
-
---------------------- ENVIRONMENT DESCRIPTION AND STORAGE ---------------------
type Storage :: Symbol -> Type
@@ -939,86 +888,6 @@ drev des = \case
(subenvNone (select SMerge des))
(ENil ext)
- EBuild1{} -> error "CHAD of EBuild1: Please use EBuild instead"
- {-
- -- TODO: either remove EBuilds1 entirely or rewrite it to work with an array of tapes instead of a vectorised tape
- EBuild1 _ ne (orige :: Ex _ eltty)
- | Ret (ne0 :: Bindings _ _ ne_binds) ne1 _ _ <- drev des ne -- allowed to ignore ne2 here because ne has a discrete result
- , let eltty = typeOf orige ->
- deleteUnused (descrList des) (occEnvPop (occCountAll orige)) $ \(usedSub :: Subenv env env') ->
- let e = unsafeWeakenWithSubenv (SEYes usedSub) orige in
- subDescr des usedSub $ \usedDes subMergeUsed subAccumUsed subD1eUsed ->
- accumPromote eltty usedDes $ \prodes (envPro :: SList _ envPro) proSub wPro ->
- case drev (prodes `DPush` (tIx, SMerge)) e of { Ret (e0 :: Bindings _ _ e_binds) e1 sub e2 ->
- case assertSubenvEmpty sub of { Refl ->
- let ve0 = vectorise1Binds (tIx `SCons` sD1eEnv usedDes) IZ e0 in
- Ret (bconcat (ne0 `BPush` (tIx, ne1))
- (fst (weakenBindings weakenExpr (WCopy (wSinksAnd (bindingsBinds ne0) (wUndoSubenv subD1eUsed))) ve0)))
- (EBuild1 ext
- (weakenExpr (autoWeak (#ve0 (bindingsBinds ve0)
- &. #binds (tIx `SCons` bindingsBinds ne0)
- &. #tl (sD1eEnv des))
- #binds
- ((#ve0 :++: #binds) :++: #tl))
- (EVar ext tIx IZ))
- (subst (\_ t i -> case splitIdx @(TIx : D1E env') (bindingsBinds e0) i of
- Left ibind ->
- let ibind' =
- autoWeak (#ix (auto1 @TIx)
- &. #ve0 (bindingsBinds ve0)
- &. #binds (tIx `SCons` bindingsBinds ne0)
- &. #tl (sD1eEnv des))
- #ve0
- (#ix :++: (#ve0 :++: #binds) :++: #tl)
- @> vectoriseIdx ibind
- in EIdx0 ext (EIdx1 ext (EVar ext (STArr (SS SZ) t) ibind')
- (EVar ext tIx IZ))
- Right IZ -> EVar ext tIx IZ -- build lambda index argument
- Right (IS ienv) -> EVar ext t (IS (wSinksAnd (sappend (bindingsBinds ve0) (tIx `SCons` bindingsBinds ne0)) (wUndoSubenv subD1eUsed) @> ienv)))
- e1))
- (subenvCompose subMergeUsed proSub)
- (ELet ext
- (uninvertTup (d2e envPro) (STArr (SS SZ) STNil) $
- makeAccumulators @_ @_ @(TArr (S Z) TNil) envPro $
- EBuild1 ext
- (weakenExpr (autoWeak (#ve0 (bindingsBinds ve0)
- &. #pro (d2ace envPro)
- &. #d (auto1 @(D2 t))
- &. #binds (tIx `SCons` bindingsBinds ne0)
- &. #tl (d2ace (select SAccum des)))
- #binds
- (#pro :++: #d :++: (#ve0 :++: #binds) :++: #tl))
- (EVar ext tIx IZ))
- (ELet ext (EIdx0 ext (EIdx1 ext (EVar ext (STArr (SS SZ) (d2 eltty))
- (IS (wSinks @(TArr (S Z) (D2 eltty) : Append (Append (Vectorise (S Z) e_binds) (TIx : ne_binds)) (D2AcE (Select env sto "accum")))
- (d2ace envPro)
- @> IZ)))
- (EVar ext tIx IZ))) $
- weakenExpr (autoWeak (#i (auto1 @TIx)
- &. #dpro (d2ace envPro)
- &. #d (d2 eltty `SCons` SNil)
- &. #darr (STArr (SS SZ) (d2 eltty) `SCons` SNil)
- &. #n (auto1 @TIx)
- &. #vbinds (bindingsBinds ve0)
- &. #ne0 (bindingsBinds ne0)
- &. #tl (d2ace (select SAccum des)))
- (#i :++: (#dpro :++: #d) :++: #vbinds :++: #tl)
- (#d :++: #i :++: #dpro :++: #darr :++: (#vbinds :++: #n :++: #ne0) :++: #tl)) $
- vectoriseExpr (sappend (d2ace envPro) (d2 eltty `SCons` SNil)) (bindingsBinds e0) (d2ace (select SAccum des)) $
- weakenExpr (autoWeak (#dpro (d2ace envPro)
- &. #d (d2 eltty `SCons` SNil)
- &. #binds (bindingsBinds e0)
- &. #tl (d2ace (select SAccum des)))
- (#dpro :++: #d :++: #binds :++: #tl)
- ((#dpro :++: #d) :++: #binds :++: #tl)) $
- weakenExpr (wCopies (d2ace envPro) (WCopy @(D2 eltty) (wCopies (bindingsBinds e0) (wUndoSubenv subAccumUsed)))) $
- weakenExpr (wPro (bindingsBinds e0)) $
- e2)) $
- ELet ext (ENil ext) $
- ESnd ext (EVar ext (STPair (STArr (SS SZ) STNil) (tTup (d2e envPro))) (IS IZ)))
- }}
- -}
-
-- TODO: merge the e0 and e1 builds in a single build just like they are merged into a single case in D[case]0, then it can really store only the parts that need to be preserved until D[build]2
EBuild _ (ndim :: SNat ndim) she (orige :: Ex _ eltty)
| Ret (she0 :: Bindings _ _ she_binds) _ she1 _ _ <- drev des she -- allowed to ignore she2 here because she has a discrete result
generated by cgit v1.2.3-70-g09d2 (git 2.48.1) at 2025-03-31 23:29:27 +0200