From eb25e315ac8bd1e75498cc92c7f3326fa582171a Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Sun, 22 Feb 2026 12:59:40 +0100 Subject: WIP: Store subset of D1 Gamma for recompute at binding sites --- src/CHAD/AST/Env.hs | 16 +++++++++ src/CHAD/AST/Weaken.hs | 22 ++++++++++++ src/CHAD/Data.hs | 5 +++ src/CHAD/Drev.hs | 96 ++++++++++++++++++++++++++++++++------------------ 4 files changed, 104 insertions(+), 35 deletions(-) diff --git a/src/CHAD/AST/Env.hs b/src/CHAD/AST/Env.hs index 8e6b745..8eb4f77 100644 --- a/src/CHAD/AST/Env.hs +++ b/src/CHAD/AST/Env.hs @@ -89,6 +89,22 @@ subenvMap _ SNil SETop = SETop subenvMap f (t `SCons` l) (SEYes s sub) = SEYes (f t s) (subenvMap f l sub) subenvMap f (_ `SCons` l) (SENo sub) = SENo (subenvMap f l sub) +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 (SEYesR sub1) (SEYesR sub2) k = + subenvUnion sub1 sub2 $ \sub3 sub31 sub32 -> + k (SEYesR sub3) (SEYesR sub31) (SEYesR sub32) +subenvUnion (SEYesR sub1) (SENo sub2) k = + subenvUnion sub1 sub2 $ \sub3 sub31 sub32 -> + k (SEYesR sub3) (SEYesR sub31) (SENo sub32) +subenvUnion (SENo sub1) (SEYes Refl sub2) k = + subenvUnion sub1 sub2 $ \sub3 sub31 sub32 -> + k (SEYesR sub3) (SENo sub31) (SEYesR sub32) +subenvUnion (SENo sub1) (SENo sub2) k = + subenvUnion sub1 sub2 $ \sub3 sub31 sub32 -> + k (SENo sub3) sub31 sub32 + subenvD2E :: Subenv env env' -> Subenv (D2E env) (D2E env') subenvD2E SETop = SETop subenvD2E (SEYesR sub) = SEYesR (subenvD2E sub) diff --git a/src/CHAD/AST/Weaken.hs b/src/CHAD/AST/Weaken.hs index ac0d152..16403dd 100644 --- a/src/CHAD/AST/Weaken.hs +++ b/src/CHAD/AST/Weaken.hs @@ -109,6 +109,25 @@ infixr 3 .> (.>) :: env2 :> env3 -> env1 :> env2 -> env1 :> env3 (.>) = flip WThen +unweakenList :: as :> bs -> SList f bs -> SList f as +unweakenList WId l = l +unweakenList WSink (SCons _ l) = l +unweakenList (WCopy w) (SCons x l) = SCons x (unweakenList w l) +unweakenList (WPop w) l = let SCons _ l' = unweakenList w l in l' +unweakenList (WThen w1 w2) l = unweakenList w1 (unweakenList w2 l) +unweakenList WClosed _ = SNil +unweakenList (WIdx i) l = SCons (slistIdx l i) l +unweakenList (WPick @_ @_ @_ @env' pre w) (SCons x l) = + let (l1, l2) = sunappend @env' pre l + in sappend l1 (SCons x (unweakenList w l2)) +unweakenList (WSwap @env @as as bs) l = + let (l1, l23) = sunappend @(Append as env) bs l + (l2, l3) = sunappend @env as l23 + in sappend l2 (sappend l1 l3) +unweakenList (WStack @_ @env2 _ bs wab w12) l = + let (l1, l2) = sunappend @env2 bs l + in sappend (unweakenList wab l1) (unweakenList w12 l2) + class KnownListSpine list where knownListSpine :: SList (Const ()) list instance KnownListSpine '[] where knownListSpine = SNil instance KnownListSpine list => KnownListSpine (t : list) where knownListSpine = SCons (Const ()) knownListSpine @@ -133,6 +152,9 @@ wRaiseAbove :: SList f env1 -> proxy env -> env1 :> Append env1 env wRaiseAbove SNil _ = WClosed wRaiseAbove (SCons _ s) env = WCopy (wRaiseAbove s env) +wUnder :: SList f as -> as :> bs -> Append as env :> Append bs env +wUnder as w = WStack (slistMap (\_ -> Const ()) as) (subList) w WId + wPops :: SList f bs -> Append bs env1 :> env2 -> env1 :> env2 wPops SNil w = w wPops (_ `SCons` bs) w = wPops bs (WPop w) diff --git a/src/CHAD/Data.hs b/src/CHAD/Data.hs index 8c7605c..63bce5d 100644 --- a/src/CHAD/Data.hs +++ b/src/CHAD/Data.hs @@ -10,6 +10,7 @@ {-# LANGUAGE TypeOperators #-} module CHAD.Data (module CHAD.Data, (:~:)(Refl), If) where +import Data.Bifunctor (first) import Data.Functor.Product import Data.GADT.Compare import Data.GADT.Show @@ -55,6 +56,10 @@ sappend :: SList f l1 -> SList f l2 -> SList f (Append l1 l2) sappend SNil l = l sappend (SCons x xs) l = SCons x (sappend xs l) +sunappend :: forall l2 l1 f g. SList f l1 -> SList g (Append l1 l2) -> (SList g l1, SList g l2) +sunappend SNil l = (SNil, l) +sunappend (SCons _ l1) (SCons x l) = first (SCons x) (sunappend l1 l) + type family Replicate n x where Replicate Z x = '[] Replicate (S n) x = x : Replicate n x diff --git a/src/CHAD/Drev.hs b/src/CHAD/Drev.hs index 9f2921c..4e39f79 100644 --- a/src/CHAD/Drev.hs +++ b/src/CHAD/Drev.hs @@ -532,13 +532,13 @@ accumPromote pdty (descr `DPush` (t :: STy t, vid, sto)) k = case sto of (SEYesR accrevsub) (VarMap.sink1 accumMap) (\shbinds -> - autoWeak (#pro (d2ace envpro) &. #d (auto1 @dt) &. #shb shbinds &. #acc (auto1 @(TAccum (D2 t))) &. #tl (d2ace (select SAccum descr))) - (#acc :++: (#pro :++: #d :++: #shb :++: #tl)) - (#pro :++: #d :++: #shb :++: #acc :++: #tl) + autoWeak (#pro (d2ace envpro) &. #d (auto1 @dt) &. #shb shbinds &. #acc (auto1 @(TAccum (D2 t))) &. #ace (d2ace (select SAccum descr))) + (#acc :++: (#pro :++: #d :++: #shb :++: #ace)) + (#pro :++: #d :++: #shb :++: #acc :++: #ace) .> WCopy (wf shbinds) - .> autoWeak (#d (auto1 @dt) &. #shb shbinds &. #acc (auto1 @(TAccum (D2 t))) &. #tl (d2ace (select SAccum storepl))) - (#d :++: #shb :++: #acc :++: #tl) - (#acc :++: (#d :++: #shb :++: #tl))) + .> autoWeak (#d (auto1 @dt) &. #shb shbinds &. #acc (auto1 @(TAccum (D2 t))) &. #ace (d2ace (select SAccum storepl))) + (#d :++: #shb :++: #acc :++: #ace) + (#acc :++: (#d :++: #shb :++: #ace))) SMerge -> case t of -- Discrete values are left as-is @@ -606,12 +606,13 @@ accumPromote pdty (descr `DPush` (t :: STy t, vid, sto)) k = case sto of ---------------------------- RETURN TRIPLE FROM CHAD --------------------------- data Ret env0 sto sd t = - forall shbinds tapebinds contribs. + forall shbinds tapebinds contribs reprim. Ret (Bindings Ex (D1E env0) shbinds) -- shared binds (Subenv shbinds tapebinds) (Ex (Append shbinds (D1E env0)) (D1 t)) (SubenvS (D2E (Select env0 sto "merge")) contribs) - (Ex (sd : Append tapebinds (D2AcE (Select env0 sto "accum"))) (Tup contribs)) + (Ex (sd : Append tapebinds (Append reprim (D2AcE (Select env0 sto "accum")))) (Tup contribs)) + (Subenv (D1E env0) reprim) deriving instance Show (Ret env0 sto sd t) type data TyTyPair = MkTyTyPair Ty Ty @@ -633,11 +634,12 @@ data SingleRet env0 sto (pair :: TyTyPair) = -- {-# COMPLETE Ret1 #-} data RetPair env0 sto env shbinds tapebinds (pair :: TyTyPair) where - RetPair :: forall sd t contribs -- existentials + RetPair :: forall sd t contribs reprim -- existentials env0 sto env shbinds tapebinds. -- universals Ex (Append shbinds env) (D1 t) -> SubenvS (D2E (Select env0 sto "merge")) contribs - -> Ex (sd : Append tapebinds (D2AcE (Select env0 sto "accum"))) (Tup contribs) + -> Ex (sd : Append tapebinds (Append reprim (D2AcE (Select env0 sto "accum")))) (Tup contribs) + -> Subenv (D1E env0) reprim -> RetPair env0 sto env shbinds tapebinds (MkTyTyPair sd t) deriving instance Show (RetPair env0 sto env shbinds tapebinds pair) @@ -649,11 +651,11 @@ data Rets env0 sto env list = deriving instance Show (Rets env0 sto env list) toSingleRet :: Ret env0 sto sd t -> SingleRet env0 sto (MkTyTyPair sd t) -toSingleRet (Ret e0 subtape e1 sub e2) = SingleRet e0 subtape (RetPair e1 sub e2) +toSingleRet (Ret e0 subtape e1 sub e2 rp) = SingleRet e0 subtape (RetPair e1 sub e2 rp) weakenRetPair :: SList STy shbinds -> env :> env' -> RetPair env0 sto env shbinds tapebinds pair -> RetPair env0 sto env' shbinds tapebinds pair -weakenRetPair bindslist w (RetPair e1 sub e2) = RetPair (weakenExpr (weakenOver bindslist w) e1) sub e2 +weakenRetPair bindslist w (RetPair e1 sub e2 rp) = RetPair (weakenExpr (weakenOver bindslist w) e1) sub e2 rp weakenRets :: env :> env' -> Rets env0 sto env list -> Rets env0 sto env' list weakenRets w (Rets binds tapesub list) = @@ -666,30 +668,33 @@ rebaseRetPair :: forall env b1 b2 tapebinds1 tapebinds2 env0 sto pair f. -> Subenv b1 tapebinds1 -> Subenv b2 tapebinds2 -> RetPair env0 sto (Append b1 env) b2 tapebinds2 pair -> RetPair env0 sto env (Append b2 b1) (Append tapebinds2 tapebinds1) pair -rebaseRetPair descr b1 b2 subtape1 subtape2 (RetPair @sd e1 sub e2) +rebaseRetPair descr b1 b2 subtape1 subtape2 (RetPair @sd e1 sub e2 rp) | Refl <- lemAppendAssoc @b2 @b1 @env = RetPair e1 sub (weakenExpr (autoWeak (#d (auto1 @sd) &. #t2 (subList b2 subtape2) &. #t1 (subList b1 subtape1) - &. #tl (d2ace (select SAccum descr))) - (#d :++: (#t2 :++: #tl)) - (#d :++: ((#t2 :++: #t1) :++: #tl))) + &. #rp (subList (desD1E descr) rp) + &. #ace (d2ace (select SAccum descr))) + (#d :++: (#t2 :++: #rp :++: #ace)) + (#d :++: ((#t2 :++: #t1) :++: #rp :++: #ace))) e2) + rp retConcat :: forall env0 sto list. Descr env0 sto -> SList (SingleRet env0 sto) list -> Rets env0 sto (D1E env0) list retConcat _ SNil = Rets BTop SETop SNil -retConcat descr (SCons (SingleRet (e0 :: Bindings _ _ shbinds1) (subtape :: Subenv _ tapebinds1) (RetPair e1 sub e2)) list) +retConcat descr (SCons (SingleRet (e0 :: Bindings _ _ shbinds1) (subtape :: Subenv _ tapebinds1) (RetPair e1 sub e2 (rp :: Subenv _ reprim))) list) | Rets (binds :: Bindings _ _ shbinds2) (subtape2 :: Subenv _ tapebinds2) pairs <- weakenRets (sinkWithBindings e0) (retConcat descr list) , Refl <- lemAppendAssoc @shbinds2 @shbinds1 @(D1E env0) - , Refl <- lemAppendAssoc @tapebinds2 @tapebinds1 @(D2AcE (Select env0 sto "accum")) + , Refl <- lemAppendAssoc @tapebinds2 @tapebinds1 @(Append reprim (D2AcE (Select env0 sto "accum"))) = Rets (bconcat e0 binds) (subenvConcat subtape subtape2) (SCons (RetPair (weakenExpr (sinkWithBindings binds) e1) sub - (weakenExpr (WCopy (sinkWithSubenv subtape2)) e2)) + (weakenExpr (WCopy (sinkWithSubenv subtape2)) e2) + rp) (slistMap (rebaseRetPair descr (bindingsBinds e0) (bindingsBinds binds) subtape subtape2) pairs)) @@ -697,25 +702,25 @@ retConcat descr (SCons (SingleRet (e0 :: Bindings _ _ shbinds1) (subtape :: Sube freezeRet :: Descr env sto -> Ret env sto (D2 t) t -> Ex (D2 t : Append (D2AcE (Select env sto "accum")) (D1E env)) (TPair (D1 t) (Tup (D2E (Select env sto "merge")))) -freezeRet descr (Ret e0 subtape e1 sub e2 :: Ret _ _ _ t) = +freezeRet descr (Ret e0 subtape e1 sub e2 rp :: Ret _ _ _ t) = let (e0', wInsertD2Ac) = weakenBindingsE (WSink .> wSinks (d2ace (select SAccum descr))) e0 - e2' = weakenExpr (WCopy (wCopies (subList (bindingsBinds e0) subtape) (wRaiseAbove (d2ace (select SAccum descr)) (desD1E descr)))) e2 tContribs = tTup (slistMap fromSMTy (subList (d2eM (select SMerge descr)) sub)) library = #d (auto1 @(D2 t)) &. #tape (subList (bindingsBinds e0) subtape) &. #shbinds (bindingsBinds e0) &. #d2ace (d2ace (select SAccum descr)) - &. #tl (desD1E descr) + &. #rp (subList (desD1E descr) rp) + &. #d1e (desD1E descr) &. #contribs (SCons tContribs SNil) in letBinds e0' $ EPair ext (weakenExpr wInsertD2Ac e1) (ELet ext (weakenExpr (autoWeak library - (#d :++: LPreW #tape #shbinds (wUndoSubenv subtape) :++: #d2ace :++: #tl) - (#shbinds :++: #d :++: #d2ace :++: #tl)) - e2') $ + (#d :++: LPreW #tape #shbinds (wUndoSubenv subtape) :++: (LPreW #rp #d1e (wUndoSubenv rp) :++: #d2ace)) + (#shbinds :++: #d :++: #d2ace :++: #d1e)) + e2) $ expandSubenvZeros - (autoWeak library #tl (#contribs :++: #shbinds :++: #d :++: #d2ace :++: #tl) + (autoWeak library #d1e (#contribs :++: #shbinds :++: #d :++: #d2ace :++: #d1e) .> wUndoSubenv (subenvD1E (selectSub SMerge descr))) (select SMerge descr) sub (EVar ext tContribs IZ)) @@ -734,11 +739,12 @@ drev des _ sd | isAbsent sd = (drevPrimal des e) (subenvNone (d2e (select SMerge des))) (ENil ext) + (subenvNone (desD1E des)) drev _ _ SpAbsent = error "Absent should be isAbsent" drev des accumMap (SpSparse sd) = \e -> - case drev des accumMap sd e of { Ret e0 subtape e1 sub e2 -> + case drev des accumMap sd e of { Ret e0 subtape e1 sub e2 rp -> subenvPlus ST ST (d2eM (select SMerge des)) sub (subenvNone (d2e (select SMerge des))) $ \sub' (Inj inj1) (Inj inj2) _ -> Ret e0 subtape @@ -747,6 +753,7 @@ drev des accumMap (SpSparse sd) = (emaybe (EVar ext (STMaybe (applySparse sd (d2 (typeOf e)))) IZ) (inj2 (ENil ext)) (inj1 (weakenExpr (WCopy WSink) e2))) + rp } drev des accumMap sd = \case @@ -759,6 +766,7 @@ drev des accumMap sd = \case (subenvNone (d2e (select SMerge des))) (let ty = applySparse sd (d2M t) in EAccum ext (d2M t) SAPHere (ENil ext) sd (EVar ext (fromSMTy ty) IZ) (EVar ext (STAccum (d2M t)) (IS accI))) + (subenvNone (desD1E des)) Idx2Me tupI -> Ret BTop @@ -766,6 +774,7 @@ drev des accumMap sd = \case (EVar ext (d1 t) (conv1Idx i)) (subenvOnehot (d2e (select SMerge des)) tupI sd) (EPair ext (ENil ext) (EVar ext (applySparse sd (d2 t)) IZ)) + (subenvNone (desD1E des)) Idx2Di _ -> Ret BTop @@ -773,7 +782,9 @@ drev des accumMap sd = \case (EVar ext (d1 t) (conv1Idx i)) (subenvNone (d2e (select SMerge des))) (ENil ext) + (subenvNone (desD1E des)) +{- ELet _ (rhs :: Expr _ _ a) body | ChosenStorage (storage :: Storage s) <- if chcLetArrayAccum ?config && typeHasArrays (typeOf rhs) then ChosenStorage SAccum else ChosenStorage SMerge , RetScoped (body0 :: Bindings _ _ body_shbinds) (subtapeBody :: Subenv _ body_tapebinds) body1 subBody sdBody body2 <- drevScoped des accumMap (typeOf rhs) storage (Just (extOf rhs)) sd body @@ -802,25 +813,36 @@ drev des accumMap sd = \case plus_RHS_Body (EVar ext (contribTupTy des subRHS) IZ) (EFst ext (EVar ext bodyResType (IS IZ)))) +-} EPair _ a b | SpPair sd1 sd2 <- sd - , Rets binds subtape (RetPair a1 subA a2 `SCons` RetPair b1 subB b2 `SCons` SNil) + , Rets binds subtape (RetPair a1 subA a2 rpA `SCons` RetPair b1 subB b2 rpB `SCons` SNil) <- retConcat des $ toSingleRet (drev des accumMap sd1 a) `SCons` toSingleRet (drev des accumMap sd2 b) `SCons` SNil , let dt = STPair (applySparse sd1 (d2 (typeOf a))) (applySparse sd2 (d2 (typeOf b))) -> subenvPlus SF SF (d2eM (select SMerge des)) subA subB $ \subBoth _ _ plus_A_B -> + subenvUnion rpA rpB $ \rp rpA' rpB' -> Ret binds subtape (EPair ext a1 b1) subBoth (ELet ext (ELet ext (EFst ext (EVar ext dt IZ)) - (weakenExpr (WCopy WSink) a2)) $ + (weakenExpr (WCopy (WSink .> _ rpA')) a2)) $ ELet ext (ELet ext (ESnd ext (EVar ext dt (IS IZ))) (weakenExpr (WCopy (WSink .> WSink)) b2)) $ plus_A_B (EVar ext (contribTupTy des subA) (IS IZ)) (EVar ext (contribTupTy des subB) IZ)) - + rp + where + rpWeak :: SList f tapebinds + -> SList g reprim1 + -> SList h reprim2 + -> Append tapebinds (Append reprim1 (D2AcE (Select env sto "accum"))) :> + Append tapebinds (Append reprim2 (D2AcE (Select env sto "accum"))) + rpWeak tb rp1 rp2 = wCopies tb (weakenOver) + +{- EFst _ e | Ret e0 subtape e1 sub e2 <- drev des accumMap (SpPair sd SpAbsent) e , STPair t1 _ <- typeOf e -> @@ -1378,6 +1400,8 @@ drev des accumMap sd = \case EFold1InnerD1{} -> err_targetlang "EFold1InnerD1" EFold1InnerD2{} -> err_targetlang "EFold1InnerD2" +-} + _ -> undefined where err_accum = error "Accumulator operations unsupported in the source program" @@ -1388,6 +1412,7 @@ drev des accumMap sd = \case contribTupTy :: Descr env sto -> SubenvS (D2E (Select env sto "merge")) contribs -> STy (Tup contribs) contribTupTy des' sub = tTup (slistMap fromSMTy (subList (d2eM (select SMerge des')) sub)) +{- deriv_extremum :: (?config :: CHADConfig, ScalIsNumeric t ~ True) => (forall env'. Ex env' (TArr (S n) (TScal t)) -> Ex env' (TArr n (TScal t))) -> Descr env sto -> VarMap Int (D2AcE (Select env sto "accum")) @@ -1413,6 +1438,7 @@ deriv_extremum extremum des accumMap sd e (inj2 (ENil ext))) $ weakenExpr (WCopy (WSink .> WSink .> WSink)) e2) } +-} data ChosenStorage = forall s. ((s == "discr") ~ False) => ChosenStorage (Storage s) @@ -1442,7 +1468,7 @@ drevScoped :: forall a s env sto sd t. -> RetScoped env sto a s sd t drevScoped des accumMap argty argsto argids sd expr = case argsto of SMerge - | Ret e0 (subtape :: Subenv _ tapebinds) e1 sub e2 <- drev (des `DPush` (argty, argids, argsto)) accumMap sd expr + | Ret e0 (subtape :: Subenv _ tapebinds) e1 sub e2 rp <- drev (des `DPush` (argty, argids, argsto)) accumMap sd expr , Refl <- lemAppendNil @tapebinds -> case sub of SEYes sp sub' -> RetScoped e0 (subenvConcat (SENo @(D1 a) SETop) subtape) e1 sub' sp e2 @@ -1453,7 +1479,7 @@ drevScoped des accumMap argty argsto argids sd expr = case argsto of , Just (VIArr i _) <- argids , Just (Some (VarMap.TypedIdx foundTy idx)) <- VarMap.lookup i accumMap , Just Refl <- testEquality foundTy (STAccum (d2M argty)) - , Ret e0 (subtape :: Subenv _ tapebinds) e1 sub e2 <- drev (des `DPush` (argty, argids, argsto)) (VarMap.sink1 accumMap) sd expr + , Ret e0 (subtape :: Subenv _ tapebinds) e1 sub e2 rp <- drev (des `DPush` (argty, argids, argsto)) (VarMap.sink1 accumMap) sd expr , Refl <- lemAppendNil @tapebinds -> -- Our contribution to the binding's cotangent _here_ is zero (absent), -- because we're contributing to an earlier binding of the same value @@ -1472,7 +1498,7 @@ drevScoped des accumMap argty argsto argids sd expr = case argsto of | let accumMap' = case argids of Just (VIArr i _) -> VarMap.insert i (STAccum (d2M argty)) IZ (VarMap.sink1 accumMap) _ -> VarMap.sink1 accumMap - , Ret e0 subtape e1 sub e2 <- drev (des `DPush` (argty, argids, argsto)) accumMap' sd expr -> + , Ret e0 subtape e1 sub e2 rp <- drev (des `DPush` (argty, argids, argsto)) accumMap' sd expr -> let library = #d (auto1 @sd) &. #p (auto1 @(D1 a)) &. #body (subList (bindingsBinds e0) subtape) @@ -1488,7 +1514,7 @@ drevScoped des accumMap argty argsto argids sd expr = case argsto of e2 SDiscr - | Ret e0 (subtape :: Subenv _ tapebinds) e1 sub e2 <- drev (des `DPush` (argty, argids, argsto)) accumMap sd expr + | Ret e0 (subtape :: Subenv _ tapebinds) e1 sub e2 rp <- drev (des `DPush` (argty, argids, argsto)) accumMap sd expr , Refl <- lemAppendNil @tapebinds -> RetScoped e0 (subenvConcat (SENo @(D1 a) SETop) subtape) e1 sub SpAbsent e2 @@ -1523,7 +1549,7 @@ drevLambda des accumMap (argty, argsto) sd origef k = let mergePrimalSub = subenvD1E (selectSub SMerge des `subenvCompose` subMergeUsed `subenvCompose` proSub) in let mergePrimalBindings = collectBindings (d1e (descrList des)) mergePrimalSub in case prf1 prodes argty argsto of { Refl -> - case drev (prodes `DPush` (argty, Nothing, argsto)) accumMapPro sd ef of { Ret (ef0 :: Bindings _ _ e_binds) (subtapeEf :: Subenv _ e_tape) ef1 subEf ef2 -> + case drev (prodes `DPush` (argty, Nothing, argsto)) accumMapPro sd ef of { Ret (ef0 :: Bindings _ _ e_binds) (subtapeEf :: Subenv _ e_tape) ef1 subEf ef2 rp -> let (efRebinds, efPrerebinds) = reconstructBindings (subList (bindingsBinds ef0) subtapeEf) in extractContrib prodes argty argsto subEf $ \argSp getSparseArg -> let library = #fbinds (bindingsBinds ef0) -- cgit v1.2.3-70-g09d2