diff options
| -rw-r--r-- | src/CHAD.hs | 47 |
1 files changed, 25 insertions, 22 deletions
diff --git a/src/CHAD.hs b/src/CHAD.hs index 9786e1e..007ffe3 100644 --- a/src/CHAD.hs +++ b/src/CHAD.hs @@ -283,14 +283,7 @@ 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)) - -- TODO: use vectoriseExpr here - (subst (\_ t' i -> case splitIdx @env (bindingsBinds bs) i of - Left i1 -> - let i1' = IS (wRaiseAbove (bindingsBinds bs') env @> vectoriseIdx i1) - in EIdx0 ext (EIdx1 ext (EVar ext (STArr (SS SZ) t') i1') - (EVar ext tIx (WSink .> sinkWithBindings bs' @> n))) - Right i2 -> EVar ext t' (IS (sinkWithBindings bs' @> i2))) - e) + (vectoriseExpr SNil (bindingsBinds bs) env e) in bs' `BPush` (STArr (SS SZ) t, e') type family D1 t where @@ -998,8 +991,9 @@ drev des = \case (ENil ext) EBuild1 _ ne e - | Ret (ne0 :: Bindings _ _ ne_binds) ne1 nsub ne2 <- drev des ne -> - accumPromote (typeOf e) des (occEnvPop (occCountAll e)) $ \vdes proSub envPro wPro -> + | Ret (ne0 :: Bindings _ _ ne_binds) ne1 nsub ne2 <- drev des ne + , let eltty = typeOf e -> + accumPromote eltty des (occEnvPop (occCountAll e)) $ \vdes proSub envPro wPro -> case drev (vdes `DPush` (tIx, SMerge)) e of { Ret e0 e1 sub e2 -> case assertSubenvEmpty sub of { Refl -> case assertSubenvEmpty proSub of { Refl -> @@ -1030,18 +1024,27 @@ drev des = \case e1)) nsub (ELet ext - (makeAccumulators 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)) - -- TODO: use vectoriseExpr - (_ (weakenExpr (wPro (bindingsBinds e0)) e2))) $ + (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)) + -- TODO: use vectoriseExpr + (_ $ + 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 (wPro (bindingsBinds e0)) e2)) $ ELet ext (ENil ext) $ weakenExpr (autoWeak (#nil (auto1 @TNil) &. #d (auto1 @(D2 t)) |