summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorTom Smeding <tom@tomsmeding.com>2025-06-18 10:10:50 +0200
committerTom Smeding <tom@tomsmeding.com>2025-06-18 10:10:50 +0200
commit58f68a4d077c2d58c3974ad12853207512277a33 (patch)
treefbd08cdc677a26a6edbfa850ec8604eda51797e7
parent3db7d00b3248d746aa99f57b117d5722cbe90df0 (diff)
Put smart accumulator redirection behind config flag
-rw-r--r--src/CHAD.hs3
-rw-r--r--src/CHAD/Types.hs6
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 ------------------------------------