3 files changed, 28 insertions, 35 deletions
diff --git a/src/CHAD/Accum.hs b/src/CHAD/Accum.hs
deleted file mode 100644
index d8a71b5..0000000
--- a/src/CHAD/Accum.hs
+++ /dev/null
@@ -1,27 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-module CHAD.Accum where
-
-import AST
-import CHAD.Types
-import Data
-
-
-
-makeAccumulators :: SList STy envPro -> Ex (Append (D2AcE envPro) env) t -> Ex env (InvTup t (D2E envPro))
-makeAccumulators SNil e = e
-makeAccumulators (t `SCons` envpro) e | Refl <- lemZeroInfoD2 t =
-  makeAccumulators envpro $
-    EWith ext (d2M t) (EZero ext (d2M t) (ENil ext)) e
-
-uninvertTup :: SList STy list -> STy core -> Ex env (InvTup core list) -> Ex env (TPair core (Tup list))
-uninvertTup SNil _ e = EPair ext e (ENil ext)
-uninvertTup (t `SCons` list) tcore e =
-  ELet ext (uninvertTup list (STPair tcore t) e) $
-    let recT = STPair (STPair tcore t) (tTup list)  -- type of the RHS of that let binding
-    in EPair ext
-         (EFst ext (EFst ext (EVar ext recT IZ)))
-         (EPair ext
-            (ESnd ext (EVar ext recT IZ))
-            (ESnd ext (EFst ext (EVar ext recT IZ))))
-
diff --git a/src/CHAD/EnvDescr.hs b/src/CHAD/EnvDescr.hs
index 4c287d7..49ae0e6 100644
--- a/src/CHAD/EnvDescr.hs
+++ b/src/CHAD/EnvDescr.hs
@@ -52,12 +52,12 @@ subDescr :: Descr env sto -> Subenv env env'
                        -> r)
          -> r
 subDescr DTop SETop k = k DTop SETop SETop SETop
-subDescr (des `DPush` (t, vid, sto)) (SEYes sub) k =
+subDescr (des `DPush` (t, vid, sto)) (SEYesR sub) k =
   subDescr des sub $ \des' submerge subaccum subd1e ->
     case sto of
-      SMerge -> k (des' `DPush` (t, vid, sto)) (SEYes submerge) subaccum (SEYes subd1e)
-      SAccum -> k (des' `DPush` (t, vid, sto)) submerge (SEYes subaccum) (SEYes subd1e)
-      SDiscr -> k (des' `DPush` (t, vid, sto)) submerge subaccum (SEYes subd1e)
+      SMerge -> k (des' `DPush` (t, vid, sto)) (SEYesR submerge) subaccum (SEYesR subd1e)
+      SAccum -> k (des' `DPush` (t, vid, sto)) submerge (SEYesR subaccum) (SEYesR subd1e)
+      SDiscr -> k (des' `DPush` (t, vid, sto)) submerge subaccum (SEYesR subd1e)
 subDescr (des `DPush` (_, _, sto)) (SENo sub) k =
   subDescr des sub $ \des' submerge subaccum subd1e ->
     case sto of
@@ -82,3 +82,15 @@ select s@SDiscr (DPush des (_, _, SMerge)) = select s des
 select s@SAccum (DPush des (_, _, SDiscr)) = select s des
 select s@SMerge (DPush des (_, _, SDiscr)) = select s des
 select s@SDiscr (DPush des (t, _, SDiscr)) = SCons t (select s des)
+
+selectSub :: Storage s -> Descr env sto -> Subenv env (Select env sto s)
+selectSub _ DTop = SETop
+selectSub s@SAccum (DPush des (_, _, SAccum)) = SEYesR (selectSub s des)
+selectSub s@SMerge (DPush des (_, _, SAccum)) = SENo (selectSub s des)
+selectSub s@SDiscr (DPush des (_, _, SAccum)) = SENo (selectSub s des)
+selectSub s@SAccum (DPush des (_, _, SMerge)) = SENo (selectSub s des)
+selectSub s@SMerge (DPush des (_, _, SMerge)) = SEYesR (selectSub s des)
+selectSub s@SDiscr (DPush des (_, _, SMerge)) = SENo (selectSub s des)
+selectSub s@SAccum (DPush des (_, _, SDiscr)) = SENo (selectSub s des)
+selectSub s@SMerge (DPush des (_, _, SDiscr)) = SENo (selectSub s des)
+selectSub s@SDiscr (DPush des (_, _, SDiscr)) = SEYesR (selectSub s des)
diff --git a/src/CHAD/Types.hs b/src/CHAD/Types.hs
index 974669d..83f013d 100644
--- a/src/CHAD/Types.hs
+++ b/src/CHAD/Types.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE TypeOperators #-}
 module CHAD.Types where
 
+import AST.Accum
 import AST.Types
 import Data
 
@@ -18,11 +19,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 +61,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
@@ -116,3 +117,10 @@ 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