{-# OPTIONS_GHC -cpp -XMagicHash #-} {- For Hugs, use the option -F"cpp -P -traditional" -} module LinearScan.Resolve where import Debug.Trace (trace, traceShow, traceShowId) 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 Hask.Utils import qualified LinearScan.Allocate as Allocate import qualified LinearScan.Blocks as Blocks import qualified LinearScan.Graph as Graph import qualified LinearScan.IntMap as IntMap import qualified LinearScan.IntSet as IntSet import qualified LinearScan.Interval as Interval import qualified LinearScan.List1 as List1 import qualified LinearScan.LiveSets as LiveSets import qualified LinearScan.Monad as Monad import qualified LinearScan.Prelude0 as Prelude0 import qualified LinearScan.Eqtype as Eqtype import qualified LinearScan.Fintype as Fintype 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 __ :: any __ = Prelude.error "Logical or arity value used" type PhysReg = Prelude.Int data ResolvingMove = Move PhysReg Blocks.VarId PhysReg | Spill PhysReg Blocks.VarId Prelude.Bool | Restore Blocks.VarId PhysReg Prelude.Bool | AllocReg Blocks.VarId PhysReg | FreeReg PhysReg Blocks.VarId | AssignReg Blocks.VarId PhysReg | ClearReg PhysReg Blocks.VarId | AllocStack Blocks.VarId | FreeStack Blocks.VarId | Looped ResolvingMove coq_ResolvingMove_rect :: Prelude.Int -> (PhysReg -> Blocks.VarId -> PhysReg -> a1) -> (PhysReg -> Blocks.VarId -> Prelude.Bool -> a1) -> (Blocks.VarId -> PhysReg -> Prelude.Bool -> a1) -> (Blocks.VarId -> PhysReg -> a1) -> (PhysReg -> Blocks.VarId -> a1) -> (Blocks.VarId -> PhysReg -> a1) -> (PhysReg -> Blocks.VarId -> a1) -> (Blocks.VarId -> a1) -> (Blocks.VarId -> a1) -> (ResolvingMove -> a1 -> a1) -> ResolvingMove -> a1 coq_ResolvingMove_rect maxReg f f0 f1 f2 f3 f4 f5 f6 f7 f8 r = case r of { Move p v p0 -> f p v p0; Spill p v b -> f0 p v b; Restore v p b -> f1 v p b; AllocReg v p -> f2 v p; FreeReg p v -> f3 p v; AssignReg v p -> f4 v p; ClearReg p v -> f5 p v; AllocStack v -> f6 v; FreeStack v -> f7 v; Looped r0 -> f8 r0 (coq_ResolvingMove_rect maxReg f f0 f1 f2 f3 f4 f5 f6 f7 f8 r0)} data ResolvingMoveSet = RSMove Prelude.Int Blocks.VarId Prelude.Int | RSSpill Prelude.Int Blocks.VarId Prelude.Bool | RSRestore Blocks.VarId Prelude.Int Prelude.Bool | RSAllocReg Blocks.VarId Prelude.Int | RSFreeReg Prelude.Int Blocks.VarId | RSAssignReg Blocks.VarId Prelude.Int | RSClearReg Prelude.Int Blocks.VarId | RSAllocStack Blocks.VarId | RSFreeStack Blocks.VarId | RSLooped ResolvingMoveSet weakenResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMoveSet weakenResolvingMove maxReg x = case x of { Move fr fv tr -> RSMove (Prelude.id fr) fv (Prelude.id tr); Spill fr tv b -> RSSpill (Prelude.id fr) tv b; Restore fv tr b -> RSRestore fv (Prelude.id tr) b; AllocReg fv tr -> RSAllocReg fv (Prelude.id tr); FreeReg fr tv -> RSFreeReg (Prelude.id fr) tv; AssignReg fv tr -> RSAssignReg fv (Prelude.id tr); ClearReg fr tv -> RSClearReg (Prelude.id fr) tv; AllocStack tv -> RSAllocStack tv; FreeStack fv -> RSFreeStack fv; Looped x0 -> RSLooped (weakenResolvingMove maxReg x0)} eqResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMove -> Prelude.Bool eqResolvingMove maxReg s1 s2 = case s1 of { Move fr1 fv1 tr1 -> case s2 of { Move fr2 fv2 tr2 -> (Prelude.&&) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce fr2)) ((Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce fv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1) (unsafeCoerce tr2))); _ -> Prelude.False}; Spill fr1 fv1 b1 -> case s2 of { Spill fr2 fv2 b2 -> (Prelude.&&) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce fr2)) ((Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce fv2)) (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1) (unsafeCoerce b2))); _ -> Prelude.False}; Restore tv1 tr1 b1 -> case s2 of { Restore tv2 tr2 b2 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce tv2)) ((Prelude.&&) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1) (unsafeCoerce tr2)) (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1) (unsafeCoerce b2))); _ -> Prelude.False}; AllocReg fv1 tr1 -> case s2 of { AllocReg fv2 tr2 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce fv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1) (unsafeCoerce tr2)); _ -> Prelude.False}; FreeReg fr1 tv1 -> case s2 of { FreeReg fr2 tv2 -> (Prelude.&&) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce fr2)) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce tv2)); _ -> Prelude.False}; AssignReg fv1 tr1 -> case s2 of { AssignReg fv2 tr2 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce fv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1) (unsafeCoerce tr2)); _ -> Prelude.False}; ClearReg fr1 tv1 -> case s2 of { ClearReg fr2 tv2 -> (Prelude.&&) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce fr2)) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce tv2)); _ -> Prelude.False}; AllocStack tv1 -> case s2 of { AllocStack tv2 -> Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce tv2); _ -> Prelude.False}; FreeStack fv1 -> case s2 of { FreeStack fv2 -> Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce fv2); _ -> Prelude.False}; Looped x -> case s2 of { Looped y -> eqResolvingMove maxReg x y; _ -> Prelude.False}} eqResolvingMoveP :: Prelude.Int -> Eqtype.Equality__Coq_axiom ResolvingMove eqResolvingMoveP maxReg _top_assumption_ = let { _evar_0_ = \fr1 fv1 tr1 _top_assumption_0 -> let { _evar_0_ = \fr2 fv2 tr2 -> let { _evar_0_ = \_ -> let { _evar_0_ = let { _evar_0_ = \_ -> let { _evar_0_ = let { _evar_0_ = \_ -> let {_evar_0_ = Ssrbool.ReflectT} in _evar_0_} in let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_ __; Ssrbool.ReflectF -> _evar_0_0 __}} in _evar_0_} in let { _evar_0_0 = \_ -> let { _evar_0_0 = \_ -> let {_evar_0_0 = Ssrbool.ReflectF} in _evar_0_0} in let {_evar_0_1 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_0 __; Ssrbool.ReflectF -> _evar_0_1 __}} in case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { Ssrbool.ReflectT -> _evar_0_ __; Ssrbool.ReflectF -> _evar_0_0 __}} in _evar_0_} in let { _evar_0_0 = \_ -> let { _evar_0_0 = \_ -> let { _evar_0_0 = let { _evar_0_0 = \_ -> let {_evar_0_0 = Ssrbool.ReflectF} in _evar_0_0} in let {_evar_0_1 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_0 __; Ssrbool.ReflectF -> _evar_0_1 __}} in _evar_0_0} in let { _evar_0_1 = \_ -> let { _evar_0_1 = \_ -> let {_evar_0_1 = Ssrbool.ReflectF} in _evar_0_1} in let {_evar_0_2 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_1 __; Ssrbool.ReflectF -> _evar_0_2 __}} in case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { Ssrbool.ReflectT -> _evar_0_0 __; Ssrbool.ReflectF -> _evar_0_1 __}} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of { Ssrbool.ReflectT -> _evar_0_ __; Ssrbool.ReflectF -> _evar_0_0 __}} in let {_evar_0_0 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_1 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in let {_evar_0_2 = \fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_3 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_4 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \tv2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \fv2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> unsafeCoerce _evar_0_ x x0 x1; Spill x x0 x1 -> _evar_0_0 x x0 x1; Restore x x0 x1 -> _evar_0_1 x x0 x1; AllocReg x x0 -> _evar_0_2 x x0; FreeReg x x0 -> _evar_0_3 x x0; AssignReg x x0 -> _evar_0_4 x x0; ClearReg x x0 -> _evar_0_5 x x0; AllocStack x -> _evar_0_6 x; FreeStack x -> _evar_0_7 x; Looped x -> _evar_0_8 x}} in let { _evar_0_0 = \fr1 fv1 b1 _top_assumption_0 -> let {_evar_0_0 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let { _evar_0_1 = \fr2 fv2 b2 -> let { _evar_0_1 = \_ -> let { _evar_0_1 = let { _evar_0_1 = \_ -> let { _evar_0_1 = let { _evar_0_1 = \_ -> let {_evar_0_1 = Ssrbool.ReflectT} in _evar_0_1} in let {_evar_0_2 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { Ssrbool.ReflectT -> _evar_0_1 __; Ssrbool.ReflectF -> _evar_0_2 __}} in _evar_0_1} in let { _evar_0_2 = \_ -> let { _evar_0_2 = \_ -> let {_evar_0_2 = Ssrbool.ReflectF} in _evar_0_2} in let {_evar_0_3 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { Ssrbool.ReflectT -> _evar_0_2 __; Ssrbool.ReflectF -> _evar_0_3 __}} in case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { Ssrbool.ReflectT -> _evar_0_1 __; Ssrbool.ReflectF -> _evar_0_2 __}} in _evar_0_1} in let { _evar_0_2 = \_ -> let { _evar_0_2 = \_ -> let { _evar_0_2 = let { _evar_0_2 = \_ -> let {_evar_0_2 = Ssrbool.ReflectF} in _evar_0_2} in let {_evar_0_3 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { Ssrbool.ReflectT -> _evar_0_2 __; Ssrbool.ReflectF -> _evar_0_3 __}} in _evar_0_2} in let { _evar_0_3 = \_ -> let { _evar_0_3 = \_ -> let {_evar_0_3 = Ssrbool.ReflectF} in _evar_0_3} in let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { Ssrbool.ReflectT -> _evar_0_3 __; Ssrbool.ReflectF -> _evar_0_4 __}} in case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { Ssrbool.ReflectT -> _evar_0_2 __; Ssrbool.ReflectF -> _evar_0_3 __}} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of { Ssrbool.ReflectT -> _evar_0_1 __; Ssrbool.ReflectF -> _evar_0_2 __}} in let {_evar_0_2 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in let {_evar_0_3 = \fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_4 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \tv2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \fv2 -> Ssrbool.ReflectF} in let {_evar_0_9 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_0 x x0 x1; Spill x x0 x1 -> unsafeCoerce _evar_0_1 x x0 x1; Restore x x0 x1 -> _evar_0_2 x x0 x1; AllocReg x x0 -> _evar_0_3 x x0; FreeReg x x0 -> _evar_0_4 x x0; AssignReg x x0 -> _evar_0_5 x x0; ClearReg x x0 -> _evar_0_6 x x0; AllocStack x -> _evar_0_7 x; FreeStack x -> _evar_0_8 x; Looped x -> _evar_0_9 x}} in let { _evar_0_1 = \tv1 tr1 b1 _top_assumption_0 -> let {_evar_0_1 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_2 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let { _evar_0_3 = \tv2 tr2 b2 -> let { _evar_0_3 = \_ -> let { _evar_0_3 = let { _evar_0_3 = \_ -> let { _evar_0_3 = let { _evar_0_3 = \_ -> let {_evar_0_3 = Ssrbool.ReflectT} in _evar_0_3} in let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { Ssrbool.ReflectT -> _evar_0_3 __; Ssrbool.ReflectF -> _evar_0_4 __}} in _evar_0_3} in let { _evar_0_4 = \_ -> let { _evar_0_4 = \_ -> let {_evar_0_4 = Ssrbool.ReflectF} in _evar_0_4} in let {_evar_0_5 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { Ssrbool.ReflectT -> _evar_0_4 __; Ssrbool.ReflectF -> _evar_0_5 __}} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_3 __; Ssrbool.ReflectF -> _evar_0_4 __}} in _evar_0_3} in let { _evar_0_4 = \_ -> let { _evar_0_4 = \_ -> let { _evar_0_4 = let { _evar_0_4 = \_ -> let {_evar_0_4 = Ssrbool.ReflectF} in _evar_0_4} in let {_evar_0_5 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { Ssrbool.ReflectT -> _evar_0_4 __; Ssrbool.ReflectF -> _evar_0_5 __}} in _evar_0_4} in let { _evar_0_5 = \_ -> let { _evar_0_5 = \_ -> let {_evar_0_5 = Ssrbool.ReflectF} in _evar_0_5} in let {_evar_0_6 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { Ssrbool.ReflectT -> _evar_0_5 __; Ssrbool.ReflectF -> _evar_0_6 __}} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_4 __; Ssrbool.ReflectF -> _evar_0_5 __}} in case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_3 __; Ssrbool.ReflectF -> _evar_0_4 __}} in let {_evar_0_4 = \fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \tv2 -> Ssrbool.ReflectF} in let {_evar_0_9 = \fv2 -> Ssrbool.ReflectF} in let {_evar_0_10 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_1 x x0 x1; Spill x x0 x1 -> _evar_0_2 x x0 x1; Restore x x0 x1 -> unsafeCoerce _evar_0_3 x x0 x1; AllocReg x x0 -> _evar_0_4 x x0; FreeReg x x0 -> _evar_0_5 x x0; AssignReg x x0 -> _evar_0_6 x x0; ClearReg x x0 -> _evar_0_7 x x0; AllocStack x -> _evar_0_8 x; FreeStack x -> _evar_0_9 x; Looped x -> _evar_0_10 x}} in let { _evar_0_2 = \fv1 tr1 _top_assumption_0 -> let {_evar_0_2 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_3 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_4 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in let { _evar_0_5 = \fv2 tr2 -> let { _evar_0_5 = \_ -> let { _evar_0_5 = let { _evar_0_5 = \_ -> let {_evar_0_5 = Ssrbool.ReflectT} in _evar_0_5} in let {_evar_0_6 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_5 __; Ssrbool.ReflectF -> _evar_0_6 __}} in _evar_0_5} in let { _evar_0_6 = \_ -> let { _evar_0_6 = \_ -> let {_evar_0_6 = Ssrbool.ReflectF} in _evar_0_6} in let {_evar_0_7 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_6 __; Ssrbool.ReflectF -> _evar_0_7 __}} in case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { Ssrbool.ReflectT -> _evar_0_5 __; Ssrbool.ReflectF -> _evar_0_6 __}} in let {_evar_0_6 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_9 = \tv2 -> Ssrbool.ReflectF} in let {_evar_0_10 = \fv2 -> Ssrbool.ReflectF} in let {_evar_0_11 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_2 x x0 x1; Spill x x0 x1 -> _evar_0_3 x x0 x1; Restore x x0 x1 -> _evar_0_4 x x0 x1; AllocReg x x0 -> unsafeCoerce _evar_0_5 x x0; FreeReg x x0 -> _evar_0_6 x x0; AssignReg x x0 -> _evar_0_7 x x0; ClearReg x x0 -> _evar_0_8 x x0; AllocStack x -> _evar_0_9 x; FreeStack x -> _evar_0_10 x; Looped x -> _evar_0_11 x}} in let { _evar_0_3 = \fr1 tv1 _top_assumption_0 -> let {_evar_0_3 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_4 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \fv2 tr2 -> Ssrbool.ReflectF} in let { _evar_0_7 = \fr2 tv2 -> let { _evar_0_7 = \_ -> let { _evar_0_7 = let { _evar_0_7 = \_ -> let {_evar_0_7 = Ssrbool.ReflectT} in _evar_0_7} in let {_evar_0_8 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_7 __; Ssrbool.ReflectF -> _evar_0_8 __}} in _evar_0_7} in let { _evar_0_8 = \_ -> let { _evar_0_8 = \_ -> let {_evar_0_8 = Ssrbool.ReflectF} in _evar_0_8} in let {_evar_0_9 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_8 __; Ssrbool.ReflectF -> _evar_0_9 __}} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of { Ssrbool.ReflectT -> _evar_0_7 __; Ssrbool.ReflectF -> _evar_0_8 __}} in let {_evar_0_8 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_9 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_10 = \tv2 -> Ssrbool.ReflectF} in let {_evar_0_11 = \fv2 -> Ssrbool.ReflectF} in let {_evar_0_12 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_3 x x0 x1; Spill x x0 x1 -> _evar_0_4 x x0 x1; Restore x x0 x1 -> _evar_0_5 x x0 x1; AllocReg x x0 -> _evar_0_6 x x0; FreeReg x x0 -> unsafeCoerce _evar_0_7 x x0; AssignReg x x0 -> _evar_0_8 x x0; ClearReg x x0 -> _evar_0_9 x x0; AllocStack x -> _evar_0_10 x; FreeStack x -> _evar_0_11 x; Looped x -> _evar_0_12 x}} in let { _evar_0_4 = \fr1 tv1 _top_assumption_0 -> let {_evar_0_4 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_5 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \fr2 tv2 -> Ssrbool.ReflectF} in let { _evar_0_9 = \fr2 tv2 -> let { _evar_0_9 = \_ -> let { _evar_0_9 = let { _evar_0_9 = \_ -> let {_evar_0_9 = Ssrbool.ReflectT} in _evar_0_9} in let {_evar_0_10 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_9 __; Ssrbool.ReflectF -> _evar_0_10 __}} in _evar_0_9} in let { _evar_0_10 = \_ -> let { _evar_0_10 = \_ -> let {_evar_0_10 = Ssrbool.ReflectF} in _evar_0_10} in let {_evar_0_11 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_10 __; Ssrbool.ReflectF -> _evar_0_11 __}} in case Eqtype.eqP Ssrnat.nat_eqType fr1 fr2 of { Ssrbool.ReflectT -> _evar_0_9 __; Ssrbool.ReflectF -> _evar_0_10 __}} in let {_evar_0_10 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_11 = \tv2 -> Ssrbool.ReflectF} in let {_evar_0_12 = \fv2 -> Ssrbool.ReflectF} in let {_evar_0_13 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_4 x x0 x1; Spill x x0 x1 -> _evar_0_5 x x0 x1; Restore x x0 x1 -> _evar_0_6 x x0 x1; AllocReg x x0 -> _evar_0_7 x x0; FreeReg x x0 -> _evar_0_8 x x0; AssignReg x x0 -> unsafeCoerce _evar_0_9 x x0; ClearReg x x0 -> _evar_0_10 x x0; AllocStack x -> _evar_0_11 x; FreeStack x -> _evar_0_12 x; Looped x -> _evar_0_13 x}} in let { _evar_0_5 = \fr1 tv1 _top_assumption_0 -> let {_evar_0_5 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_6 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_9 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_10 = \fr2 tv2 -> Ssrbool.ReflectF} in let { _evar_0_11 = \fr2 tv2 -> let { _evar_0_11 = \_ -> let { _evar_0_11 = let { _evar_0_11 = \_ -> let {_evar_0_11 = Ssrbool.ReflectT} in _evar_0_11} in let {_evar_0_12 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_11 __; Ssrbool.ReflectF -> _evar_0_12 __}} in _evar_0_11} in let { _evar_0_12 = \_ -> let { _evar_0_12 = \_ -> let {_evar_0_12 = Ssrbool.ReflectF} in _evar_0_12} in let {_evar_0_13 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_12 __; Ssrbool.ReflectF -> _evar_0_13 __}} in case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of { Ssrbool.ReflectT -> _evar_0_11 __; Ssrbool.ReflectF -> _evar_0_12 __}} in let {_evar_0_12 = \tv2 -> Ssrbool.ReflectF} in let {_evar_0_13 = \fv2 -> Ssrbool.ReflectF} in let {_evar_0_14 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_5 x x0 x1; Spill x x0 x1 -> _evar_0_6 x x0 x1; Restore x x0 x1 -> _evar_0_7 x x0 x1; AllocReg x x0 -> _evar_0_8 x x0; FreeReg x x0 -> _evar_0_9 x x0; AssignReg x x0 -> _evar_0_10 x x0; ClearReg x x0 -> unsafeCoerce _evar_0_11 x x0; AllocStack x -> _evar_0_12 x; FreeStack x -> _evar_0_13 x; Looped x -> _evar_0_14 x}} in let { _evar_0_6 = \tv1 _top_assumption_0 -> let {_evar_0_6 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_7 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in let {_evar_0_9 = \fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_10 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_11 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_12 = \fr2 tv2 -> Ssrbool.ReflectF} in let { _evar_0_13 = \tv2 -> let { _evar_0_13 = \_ -> let {_evar_0_13 = Ssrbool.ReflectT} in _evar_0_13} in let {_evar_0_14 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_13 __; Ssrbool.ReflectF -> _evar_0_14 __}} in let {_evar_0_14 = \fv2 -> Ssrbool.ReflectF} in let {_evar_0_15 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_6 x x0 x1; Spill x x0 x1 -> _evar_0_7 x x0 x1; Restore x x0 x1 -> _evar_0_8 x x0 x1; AllocReg x x0 -> _evar_0_9 x x0; FreeReg x x0 -> _evar_0_10 x x0; AssignReg x x0 -> _evar_0_11 x x0; ClearReg x x0 -> _evar_0_12 x x0; AllocStack x -> unsafeCoerce _evar_0_13 x; FreeStack x -> _evar_0_14 x; Looped x -> _evar_0_15 x}} in let { _evar_0_7 = \fv1 _top_assumption_0 -> let {_evar_0_7 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_8 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_9 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in let {_evar_0_10 = \fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_11 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_12 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_13 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_14 = \tv2 -> Ssrbool.ReflectF} in let { _evar_0_15 = \fv2 -> let { _evar_0_15 = \_ -> let {_evar_0_15 = Ssrbool.ReflectT} in _evar_0_15} in let {_evar_0_16 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { Ssrbool.ReflectT -> _evar_0_15 __; Ssrbool.ReflectF -> _evar_0_16 __}} in let {_evar_0_16 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { Move x x0 x1 -> _evar_0_7 x x0 x1; Spill x x0 x1 -> _evar_0_8 x x0 x1; Restore x x0 x1 -> _evar_0_9 x x0 x1; AllocReg x x0 -> _evar_0_10 x x0; FreeReg x x0 -> _evar_0_11 x x0; AssignReg x x0 -> _evar_0_12 x x0; ClearReg x x0 -> _evar_0_13 x x0; AllocStack x -> _evar_0_14 x; FreeStack x -> unsafeCoerce _evar_0_15 x; Looped x -> _evar_0_16 x}} in let { _evar_0_8 = \x iHx _top_assumption_0 -> let {_evar_0_8 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_9 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let {_evar_0_10 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in let {_evar_0_11 = \fv2 tr2 -> Ssrbool.ReflectF} in let {_evar_0_12 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_13 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_14 = \fr2 tv2 -> Ssrbool.ReflectF} in let {_evar_0_15 = \tv2 -> Ssrbool.ReflectF} in let {_evar_0_16 = \fv2 -> Ssrbool.ReflectF} in let { _evar_0_17 = \y -> let {iHx0 = iHx y} in let {_evar_0_17 = \_ -> Ssrbool.ReflectT} in let {_evar_0_18 = \_ -> Ssrbool.ReflectF} in case iHx0 of { Ssrbool.ReflectT -> _evar_0_17 __; Ssrbool.ReflectF -> _evar_0_18 __}} in case _top_assumption_0 of { Move x0 x1 x2 -> _evar_0_8 x0 x1 x2; Spill x0 x1 x2 -> _evar_0_9 x0 x1 x2; Restore x0 x1 x2 -> _evar_0_10 x0 x1 x2; AllocReg x0 x1 -> _evar_0_11 x0 x1; FreeReg x0 x1 -> _evar_0_12 x0 x1; AssignReg x0 x1 -> _evar_0_13 x0 x1; ClearReg x0 x1 -> _evar_0_14 x0 x1; AllocStack x0 -> _evar_0_15 x0; FreeStack x0 -> _evar_0_16 x0; Looped x0 -> _evar_0_17 x0}} in coq_ResolvingMove_rect maxReg (unsafeCoerce _evar_0_) (unsafeCoerce _evar_0_0) (unsafeCoerce _evar_0_1) (unsafeCoerce _evar_0_2) (unsafeCoerce _evar_0_3) (unsafeCoerce _evar_0_4) (unsafeCoerce _evar_0_5) (unsafeCoerce _evar_0_6) (unsafeCoerce _evar_0_7) _evar_0_8 _top_assumption_ coq_ResolvingMove_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of ResolvingMove coq_ResolvingMove_eqMixin maxReg = Eqtype.Equality__Mixin (eqResolvingMove maxReg) (eqResolvingMoveP maxReg) coq_ResolvingMove_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type coq_ResolvingMove_eqType maxReg = unsafeCoerce (coq_ResolvingMove_eqMixin maxReg) shouldAddResolvingEdge :: Prelude.Int -> ResolvingMove -> ResolvingMove -> Prelude.Bool shouldAddResolvingEdge maxReg x y = case x of { Move fr1 fv1 tr1 -> case y of { Move p v tr2 -> Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2); Spill fr2 fv2 b -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce fv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1) (unsafeCoerce fr2)); Restore v tr2 b -> Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2); FreeReg fr2 tv2 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce tv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce fr2)); AssignReg fv2 tr2 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce fv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1) (unsafeCoerce tr2)); _ -> Prelude.False}; Spill fr1 fv1 b -> case y of { Restore v tr2 b0 -> Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2); AllocReg v tr2 -> Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2); FreeReg fr2 tv2 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) (unsafeCoerce tv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce fr2)); _ -> Prelude.False}; Restore tv1 tr1 b -> case y of { Move fr2 fv2 p -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce fv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1) (unsafeCoerce fr2)); Spill fr2 fv2 b0 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce fv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1) (unsafeCoerce fr2)); AssignReg fv2 tr2 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce fv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1) (unsafeCoerce tr2)); FreeStack fv2 -> Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce fv2); _ -> Prelude.False}; AllocReg fv2 tr2 -> case y of { Move p fv3 tr3 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv2) (unsafeCoerce fv3)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr2) (unsafeCoerce tr3)); Restore tv2 tr3 b -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv2) (unsafeCoerce tv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr2) (unsafeCoerce tr3)); FreeReg fr1 tv1 -> (Prelude.&&) (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce fv2)) (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2)); _ -> Prelude.False}; FreeReg fr1 v -> case y of { Restore v0 tr2 b -> Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2); AllocReg v0 tr2 -> Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) (unsafeCoerce tr2); _ -> Prelude.False}; AllocStack tv1 -> case y of { Spill p fv2 b -> Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1) (unsafeCoerce fv2); _ -> Prelude.False}; _ -> Prelude.False} addResolution :: Prelude.Int -> ResolvingMove -> Graph.Graph -> Graph.Graph addResolution maxReg x g = let { f = \x0 y z -> case shouldAddResolvingEdge maxReg x0 y of { Prelude.True -> Graph.addEdge (coq_ResolvingMove_eqType maxReg) (unsafeCoerce ((,) x0 y)) z; Prelude.False -> z}} in Prelude.foldr (\y -> (Prelude..) (unsafeCoerce f y x) (unsafeCoerce f x y)) (Graph.addVertex (coq_ResolvingMove_eqType maxReg) (unsafeCoerce x) g) (Graph.vertices (coq_ResolvingMove_eqType maxReg) g) addResolutions :: Prelude.Int -> Graph.Graph -> ([] ResolvingMove) -> Graph.Graph addResolutions maxReg = Prelude.foldr (addResolution maxReg) isMoveSplittable :: Prelude.Int -> ResolvingMove -> Prelude.Bool isMoveSplittable maxReg x = case x of { Move p v p0 -> Prelude.True; _ -> Prelude.False} splitMove :: Prelude.Int -> ResolvingMove -> Graph.Graph -> Graph.Graph splitMove maxReg x g = case x of { Move fr fv tr -> addResolutions maxReg (Graph.removeVertex (coq_ResolvingMove_eqType maxReg) (unsafeCoerce x) g) ((:) (Spill fr fv Prelude.True) ((:) (Restore fv tr Prelude.True) [])); Looped r -> g; _ -> Graph.addVertex (coq_ResolvingMove_eqType maxReg) (unsafeCoerce (Looped x)) (Graph.removeVertex (coq_ResolvingMove_eqType maxReg) (unsafeCoerce x) g)} resolvingMoves :: Prelude.Int -> ([] Allocate.Allocation) -> (Prelude.Maybe IntSet.IntSet) -> Prelude.Int -> Prelude.Int -> IntMap.IntMap ([] ResolvingMove) resolvingMoves maxReg allocs liveIn from to = let { allocsAt = \pos -> Prelude.foldr (\a rest -> let {i = Allocate.intVal maxReg a} in case (Prelude.&&) ((Prelude.<=) (Interval.ibeg i) pos) ((Prelude.<=) ((Prelude.succ) pos) (Interval.iend i)) of { Prelude.True -> IntMap.coq_IntMap_insert (Interval.ivar i) a rest; Prelude.False -> rest}) IntMap.emptyIntMap allocs} in let { varNotLive = \vid -> case liveIn of { Prelude.Just ins -> Prelude.not (IntSet.coq_IntSet_member vid ins); Prelude.Nothing -> Prelude.False}} in IntMap.coq_IntMap_combine (\vid mx my -> case mx of { Prelude.Just x -> case my of { Prelude.Just y -> case Eqtype.eq_op (Eqtype.option_eqType (Fintype.ordinal_eqType maxReg)) (unsafeCoerce (Allocate.intReg maxReg x)) (unsafeCoerce (Allocate.intReg maxReg y)) of { Prelude.True -> Prelude.Nothing; Prelude.False -> case Allocate.intReg maxReg x of { Prelude.Just xr -> case Allocate.intReg maxReg y of { Prelude.Just yr -> Prelude.Just (case (Prelude.||) (varNotLive vid) (Prelude.not (Ssrnat.odd to)) of { Prelude.True -> (:) (FreeReg xr vid) ((:) (AllocReg vid yr) []); Prelude.False -> (:) (FreeReg xr vid) ((:) (AllocReg vid yr) ((:) (Move xr vid yr) ((:) (AssignReg vid yr) [])))}); Prelude.Nothing -> Prelude.Just ((:) (FreeReg xr vid) ((:) (AllocStack vid) ((:) (Spill xr vid Prelude.False) [])))}; Prelude.Nothing -> case Allocate.intReg maxReg y of { Prelude.Just yr -> Prelude.Just (case (Prelude.||) (varNotLive vid) (Prelude.not (Ssrnat.odd to)) of { Prelude.True -> (:) (AllocReg vid yr) []; Prelude.False -> (:) (AllocReg vid yr) ((:) (Restore vid yr Prelude.False) ((:) (AssignReg vid yr) ((:) (FreeStack vid) [])))}); Prelude.Nothing -> Prelude.Nothing}}}; Prelude.Nothing -> case Allocate.intReg maxReg x of { Prelude.Just r -> Prelude.Just ((:) (FreeReg r vid) []); Prelude.Nothing -> Prelude.Just ((:) (FreeStack vid) [])}}; Prelude.Nothing -> case my of { Prelude.Just y -> case Allocate.intReg maxReg y of { Prelude.Just r -> Prelude.Just ((:) (AllocReg vid r) []); Prelude.Nothing -> Prelude.Just ((:) (AllocStack vid) [])}; Prelude.Nothing -> Prelude.Nothing}}) (allocsAt from) (allocsAt to) determineMoves :: Prelude.Int -> ([] Allocate.Allocation) -> (Prelude.Maybe IntSet.IntSet) -> Prelude.Int -> Prelude.Int -> [] ResolvingMove determineMoves maxReg allocs liveIn from to = let { sortMoves = Graph.topsort (coq_ResolvingMove_eqType maxReg) (unsafeCoerce (isMoveSplittable maxReg)) (unsafeCoerce (splitMove maxReg))} in unsafeCoerce sortMoves (IntMap.coq_IntMap_foldr (Prelude0.flip (addResolutions maxReg)) (Graph.emptyGraph (coq_ResolvingMove_eqType maxReg)) (resolvingMoves maxReg allocs liveIn from to)) type BlockMoves = (,) ([] ResolvingMove) ([] ResolvingMove) checkBlockBoundary :: Prelude.Int -> ([] Allocate.Allocation) -> IntSet.IntSet -> Prelude.Int -> Prelude.Bool -> (Prelude.Maybe LiveSets.BlockLiveSets) -> LiveSets.BlockLiveSets -> (IntMap.IntMap BlockMoves) -> IntMap.IntMap BlockMoves checkBlockBoundary maxReg allocs liveIn bid in_from mfrom to mappings = let { moves = determineMoves maxReg allocs (Prelude.Just liveIn) (case mfrom of { Prelude.Just from -> LiveSets.blockLastOpId from; Prelude.Nothing -> 0}) (LiveSets.blockFirstOpId to)} in IntMap.coq_IntMap_alter (\mx -> case case mx of { Prelude.Just x -> x; Prelude.Nothing -> (,) [] []} of { (,) begs ends -> Prelude.Just (case in_from of { Prelude.True -> (,) begs moves; Prelude.False -> (,) moves ends})}) bid mappings resolveDataFlow :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo a5 a1 a2 a3 a4) -> ([] Allocate.Allocation) -> ([] a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> IntMap.IntMap BlockMoves resolveDataFlow maxReg mDict binfo allocs blocks liveSets = Prelude.fst (List1.forFold ((,) IntMap.emptyIntMap Prelude.True) blocks (\z b -> case z of { (,) mappings isFirst -> let {bid = Blocks.blockId mDict binfo b} in case IntMap.coq_IntMap_lookup bid liveSets of { Prelude.Just from -> let { mappings' = case isFirst of { Prelude.True -> checkBlockBoundary maxReg allocs (LiveSets.blockLiveIn from) bid Prelude.False Prelude.Nothing from mappings; Prelude.False -> mappings}} in let {suxs = Blocks.blockSuccessors mDict binfo b} in let { in_from = (Prelude.<=) (Data.List.length suxs) ((Prelude.succ) 0)} in let { mappings'' = case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Data.List.length suxs)) (unsafeCoerce 0) of { Prelude.True -> mappings'; Prelude.False -> List1.forFold mappings' suxs (\ms s_bid -> case IntMap.coq_IntMap_lookup s_bid liveSets of { Prelude.Just to -> let { key = case in_from of { Prelude.True -> bid; Prelude.False -> s_bid}} in checkBlockBoundary maxReg allocs (LiveSets.blockLiveIn to) key in_from (Prelude.Just from) to ms; Prelude.Nothing -> ms})}} in (,) mappings'' Prelude.False; Prelude.Nothing -> (,) mappings Prelude.False}}))