{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -} module LinearScan.Loops where import Debug.Trace (trace, traceShow) import qualified Prelude import qualified Data.IntMap import qualified Data.IntSet import qualified Data.List import qualified Data.Ord import qualified Data.Functor.Identity import qualified LinearScan.Utils import qualified LinearScan.Blocks as Blocks import qualified LinearScan.IntMap as IntMap import qualified LinearScan.Lib as Lib import qualified LinearScan.Monad as Monad import qualified LinearScan.Yoneda as Yoneda import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Seq as Seq import qualified LinearScan.Ssrbool as Ssrbool import qualified LinearScan.Ssrnat as Ssrnat #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base as GHC.Base import qualified GHC.Prim as GHC.Prim #else -- HUGS import qualified LinearScan.IOExts as IOExts #endif #ifdef __GLASGOW_HASKELL__ --unsafeCoerce :: a -> b unsafeCoerce = GHC.Base.unsafeCoerce# #else -- HUGS --unsafeCoerce :: a -> b unsafeCoerce = IOExts.unsafeCoerce #endif data LoopState = Build_LoopState IntMap.IntSet IntMap.IntSet ([] Blocks.BlockId) IntMap.IntSet (IntMap.IntMap IntMap.IntSet) (IntMap.IntMap IntMap.IntSet) (IntMap.IntMap IntMap.IntSet) (IntMap.IntMap ((,) Prelude.Int Prelude.Int)) activeBlocks :: LoopState -> IntMap.IntSet activeBlocks l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> activeBlocks0} visitedBlocks :: LoopState -> IntMap.IntSet visitedBlocks l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> visitedBlocks0} loopHeaderBlocks :: LoopState -> [] Blocks.BlockId loopHeaderBlocks l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> loopHeaderBlocks0} loopEndBlocks :: LoopState -> IntMap.IntSet loopEndBlocks l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> loopEndBlocks0} forwardBranches :: LoopState -> IntMap.IntMap IntMap.IntSet forwardBranches l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> forwardBranches0} backwardBranches :: LoopState -> IntMap.IntMap IntMap.IntSet backwardBranches l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> backwardBranches0} loopIndices :: LoopState -> IntMap.IntMap IntMap.IntSet loopIndices l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> loopIndices0} loopDepths :: LoopState -> IntMap.IntMap ((,) Prelude.Int Prelude.Int) loopDepths l = case l of { Build_LoopState activeBlocks0 visitedBlocks0 loopHeaderBlocks0 loopEndBlocks0 forwardBranches0 backwardBranches0 loopIndices0 loopDepths0 -> loopDepths0} emptyLoopState :: LoopState emptyLoopState = Build_LoopState IntMap.emptyIntSet IntMap.emptyIntSet [] IntMap.emptyIntSet IntMap.emptyIntMap IntMap.emptyIntMap IntMap.emptyIntMap IntMap.emptyIntMap modifyActiveBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> Monad.State LoopState () modifyActiveBlocks f = Monad.modify (\st -> Build_LoopState (f (activeBlocks st)) (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st) (backwardBranches st) (loopIndices st) (loopDepths st)) modifyVisitedBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> Monad.State LoopState () modifyVisitedBlocks f = Monad.modify (\st -> Build_LoopState (activeBlocks st) (f (visitedBlocks st)) (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st) (backwardBranches st) (loopIndices st) (loopDepths st)) modifyLoopHeaderBlocks :: (([] Blocks.BlockId) -> [] Blocks.BlockId) -> Monad.State LoopState () modifyLoopHeaderBlocks f = Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st) (f (loopHeaderBlocks st)) (loopEndBlocks st) (forwardBranches st) (backwardBranches st) (loopIndices st) (loopDepths st)) modifyLoopEndBlocks :: (IntMap.IntSet -> IntMap.IntSet) -> Monad.State LoopState () modifyLoopEndBlocks f = Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st) (loopHeaderBlocks st) (f (loopEndBlocks st)) (forwardBranches st) (backwardBranches st) (loopIndices st) (loopDepths st)) modifyForwardBranches :: ((IntMap.IntMap IntMap.IntSet) -> IntMap.IntMap IntMap.IntSet) -> Monad.State LoopState () modifyForwardBranches f = Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st) (f (forwardBranches st)) (backwardBranches st) (loopIndices st) (loopDepths st)) modifyBackwardBranches :: ((IntMap.IntMap IntMap.IntSet) -> IntMap.IntMap IntMap.IntSet) -> Monad.State LoopState () modifyBackwardBranches f = Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st) (f (backwardBranches st)) (loopIndices st) (loopDepths st)) setLoopIndices :: (IntMap.IntMap IntMap.IntSet) -> Monad.State LoopState () setLoopIndices indices = Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st) (backwardBranches st) indices (loopDepths st)) setLoopDepths :: (IntMap.IntMap ((,) Prelude.Int Prelude.Int)) -> Monad.State LoopState () setLoopDepths depths = Monad.modify (\st -> Build_LoopState (activeBlocks st) (visitedBlocks st) (loopHeaderBlocks st) (loopEndBlocks st) (forwardBranches st) (backwardBranches st) (loopIndices st) depths) addReference :: Prelude.Int -> Prelude.Int -> (IntMap.IntMap IntMap.IntSet) -> IntMap.IntMap IntMap.IntSet addReference i x = IntMap.coq_IntMap_alter (\macc -> case macc of { Prelude.Just acc -> Prelude.Just (IntMap.coq_IntSet_insert x acc); Prelude.Nothing -> Prelude.Just (IntMap.coq_IntSet_singleton x)}) i pathToLoopHeader :: Blocks.BlockId -> Prelude.Int -> LoopState -> Prelude.Maybe IntMap.IntSet pathToLoopHeader blk header st = let { go = let { go fuel visited b = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> (,) visited Prelude.Nothing) (\n -> let {visited' = IntMap.coq_IntSet_insert b visited} in let { forwardPreds = case IntMap.coq_IntMap_lookup b (forwardBranches st) of { Prelude.Just preds -> IntMap.coq_IntSet_toList preds; Prelude.Nothing -> []}} in let { backwardPreds = case IntMap.coq_IntMap_lookup b (backwardBranches st) of { Prelude.Just preds -> IntMap.coq_IntSet_toList preds; Prelude.Nothing -> []}} in let {preds = (Prelude.++) forwardPreds backwardPreds} in Lib.forFold ((,) visited' (Prelude.Just (IntMap.coq_IntSet_singleton b))) (unsafeCoerce preds) (\mxs pred -> case mxs of { (,) vis o -> case o of { Prelude.Just xs -> case Eqtype.eq_op Ssrnat.nat_eqType pred (unsafeCoerce header) of { Prelude.True -> (,) vis (Prelude.Just (IntMap.coq_IntSet_union xs (IntMap.coq_IntSet_singleton (unsafeCoerce pred)))); Prelude.False -> case IntMap.coq_IntSet_member (unsafeCoerce pred) vis of { Prelude.True -> (,) vis (Prelude.Just xs); Prelude.False -> case unsafeCoerce go n vis pred of { (,) vis' o0 -> case o0 of { Prelude.Just ys -> (,) vis' (Prelude.Just (IntMap.coq_IntSet_union xs ys)); Prelude.Nothing -> (,) vis Prelude.Nothing}}}}; Prelude.Nothing -> mxs}})) fuel} in go} in Prelude.snd (go (IntMap.coq_IntSet_size (visitedBlocks st)) IntMap.emptyIntSet blk) liftStateT :: (Monad.Monad a1) -> (Monad.State a2 a3) -> Monad.StateT a2 a1 a3 liftStateT h x = Monad.bind (Monad.coq_StateT_Monad h) (\st -> case x st of { (,) a st' -> Monad.bind (Monad.coq_StateT_Monad h) (\x0 -> Monad.pure (Monad.coq_StateT_Applicative h) a) (Monad.putT (Monad.is_applicative h) st')}) (Monad.getT (Monad.is_applicative h)) computeLoopDepths :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (IntMap.IntMap a1) -> Monad.StateT LoopState a5 () computeLoopDepths mDict binfo bs = Monad.bind (Monad.coq_StateT_Monad mDict) (\st -> Monad.bind (Monad.coq_StateT_Monad mDict) (\m -> let { f = \acc loopIndex refs -> IntMap.coq_IntSet_forFold acc refs (\m' blk -> let { f = \mx -> case mx of { Prelude.Just y -> case y of { (,) idx depth -> Prelude.Just ((,) (Prelude.min idx loopIndex) ((Prelude.succ) depth))}; Prelude.Nothing -> Prelude.Just ((,) loopIndex ((Prelude.succ) 0))}} in IntMap.coq_IntMap_alter f blk m')} in liftStateT mDict (Monad.bind (unsafeCoerce Monad.coq_State_Monad) (\x -> setLoopDepths (IntMap.coq_IntMap_foldlWithKey f IntMap.emptyIntMap m)) (setLoopIndices m))) (Monad.lift mDict (Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) IntMap.emptyIntMap (IntMap.coq_IntSet_toList (loopEndBlocks st)) (\m endBlock -> case IntMap.coq_IntMap_lookup endBlock bs of { Prelude.Just b -> Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\suxs -> Monad.pure (unsafeCoerce (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict))) (Lib.forFold m suxs (\m' sux -> let {headers = loopHeaderBlocks st} in let { loopIndex = Seq.find (\x -> Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce x) sux) headers} in case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce loopIndex) (unsafeCoerce (Data.List.length headers)) of { Prelude.True -> m'; Prelude.False -> let { mres = pathToLoopHeader endBlock (unsafeCoerce sux) st} in case mres of { Prelude.Just path -> Lib.forFold m' (IntMap.coq_IntSet_toList path) (\m'' blk -> addReference loopIndex blk m''); Prelude.Nothing -> m'}}))) (\_ -> Blocks.blockSuccessors mDict binfo b); Prelude.Nothing -> Monad.pure (unsafeCoerce (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict))) m}))))) (Monad.getT (Monad.is_applicative mDict)) computeVarReferences :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (Blocks.OpInfo a5 a3 a4) -> ([] a1) -> LoopState -> a5 computeVarReferences maxReg mDict binfo oinfo bs st = Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (Monad.forFoldM (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) IntMap.emptyIntMap bs (\acc b -> Monad.bind (unsafeCoerce (Yoneda.coq_Yoneda_Monad mDict)) (\bid -> let { g = \acc1 loopIndex blks -> case Prelude.not (IntMap.coq_IntSet_member bid blks) of { Prelude.True -> acc1; Prelude.False -> case Blocks.blockOps mDict binfo b of { (,) p zs -> case p of { (,) xs ys -> Lib.forFold acc1 ((Prelude.++) xs ((Prelude.++) ys zs)) (\acc2 op -> Lib.forFold acc2 (Blocks.opRefs maxReg mDict oinfo op) (\acc3 v -> case Blocks.varId maxReg v of { Prelude.Left p0 -> acc3; Prelude.Right vid -> addReference loopIndex vid acc3}))}}}} in Monad.pure (unsafeCoerce (Yoneda.coq_Yoneda_Applicative (Monad.is_applicative mDict))) (IntMap.coq_IntMap_foldlWithKey g acc (loopIndices st))) (\_ -> Blocks.blockId mDict binfo b))) findLoopEnds :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> (IntMap.IntMap a1) -> Monad.StateT LoopState a5 () findLoopEnds mDict binfo bs = let { go = let { go n b = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> Monad.pure (Monad.coq_StateT_Applicative mDict) ()) (\n0 -> Monad.bind (Monad.coq_StateT_Monad mDict) (\bid -> Monad.bind (Monad.coq_StateT_Monad mDict) (\x -> Monad.bind (Monad.coq_StateT_Monad mDict) (\suxs -> Monad.bind (Monad.coq_StateT_Monad mDict) (\x0 -> liftStateT mDict (modifyActiveBlocks (IntMap.coq_IntSet_delete bid))) (Monad.forM_ (Monad.coq_StateT_Monad mDict) suxs (\sux -> Monad.bind (Monad.coq_StateT_Monad mDict) (\active -> Monad.bind (Monad.coq_StateT_Monad mDict) (\x0 -> Monad.bind (Monad.coq_StateT_Monad mDict) (\visited -> case IntMap.coq_IntSet_member sux visited of { Prelude.True -> Monad.pure (Monad.coq_StateT_Applicative mDict) (); Prelude.False -> case IntMap.coq_IntMap_lookup sux bs of { Prelude.Just x1 -> go n0 x1; Prelude.Nothing -> Monad.pure (Monad.coq_StateT_Applicative mDict) ()}}) (Monad.getsT (Monad.is_applicative mDict) visitedBlocks)) (liftStateT mDict (case IntMap.coq_IntSet_member sux active of { Prelude.True -> Monad.bind (unsafeCoerce Monad.coq_State_Monad) (\x0 -> Monad.bind (unsafeCoerce Monad.coq_State_Monad) (\x1 -> modifyBackwardBranches (addReference sux bid)) (modifyLoopEndBlocks (IntMap.coq_IntSet_insert bid))) (modifyLoopHeaderBlocks (\l -> case Prelude.not (Ssrbool.in_mem (unsafeCoerce sux) (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce l))) of { Prelude.True -> (:) sux l; Prelude.False -> l})); Prelude.False -> modifyForwardBranches (addReference sux bid)}))) (Monad.getsT (Monad.is_applicative mDict) activeBlocks)))) (Monad.lift mDict (Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (\_ -> Blocks.blockSuccessors mDict binfo b)))) (liftStateT mDict (Monad.bind (unsafeCoerce Monad.coq_State_Monad) (\x -> modifyActiveBlocks (IntMap.coq_IntSet_insert bid)) (modifyVisitedBlocks (IntMap.coq_IntSet_insert bid))))) (Monad.lift mDict (Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (\_ -> Blocks.blockId mDict binfo b)))) n} in go} in case IntMap.coq_IntMap_toList bs of { [] -> Monad.pure (Monad.coq_StateT_Applicative mDict) (); (:) p l -> case p of { (,) n b -> go (IntMap.coq_IntMap_size bs) b}} computeBlockOrder :: (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] a1) -> a5 computeBlockOrder mDict binfo blocks = case blocks of { [] -> Monad.pure (Monad.is_applicative mDict) ((,) emptyLoopState []); (:) b bs -> Monad.bind mDict (\keys -> let {blockMap = IntMap.coq_IntMap_fromList keys} in Monad.bind mDict (\z -> case z of { (,) y st0 -> Monad.bind mDict (\blocks' -> Monad.bind mDict (\keys' -> let {blockMap' = IntMap.coq_IntMap_fromList keys'} in Monad.bind mDict (\z' -> case z' of { (,) y0 st1 -> case blocks' of { [] -> Monad.pure (Monad.is_applicative mDict) ((,) emptyLoopState []); (:) b' bs' -> Monad.bind mDict (\w -> case w of { (,) y1 st2 -> let { isHeavier = \x y2 -> Monad.bind mDict (\x_id -> Monad.bind mDict (\y_id -> let { x_depth = case IntMap.coq_IntMap_lookup x_id (loopDepths st2) of { Prelude.Just p -> case p of { (,) idx depth -> depth}; Prelude.Nothing -> 0}} in let { y_depth = case IntMap.coq_IntMap_lookup y_id (loopDepths st2) of { Prelude.Just p -> case p of { (,) idx depth -> depth}; Prelude.Nothing -> 0}} in Monad.pure (Monad.is_applicative mDict) ((Prelude.<=) ((Prelude.succ) y_depth) x_depth)) (Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (\_ -> Blocks.blockId mDict binfo y2))) (Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (\_ -> Blocks.blockId mDict binfo x))} in let { go = let { go n branches work_list = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> Monad.pure (Monad.is_applicative mDict) []) (\n0 -> case work_list of { [] -> Monad.pure (Monad.is_applicative mDict) []; (:) w0 ws -> Monad.bind mDict (\bid -> Monad.bind mDict (\suxs -> Monad.bind mDict (\x -> case x of { (,) branches' ws' -> Monad.fmap (Monad.is_functor (Monad.is_applicative mDict)) (\x0 -> (:) w0 x0) (go n0 branches' ws')}) (Monad.forFoldM mDict ((,) branches ws) suxs (\acc sux -> case acc of { (,) branches' ws' -> Monad.bind mDict (\insertion -> Monad.pure (Monad.is_applicative mDict) (case IntMap.coq_IntMap_lookup sux branches' of { Prelude.Just incs -> (,) (IntMap.coq_IntMap_insert sux (IntMap.coq_IntSet_delete bid incs) branches') (case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (IntMap.coq_IntSet_size incs)) (unsafeCoerce ((Prelude.succ) 0)) of { Prelude.True -> insertion; Prelude.False -> ws'}); Prelude.Nothing -> (,) branches' insertion})) (case IntMap.coq_IntMap_lookup sux blockMap' of { Prelude.Just s -> Monad.insertM mDict isHeavier s ws'; Prelude.Nothing -> Monad.pure (Monad.is_applicative mDict) ws'})}))) (Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (\_ -> Blocks.blockSuccessors mDict binfo w0))) (Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (\_ -> Blocks.blockId mDict binfo w0))}) n} in go} in Monad.bind mDict (\res -> Monad.pure (Monad.is_applicative mDict) ((,) st2 res)) (go (Data.List.length blocks') (forwardBranches st2) ((:) b' []))}) (computeLoopDepths mDict binfo blockMap st1)}}) (findLoopEnds mDict binfo blockMap' emptyLoopState)) (Monad.mapM (Monad.is_applicative mDict) (\x -> Monad.bind mDict (\bid -> Monad.pure (Monad.is_applicative mDict) ((,) bid x)) (Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (\_ -> Blocks.blockId mDict binfo x))) blocks')) (Monad.forFoldrM mDict [] blocks (\b0 rest -> Monad.bind mDict (\suxs -> case (Prelude.<=) (Data.List.length suxs) ((Prelude.succ) 0) of { Prelude.True -> Monad.pure (Monad.is_applicative mDict) ((:) b0 rest); Prelude.False -> Monad.fmap (Monad.is_functor (Monad.is_applicative mDict)) (\x -> case x of { (,) b' rest' -> (:) b' rest'}) (Monad.forFoldrM mDict ((,) b0 rest) suxs (\sux x -> case x of { (,) b' rest' -> let { fsz = case IntMap.coq_IntMap_lookup sux (forwardBranches st0) of { Prelude.Just fwds -> IntMap.coq_IntSet_size fwds; Prelude.Nothing -> 0}} in let { bsz = case IntMap.coq_IntMap_lookup sux (backwardBranches st0) of { Prelude.Just bwds -> IntMap.coq_IntSet_size bwds; Prelude.Nothing -> 0}} in case (Prelude.<=) ((Prelude.+) fsz bsz) ((Prelude.succ) 0) of { Prelude.True -> Monad.pure (Monad.is_applicative mDict) ((,) b' rest'); Prelude.False -> case IntMap.coq_IntMap_lookup sux blockMap of { Prelude.Just sux' -> Monad.bind mDict (\z0 -> case z0 of { (,) b'' sux'' -> Monad.pure (Monad.is_applicative mDict) ((,) b'' ((:) sux'' rest'))}) (Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (\_ -> Blocks.splitCriticalEdge mDict binfo b' sux')); Prelude.Nothing -> Monad.pure (Monad.is_applicative mDict) ((,) b' rest')}}}))}) (Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (\_ -> Blocks.blockSuccessors mDict binfo b0))))}) (findLoopEnds mDict binfo blockMap emptyLoopState)) (Monad.mapM (Monad.is_applicative mDict) (\x -> Monad.bind mDict (\bid -> Monad.pure (Monad.is_applicative mDict) ((,) bid x)) (Yoneda.iso_to (Yoneda.coq_Yoneda_lemma (Monad.is_functor (Monad.is_applicative mDict))) (\_ -> Blocks.blockId mDict binfo x))) blocks)}