1 files changed, 40 insertions, 5 deletions
diff --git a/src/CHAD/Types.hs b/src/CHAD/Types.hs
index 974669d..44ac20e 100644
--- a/src/CHAD/Types.hs
+++ b/src/CHAD/Types.hs
@@ -1,8 +1,10 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 module CHAD.Types where
 
+import AST.Accum
 import AST.Types
 import Data
 
@@ -18,11 +20,11 @@ type family D1 t where
 
 type family D2 t where
   D2 TNil = TNil
-  D2 (TPair a b) = TMaybe (TPair (D2 a) (D2 b))
+  D2 (TPair a b) = TPair (D2 a) (D2 b)
   D2 (TEither a b) = TLEither (D2 a) (D2 b)
   D2 (TLEither a b) = TLEither (D2 a) (D2 b)
   D2 (TMaybe t) = TMaybe (D2 t)
-  D2 (TArr n t) = TMaybe (TArr n (D2 t))
+  D2 (TArr n t) = TArr n (D2 t)
   D2 (TScal t) = D2s t
 
 type family D2s t where
@@ -60,11 +62,11 @@ d1e (t `SCons` env) = d1 t `SCons` d1e env
 
 d2M :: STy t -> SMTy (D2 t)
 d2M STNil = SMTNil
-d2M (STPair a b) = SMTMaybe (SMTPair (d2M a) (d2M b))
+d2M (STPair a b) = SMTPair (d2M a) (d2M b)
 d2M (STEither a b) = SMTLEither (d2M a) (d2M b)
 d2M (STLEither a b) = SMTLEither (d2M a) (d2M b)
 d2M (STMaybe t) = SMTMaybe (d2M t)
-d2M (STArr n t) = SMTMaybe (SMTArr n (d2M t))
+d2M (STArr n t) = SMTArr n (d2M t)
 d2M (STScal t) = case t of
   STI32 -> SMTNil
   STI64 -> SMTNil
@@ -95,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)
 
@@ -103,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 ------------------------------------
@@ -116,3 +122,32 @@ chcSetAccum c = c { chcLetArrayAccum = True
 indexTupD1Id :: SNat n -> Tup (Replicate n TIx) :~: D1 (Tup (Replicate n TIx))
 indexTupD1Id SZ = Refl
 indexTupD1Id (SS n) | Refl <- indexTupD1Id n = Refl
+
+lemZeroInfoScal :: SScalTy t -> ZeroInfo (D2s t) :~: TNil
+lemZeroInfoScal STI32 = Refl
+lemZeroInfoScal STI64 = Refl
+lemZeroInfoScal STF32 = Refl
+lemZeroInfoScal STF64 = Refl
+lemZeroInfoScal STBool = Refl
+
+lemDeepZeroInfoScal :: SScalTy t -> DeepZeroInfo (D2s t) :~: TNil
+lemDeepZeroInfoScal STI32 = Refl
+lemDeepZeroInfoScal STI64 = Refl
+lemDeepZeroInfoScal STF32 = Refl
+lemDeepZeroInfoScal STF64 = Refl
+lemDeepZeroInfoScal STBool = Refl
+
+d1Identity :: STy t -> D1 t :~: t
+d1Identity = \case
+  STNil -> Refl
+  STPair a b | Refl <- d1Identity a, Refl <- d1Identity b -> Refl
+  STEither a b | Refl <- d1Identity a, Refl <- d1Identity b -> Refl
+  STLEither a b | Refl <- d1Identity a, Refl <- d1Identity b -> Refl
+  STMaybe t | Refl <- d1Identity t -> Refl
+  STArr _ t | Refl <- d1Identity t -> Refl
+  STScal _ -> Refl
+  STAccum{} -> error "Accumulators not allowed in input program"
+
+d1eIdentity :: SList STy env -> D1E env :~: env
+d1eIdentity SNil = Refl
+d1eIdentity (t `SCons` env) | Refl <- d1Identity t, Refl <- d1eIdentity env = Refl