diff options
Diffstat (limited to 'src/CHAD.hs')
| -rw-r--r-- | src/CHAD.hs | 26 |
1 files changed, 1 insertions, 25 deletions
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 = |