diff options
author | Tom Smeding <tom@tomsmeding.com> | 2025-06-18 10:10:50 +0200 |
---|---|---|
committer | Tom Smeding <tom@tomsmeding.com> | 2025-06-18 10:10:50 +0200 |
commit | 58f68a4d077c2d58c3974ad12853207512277a33 (patch) | |
tree | fbd08cdc677a26a6edbfa850ec8604eda51797e7 | |
parent | 3db7d00b3248d746aa99f57b117d5722cbe90df0 (diff) |
Put smart accumulator redirection behind config flag
-rw-r--r-- | src/CHAD.hs | 3 | ||||
-rw-r--r-- | src/CHAD/Types.hs | 6 |
2 files changed, 7 insertions, 2 deletions
diff --git a/src/CHAD.hs b/src/CHAD.hs index 9fa7f9a..3399de2 100644 --- a/src/CHAD.hs +++ b/src/CHAD.hs @@ -1310,7 +1310,8 @@ drevScoped des accumMap argty argsto argids sd expr = case argsto of SENo sub' -> RetScoped e0 (subenvConcat (SENo @(D1 a) SETop) subtape) e1 sub' SpAbsent (EPair ext e2 (ENil ext)) SAccum - | Just (VIArr i _) <- argids + | chcSmartWith ?config + , Just (VIArr i _) <- argids , Just (Some (VarMap.TypedIdx foundTy idx)) <- VarMap.lookup i accumMap , Just Refl <- testEquality foundTy (STAccum (d2M argty)) , Ret e0 (subtape :: Subenv _ tapebinds) e1 sub e2 <- drev (des `DPush` (argty, argids, argsto)) (VarMap.sink1 accumMap) sd expr diff --git a/src/CHAD/Types.hs b/src/CHAD/Types.hs index e061588..44ac20e 100644 --- a/src/CHAD/Types.hs +++ b/src/CHAD/Types.hs @@ -97,6 +97,8 @@ data CHADConfig = CHADConfig chcCaseArrayAccum :: Bool , -- | Introduce top-level arguments containing arrays in accumulator mode. chcArgArrayAccum :: Bool + , -- | Place with-blocks around array variable scopes, and redirect accumulations there. + chcSmartWith :: Bool } deriving (Show) @@ -105,12 +107,14 @@ defaultConfig = CHADConfig { chcLetArrayAccum = False , chcCaseArrayAccum = False , chcArgArrayAccum = False + , chcSmartWith = False } chcSetAccum :: CHADConfig -> CHADConfig chcSetAccum c = c { chcLetArrayAccum = True , chcCaseArrayAccum = True - , chcArgArrayAccum = True } + , chcArgArrayAccum = True + , chcSmartWith = True } ------------------------------------ LEMMAS ------------------------------------ |