diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/CHAD.hs | 365 |
1 files changed, 99 insertions, 266 deletions
diff --git a/src/CHAD.hs b/src/CHAD.hs index 9e1f038..b1251aa 100644 --- a/src/CHAD.hs +++ b/src/CHAD.hs @@ -16,7 +16,6 @@ module CHAD where import Data.Bifunctor (first, second) import Data.Kind (Type) -import Data.Proxy import Data.Some import GHC.TypeLits (Symbol) @@ -274,16 +273,43 @@ subenvOnehot (SCons _ env) IZ = SEYes (subenvNone env) subenvOnehot (SCons _ env) (IS i) = SENo (subenvOnehot env i) subenvOnehot SNil i = case i of {} -subenvUnion :: Subenv env env1 -> Subenv env env2 -> (forall env3. Subenv env env3 -> Subenv env3 env1 -> Subenv env3 env2 -> r) -> r -subenvUnion SETop SETop k = k SETop SETop SETop -subenvUnion (SENo sub1) (SENo sub2) k = - subenvUnion sub1 sub2 $ \sub3 s31 s32 -> k (SENo sub3) s31 s32 -subenvUnion (SEYes sub1) (SENo sub2) k = - subenvUnion sub1 sub2 $ \sub3 s31 s32 -> k (SEYes sub3) (SEYes s31) (SENo s32) -subenvUnion (SENo sub1) (SEYes sub2) k = - subenvUnion sub1 sub2 $ \sub3 s31 s32 -> k (SEYes sub3) (SENo s31) (SEYes s32) -subenvUnion (SEYes sub1) (SEYes sub2) k = - subenvUnion sub1 sub2 $ \sub3 s31 s32 -> k (SEYes sub3) (SEYes s31) (SEYes s32) +subenvPlus :: SList STy env + -> Subenv env env1 -> Subenv env env2 + -> (forall env3. Subenv env env3 + -> Subenv env3 env1 + -> Subenv env3 env2 + -> (Ex exenv (Tup (D2E env1)) + -> Ex exenv (Tup (D2E env2)) + -> Ex exenv (Tup (D2E env3))) + -> r) + -> r +subenvPlus SNil SETop SETop k = k SETop SETop SETop (\_ _ -> ENil ext) +subenvPlus (SCons _ env) (SENo sub1) (SENo sub2) k = + subenvPlus env sub1 sub2 $ \sub3 s31 s32 pl -> k (SENo sub3) s31 s32 pl +subenvPlus (SCons _ env) (SEYes sub1) (SENo sub2) k = + subenvPlus env sub1 sub2 $ \sub3 s31 s32 pl -> + k (SEYes sub3) (SEYes s31) (SENo s32) $ \e1 e2 -> + ELet ext e1 $ + EPair ext (pl (EFst ext (EVar ext (typeOf e1) IZ)) + (weakenExpr WSink e2)) + (ESnd ext (EVar ext (typeOf e1) IZ)) +subenvPlus (SCons _ env) (SENo sub1) (SEYes sub2) k = + subenvPlus env sub1 sub2 $ \sub3 s31 s32 pl -> + k (SEYes sub3) (SENo s31) (SEYes s32) $ \e1 e2 -> + ELet ext e2 $ + EPair ext (pl (weakenExpr WSink e1) + (EFst ext (EVar ext (typeOf e2) IZ))) + (ESnd ext (EVar ext (typeOf e2) IZ)) +subenvPlus (SCons t env) (SEYes sub1) (SEYes sub2) k = + subenvPlus env sub1 sub2 $ \sub3 s31 s32 pl -> + k (SEYes sub3) (SEYes s31) (SEYes s32) $ \e1 e2 -> + ELet ext e1 $ + ELet ext (weakenExpr WSink e2) $ + EPair ext (pl (EFst ext (EVar ext (typeOf e1) (IS IZ))) + (EFst ext (EVar ext (typeOf e2) IZ))) + (plus t + (ESnd ext (EVar ext (typeOf e1) (IS IZ))) + (ESnd ext (EVar ext (typeOf e2) IZ))) expandSubenvZeros :: SList STy env0 -> Subenv env0 env0F -> Ex env (Tup (D2E env0F)) -> Ex env (Tup (D2E env0)) expandSubenvZeros _ SETop _ = ENil ext @@ -293,6 +319,25 @@ expandSubenvZeros (SCons t ts) (SEYes sub) e = in EPair ext (expandSubenvZeros ts sub (EFst ext var)) (ESnd ext var) expandSubenvZeros (SCons t ts) (SENo sub) e = EPair ext (expandSubenvZeros ts sub e) (zero t) +unscope :: Descr env0 sto + -> STy a -> Storage s + -> Subenv (Select (a : env0) (s : sto) "merge") envSub + -> Ex env (TEVM (D2E (Select (a : env0) (s : sto) "accum")) (Tup (D2E envSub))) + -> (forall envSub'. + Subenv (Select env0 sto "merge") envSub' + -> Ex env (TEVM (D2E (Select env0 sto "accum")) (TPair (Tup (D2E envSub')) (D2 a))) + -> r) + -> r +unscope des ty s sub e k = case s of + SAccum -> k sub (EMScope e) + SMerge -> case sub of + SEYes sub' -> k sub' e + SENo sub' -> k sub' $ + EMBind e $ + EMReturn (d2e (select SAccum des)) $ + EPair ext (EVar ext (tTup (d2e (subList (select SMerge des) sub'))) IZ) + (zero ty) + -- d1W :: env :> env' -> D1E env :> D1E env' -- d1W WId = WId -- d1W WSink = WSink @@ -425,60 +470,26 @@ drev des policy = \case , Some storage <- policy des (typeOf rhs) , Ret body0 body1 subBody body2 <- drev (des `DPush` (typeOf rhs, storage)) policy body -> weakenBindings weakenExpr (WCopy (sinkWithBindings rhs0)) body0 $ \body0' wbody0' -> - case storage of - SAccum -> - subenvUnion subRHS subBody $ \subBoth subRHS2Both subBody2Both -> - let bodyResType = STPair (tTup (d2e (subList (select SMerge des) subBody))) (d2 (typeOf rhs)) in - Ret (bconcat (rhs0 `BPush` (d1 (typeOf rhs), rhs1)) body0') - (weakenExpr wbody0' body1) - subBoth - (EMBind - (weakenExpr (WCopy wbody0') (EMScope body2)) - (ELet ext (ESnd ext (EVar ext bodyResType IZ)) $ - EMBind - (weakenExpr (WCopy (wSinks @[_,_] .> WPop (sinkWithBindings body0'))) rhs2) - (EMReturn d2acc (plusTup (subList (select SMerge des) subBoth) - (expandSubenvZeros - (subList (select SMerge des) subBoth) - subBody2Both - (EFst ext (EVar ext bodyResType (IS (IS IZ))))) - (expandSubenvZeros - (subList (select SMerge des) subBoth) - subRHS2Both - (EVar ext (tTup (d2e (subList (select SMerge des) subRHS))) IZ)))))) - - SMerge -> case subBody of -- is the let-bound variable used in the body? - SENo subBody' -> -- it isn't, so the RHS was dead code? Let's not differentiate through the RHS then, in any case - Ret (bconcat (rhs0 `BPush` (d1 (typeOf rhs), rhs1)) body0') - (weakenExpr wbody0' body1) - subBody' - (weakenExpr (WCopy wbody0') body2) -- we have no cotangent for the RHS, nothing to pass on, so it's just this - SEYes subBody' -> - subenvUnion subRHS subBody' $ \subBoth subRHS2Both subBody2Both -> - let bodyResType = STPair (tTup (d2e (subList (select SMerge des) subBody'))) (d2 (typeOf rhs)) in - Ret (bconcat (rhs0 `BPush` (d1 (typeOf rhs), rhs1)) body0') - (weakenExpr wbody0' body1) - subBoth - (EMBind - (weakenExpr (WCopy wbody0') body2) - (ELet ext (ESnd ext (EVar ext bodyResType IZ)) $ - EMBind - (weakenExpr (WCopy (wSinks @[_,_] .> WPop (sinkWithBindings body0'))) rhs2) - (EMReturn d2acc (plusTup (subList (select SMerge des) subBoth) - (expandSubenvZeros - (subList (select SMerge des) subBoth) - subBody2Both - (EFst ext (EVar ext bodyResType (IS (IS IZ))))) - (expandSubenvZeros - (subList (select SMerge des) subBoth) - subRHS2Both - (EVar ext (tTup (d2e (subList (select SMerge des) subRHS))) IZ)))))) + unscope des (typeOf rhs) storage subBody body2 $ \subBody' body2' -> + subenvPlus (select SMerge des) subRHS subBody' $ \subBoth _ _ plus_RHS_Body -> + let bodyResType = STPair (tTup (d2e (subList (select SMerge des) subBody'))) (d2 (typeOf rhs)) in + Ret (bconcat (rhs0 `BPush` (d1 (typeOf rhs), rhs1)) body0') + (weakenExpr wbody0' body1) + subBoth + (EMBind + (weakenExpr (WCopy wbody0') body2') + (EMBind + (ELet ext (ESnd ext (EVar ext bodyResType IZ)) $ + weakenExpr (WCopy (wSinks @[_,_] .> WPop (sinkWithBindings body0'))) rhs2) + (EMReturn d2acc (plus_RHS_Body + (EVar ext (tTup (d2e (subList (select SMerge des) subRHS))) IZ) + (EFst ext (EVar ext bodyResType (IS IZ))))))) EPair _ a b | Rets binds (RetPair a1 subA a2 `SCons` RetPair b1 subB b2 `SCons` SNil) <- retConcat $ drev des policy a `SCons` drev des policy b `SCons` SNil , let dt = STPair (d2 (typeOf a)) (d2 (typeOf b)) -> - subenvUnion subA subB $ \subBoth subA2Both subB2Both -> + subenvPlus (select SMerge des) subA subB $ \subBoth _ _ plus_A_B -> Ret binds (EPair ext a1 b1) subBoth @@ -489,15 +500,9 @@ drev des policy = \case EMBind (ELet ext (ESnd ext (EVar ext dt (IS IZ))) (weakenExpr (WCopy (wSinks @[_,_,_])) b2)) $ EMReturn d2acc - (plusTup (subList (select SMerge des) subBoth) - (expandSubenvZeros - (subList (select SMerge des) subBoth) - subA2Both - (EVar ext (tTup (d2e (subList (select SMerge des) subA))) (IS IZ))) - (expandSubenvZeros - (subList (select SMerge des) subBoth) - subB2Both - (EVar ext (tTup (d2e (subList (select SMerge des) subB))) IZ))))) + (plus_A_B + (EVar ext (tTup (d2e (subList (select SMerge des) subA))) (IS IZ)) + (EVar ext (tTup (d2e (subList (select SMerge des) subB))) IZ)))) EFst _ e | Ret e0 e1 sub e2 <- drev des policy e @@ -553,7 +558,11 @@ drev des policy = \case , 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' -> - caseOutSubenv des t1 storageA t2 storageB Proxy Proxy subE subA subB $ \subOut subOutE expandA2 expandB2 -> + unscope des t1 storageA subA a2 $ \subA' a2' -> + unscope des t2 storageB subB b2 $ \subB' b2' -> + subenvPlus (select SMerge des) subA' subB' $ \subAB sAB_A sAB_B _ -> + subenvPlus (select SMerge des) subAB subE $ \subOut _ _ plus_AB_E -> + let tCaseRet = STPair (tTup (d2e (subList (select SMerge des) subAB))) (STEither (d2 t1) (d2 t2)) in Ret (e0 `BPush` (d1 (typeOf e), e1) `BPush` (tPrimal, @@ -569,27 +578,33 @@ drev des policy = \case TupBindsReconstruct rebinds wrebinds -> letBinds rebinds $ ELet ext (EVar ext (d2 (typeOf a)) (sinkWithBindings rebinds @> IS (IS IZ))) $ - EMBind (weakenExpr (WCopy wrebinds) $ expandA2 a2) + EMBind (weakenExpr (WCopy wrebinds) a2') (EMReturn d2acc - (EInr ext STNil (EInl ext (d2 t2) - (ESnd ext (EVar ext (STPair (tTup (d2e (subList (select SMerge des) subOut))) (d2 t1)) IZ)))))) - (EError (STEVM d2acc (STEither STNil (STEither (d2 t1) (d2 t2)))) "dcase l/rtape")) + (EPair ext + (expandSubenvZeros (subList (select SMerge des) subAB) sAB_A $ + EFst ext (EVar ext (STPair (tTup (d2e (subList (select SMerge des) subA'))) (d2 t1)) IZ)) + (EInl ext (d2 t2) + (ESnd ext (EVar ext (STPair (tTup (d2e (subList (select SMerge des) subA'))) (d2 t1)) IZ)))))) + (EError (STEVM d2acc tCaseRet) "dcase l/rtape")) (ECase ext (ESnd ext (EVar ext tPrimal (IS (IS IZ)))) - (EError (STEVM d2acc (STEither STNil (STEither (d2 t1) (d2 t2)))) "dcase r/ltape") + (EError (STEVM d2acc tCaseRet) "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) $ expandB2 b2) + EMBind (weakenExpr (WCopy wrebinds) b2') (EMReturn d2acc - (EInr ext STNil (EInr ext (d2 t1) - (ESnd ext (EVar ext (STPair (tTup (d2e (subList (select SMerge des) subOut))) (d2 t2)) IZ)))))))) - (weakenExpr (WCopy (wSinks @[_,_,_])) $ - EMBind e2 $ - EMReturn d2acc (expandSubenvZeros - (subList (select SMerge des) subOut) - subOutE - (EVar ext (tTup (d2e (subList (select SMerge des) subE))) IZ)))) + (EPair ext + (expandSubenvZeros (subList (select SMerge des) subAB) sAB_B $ + EFst ext (EVar ext (STPair (tTup (d2e (subList (select SMerge des) subB'))) (d2 t2)) IZ)) + (EInr ext (d2 t1) + (ESnd ext (EVar ext (STPair (tTup (d2e (subList (select SMerge des) subB'))) (d2 t2)) IZ)))))))) + (EMBind (ELet ext (EInr ext STNil (ESnd ext (EVar ext tCaseRet IZ))) $ + weakenExpr (WCopy (wSinks @[_,_,_,_])) e2) $ + EMReturn d2acc $ + plus_AB_E + (EFst ext (EVar ext tCaseRet (IS IZ))) + (EVar ext (tTup (d2e (subList (select SMerge des) subE))) IZ))) EConst _ t val -> Ret BTop @@ -618,185 +633,3 @@ drev des policy = \case where d2acc = d2e (select SAccum des) - -caseOutSubenv - :: Descr env sto - -> STy a1 -> Storage s1 - -> STy a2 -> Storage s2 - -> Proxy exenv2 -> Proxy exenv3 - -> Subenv (Select env sto "merge") envE - -> Subenv (Select (a1 : env) (s1 : sto) "merge") env1 - -> Subenv (Select (a2 : env) (s2 : sto) "merge") env2 - -> (forall envOut. - Subenv (Select env sto "merge") envOut - -> Subenv envOut envE - -> (Ex exenv2 (TEVM (D2E (Select (a1 : env) (s1 : sto) "accum")) (Tup (D2E env1))) - -> Ex exenv2 (TEVM (D2E (Select env sto "accum")) (TPair (Tup (D2E envOut)) (D2 a1)))) - -> (Ex exenv3 (TEVM (D2E (Select (a2 : env) (s2 : sto) "accum")) (Tup (D2E env2))) - -> Ex exenv3 (TEVM (D2E (Select env sto "accum")) (TPair (Tup (D2E envOut)) (D2 a2)))) - -> r) - -> r -caseOutSubenv des t1 s1 t2 s2 _ _ subE sub1 sub2 k = - case (s1, sub1, s2, sub2) of - (SAccum, _, SAccum, _) -> - subenvUnion sub1 sub2 $ \sub3 s31 s32 -> - subenvUnion subE sub3 $ \sub4 s4E s43 -> - k sub4 s4E - (\e1 -> EMBind (EMScope e1) $ - EMReturn (d2e (select SAccum des)) $ - let t = STPair (tTup (d2e (subList (select SMerge des) sub1))) (d2 t1) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s31 $ - EFst ext (EVar ext t IZ)) - (ESnd ext (EVar ext t IZ))) - (\e2 -> EMBind (EMScope e2) $ - EMReturn (d2e (select SAccum des)) $ - let t = STPair (tTup (d2e (subList (select SMerge des) sub2))) (d2 t2) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s32 $ - EFst ext (EVar ext t IZ)) - (ESnd ext (EVar ext t IZ))) - (SAccum, _, SMerge, SEYes sub2') -> - subenvUnion sub1 sub2' $ \sub3 s31 s32 -> - subenvUnion subE sub3 $ \sub4 s4E s43 -> - k sub4 s4E - (\e1 -> EMBind (EMScope e1) $ - EMReturn (d2e (select SAccum des)) $ - let t = STPair (tTup (d2e (subList (select SMerge des) sub1))) (d2 t1) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s31 $ - EFst ext (EVar ext t IZ)) - (ESnd ext (EVar ext t IZ))) - (\e2 -> EMBind e2 $ - EMReturn (d2e (select SAccum des)) $ - let t = STPair (tTup (d2e (subList (select SMerge des) sub2'))) (d2 t2) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s32 $ - EFst ext (EVar ext t IZ)) - (ESnd ext (EVar ext t IZ))) - (SAccum, _, SMerge, SENo sub2') -> - subenvUnion sub1 sub2' $ \sub3 s31 s32 -> - subenvUnion subE sub3 $ \sub4 s4E s43 -> - k sub4 s4E - (\e1 -> EMBind (EMScope e1) $ - EMReturn (d2e (select SAccum des)) $ - let t = STPair (tTup (d2e (subList (select SMerge des) sub1))) (d2 t1) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s31 $ - EFst ext (EVar ext t IZ)) - (ESnd ext (EVar ext t IZ))) - (\e2 -> EMBind e2 $ - EMReturn (d2e (select SAccum des)) $ - let t = tTup (d2e (subList (select SMerge des) sub2')) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s32 $ - EVar ext t IZ) - (zero t2)) - (SMerge, SEYes sub1', SAccum, _) -> - subenvUnion sub1' sub2 $ \sub3 s31 s32 -> - subenvUnion subE sub3 $ \sub4 s4E s43 -> - k sub4 s4E - (\e1 -> EMBind e1 $ - EMReturn (d2e (select SAccum des)) $ - let t = STPair (tTup (d2e (subList (select SMerge des) sub1'))) (d2 t1) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s31 $ - EFst ext (EVar ext t IZ)) - (ESnd ext (EVar ext t IZ))) - (\e2 -> EMBind (EMScope e2) $ - EMReturn (d2e (select SAccum des)) $ - let t = STPair (tTup (d2e (subList (select SMerge des) sub2))) (d2 t2) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s32 $ - EFst ext (EVar ext t IZ)) - (ESnd ext (EVar ext t IZ))) - (SMerge, SENo sub1', SAccum, _) -> - subenvUnion sub1' sub2 $ \sub3 s31 s32 -> - subenvUnion subE sub3 $ \sub4 s4E s43 -> - k sub4 s4E - (\e1 -> EMBind e1 $ - EMReturn (d2e (select SAccum des)) $ - let t = tTup (d2e (subList (select SMerge des) sub1')) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s31 $ - EVar ext t IZ) - (zero t1)) - (\e2 -> EMBind (EMScope e2) $ - EMReturn (d2e (select SAccum des)) $ - let t = STPair (tTup (d2e (subList (select SMerge des) sub2))) (d2 t2) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s32 $ - EFst ext (EVar ext t IZ)) - (ESnd ext (EVar ext t IZ))) - (SMerge, SEYes sub1', SMerge, SEYes sub2') -> - subenvUnion sub1' sub2' $ \sub3 s31 s32 -> - subenvUnion subE sub3 $ \sub4 s4E s43 -> - k sub4 s4E - (\e1 -> EMBind e1 $ - EMReturn (d2e (select SAccum des)) $ - let t = STPair (tTup (d2e (subList (select SMerge des) sub1'))) (d2 t1) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s31 $ - EFst ext (EVar ext t IZ)) - (ESnd ext (EVar ext t IZ))) - (\e2 -> EMBind e2 $ - EMReturn (d2e (select SAccum des)) $ - let t = STPair (tTup (d2e (subList (select SMerge des) sub2'))) (d2 t2) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s32 $ - EFst ext (EVar ext t IZ)) - (ESnd ext (EVar ext t IZ))) - (SMerge, SEYes sub1', SMerge, SENo sub2') -> - subenvUnion sub1' sub2' $ \sub3 s31 s32 -> - subenvUnion subE sub3 $ \sub4 s4E s43 -> - k sub4 s4E - (\e1 -> EMBind e1 $ - EMReturn (d2e (select SAccum des)) $ - let t = STPair (tTup (d2e (subList (select SMerge des) sub1'))) (d2 t1) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s31 $ - EFst ext (EVar ext t IZ)) - (ESnd ext (EVar ext t IZ))) - (\e2 -> EMBind e2 $ - EMReturn (d2e (select SAccum des)) $ - let t = tTup (d2e (subList (select SMerge des) sub2')) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s32 $ - EVar ext t IZ) - (zero t2)) - (SMerge, SENo sub1', SMerge, SEYes sub2') -> - subenvUnion sub1' sub2' $ \sub3 s31 s32 -> - subenvUnion subE sub3 $ \sub4 s4E s43 -> - k sub4 s4E - (\e1 -> EMBind e1 $ - EMReturn (d2e (select SAccum des)) $ - let t = tTup (d2e (subList (select SMerge des) sub1')) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s31 $ - EVar ext t IZ) - (zero t1)) - (\e2 -> EMBind e2 $ - EMReturn (d2e (select SAccum des)) $ - let t = STPair (tTup (d2e (subList (select SMerge des) sub2'))) (d2 t2) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s32 $ - EFst ext (EVar ext t IZ)) - (ESnd ext (EVar ext t IZ))) - (SMerge, SENo sub1', SMerge, SENo sub2') -> - subenvUnion sub1' sub2' $ \sub3 s31 s32 -> - subenvUnion subE sub3 $ \sub4 s4E s43 -> - k sub4 s4E - (\e1 -> EMBind e1 $ - EMReturn (d2e (select SAccum des)) $ - let t = tTup (d2e (subList (select SMerge des) sub1')) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s31 $ - EVar ext t IZ) - (zero t1)) - (\e2 -> EMBind e2 $ - EMReturn (d2e (select SAccum des)) $ - let t = tTup (d2e (subList (select SMerge des) sub2')) in - EPair ext (expandSubenvZeros (subList (select SMerge des) sub4) s43 $ - expandSubenvZeros (subList (select SMerge des) sub3) s32 $ - EVar ext t IZ) - (zero t2)) |