Prepare for introducing top-level args in accum mod

4 files changed, 30 insertions, 25 deletions

diff --git a/chad-fast.cabal b/chad-fast.cabal
index 5306595..6c60a31 100644
--- a/chad-fast.cabal
+++ b/chad-fast.cabal
@@ -20,6 +20,7 @@ library
     AST.Weaken
     AST.Weaken.Auto
     CHAD
+    CHAD.Heuristics
     CHAD.Top
     CHAD.Types
     -- Compile
diff --git a/src/CHAD.hs b/src/CHAD.hs
index 5ee13fa..9f58f73 100644
--- a/src/CHAD.hs
+++ b/src/CHAD.hs
@@ -43,6 +43,7 @@ import AST.Bindings
 import AST.Count
 import AST.Env
 import AST.Weaken.Auto
+import CHAD.Heuristics
 import CHAD.Types
 import Data
 import Lemmas
@@ -715,22 +716,6 @@ freezeRet descr (Ret e0 subtape e1 sub e2 :: Ret _ _ t) =
           expandSubenvZeros (select SMerge descr) sub (EVar ext (tTup (d2e (subList (select SMerge descr) sub))) IZ))
 
 
---------------------------------- CONFIGURATION --------------------------------
-
-data CHADConfig = CHADConfig
-  { -- | D[let] will bind variables containing arrays in accumulator mode.
-    chcLetArrayAccum :: Bool
-  , -- | D[case] will bind variables containing arrays in accumulator mode.
-    chcCaseArrayAccum :: Bool
-  }
-
-defaultConfig :: CHADConfig
-defaultConfig = CHADConfig
-  { chcLetArrayAccum = False
-  , chcCaseArrayAccum = False
-  }
-
-
 ---------------------------- THE CHAD TRANSFORMATION ---------------------------
 
 drev :: forall env sto t.
@@ -1193,15 +1178,6 @@ drev des = \case
                          (EZero t)) $
             weakenExpr (WCopy (WSink .> WSink .> WSink)) e2)
 
-    hasArrays :: STy t' -> Bool
-    hasArrays STNil = False
-    hasArrays (STPair a b) = hasArrays a || hasArrays b
-    hasArrays (STEither a b) = hasArrays a || hasArrays b
-    hasArrays (STMaybe t) = hasArrays t
-    hasArrays STArr{} = True
-    hasArrays STScal{} = False
-    hasArrays STAccum{} = error "Accumulators not allowed in source program"
-
 data ChosenStorage = forall s. ((s == "discr") ~ False) => ChosenStorage (Storage s)
 
 data RetScoped env0 sto a s t =
diff --git a/src/CHAD/Heuristics.hs b/src/CHAD/Heuristics.hs
new file mode 100644
index 0000000..6ab8222
--- /dev/null
+++ b/src/CHAD/Heuristics.hs
@@ -0,0 +1,14 @@
+{-# LANGUAGE GADTs #-}
+module CHAD.Heuristics where
+
+import AST
+
+
+hasArrays :: STy t' -> Bool
+hasArrays STNil = False
+hasArrays (STPair a b) = hasArrays a || hasArrays b
+hasArrays (STEither a b) = hasArrays a || hasArrays b
+hasArrays (STMaybe t) = hasArrays t
+hasArrays STArr{} = True
+hasArrays STScal{} = False
+hasArrays STAccum{} = error "Accumulators not allowed in source program"
diff --git a/src/CHAD/Types.hs b/src/CHAD/Types.hs
index 0b73a3a..130493d 100644
--- a/src/CHAD/Types.hs
+++ b/src/CHAD/Types.hs
@@ -68,3 +68,17 @@ d2 STAccum{} = error "Accumulators not allowed in input program"
 d2e :: SList STy env -> SList STy (D2E env)
 d2e SNil = SNil
 d2e (SCons t ts) = SCons (d2 t) (d2e ts)
+
+
+data CHADConfig = CHADConfig
+  { -- | D[let] will bind variables containing arrays in accumulator mode.
+    chcLetArrayAccum :: Bool
+  , -- | D[case] will bind variables containing arrays in accumulator mode.
+    chcCaseArrayAccum :: Bool
+  }
+
+defaultConfig :: CHADConfig
+defaultConfig = CHADConfig
+  { chcLetArrayAccum = False
+  , chcCaseArrayAccum = False
+  }