CHAD case

4 files changed, 289 insertions, 26 deletions

diff --git a/chad-fast.cabal b/chad-fast.cabal
index 35fa7f8..efcf44e 100644
--- a/chad-fast.cabal
+++ b/chad-fast.cabal
@@ -11,6 +11,7 @@ build-type:          Simple
 library
   exposed-modules:
     AST
+    AST.Weaken
     CHAD
     -- Compile
     PreludeCu
diff --git a/src/AST.hs b/src/AST.hs
index 3179d92..b1f3e5d 100644
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -11,11 +11,13 @@
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE DeriveFunctor #-}
 {-# LANGUAGE DeriveFoldable #-}
-module AST where
+module AST (module AST, module AST.Weaken) where
 
 import Data.Kind (Type)
 import Data.Int
 
+import AST.Weaken
+
 
 data Nat = Z | S Nat
   deriving (Show, Eq, Ord)
@@ -36,10 +38,12 @@ data SList f l where
   SNil :: SList f '[]
   SCons :: f a -> SList f l -> SList f (a : l)
 deriving instance (forall a. Show (f a)) => Show (SList f l)
+infixr `SCons`
 
 data Ty
   = TNil
   | TPair Ty Ty
+  | TEither Ty Ty
   | TArr Nat Ty  -- ^ rank, element type
   | TScal ScalTy
   | TEVM [Ty] Ty
@@ -52,6 +56,7 @@ type STy :: Ty -> Type
 data STy t where
   STNil :: STy TNil
   STPair :: STy a -> STy b -> STy (TPair a b)
+  STEither :: STy a -> STy b -> STy (TEither a b)
   STArr :: SNat n -> STy t -> STy (TArr n t)
   STScal :: SScalTy t -> STy (TScal t)
   STEVM :: SList STy env -> STy t -> STy (TEVM env t)
@@ -93,8 +98,12 @@ data Expr x env t where
 
   -- base types
   EPair :: x (TPair a b) -> Expr x env a -> Expr x env b -> Expr x env (TPair a b)
-  EFst :: x a -> STy b -> Expr x env (TPair a b) -> Expr x env a
-  ESnd :: x b -> STy a -> Expr x env (TPair a b) -> Expr x env b
+  EFst :: x a -> Expr x env (TPair a b) -> Expr x env a
+  ESnd :: x b -> Expr x env (TPair a b) -> Expr x env b
+  ENil :: x TNil -> Expr x env TNil
+  EInl :: x (TEither a b) -> STy b -> Expr x env a -> Expr x env (TEither a b)
+  EInr :: x (TEither a b) -> STy a -> Expr x env b -> Expr x env (TEither a b)
+  ECase :: x c -> Expr x env (TEither a b) -> Expr x (a : env) c -> Expr x (b : env) c -> Expr x env c
 
   -- array operations
   EBuild1 :: x (TArr (S Z) t) -> Expr x env TIx -> Expr x (TIx : env) t -> Expr x env (TArr (S Z) t)
@@ -112,6 +121,9 @@ data Expr x env t where
   EMScope :: Expr x env (TEVM (t : venv) a) -> Expr x env (TEVM venv (TPair a t))
   EMReturn :: SList STy venv -> Expr x env t -> Expr x env (TEVM venv t)
   EMBind :: Expr x env (TEVM venv a) -> Expr x (a : env) (TEVM venv b) -> Expr x env (TEVM venv b)
+
+  -- partiality
+  EError :: STy a -> String -> Expr x env a
 deriving instance (forall ty. Show (x ty)) => Show (Expr x env t)
 
 type SOp :: Ty -> Ty -> Type
@@ -139,17 +151,30 @@ typeOf :: Expr x env t -> STy t
 typeOf = \case
   EVar _ t _ -> t
   ELet _ _ e -> typeOf e
+
+  EPair _ a b -> STPair (typeOf a) (typeOf b)
+  EFst _ e | STPair t _ <- typeOf e -> t
+  ESnd _ e | STPair _ t <- typeOf e -> t
+  ENil _ -> STNil
+  EInl _ t2 e -> STEither (typeOf e) t2
+  EInr _ t1 e -> STEither t1 (typeOf e)
+  ECase _ _ a _ -> typeOf a
+
   EBuild1 _ _ e -> STArr (SS SZ) (typeOf e)
   EBuild _ n _ e -> STArr n (typeOf e)
   EFold1 _ _ e | STArr (SS n) t <- typeOf e -> STArr n t
 
-  -- expression operations
   EConst _ t _ -> STScal t
   EIdx1 _ e _ | STArr (SS n) t <- typeOf e -> STArr n t
   EIdx _ e _ | STArr _ t <- typeOf e -> t
   EOp _ op _ -> opt2 op
 
   EMOne t _ _ -> STEVM t STNil
+  EMScope e | STEVM (SCons t env) a <- typeOf e -> STEVM env (STPair a t)
+  EMReturn env e -> STEVM env (typeOf e)
+  EMBind _ e -> typeOf e
+
+  EError t _ -> t
 
 unSNat :: SNat n -> Nat
 unSNat SZ = Z
@@ -159,6 +184,7 @@ unSTy :: STy t -> Ty
 unSTy = \case
   STNil -> TNil
   STPair a b -> TPair (unSTy a) (unSTy b)
+  STEither a b -> TEither (unSTy a) (unSTy b)
   STArr n t -> TArr (unSNat n) (unSTy t)
   STScal t -> TScal (unSScalTy t)
   STEVM l t -> TEVM (unSList l) (unSTy t)
@@ -179,17 +205,6 @@ fromNat :: Nat -> Int
 fromNat Z = 0
 fromNat (S n) = succ (fromNat n)
 
-data env :> env' where
-  WId :: env :> env
-  WSink :: env :> (t : env)
-  WCopy :: env :> env' -> (t : env) :> (t : env')
-  WPop :: (t : env) :> env' -> env :> env'
-  WThen :: env1 :> env2 -> env2 :> env3 -> env1 :> env3
-deriving instance Show (env :> env')
-
-(.>) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3
-(.>) = flip WThen
-
 infixr @>
 (@>) :: env :> env' -> Idx env t -> Idx env' t
 WId @> i = i
@@ -203,6 +218,13 @@ weakenExpr :: env :> env' -> Expr x env t -> Expr x env' t
 weakenExpr w = \case
   EVar x t i -> EVar x t (w @> i)
   ELet x rhs body -> ELet x (weakenExpr w rhs) (weakenExpr (WCopy w) body)
+  EPair x e1 e2 -> EPair x (weakenExpr w e1) (weakenExpr w e2)
+  EFst x e -> EFst x (weakenExpr w e)
+  ESnd x e -> ESnd x (weakenExpr w e)
+  ENil x -> ENil x
+  EInl x t e -> EInl x t (weakenExpr w e)
+  EInr x t e -> EInr x t (weakenExpr w e)
+  ECase x e1 e2 e3 -> ECase x (weakenExpr w e1) (weakenExpr (WCopy w) e2) (weakenExpr (WCopy w) e3)
   EBuild1 x e1 e2 -> EBuild1 x (weakenExpr w e1) (weakenExpr (WCopy w) e2)
   EBuild x n es e -> EBuild x n (weakenVec w es) (weakenExpr (wcopyN n w) e)
   EFold1 x e1 e2 -> EFold1 x (weakenExpr (WCopy (WCopy w)) e1) (weakenExpr w e2)
@@ -211,6 +233,10 @@ weakenExpr w = \case
   EIdx x e1 es -> EIdx x (weakenExpr w e1) (weakenVec w es)
   EOp x op e -> EOp x op (weakenExpr w e)
   EMOne t i e -> EMOne t i (weakenExpr w e)
+  EMScope e -> EMScope (weakenExpr w e)
+  EMReturn t e -> EMReturn t (weakenExpr w e)
+  EMBind e1 e2 -> EMBind (weakenExpr w e1) (weakenExpr (WCopy w) e2)
+  EError t s -> EError t s
 
 wcopyN :: SNat n -> env :> env' -> ConsN n TIx env :> ConsN n TIx env'
 wcopyN SZ w = w
@@ -219,3 +245,7 @@ wcopyN (SS n) w = WCopy (wcopyN n w)
 weakenVec :: (env :> env') -> Vec n (Expr x env TIx) -> Vec n (Expr x env' TIx)
 weakenVec _ VNil = VNil
 weakenVec w (e :< v) = weakenExpr w e :< weakenVec w v
+
+slistMap :: (forall t. f t -> g t) -> SList f list -> SList g list
+slistMap _ SNil = SNil
+slistMap f (SCons x list) = SCons (f x) (slistMap f list)
diff --git a/src/AST/Weaken.hs b/src/AST/Weaken.hs
new file mode 100644
index 0000000..56b7a74
--- /dev/null
+++ b/src/AST/Weaken.hs
@@ -0,0 +1,43 @@
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+
+-- The reason why this is a separate module with little in it:
+{-# LANGUAGE AllowAmbiguousTypes #-}
+
+module AST.Weaken where
+
+
+data env :> env' where
+  WId :: env :> env
+  WSink :: env :> (t : env)
+  WCopy :: env :> env' -> (t : env) :> (t : env')
+  WPop :: (t : env) :> env' -> env :> env'
+  WThen :: env1 :> env2 -> env2 :> env3 -> env1 :> env3
+deriving instance Show (env :> env')
+
+(.>) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3
+(.>) = flip WThen
+
+type family Append a b where
+  Append '[] l = l
+  Append (x : xs) l = x : Append xs l
+
+data ListSpine list where
+  LSNil :: ListSpine '[]
+  LSCons :: ListSpine list -> ListSpine (t : list)
+
+class KnownListSpine list where knownListSpine :: ListSpine list
+instance KnownListSpine '[] where knownListSpine = LSNil
+instance KnownListSpine list => KnownListSpine (t : list) where knownListSpine = LSCons knownListSpine
+
+wSinks :: forall list env. KnownListSpine list => env :> Append list env
+wSinks = go (knownListSpine :: ListSpine list)
+  where
+    go :: forall list'. ListSpine list' -> env :> Append list' env
+    go LSNil = WId
+    go (LSCons spine) = WSink .> go spine
diff --git a/src/CHAD.hs b/src/CHAD.hs
index f01ab9e..cd4445e 100644
--- a/src/CHAD.hs
+++ b/src/CHAD.hs
@@ -7,6 +7,8 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 module CHAD where
 
 import Data.Functor.Const
@@ -18,15 +20,16 @@ type Ex = Expr (Const ())
 
 data Bindings f env env' where
   BTop :: Bindings f env env
-  BPush :: Bindings f env env' -> f env' t -> Bindings f env (t : env')
+  BPush :: Bindings f env env' -> (STy t, f env' t) -> Bindings f env (t : env')
 deriving instance (forall e t. Show (f e t)) => Show (Bindings f env env')
+infixl `BPush`
 
 weakenBindings :: (forall e1 e2 t. e1 :> e2 -> f e1 t -> f e2 t)
                -> env1 :> env2 -> Bindings f env1 env'
                -> (forall env2'. Bindings f env2 env2' -> env' :> env2' -> r) -> r
 weakenBindings _ w BTop k = k BTop w
-weakenBindings wf w (BPush b x) k =
-  weakenBindings wf w b $ \b' w' -> k (BPush b' (wf w' x)) (WCopy w')
+weakenBindings wf w (BPush b (t, x)) k =
+  weakenBindings wf w b $ \b' w' -> k (BPush b' (t, wf w' x)) (WCopy w')
 
 sinkWithBindings :: Bindings f env env' -> env :> env'
 sinkWithBindings BTop = WId
@@ -34,22 +37,59 @@ sinkWithBindings (BPush b _) = WSink .> sinkWithBindings b
 
 bconcat :: Bindings f env1 env2 -> Bindings f env2 env3 -> Bindings f env1 env3
 bconcat b1 BTop = b1
-bconcat b1 (BPush b2 x) = BPush (bconcat b1 b2) x
+bconcat b1 (BPush b2 (t, x)) = BPush (bconcat b1 b2) (t, x)
 
 bconcat' :: (forall e1 e2 t. e1 :> e2 -> f e1 t -> f e2 t)
          -> Bindings f env env1 -> Bindings f env env2
          -> (forall env12. Bindings f env env12 -> r) -> r
 bconcat' wf b1 b2 k = weakenBindings wf (sinkWithBindings b1) b2 $ \b2' _ -> k (bconcat b1 b2')
 
+bsnoc :: STy t -> f env t -> Bindings f (t : env) env' -> Bindings f env env'
+bsnoc t x b = bconcat (BTop `BPush` (t, x)) b
+
+data TupBindsReconstruct f env1 env2 env3 =
+  forall env4.
+    TupBindsReconstruct (Bindings f env3 env4)
+                        (env2 :> env4)
+
+data TupBinds f env1 env2 =
+  forall tape.
+    TupBinds (STy tape)
+             (forall env2'. env2 :> env2' -> Ex env2' tape)
+             (forall env3. env1 :> env3 -> Idx env3 tape -> TupBindsReconstruct f env1 env2 env3)
+
+tupBinds :: Bindings Ex env1 env2 -> TupBinds Ex env1 env2
+tupBinds BTop = TupBinds STNil (\_ -> ENil ext) (\w _ -> TupBindsReconstruct BTop w)
+tupBinds (BPush binds (t, _))
+  | TupBinds tape collect recon <- tupBinds binds
+  = TupBinds (STPair tape t)
+             (\w -> EPair ext (collect (w .> WSink))
+                              (EVar ext t (w @> IZ)))
+             (\w tapeidx ->
+               case recon (WSink .> w) IZ of
+                 TupBindsReconstruct rebinds wunder ->
+                   let rebinds1 = bsnoc tape (EFst ext (EVar ext (STPair tape t) tapeidx)) rebinds
+                   in TupBindsReconstruct
+                        (rebinds1 `BPush`
+                          (t, ESnd ext (EVar ext (STPair tape t)
+                                             (sinkWithBindings rebinds1 @> tapeidx))))
+                        (WCopy wunder))
+
+letBinds :: Bindings Ex env env' -> Ex env' t -> Ex env t
+letBinds BTop = id
+letBinds (BPush b (_, rhs)) = letBinds b . ELet ext rhs
+
 type family D1 t where
   D1 TNil = TNil
   D1 (TPair a b) = TPair (D1 a) (D1 b)
+  D1 (TEither a b) = TEither (D1 a) (D1 b)
   D1 (TArr n t) = TArr n (D1 t)
   D1 (TScal t) = TScal t
 
 type family D2 t where
   D2 TNil = TNil
-  D2 (TPair a b) = TPair (D2 a) (D2 b)
+  D2 (TPair a b) = TEither TNil (TPair (D2 a) (D2 b))
+  D2 (TEither a b) = TEither TNil (TEither (D2 a) (D2 b))
   -- D2 (TArr n t) = _
   D2 (TScal t) = D2s t
 
@@ -71,13 +111,15 @@ type family D2E env where
 d1 :: STy t -> STy (D1 t)
 d1 STNil = STNil
 d1 (STPair a b) = STPair (d1 a) (d1 b)
+d1 (STEither a b) = STEither (d1 a) (d1 b)
 d1 (STArr n t) = STArr n (d1 t)
 d1 (STScal t) = STScal t
 d1 STEVM{} = error "EVM not allowed in input program"
 
 d2 :: STy t -> STy (D2 t)
 d2 STNil = STNil
-d2 (STPair a b) = STPair (d2 a) (d2 b)
+d2 (STPair a b) = STEither STNil (STPair (d2 a) (d2 b))
+d2 (STEither a b) = STEither STNil (STEither (d2 a) (d2 b))
 d2 STArr{} = error "TODO arrays"
 d2 (STScal t) = case t of
   STI32 -> STNil
@@ -87,6 +129,10 @@ d2 (STScal t) = case t of
   STBool -> STNil
 d2 STEVM{} = error "EVM not allowed in input program"
 
+d2e :: SList STy list -> SList STy (D2E list)
+d2e SNil = SNil
+d2e (SCons t list) = SCons (d2 t) (d2e list)
+
 d2list :: SList STy env -> SList STy (D2E env)
 d2list SNil = SNil
 d2list (SCons x l) = SCons (d2 x) (d2list l)
@@ -99,6 +145,19 @@ conv2Idx :: Idx env t -> Idx (D2E env) (D2 t)
 conv2Idx IZ = IZ
 conv2Idx (IS i) = IS (conv2Idx i)
 
+zero :: STy t -> Ex env (D2 t)
+zero STNil = ENil ext
+zero (STPair t1 t2) = EInl ext (STPair (d2 t1) (d2 t2)) (ENil ext)
+zero (STEither t1 t2) = EInl ext (STEither (d2 t1) (d2 t2)) (ENil ext)
+zero STArr{} = error "TODO arrays"
+zero (STScal t) = case t of
+  STI32 -> ENil ext
+  STI64 -> ENil ext
+  STF32 -> EConst ext STF32 0.0
+  STF64 -> EConst ext STF64 0.0
+  STBool -> ENil ext
+zero STEVM{} = error "EVM not allowed in input program"
+
 data Ret env t =
   forall env'.
     Ret (Bindings Ex (D1E env) env')
@@ -106,21 +165,151 @@ data Ret env t =
         (Ex (D2 t : env') (TEVM (D2E env) TNil))
 deriving instance Show (Ret env t)
 
+data RetPair env0 env t =
+    RetPair (Ex env (D1 t))
+            (Ex (D2 t : env) (TEVM (D2E env0) TNil))
+  deriving (Show)
+
+data Rets env0 env list =
+  forall env'.
+    Rets (Bindings Ex env env')
+         (SList (RetPair env0 env') list)
+deriving instance Show (Rets env0 env list)
+
+-- d1W :: env :> env' -> D1E env :> D1E env'
+-- d1W WId = WId
+-- d1W WSink = WSink
+-- d1W (WCopy w) = WCopy (d1W w)
+-- d1W (WPop w) = WPop (d1W w)
+-- d1W (WThen u w) = WThen (d1W u) (d1W w)
+
+weakenRetPair :: env :> env' -> RetPair env0 env t -> RetPair env0 env' t
+weakenRetPair w (RetPair e1 e2) = RetPair (weakenExpr w e1) (weakenExpr (WCopy w) e2)
+
+weakenRets :: env :> env' -> Rets env0 env list -> Rets env0 env' list
+weakenRets w (Rets binds list) =
+  weakenBindings weakenExpr w binds $ \binds' wbinds' ->
+    Rets binds' (slistMap (weakenRetPair wbinds') list)
+
+retConcat :: forall env list. SList (Ret env) list -> Rets env (D1E env) list
+retConcat SNil = Rets BTop SNil
+retConcat (SCons (Ret (b :: Bindings Ex (D1E env) env2) p d) list)
+  | Rets binds pairs <- weakenRets (sinkWithBindings b) (retConcat list)
+  = Rets (bconcat b binds)
+         (SCons (RetPair (weakenExpr (sinkWithBindings binds) p)
+                         (weakenExpr (WCopy (sinkWithBindings binds)) d))
+                pairs)
+
 drev :: SList STy env -> Ex env t -> Ret env t
 drev senv = \case
   EVar _ t i ->
     Ret BTop
         (EVar ext (d1 t) (conv1Idx i))
         (EMOne (d2list senv) (conv2Idx i) (EVar ext (d2 t) IZ))
+
   ELet _ rhs body
     | Ret rhs0 rhs1 rhs2 <- drev senv rhs
     , Ret body0 body1 body2 <- drev (SCons (typeOf rhs) senv) body ->
     weakenBindings weakenExpr (WCopy (sinkWithBindings rhs0)) body0 $ \body0' wbody0' ->
-    Ret (bconcat (BPush rhs0 rhs1) body0')
+    Ret (bconcat (rhs0 `BPush` (d1 (typeOf rhs), rhs1)) body0')
         (weakenExpr wbody0' body1)
         (EMBind (EMScope (weakenExpr (WCopy wbody0') body2))
-                (ELet ext (ESnd ext STNil (EVar ext (STPair STNil (d2 (typeOf rhs))) IZ)) $
-                  weakenExpr (WCopy (WSink .> WSink .> WPop (sinkWithBindings body0'))) rhs2))
+                (ELet ext (ESnd ext (EVar ext (STPair STNil (d2 (typeOf rhs))) IZ)) $
+                  weakenExpr (WCopy (wSinks @[_,_] .> WPop (sinkWithBindings body0'))) rhs2))
+
+  EPair _ a b
+    | Rets binds (RetPair a1 a2 `SCons` RetPair b1 b2 `SCons` SNil)
+        <- retConcat $ drev senv a `SCons` drev senv b `SCons` SNil
+    , let dt = STPair (d2 (typeOf a)) (d2 (typeOf b)) ->
+    Ret binds
+        (EPair ext a1 b1)
+        (ECase ext (EVar ext (STEither STNil (STPair (d2 (typeOf a)) (d2 (typeOf b)))) IZ)
+           (EMReturn (d2e senv) (ENil ext))
+           (EMBind (ELet ext (EFst ext (EVar ext dt IZ))
+                      (weakenExpr (WCopy (wSinks @[_,_])) a2))
+                   (ELet ext (ESnd ext (EVar ext dt (IS IZ)))
+                      (weakenExpr (WCopy (wSinks @[_,_,_])) b2))))
+
+  EFst _ e
+    | Ret e0 e1 e2 <- drev senv e
+    , STPair t1 t2 <- typeOf e ->
+    Ret e0
+        (EFst ext e1)
+        (ELet ext (EInr ext STNil (EPair ext (EVar ext (d2 t1) IZ) (zero t2))) $
+           weakenExpr (WCopy WSink) e2)
+
+  ESnd _ e
+    | Ret e0 e1 e2 <- drev senv e
+    , STPair t1 t2 <- typeOf e ->
+    Ret e0
+        (ESnd ext e1)
+        (ELet ext (EInr ext STNil (EPair ext (zero t1) (EVar ext (d2 t2) IZ))) $
+           weakenExpr (WCopy WSink) e2)
+
+  ENil _ -> Ret BTop (ENil ext) (EMReturn (d2e senv) (ENil ext))
+
+  EInl _ t2 e
+    | Ret e0 e1 e2 <- drev senv e ->
+    Ret e0
+        (EInl ext (d1 t2) e1)
+        (ECase ext (EVar ext (STEither STNil (STEither (d2 (typeOf e)) (d2 t2))) IZ)
+           (EMReturn (d2e senv) (ENil ext))
+           (ECase ext (EVar ext (STEither (d2 (typeOf e)) (d2 t2)) IZ)
+              (weakenExpr (WCopy (wSinks @[_,_])) e2)
+              (EError (STEVM (d2e senv) STNil) "inl<-dinr")))
+
+  EInr _ t1 e
+    | Ret e0 e1 e2 <- drev senv e ->
+    Ret e0
+        (EInr ext (d1 t1) e1)
+        (ECase ext (EVar ext (STEither STNil (STEither (d2 t1) (d2 (typeOf e)))) IZ)
+           (EMReturn (d2e senv) (ENil ext))
+           (ECase ext (EVar ext (STEither (d2 t1) (d2 (typeOf e))) IZ)
+              (EError (STEVM (d2e senv) STNil) "inr<-dinl")
+              (weakenExpr (WCopy (wSinks @[_,_])) e2)))
+
+  ECase _ e a b
+    | STEither t1 t2 <- typeOf e
+    , Ret e0 e1 e2 <- drev senv e
+    , Ret a0 a1 a2 <- drev (SCons t1 senv) a
+    , Ret b0 b1 b2 <- drev (SCons t2 senv) b
+    , TupBinds tapeA collectA reconA <- tupBinds a0
+    , TupBinds tapeB collectB reconB <- tupBinds b0
+    , let tPrimal = STPair (d1 (typeOf a)) (STEither tapeA tapeB) ->
+    weakenBindings weakenExpr (WCopy (WSink .> sinkWithBindings e0)) a0 $ \a0' wa0' ->
+    weakenBindings weakenExpr (WCopy (WSink .> sinkWithBindings e0)) b0 $ \b0' wb0' ->
+    Ret (e0 `BPush`
+         (d1 (typeOf e), e1) `BPush`
+         (tPrimal,
+            ECase ext (EVar ext (d1 (typeOf e)) IZ)
+              (letBinds a0' (EPair ext (weakenExpr wa0' a1) (EInl ext tapeB (collectA wa0'))))
+              (letBinds b0' (EPair ext (weakenExpr wb0' b1) (EInr ext tapeA (collectB wb0'))))))
+        (EFst ext (EVar ext tPrimal IZ))
+        (EMBind
+           (ECase ext (EVar ext (STEither (d1 t1) (d1 t2)) (IS (IS IZ)))
+              (ECase ext (ESnd ext (EVar ext tPrimal (IS (IS IZ))))
+                 (case reconA (WSink .> WCopy (wSinks @[_,_,_] .> sinkWithBindings e0)) IZ of
+                    TupBindsReconstruct rebinds wrebinds ->
+                      letBinds rebinds $
+                        ELet ext (EVar ext (d2 (typeOf a)) (sinkWithBindings rebinds @> IS (IS IZ))) $
+                          EMBind (weakenExpr (WCopy wrebinds) (EMScope a2))
+                                 (EMReturn (d2e senv)
+                                    (EInr ext STNil (EInl ext (d2 t2)
+                                       (ESnd ext (EVar ext (STPair STNil (d2 t1)) IZ))))))
+                 (EError (STEVM (d2e senv) (STEither STNil (STEither (d2 t1) (d2 t2)))) "dcase l/rtape"))
+              (ECase ext (ESnd ext (EVar ext tPrimal (IS (IS IZ))))
+                 (EError (STEVM (d2e senv) (STEither STNil (STEither (d2 t1) (d2 t2)))) "dcase r/ltape")
+                 (case reconB (WSink .> WCopy (wSinks @[_,_,_] .> sinkWithBindings e0)) IZ of
+                    TupBindsReconstruct rebinds wrebinds ->
+                      letBinds rebinds $
+                        ELet ext (EVar ext (d2 (typeOf a)) (sinkWithBindings rebinds @> IS (IS IZ))) $
+                          EMBind (weakenExpr (WCopy wrebinds) (EMScope b2))
+                                 (EMReturn (d2e senv)
+                                    (EInr ext STNil (EInr ext (d2 t1)
+                                       (ESnd ext (EVar ext (STPair STNil (d2 t2)) IZ))))))))
+           (weakenExpr (WCopy (wSinks @[_,_,_])) e2))
+
   _ -> undefined
-  where
-    ext = Const ()
+
+ext :: Const () a
+ext = Const ()