linearscan-0.7.0: LinearScan/Resolve.hs
{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}
module LinearScan.Resolve 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 Hask.Utils
import qualified LinearScan.Allocate as Allocate
import qualified LinearScan.Applicative as Applicative
import qualified LinearScan.Blocks as Blocks
import qualified LinearScan.Functor as Functor
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.Maybe as Maybe
import qualified LinearScan.Monad as Monad
import qualified LinearScan.Prelude0 as Prelude0
import qualified LinearScan.UsePos as UsePos
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
| Swap PhysReg Blocks.VarId PhysReg Blocks.VarId
| Spill PhysReg Blocks.VarId
| Restore Blocks.VarId PhysReg
| AllocReg Blocks.VarId PhysReg
| FreeReg PhysReg Blocks.VarId
data ResolvingMoveSet =
RSMove Prelude.Int Blocks.VarId Prelude.Int
| RSSwap Prelude.Int Blocks.VarId Prelude.Int Blocks.VarId
| RSSpill Prelude.Int Blocks.VarId
| RSRestore Blocks.VarId Prelude.Int
| RSAllocReg Blocks.VarId Prelude.Int
| RSFreeReg Prelude.Int Blocks.VarId
| RSAssignReg Prelude.Int Blocks.VarId
| RSClearReg Prelude.Int Blocks.VarId
weakenResolvingMove :: Prelude.Int -> ResolvingMove -> ResolvingMoveSet
weakenResolvingMove maxReg x =
case x of {
Move fr fv tr -> RSMove ( fr) fv ( tr);
Swap fr fv tr tv -> RSSwap ( fr) fv ( tr) tv;
Spill fr tv -> RSSpill ( fr) tv;
Restore fv tr -> RSRestore fv ( tr);
AllocReg fv tr -> RSAllocReg fv ( tr);
FreeReg fr tv -> RSFreeReg ( fr) tv}
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};
Swap fr1 fv1 tr1 tv1 ->
case s2 of {
Swap fr2 fv2 tr2 tv2 ->
(Prelude.&&)
(Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1)
(unsafeCoerce fr2))
((Prelude.&&)
(Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1)
(unsafeCoerce fv2))
((Prelude.&&)
(Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)
(unsafeCoerce tr2))
(Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1)
(unsafeCoerce tv2))));
_ -> Prelude.False};
Spill fr1 fv1 ->
case s2 of {
Spill fr2 fv2 ->
(Prelude.&&)
(Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1)
(unsafeCoerce fr2))
(Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1)
(unsafeCoerce fv2));
_ -> Prelude.False};
Restore tv1 tr1 ->
case s2 of {
Restore tv2 tr2 ->
(Prelude.&&)
(Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce tv1)
(unsafeCoerce tv2))
(Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1)
(unsafeCoerce tr2));
_ -> 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}}
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 tr2 tv2 -> Ssrbool.ReflectF} in
let {_evar_0_1 = \fr2 fv2 -> Ssrbool.ReflectF} in
let {_evar_0_2 = \tv2 tr2 -> Ssrbool.ReflectF} in
let {_evar_0_3 = \fv2 tr2 -> Ssrbool.ReflectF} in
let {_evar_0_4 = \fr2 tv2 -> Ssrbool.ReflectF} in
case _top_assumption_0 of {
Move x x0 x1 -> unsafeCoerce _evar_0_ x x0 x1;
Swap x x0 x1 x2 -> _evar_0_0 x x0 x1 x2;
Spill x x0 -> _evar_0_1 x x0;
Restore x x0 -> _evar_0_2 x x0;
AllocReg x x0 -> _evar_0_3 x x0;
FreeReg x x0 -> _evar_0_4 x x0}}
in
let {
_evar_0_0 = \fr1 fv1 tr1 tv1 _top_assumption_0 ->
let {_evar_0_0 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
let {
_evar_0_1 = \fr2 fv2 tr2 tv2 ->
let {
_evar_0_1 = \_ ->
let {
_evar_0_1 = 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
Ssrnat.nat_eqType
tv1 tv2 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 Ssrnat.nat_eqType tv1
tv2 of {
Ssrbool.ReflectT -> _evar_0_2 __;
Ssrbool.ReflectF -> _evar_0_3 __}}
in
case Eqtype.eqP
(Fintype.ordinal_eqType maxReg)
tr1 tr2 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 Ssrnat.nat_eqType tv1
tv2 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 Ssrnat.nat_eqType tv1 tv2 of {
Ssrbool.ReflectT -> _evar_0_3 __;
Ssrbool.ReflectF -> _evar_0_4 __}}
in
case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1
tr2 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 = 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 Ssrnat.nat_eqType tv1
tv2 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 Ssrnat.nat_eqType tv1 tv2 of {
Ssrbool.ReflectT -> _evar_0_3 __;
Ssrbool.ReflectF -> _evar_0_4 __}}
in
case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1
tr2 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 = 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 Ssrnat.nat_eqType tv1 tv2 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 Ssrnat.nat_eqType tv1 tv2 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
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 = \fr2 fv2 -> Ssrbool.ReflectF} in
let {_evar_0_3 = \tv2 tr2 -> Ssrbool.ReflectF} in
let {_evar_0_4 = \fv2 tr2 -> Ssrbool.ReflectF} in
let {_evar_0_5 = \fr2 tv2 -> Ssrbool.ReflectF} in
case _top_assumption_0 of {
Move x x0 x1 -> _evar_0_0 x x0 x1;
Swap x x0 x1 x2 -> unsafeCoerce _evar_0_1 x x0 x1 x2;
Spill x x0 -> _evar_0_2 x x0;
Restore x x0 -> _evar_0_3 x x0;
AllocReg x x0 -> _evar_0_4 x x0;
FreeReg x x0 -> _evar_0_5 x x0}}
in
let {
_evar_0_1 = \fr1 fv1 _top_assumption_0 ->
let {_evar_0_1 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
let {_evar_0_2 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in
let {
_evar_0_3 = \fr2 fv2 ->
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 Ssrnat.nat_eqType fv1 fv2 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 Ssrnat.nat_eqType fv1 fv2 of {
Ssrbool.ReflectT -> _evar_0_4 __;
Ssrbool.ReflectF -> _evar_0_5 __}}
in
case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of {
Ssrbool.ReflectT -> _evar_0_3 __;
Ssrbool.ReflectF -> _evar_0_4 __}}
in
let {_evar_0_4 = \tv2 tr2 -> Ssrbool.ReflectF} in
let {_evar_0_5 = \fv2 tr2 -> Ssrbool.ReflectF} in
let {_evar_0_6 = \fr2 tv2 -> Ssrbool.ReflectF} in
case _top_assumption_0 of {
Move x x0 x1 -> _evar_0_1 x x0 x1;
Swap x x0 x1 x2 -> _evar_0_2 x x0 x1 x2;
Spill x x0 -> unsafeCoerce _evar_0_3 x x0;
Restore x x0 -> _evar_0_4 x x0;
AllocReg x x0 -> _evar_0_5 x x0;
FreeReg x x0 -> _evar_0_6 x x0}}
in
let {
_evar_0_2 = \tv1 tr1 _top_assumption_0 ->
let {_evar_0_2 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
let {_evar_0_3 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in
let {_evar_0_4 = \fr2 fv2 -> Ssrbool.ReflectF} in
let {
_evar_0_5 = \tv2 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 tv1 tv2 of {
Ssrbool.ReflectT -> _evar_0_5 __;
Ssrbool.ReflectF -> _evar_0_6 __}}
in
let {_evar_0_6 = \fv2 tr2 -> Ssrbool.ReflectF} in
let {_evar_0_7 = \fr2 tv2 -> Ssrbool.ReflectF} in
case _top_assumption_0 of {
Move x x0 x1 -> _evar_0_2 x x0 x1;
Swap x x0 x1 x2 -> _evar_0_3 x x0 x1 x2;
Spill x x0 -> _evar_0_4 x x0;
Restore x x0 -> unsafeCoerce _evar_0_5 x x0;
AllocReg x x0 -> _evar_0_6 x x0;
FreeReg x x0 -> _evar_0_7 x x0}}
in
let {
_evar_0_3 = \fv1 tr1 _top_assumption_0 ->
let {_evar_0_3 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in
let {_evar_0_4 = \fr2 fv2 tr2 tv2 -> Ssrbool.ReflectF} in
let {_evar_0_5 = \fr2 fv2 -> Ssrbool.ReflectF} in
let {_evar_0_6 = \tv2 tr2 -> Ssrbool.ReflectF} in
let {
_evar_0_7 = \fv2 tr2 ->
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 (Fintype.ordinal_eqType maxReg) tr1 tr2 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 (Fintype.ordinal_eqType maxReg) tr1 tr2 of {
Ssrbool.ReflectT -> _evar_0_8 __;
Ssrbool.ReflectF -> _evar_0_9 __}}
in
case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of {
Ssrbool.ReflectT -> _evar_0_7 __;
Ssrbool.ReflectF -> _evar_0_8 __}}
in
let {_evar_0_8 = \fr2 tv2 -> Ssrbool.ReflectF} in
case _top_assumption_0 of {
Move x x0 x1 -> _evar_0_3 x x0 x1;
Swap x x0 x1 x2 -> _evar_0_4 x x0 x1 x2;
Spill x x0 -> _evar_0_5 x x0;
Restore x x0 -> _evar_0_6 x x0;
AllocReg x x0 -> unsafeCoerce _evar_0_7 x x0;
FreeReg x x0 -> _evar_0_8 x x0}}
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 tr2 tv2 -> Ssrbool.ReflectF} in
let {_evar_0_6 = \fr2 fv2 -> Ssrbool.ReflectF} in
let {_evar_0_7 = \tv2 tr2 -> Ssrbool.ReflectF} in
let {_evar_0_8 = \fv2 tr2 -> 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 Ssrnat.nat_eqType 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 Ssrnat.nat_eqType tv1 tv2 of {
Ssrbool.ReflectT -> _evar_0_10 __;
Ssrbool.ReflectF -> _evar_0_11 __}}
in
case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of {
Ssrbool.ReflectT -> _evar_0_9 __;
Ssrbool.ReflectF -> _evar_0_10 __}}
in
case _top_assumption_0 of {
Move x x0 x1 -> _evar_0_4 x x0 x1;
Swap x x0 x1 x2 -> _evar_0_5 x x0 x1 x2;
Spill x x0 -> _evar_0_6 x x0;
Restore x x0 -> _evar_0_7 x x0;
AllocReg x x0 -> _evar_0_8 x x0;
FreeReg x x0 -> unsafeCoerce _evar_0_9 x x0}}
in
case _top_assumption_ of {
Move x x0 x1 -> unsafeCoerce _evar_0_ x x0 x1;
Swap x x0 x1 x2 -> unsafeCoerce _evar_0_0 x x0 x1 x2;
Spill x x0 -> unsafeCoerce _evar_0_1 x x0;
Restore x x0 -> unsafeCoerce _evar_0_2 x x0;
AllocReg x x0 -> unsafeCoerce _evar_0_3 x x0;
FreeReg x x0 -> unsafeCoerce _evar_0_4 x x0}
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)
coq_ResGraphNode :: Prelude.Int -> Eqtype.Equality__Coq_type
coq_ResGraphNode maxReg =
Eqtype.sum_eqType (Fintype.ordinal_eqType maxReg) Ssrnat.nat_eqType
data ResGraphEdge =
Build_ResGraphEdge ResolvingMove Prelude.Bool (Prelude.Maybe
Eqtype.Equality__Coq_sort)
(Prelude.Maybe Eqtype.Equality__Coq_sort)
resMove :: Prelude.Int -> ResGraphEdge -> ResolvingMove
resMove maxReg r =
case r of {
Build_ResGraphEdge resMove0 resGhost0 resBeg0 resEnd0 -> resMove0}
resGhost :: Prelude.Int -> ResGraphEdge -> Prelude.Bool
resGhost maxReg r =
case r of {
Build_ResGraphEdge resMove0 resGhost0 resBeg0 resEnd0 -> resGhost0}
resBeg :: Prelude.Int -> ResGraphEdge -> Prelude.Maybe
Eqtype.Equality__Coq_sort
resBeg maxReg r =
case r of {
Build_ResGraphEdge resMove0 resGhost0 resBeg0 resEnd0 -> resBeg0}
resEnd :: Prelude.Int -> ResGraphEdge -> Prelude.Maybe
Eqtype.Equality__Coq_sort
resEnd maxReg r =
case r of {
Build_ResGraphEdge resMove0 resGhost0 resBeg0 resEnd0 -> resEnd0}
eqResGraphEdge :: Prelude.Int -> ResGraphEdge -> ResGraphEdge -> Prelude.Bool
eqResGraphEdge maxReg s1 s2 =
case s1 of {
Build_ResGraphEdge a1 b1 c1 d1 ->
case s2 of {
Build_ResGraphEdge a2 b2 c2 d2 ->
(Prelude.&&)
(Eqtype.eq_op (coq_ResolvingMove_eqType maxReg) (unsafeCoerce a1)
(unsafeCoerce a2))
((Prelude.&&)
(Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1)
(unsafeCoerce b2))
((Prelude.&&)
(Eqtype.eq_op (Eqtype.option_eqType (coq_ResGraphNode maxReg))
(unsafeCoerce c1) (unsafeCoerce c2))
(Eqtype.eq_op (Eqtype.option_eqType (coq_ResGraphNode maxReg))
(unsafeCoerce d1) (unsafeCoerce d2))))}}
eqResGraphEdgeP :: Prelude.Int -> Eqtype.Equality__Coq_axiom ResGraphEdge
eqResGraphEdgeP maxReg _top_assumption_ =
let {
_evar_0_ = \a1 b1 c1 d1 _top_assumption_0 ->
let {
_evar_0_ = \a2 b2 c2 d2 ->
let {
_evar_0_ = \_ ->
let {
_evar_0_ = 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
(Eqtype.option_eqType
(coq_ResGraphNode
maxReg)) d1 d2 of {
Ssrbool.ReflectT ->
_evar_0_ __;
Ssrbool.ReflectF ->
_evar_0_0 __}}
in
_evar_0_}
in
let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
case Eqtype.eqP
(Eqtype.option_eqType
(coq_ResGraphNode maxReg)) c1 c2 of {
Ssrbool.ReflectT -> _evar_0_ __;
Ssrbool.ReflectF -> _evar_0_0 __}}
in
_evar_0_}
in
let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
case Eqtype.eqP Eqtype.bool_eqType b1 b2 of {
Ssrbool.ReflectT -> _evar_0_ __;
Ssrbool.ReflectF -> _evar_0_0 __}}
in
_evar_0_}
in
let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
case Eqtype.eqP (coq_ResolvingMove_eqType maxReg) a1 a2 of {
Ssrbool.ReflectT -> _evar_0_ __;
Ssrbool.ReflectF -> _evar_0_0 __}}
in
case _top_assumption_0 of {
Build_ResGraphEdge x x0 x1 x2 -> unsafeCoerce _evar_0_ x x0 x1 x2}}
in
case _top_assumption_ of {
Build_ResGraphEdge x x0 x1 x2 -> unsafeCoerce _evar_0_ x x0 x1 x2}
coq_ResGraphEdge_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of
ResGraphEdge
coq_ResGraphEdge_eqMixin maxReg =
Eqtype.Equality__Mixin (eqResGraphEdge maxReg) (eqResGraphEdgeP maxReg)
coq_ResGraphEdge_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type
coq_ResGraphEdge_eqType maxReg =
unsafeCoerce (coq_ResGraphEdge_eqMixin maxReg)
determineEdge :: Prelude.Int -> ResGraphEdge -> (,)
(Prelude.Maybe Eqtype.Equality__Coq_sort)
(Prelude.Maybe Eqtype.Equality__Coq_sort)
determineEdge maxReg x =
(,) (resBeg maxReg x) (resEnd maxReg x)
splitEdge :: Prelude.Int -> ResGraphEdge -> [] ResGraphEdge
splitEdge maxReg x =
case resMove maxReg x of {
Move fr fv tr -> (:) (Build_ResGraphEdge (Spill fr fv) Prelude.False
(resBeg maxReg x) Prelude.Nothing) ((:) (Build_ResGraphEdge (Restore fv
tr) (resGhost maxReg x) Prelude.Nothing (resEnd maxReg x)) []);
Swap fr fv tr tv -> (:) (Build_ResGraphEdge (Swap tr tv fr fv)
(resGhost maxReg x) (resEnd maxReg x) (resBeg maxReg x)) [];
_ -> []}
determineMoves :: Prelude.Int -> (IntMap.IntMap ResGraphEdge) -> []
ResGraphEdge
determineMoves maxReg moves =
unsafeCoerce
(Graph.topsort (coq_ResGraphNode maxReg) (coq_ResGraphEdge_eqType maxReg)
(IntMap.coq_IntMap_foldl
(Prelude0.flip
(unsafeCoerce
(Graph.addEdge (coq_ResGraphNode maxReg)
(coq_ResGraphEdge_eqType maxReg))))
(Graph.emptyGraph (coq_ResGraphNode maxReg)
(coq_ResGraphEdge_eqType maxReg)
(unsafeCoerce (determineEdge maxReg))) moves)
(unsafeCoerce (splitEdge maxReg)))
resolvingMoves :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int ->
Prelude.Int -> IntMap.IntMap ResGraphEdge
resolvingMoves maxReg allocs from to =
let {
liveAtFrom = IntMap.coq_IntMap_fromList
(Prelude.map (\i -> (,)
(Interval.ivar (Allocate.intVal maxReg i)) i)
(Prelude.filter (\i ->
(Prelude.&&)
((Prelude.<=)
(Interval.ibeg (Allocate.intVal maxReg i)) from)
((Prelude.<=) ((Prelude.succ) from)
(Interval.iend (Allocate.intVal maxReg i))))
allocs))}
in
let {
shouldKeep = \int pos ->
case (Prelude.<=) (Interval.ibeg int) pos of {
Prelude.True ->
case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)
(unsafeCoerce (Interval.iend int)) of {
Prelude.True -> (,)
(case Interval.lastUsePos int of {
Prelude.Just u -> (Prelude.<=) to (UsePos.uloc u);
Prelude.Nothing -> Prelude.False}) Prelude.True;
Prelude.False -> (,)
((Prelude.<=) ((Prelude.succ) to) (Interval.iend int)) Prelude.False};
Prelude.False -> (,) Prelude.False Prelude.False}}
in
let {
liveAtTo = IntMap.coq_IntMap_fromList
(Prelude.map (\i -> (,)
(Interval.ivar (Allocate.intVal maxReg i)) ((,) i
(Prelude.snd (shouldKeep (Allocate.intVal maxReg i) to))))
(Prelude.filter (\i ->
Prelude.fst (shouldKeep (Allocate.intVal maxReg i) to))
allocs))}
in
IntMap.coq_IntMap_mergeWithKey (\vid x yp ->
case yp of {
(,) y ghost ->
case Eqtype.eq_op
(Eqtype.option_eqType (Fintype.ordinal_eqType maxReg))
(unsafeCoerce (Allocate.intReg maxReg x))
(unsafeCoerce (Allocate.intReg maxReg y)) of {
Prelude.True ->
case Allocate.intReg maxReg y of {
Prelude.Just reg ->
case ghost of {
Prelude.True -> Prelude.Just (Build_ResGraphEdge (FreeReg reg vid)
Prelude.True (Prelude.Just (unsafeCoerce (Prelude.Left reg)))
(Prelude.Just (unsafeCoerce (Prelude.Right vid))));
Prelude.False -> Prelude.Nothing};
Prelude.Nothing -> Prelude.Nothing};
Prelude.False ->
let {
mmv = case Allocate.intReg maxReg x of {
Prelude.Just xr ->
case Allocate.intReg maxReg y of {
Prelude.Just yr -> Prelude.Just (Move xr vid yr);
Prelude.Nothing -> Prelude.Just (Spill xr vid)};
Prelude.Nothing ->
case Allocate.intReg maxReg y of {
Prelude.Just xr -> Prelude.Just (Restore vid xr);
Prelude.Nothing -> Prelude.Nothing}}}
in
let {
anchor = \x0 ->
Applicative.choose (unsafeCoerce Maybe.option_Alternative)
(Functor.fmap (unsafeCoerce Maybe.coq_Maybe_Functor) (\x1 ->
Prelude.Left x1) (unsafeCoerce (Allocate.intReg maxReg x0)))
(Prelude.Just (Prelude.Right vid))}
in
case mmv of {
Prelude.Just mv -> Prelude.Just (Build_ResGraphEdge mv ghost
(unsafeCoerce anchor x) (unsafeCoerce anchor y));
Prelude.Nothing -> Prelude.Nothing}}})
(IntMap.coq_IntMap_foldlWithKey (\acc vid x ->
case Allocate.intReg maxReg x of {
Prelude.Just r ->
IntMap.coq_IntMap_insert vid (Build_ResGraphEdge (FreeReg r vid)
Prelude.False (Prelude.Just (unsafeCoerce (Prelude.Left r)))
(Prelude.Just (unsafeCoerce (Prelude.Right vid)))) acc;
Prelude.Nothing -> acc}) IntMap.emptyIntMap)
(IntMap.coq_IntMap_foldlWithKey (\acc vid yp ->
case yp of {
(,) y ghost ->
case Allocate.intReg maxReg y of {
Prelude.Just r ->
IntMap.coq_IntMap_insert vid (Build_ResGraphEdge (AllocReg vid r)
ghost (Prelude.Just (unsafeCoerce (Prelude.Right vid)))
(Prelude.Just (unsafeCoerce (Prelude.Left r)))) acc;
Prelude.Nothing -> acc}}) IntMap.emptyIntMap) liveAtFrom liveAtTo
type BlockMoves = (,) Graph.Graph Graph.Graph
movesBetween :: Prelude.Int -> ([] Allocate.Allocation) -> Prelude.Int ->
Prelude.Int -> [] ResGraphEdge
movesBetween maxReg allocs from to =
IntMap.coq_IntMap_foldl (Prelude0.flip (\x x0 -> (:) x x0)) []
(resolvingMoves maxReg allocs from to)
applyMappings :: Prelude.Int -> Blocks.BlockId -> (IntMap.IntMap BlockMoves)
-> Prelude.Bool -> ([] ResGraphEdge) -> IntMap.IntMap
BlockMoves
applyMappings maxReg bid mappings in_from moves =
List1.forFold mappings (unsafeCoerce moves) (\ms mv ->
let {
addToGraphs = \e xs ->
case xs of {
(,) gbeg gend ->
case in_from of {
Prelude.True -> (,) gbeg
(Graph.addEdge (coq_ResGraphNode maxReg)
(coq_ResGraphEdge_eqType maxReg) e gend);
Prelude.False -> (,)
(Graph.addEdge (coq_ResGraphNode maxReg)
(coq_ResGraphEdge_eqType maxReg) e gbeg) gend}}}
in
let {
eg = Graph.emptyGraph (coq_ResGraphNode maxReg)
(coq_ResGraphEdge_eqType maxReg)
(unsafeCoerce (determineEdge maxReg))}
in
let {
f = \mxs ->
addToGraphs mv
(case mxs of {
Prelude.Just xs -> xs;
Prelude.Nothing -> (,) eg eg})}
in
IntMap.coq_IntMap_alter ((Prelude..) (\x -> Prelude.Just x) f) bid ms)
checkBlockBoundary :: Prelude.Int -> ([] Allocate.Allocation) ->
Blocks.BlockId -> Prelude.Bool ->
LiveSets.BlockLiveSets -> LiveSets.BlockLiveSets ->
IntSet.IntSet -> (IntMap.IntMap BlockMoves) ->
IntMap.IntMap BlockMoves
checkBlockBoundary maxReg allocs bid in_from from to liveIn mappings =
applyMappings maxReg bid mappings in_from
(movesBetween maxReg allocs (LiveSets.blockLastOpId from)
(LiveSets.blockFirstOpId to))
resolveDataFlow :: Prelude.Int -> (Monad.Monad a5) -> (Blocks.BlockInfo
a5 a1 a2 a3 a4) -> ([] Allocate.Allocation) -> ([]
a1) -> (IntMap.IntMap LiveSets.BlockLiveSets) -> a5
resolveDataFlow maxReg mDict binfo allocs blocks liveSets =
Functor.fmap (Applicative.is_functor (Monad.is_applicative mDict))
Prelude.fst
(Monad.forFoldM mDict ((,) IntMap.emptyIntMap Prelude.True) blocks
(\z b ->
case z of {
(,) mappings isFirst ->
Monad.bind mDict (\bid ->
case IntMap.coq_IntMap_lookup bid liveSets of {
Prelude.Just from ->
let {
mappings' = case isFirst of {
Prelude.True ->
applyMappings maxReg bid mappings Prelude.False
(movesBetween maxReg allocs ((Prelude.succ) 0)
(LiveSets.blockFirstOpId from));
Prelude.False -> mappings}}
in
Monad.bind mDict (\suxs ->
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 ->
applyMappings maxReg bid mappings' Prelude.True
(movesBetween maxReg allocs
(LiveSets.blockLastOpId from)
((Prelude.succ) ((Prelude.succ)
(LiveSets.blockLastOpId from))));
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 key
in_from from to (LiveSets.blockLiveIn to)
ms;
Prelude.Nothing -> ms})}}
in
Applicative.pure (Monad.is_applicative mDict) ((,) mappings''
Prelude.False)) (Blocks.blockSuccessors mDict binfo b);
Prelude.Nothing ->
Applicative.pure (Monad.is_applicative mDict) ((,) mappings
Prelude.False)}) (Blocks.blockId mDict binfo b)}))