diff options
Diffstat (limited to 'src/CHAD.hs')
| -rw-r--r-- | src/CHAD.hs | 24 |
1 files changed, 11 insertions, 13 deletions
diff --git a/src/CHAD.hs b/src/CHAD.hs index 4675434..d7d7da2 100644 --- a/src/CHAD.hs +++ b/src/CHAD.hs @@ -286,7 +286,7 @@ conv1Idx IZ = IZ conv1Idx (IS i) = IS (conv1Idx i) data Idx2 env sto t - = Idx2Ac (Idx (D2AcE (Select env sto "accum")) (TAccum (D2 t))) + = Idx2Ac (Idx (D2AcE (Select env sto "accum")) (TAccum t)) | Idx2Me (Idx (Select env sto "merge") t) | Idx2Di (Idx (Select env sto "discr") t) @@ -409,11 +409,11 @@ accumPromote pdty (descr `DPush` (t :: STy t, sto)) k = envpro prosub (\shbinds -> - autoWeak (#pro (d2ace envpro) &. #d (auto1 @(D2 dt)) &. #shb shbinds &. #acc (auto1 @(TAccum (D2 t))) &. #tl (d2ace (select SAccum descr))) + autoWeak (#pro (d2ace envpro) &. #d (auto1 @(D2 dt)) &. #shb shbinds &. #acc (auto1 @(TAccum t)) &. #tl (d2ace (select SAccum descr))) (#acc :++: (#pro :++: #d :++: #shb :++: #tl)) (#pro :++: #d :++: #shb :++: #acc :++: #tl) .> WCopy (wf shbinds) - .> autoWeak (#d (auto1 @(D2 dt)) &. #shb shbinds &. #acc (auto1 @(TAccum (D2 t))) &. #tl (d2ace (select SAccum storepl))) + .> autoWeak (#d (auto1 @(D2 dt)) &. #shb shbinds &. #acc (auto1 @(TAccum t)) &. #tl (d2ace (select SAccum storepl))) (#d :++: #shb :++: #acc :++: #tl) (#acc :++: (#d :++: #shb :++: #tl))) @@ -441,7 +441,7 @@ accumPromote pdty (descr `DPush` (t :: STy t, sto)) k = -- goal: | ARE EQUAL || -- D2 t : Append shbinds (TAccum n t3 : D2AcE (Select envPro stoRepl "accum")) :> TAccum n t3 : Append envPro (D2 t : Append shbinds (D2AcE (Select envPro sto1 "accum"))) WCopy (wf shbinds) - .> WPick @(TAccum (D2 t)) @(D2 dt : shbinds) (Const () `SCons` shbindsC) + .> WPick @(TAccum t) @(D2 dt : shbinds) (Const () `SCons` shbindsC) (WId @(D2AcE (Select env1 stoRepl "accum")))) -- Discrete values are left as-is, nothing to do @@ -568,7 +568,7 @@ drev des = \case SETop (EVar ext (d1 t) (conv1Idx i)) (subenvNone (select SMerge des)) - (EAccum ext SZ (ENil ext) (EVar ext (d2 t) IZ) (EVar ext (STAccum (d2 t)) (IS accI))) + (EAccum ext t SAPHere (ENil ext) (EVar ext (d2 t) IZ) (EVar ext (STAccum t) (IS accI))) Idx2Me tupI -> Ret BTop @@ -944,12 +944,10 @@ drev des = \case (EIdx ext (EVar ext (STArr n (d1 eltty)) (IS (IS IZ))) (EVar ext (tTup (sreplicate n tIx)) IZ)) sub - (ELet ext (EOneHot ext (STArr n eltty) n - (arrIdxToAcIdx (d2 eltty) n $ EVar ext tIxN (IS IZ)) - (case n of SZ -> EUnit ext (EVar ext (d2 eltty) IZ) - SS{} | Refl <- lemAcValArrN (d2 eltty) n -> - EPair ext (EVar ext tIxN (IS (IS IZ))) - (EUnit ext (EVar ext (d2 eltty) IZ)))) $ + (ELet ext (EOneHot ext (STArr n eltty) (SAPArrIdx SAPHere n) + (EPair ext (EPair ext (EVar ext tIxN (IS IZ)) (EVar ext tIxN (IS (IS IZ)))) + (ENil ext)) + (EVar ext (d2 eltty) IZ)) $ weakenExpr (WCopy (WSink .> WSink .> WSink)) e2) EShape _ e @@ -1050,10 +1048,10 @@ drevScoped des argty argsto expr SENo sub' -> RetScoped e0 subtape e1 sub' (EPair ext e2 (EZero ext argty)) SAccum -> RetScoped e0 subtape e1 sub $ - EWith ext (EZero ext argty) $ + EWith ext argty (EZero ext argty) $ weakenExpr (autoWeak (#d (auto1 @(D2 t)) &. #body (subList (bindingsBinds e0) subtape) - &. #ac (auto1 @(TAccum (D2 a))) + &. #ac (auto1 @(TAccum a)) &. #tl (d2ace (select SAccum des))) (#d :++: #body :++: #ac :++: #tl) (#ac :++: #d :++: #body :++: #tl)) |