From 58f68a4d077c2d58c3974ad12853207512277a33 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Wed, 18 Jun 2025 10:10:50 +0200
Subject: Put smart accumulator redirection behind config flag

---
 src/CHAD.hs       | 3 ++-
 src/CHAD/Types.hs | 6 +++++-
 2 files changed, 7 insertions(+), 2 deletions(-)

(limited to 'src')

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 ------------------------------------
-- 
cgit v1.2.3-70-g09d2