diff --git a/LinearScan.hs b/LinearScan.hs --- a/LinearScan.hs +++ b/LinearScan.hs @@ -479,9 +479,6 @@ show (LS.RSMove fr fv tr) = "move (r" ++ show fr ++ " v" ++ show fv ++ ") " ++ "(r" ++ show tr ++ " v" ++ show fv ++ ")" - show (LS.RSTransfer fr fv tr) = - " (r" ++ show fr ++ " v" ++ show fv ++ ") " ++ - "(r" ++ show tr ++ " v" ++ show fv ++ ")" show (LS.RSSpill fr tv b) = "spill (r" ++ show fr ++ " v" ++ show tv ++ ")" ++ showSplit b show (LS.RSRestore fv tr b) = diff --git a/LinearScan/Allocate.hs b/LinearScan/Allocate.hs --- a/LinearScan/Allocate.hs +++ b/LinearScan/Allocate.hs @@ -517,21 +517,21 @@ go count0 ss = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) (\_ -> Prelude.Right (Morph.Build_SSInfo - (Morph.thisDesc maxReg sd ss) + (Morph.thisDesc maxReg ss) __)) (\cnt -> case handleInterval maxReg sd [] ss of { Prelude.Left err -> Prelude.Left ((,) err (ScanState.packScanState maxReg ScanState.InUse - (Morph.thisDesc maxReg sd ss))); + (Morph.thisDesc maxReg ss))); Prelude.Right p -> case p of { (,) o ss' -> case Morph.strengthenHasLen maxReg sd - (Morph.thisDesc maxReg sd ss') of { + (Morph.thisDesc maxReg ss') of { Prelude.Just _ -> - go cnt (Morph.Build_SSInfo - (Morph.thisDesc maxReg sd ss') __); + go cnt (Morph.Build_SSInfo (Morph.thisDesc maxReg ss') + __); Prelude.Nothing -> Prelude.Right ss'}}}) count0} in go} @@ -550,7 +550,7 @@ __) of { Prelude.Left err -> Prelude.Left err; Prelude.Right ss -> - walkIntervals maxReg (Morph.thisDesc maxReg sd ss) n}}}; + walkIntervals maxReg (Morph.thisDesc maxReg ss) n}}}; Prelude.Nothing -> Prelude.Right (ScanState.packScanState maxReg ScanState.InUse sd)}) positions diff --git a/LinearScan/Assign.hs b/LinearScan/Assign.hs --- a/LinearScan/Assign.hs +++ b/LinearScan/Assign.hs @@ -114,8 +114,6 @@ (case mv of { Resolve.Move sreg svid dreg -> k (Blocks.moveOp maxReg mDict oinfo sreg svid dreg); - Resolve.Transfer p v p0 -> - Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.Spill sreg svid b -> k (Blocks.saveOp maxReg mDict oinfo sreg svid); Resolve.Restore dvid dreg b -> @@ -123,6 +121,10 @@ Resolve.AllocReg v p b -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.FreeReg p v b -> + Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; + Resolve.AssignReg v p -> + Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; + Resolve.ClearReg p v -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; Resolve.AllocStack v -> Applicative.pure (Monad.is_applicative mDict) Prelude.Nothing; diff --git a/LinearScan/Graph.hs b/LinearScan/Graph.hs --- a/LinearScan/Graph.hs +++ b/LinearScan/Graph.hs @@ -39,125 +39,95 @@ #endif data Graph = - Build_Graph ([] Eqtype.Equality__Coq_sort) ([] Eqtype.Equality__Coq_sort) - (Eqtype.Equality__Coq_sort -> (,) Eqtype.Equality__Coq_sort - Eqtype.Equality__Coq_sort) - -vertices :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph - -> [] Eqtype.Equality__Coq_sort -vertices a b g = - case g of { - Build_Graph vertices0 edges0 edge_f0 -> vertices0} + Build_Graph ([] Eqtype.Equality__Coq_sort) ([] + ((,) Eqtype.Equality__Coq_sort + Eqtype.Equality__Coq_sort)) -edges :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph -> - [] Eqtype.Equality__Coq_sort -edges a b g = +vertices :: Eqtype.Equality__Coq_type -> Graph -> [] + Eqtype.Equality__Coq_sort +vertices a g = case g of { - Build_Graph vertices0 edges0 edge_f0 -> edges0} + Build_Graph vertices0 edges0 -> vertices0} -edge_f :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph -> - Eqtype.Equality__Coq_sort -> (,) Eqtype.Equality__Coq_sort - Eqtype.Equality__Coq_sort -edge_f a b g = +edges :: Eqtype.Equality__Coq_type -> Graph -> [] + ((,) Eqtype.Equality__Coq_sort Eqtype.Equality__Coq_sort) +edges a g = case g of { - Build_Graph vertices0 edges0 edge_f0 -> edge_f0} + Build_Graph vertices0 edges0 -> edges0} -emptyGraph :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> - (Eqtype.Equality__Coq_sort -> (,) Eqtype.Equality__Coq_sort - Eqtype.Equality__Coq_sort) -> Graph -emptyGraph a b f = - Build_Graph [] [] f +emptyGraph :: Eqtype.Equality__Coq_type -> Graph +emptyGraph a = + Build_Graph [] [] -addVertex :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> - Eqtype.Equality__Coq_sort -> Graph -> Graph -addVertex a b v g = - let {vg = vertices a b g} in +addVertex :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph + -> Graph +addVertex a v g = + let {vg = vertices a g} in Build_Graph (case Ssrbool.in_mem v (Ssrbool.mem (Seq.seq_predType a) (unsafeCoerce vg)) of { Prelude.True -> vg; - Prelude.False -> (:) v vg}) (edges a b g) (edge_f a b g) - -addEdge :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> - Eqtype.Equality__Coq_sort -> Graph -> Graph -addEdge a b e g = - let { - g' = let {eg = edges a b g} in - Build_Graph (vertices a b g) - (case Ssrbool.in_mem e - (Ssrbool.mem (Seq.seq_predType b) (unsafeCoerce eg)) of { - Prelude.True -> eg; - Prelude.False -> (:) e eg}) (edge_f a b g)} - in - case edge_f a b g' e of { - (,) a0 z -> addVertex a b a0 (addVertex a b z g')} + Prelude.False -> (:) v vg}) (edges a g) -removeEdge :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> - Eqtype.Equality__Coq_sort -> Graph -> Graph -removeEdge a b x g = - Build_Graph (vertices a b g) (Seq.rem b x (edges a b g)) (edge_f a b g) +addEdge :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph -> + Graph +addEdge a e g = + let {eg = edges a g} in + Build_Graph (vertices a g) + (case Ssrbool.in_mem e + (Ssrbool.mem (Seq.seq_predType (Eqtype.prod_eqType a a)) + (unsafeCoerce eg)) of { + Prelude.True -> eg; + Prelude.False -> (:) (unsafeCoerce e) eg}) -connections :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> - (((,) Eqtype.Equality__Coq_sort Eqtype.Equality__Coq_sort) -> - Eqtype.Equality__Coq_sort) -> Eqtype.Equality__Coq_sort -> - Graph -> [] Eqtype.Equality__Coq_sort -connections a b f x g = - Prelude.filter - ((Prelude..) ((Prelude..) (\y -> Eqtype.eq_op a y x) f) (edge_f a b g)) - (edges a b g) +removeEdge :: Eqtype.Equality__Coq_type -> ((,) Eqtype.Equality__Coq_sort + Eqtype.Equality__Coq_sort) -> Graph -> Graph +removeEdge a x g = + Build_Graph (vertices a g) + (unsafeCoerce + (Seq.rem (Eqtype.prod_eqType a a) (unsafeCoerce x) + (unsafeCoerce (edges a g)))) -outbound :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> - Eqtype.Equality__Coq_sort -> Graph -> [] - Eqtype.Equality__Coq_sort -outbound a b = - connections a b Prelude.fst +outbound :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph + -> [] ((,) Eqtype.Equality__Coq_sort Eqtype.Equality__Coq_sort) +outbound a x g = + Prelude.filter (\e -> Eqtype.eq_op a x (Prelude.fst e)) (edges a g) -inbound :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> - Eqtype.Equality__Coq_sort -> Graph -> [] Eqtype.Equality__Coq_sort -inbound a b = - connections a b Prelude.snd +inbound :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> Graph -> + [] ((,) Eqtype.Equality__Coq_sort Eqtype.Equality__Coq_sort) +inbound a x g = + Prelude.filter (\e -> Eqtype.eq_op a x (Prelude.snd e)) (edges a g) -removeVertex :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> - Eqtype.Equality__Coq_sort -> Graph -> Graph -removeVertex a b v g = - Prelude.foldr (removeEdge a b) (Build_Graph (Seq.rem a v (vertices a b g)) - (edges a b g) (edge_f a b g)) (outbound a b v g) +removeVertex :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> + Graph -> Graph +removeVertex a v g = + Prelude.foldr (removeEdge a) (Build_Graph (Seq.rem a v (vertices a g)) + (edges a g)) ((Prelude.++) (inbound a v g) (outbound a v g)) -topsort :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type -> Graph -> - (Eqtype.Equality__Coq_sort -> Prelude.Bool) -> - (Eqtype.Equality__Coq_sort -> [] Eqtype.Equality__Coq_sort) -> (,) - ([] Eqtype.Equality__Coq_sort) - ([] ((,) Prelude.Int Eqtype.Equality__Coq_sort)) -topsort a b g0 splittable split = +topsort :: Eqtype.Equality__Coq_type -> (Eqtype.Equality__Coq_sort -> + Prelude.Bool) -> (Eqtype.Equality__Coq_sort -> Graph -> Graph) -> + Graph -> [] Eqtype.Equality__Coq_sort +topsort a splittable split g0 = let { - go fuel depth g = + go fuel g = (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1)) - (\_ -> (,) (vertices a b g) - (Prelude.map (\i -> (,) depth i) (edges a b g))) + (\_ -> + vertices a g) (\fuel0 -> let { - noInbound = Prelude.filter (\v -> Seq.nilp (inbound a b v g)) - (vertices a b g)} + noInbound = Prelude.filter (\v -> Seq.nilp (inbound a v g)) + (vertices a g)} in case noInbound of { [] -> - case edges a b g of { - [] -> (,) [] []; - (:) e l -> - let { - x = case Prelude.filter (\e0 -> splittable e0) (edges a b g) of { - [] -> e; - (:) e' l0 -> e'}} - in - go fuel0 ((Prelude.succ) depth) - (Prelude.foldr (addEdge a b) (removeEdge a b x g) (split x))}; + case vertices a g of { + [] -> []; + (:) v vs -> + case Prelude.filter (\x -> splittable x) ((:) v vs) of { + [] -> vertices a g; + (:) x l -> go fuel0 (split x g)}}; (:) s l -> - case go fuel0 ((Prelude.succ) depth) - (Prelude.foldr (removeVertex a b) g noInbound) of { - (,) ns' es' -> (,) ((Prelude.++) noInbound ns') - ((Prelude.++) - (Prelude.map (\i -> (,) depth i) - (Seq.flatten (Prelude.map (\n -> outbound a b n g) noInbound))) - es')}}) + (Prelude.++) noInbound + (go fuel0 (Prelude.foldr (removeVertex a) g noInbound))}) fuel} - in go (Ssrnat.double (Data.List.length (vertices a b g0))) 0 g0 + in go (Ssrnat.double (Data.List.length (vertices a g0))) g0 diff --git a/LinearScan/Main.hs b/LinearScan/Main.hs --- a/LinearScan/Main.hs +++ b/LinearScan/Main.hs @@ -96,8 +96,8 @@ let { opCount = (Prelude.succ) (Blocks.countOps dict binfo blocks1)} in - case Allocate.walkIntervals maxReg ( ssig) - (Ssrnat.double opCount) of { + case Allocate.walkIntervals maxReg ( ssig) ((Prelude.succ) + (Ssrnat.double opCount)) of { Prelude.Left p -> case p of { (,) err ssig' -> diff --git a/LinearScan/Morph.hs b/LinearScan/Morph.hs --- a/LinearScan/Morph.hs +++ b/LinearScan/Morph.hs @@ -54,9 +54,8 @@ data SSInfo p = Build_SSInfo ScanState.ScanStateDesc p -thisDesc :: Prelude.Int -> ScanState.ScanStateDesc -> (SSInfo a1) -> - ScanState.ScanStateDesc -thisDesc maxReg startDesc s = +thisDesc :: Prelude.Int -> (SSInfo a1) -> ScanState.ScanStateDesc +thisDesc maxReg s = case s of { Build_SSInfo thisDesc0 thisHolds -> thisDesc0} diff --git a/LinearScan/Resolve.hs b/LinearScan/Resolve.hs --- a/LinearScan/Resolve.hs +++ b/LinearScan/Resolve.hs @@ -24,6 +24,7 @@ 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 @@ -56,40 +57,41 @@ data ResolvingMove = Move PhysReg Blocks.VarId PhysReg - | Transfer PhysReg Blocks.VarId PhysReg | Spill PhysReg Blocks.VarId Prelude.Bool | Restore Blocks.VarId PhysReg Prelude.Bool | AllocReg Blocks.VarId PhysReg Prelude.Bool | FreeReg PhysReg Blocks.VarId Prelude.Bool + | 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 -> PhysReg -> - a1) -> (PhysReg -> Blocks.VarId -> Prelude.Bool -> - a1) -> (Blocks.VarId -> PhysReg -> Prelude.Bool -> - a1) -> (Blocks.VarId -> PhysReg -> Prelude.Bool -> - a1) -> (PhysReg -> Blocks.VarId -> Prelude.Bool -> - 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 r = + -> a1) -> (PhysReg -> Blocks.VarId -> Prelude.Bool + -> a1) -> (Blocks.VarId -> PhysReg -> Prelude.Bool + -> a1) -> (Blocks.VarId -> PhysReg -> Prelude.Bool + -> a1) -> (PhysReg -> Blocks.VarId -> Prelude.Bool + -> 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; - Transfer p v p0 -> f0 p v p0; - Spill p v b -> f1 p v b; - Restore v p b -> f2 v p b; - AllocReg v p b -> f3 v p b; - FreeReg p v b -> f4 p v b; - AllocStack v -> f5 v; - FreeStack v -> f6 v; + Spill p v b -> f0 p v b; + Restore v p b -> f1 v p b; + AllocReg v p b -> f2 v p b; + FreeReg p v b -> f3 p v b; + AssignReg v p -> f4 v p; + ClearReg p v -> f5 p v; + AllocStack v -> f6 v; + FreeStack v -> f7 v; Looped r0 -> - f7 r0 (coq_ResolvingMove_rect maxReg f f0 f1 f2 f3 f4 f5 f6 f7 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 - | RSTransfer 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 Prelude.Bool @@ -104,11 +106,12 @@ weakenResolvingMove maxReg x = case x of { Move fr fv tr -> RSMove ( fr) fv ( tr); - Transfer fr fv tr -> RSTransfer ( fr) fv ( tr); Spill fr tv b -> RSSpill ( fr) tv b; Restore fv tr b -> RSRestore fv ( tr) b; AllocReg fv tr b -> RSAllocReg fv ( tr) b; FreeReg fr tv b -> RSFreeReg ( fr) tv b; + AssignReg fv tr -> RSAssignReg fv ( tr); + ClearReg fr tv -> RSClearReg ( fr) tv; AllocStack tv -> RSAllocStack tv; FreeStack fv -> RSFreeStack fv; Looped x0 -> RSLooped (weakenResolvingMove maxReg x0)} @@ -129,18 +132,6 @@ (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce tr1) (unsafeCoerce tr2))); _ -> Prelude.False}; - Transfer fr1 fv1 tr1 -> - case s2 of { - Transfer 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 -> @@ -189,6 +180,24 @@ (Eqtype.eq_op Eqtype.bool_eqType (unsafeCoerce b1) (unsafeCoerce b2))); _ -> 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 -> @@ -283,30 +292,32 @@ Ssrbool.ReflectT -> _evar_0_ __; Ssrbool.ReflectF -> _evar_0_0 __}} in - let {_evar_0_0 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in - let {_evar_0_1 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in - let {_evar_0_2 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in - let {_evar_0_3 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in - let {_evar_0_4 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in - let {_evar_0_5 = \tv2 -> Ssrbool.ReflectF} in - let {_evar_0_6 = \fv2 -> Ssrbool.ReflectF} in - let {_evar_0_7 = \y -> Ssrbool.ReflectF} 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 b2 -> Ssrbool.ReflectF} in + let {_evar_0_3 = \fr2 tv2 b2 -> 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; - Transfer x x0 x1 -> _evar_0_0 x x0 x1; - Spill x x0 x1 -> _evar_0_1 x x0 x1; - Restore x x0 x1 -> _evar_0_2 x x0 x1; - AllocReg x x0 x1 -> _evar_0_3 x x0 x1; - FreeReg x x0 x1 -> _evar_0_4 x x0 x1; - AllocStack x -> _evar_0_5 x; - FreeStack x -> _evar_0_6 x; - Looped x -> _evar_0_7 x}} + Spill x x0 x1 -> _evar_0_0 x x0 x1; + Restore x x0 x1 -> _evar_0_1 x x0 x1; + AllocReg x x0 x1 -> _evar_0_2 x x0 x1; + FreeReg x x0 x1 -> _evar_0_3 x x0 x1; + 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 tr1 _top_assumption_0 -> + _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 tr2 -> + _evar_0_1 = \fr2 fv2 b2 -> let { _evar_0_1 = \_ -> let { @@ -320,9 +331,7 @@ in let {_evar_0_2 = \_ -> Ssrbool.ReflectF} in - case Eqtype.eqP - (Fintype.ordinal_eqType maxReg) - tr1 tr2 of { + case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { Ssrbool.ReflectT -> _evar_0_1 __; Ssrbool.ReflectF -> _evar_0_2 __}} in @@ -335,8 +344,7 @@ let {_evar_0_2 = Ssrbool.ReflectF} in _evar_0_2} in let {_evar_0_3 = \_ -> Ssrbool.ReflectF} in - case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 - tr2 of { + case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { Ssrbool.ReflectT -> _evar_0_2 __; Ssrbool.ReflectF -> _evar_0_3 __}} in @@ -356,8 +364,7 @@ let {_evar_0_2 = Ssrbool.ReflectF} in _evar_0_2} in let {_evar_0_3 = \_ -> Ssrbool.ReflectF} in - case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 - tr2 of { + case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { Ssrbool.ReflectT -> _evar_0_2 __; Ssrbool.ReflectF -> _evar_0_3 __}} in @@ -370,7 +377,7 @@ let {_evar_0_3 = Ssrbool.ReflectF} in _evar_0_3} in let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in - case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { + case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { Ssrbool.ReflectT -> _evar_0_3 __; Ssrbool.ReflectF -> _evar_0_4 __}} in @@ -382,30 +389,32 @@ Ssrbool.ReflectT -> _evar_0_1 __; Ssrbool.ReflectF -> _evar_0_2 __}} in - let {_evar_0_2 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in - let {_evar_0_3 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in - let {_evar_0_4 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in - let {_evar_0_5 = \fr2 tv2 b2 -> 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 + let {_evar_0_2 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in + let {_evar_0_3 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in + let {_evar_0_4 = \fr2 tv2 b2 -> 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; - Transfer x x0 x1 -> unsafeCoerce _evar_0_1 x x0 x1; - Spill x x0 x1 -> _evar_0_2 x x0 x1; - Restore x x0 x1 -> _evar_0_3 x x0 x1; - AllocReg x x0 x1 -> _evar_0_4 x x0 x1; - FreeReg x x0 x1 -> _evar_0_5 x x0 x1; - AllocStack x -> _evar_0_6 x; - FreeStack x -> _evar_0_7 x; - Looped x -> _evar_0_8 x}} + Spill x x0 x1 -> unsafeCoerce _evar_0_1 x x0 x1; + Restore x x0 x1 -> _evar_0_2 x x0 x1; + AllocReg x x0 x1 -> _evar_0_3 x x0 x1; + FreeReg x x0 x1 -> _evar_0_4 x x0 x1; + 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 = \fr1 fv1 b1 _top_assumption_0 -> + _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 tr2 -> Ssrbool.ReflectF} in + let {_evar_0_2 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in let { - _evar_0_3 = \fr2 fv2 b2 -> + _evar_0_3 = \tv2 tr2 b2 -> let { _evar_0_3 = \_ -> let { @@ -436,7 +445,7 @@ Ssrbool.ReflectT -> _evar_0_4 __; Ssrbool.ReflectF -> _evar_0_5 __}} in - case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { + case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_3 __; Ssrbool.ReflectF -> _evar_0_4 __}} in @@ -469,38 +478,40 @@ Ssrbool.ReflectT -> _evar_0_5 __; Ssrbool.ReflectF -> _evar_0_6 __}} in - case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { + case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { Ssrbool.ReflectT -> _evar_0_4 __; Ssrbool.ReflectF -> _evar_0_5 __}} in - case Eqtype.eqP (Fintype.ordinal_eqType maxReg) fr1 fr2 of { + case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_3 __; Ssrbool.ReflectF -> _evar_0_4 __}} in - let {_evar_0_4 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in - let {_evar_0_5 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in - let {_evar_0_6 = \fr2 tv2 b2 -> 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 + let {_evar_0_4 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in + let {_evar_0_5 = \fr2 tv2 b2 -> 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; - Transfer x x0 x1 -> _evar_0_2 x x0 x1; - Spill x x0 x1 -> unsafeCoerce _evar_0_3 x x0 x1; - Restore x x0 x1 -> _evar_0_4 x x0 x1; - AllocReg x x0 x1 -> _evar_0_5 x x0 x1; - FreeReg x x0 x1 -> _evar_0_6 x x0 x1; - AllocStack x -> _evar_0_7 x; - FreeStack x -> _evar_0_8 x; - Looped x -> _evar_0_9 x}} + Spill x x0 x1 -> _evar_0_2 x x0 x1; + Restore x x0 x1 -> unsafeCoerce _evar_0_3 x x0 x1; + AllocReg x x0 x1 -> _evar_0_4 x x0 x1; + FreeReg x x0 x1 -> _evar_0_5 x x0 x1; + 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 = \tv1 tr1 b1 _top_assumption_0 -> + _evar_0_2 = \fv1 tr1 b1 _top_assumption_0 -> let {_evar_0_2 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in - let {_evar_0_3 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in - let {_evar_0_4 = \fr2 fv2 b2 -> 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 = \tv2 tr2 b2 -> + _evar_0_5 = \fv2 tr2 b2 -> let { _evar_0_5 = \_ -> let { @@ -568,34 +579,36 @@ Ssrbool.ReflectT -> _evar_0_6 __; Ssrbool.ReflectF -> _evar_0_7 __}} in - case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { + case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { Ssrbool.ReflectT -> _evar_0_5 __; Ssrbool.ReflectF -> _evar_0_6 __}} in - let {_evar_0_6 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in - let {_evar_0_7 = \fr2 tv2 b2 -> 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 + let {_evar_0_6 = \fr2 tv2 b2 -> 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; - Transfer x x0 x1 -> _evar_0_3 x x0 x1; - Spill x x0 x1 -> _evar_0_4 x x0 x1; - Restore x x0 x1 -> unsafeCoerce _evar_0_5 x x0 x1; - AllocReg x x0 x1 -> _evar_0_6 x x0 x1; - FreeReg x x0 x1 -> _evar_0_7 x x0 x1; - AllocStack x -> _evar_0_8 x; - FreeStack x -> _evar_0_9 x; - Looped x -> _evar_0_10 x}} + Spill x x0 x1 -> _evar_0_3 x x0 x1; + Restore x x0 x1 -> _evar_0_4 x x0 x1; + AllocReg x x0 x1 -> unsafeCoerce _evar_0_5 x x0 x1; + FreeReg x x0 x1 -> _evar_0_6 x x0 x1; + 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 = \fv1 tr1 b1 _top_assumption_0 -> + _evar_0_3 = \fr1 tv1 b1 _top_assumption_0 -> let {_evar_0_3 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in - 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_4 = \fr2 fv2 b2 -> Ssrbool.ReflectF} in + let {_evar_0_5 = \tv2 tr2 b2 -> Ssrbool.ReflectF} in + let {_evar_0_6 = \fv2 tr2 b2 -> Ssrbool.ReflectF} in let { - _evar_0_7 = \fv2 tr2 b2 -> + _evar_0_7 = \fr2 tv2 b2 -> let { _evar_0_7 = \_ -> let { @@ -626,7 +639,7 @@ Ssrbool.ReflectT -> _evar_0_8 __; Ssrbool.ReflectF -> _evar_0_9 __}} in - case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { + case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_7 __; Ssrbool.ReflectF -> _evar_0_8 __}} in @@ -659,69 +672,49 @@ Ssrbool.ReflectT -> _evar_0_9 __; Ssrbool.ReflectF -> _evar_0_10 __}} in - case Eqtype.eqP (Fintype.ordinal_eqType maxReg) tr1 tr2 of { + case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { Ssrbool.ReflectT -> _evar_0_8 __; Ssrbool.ReflectF -> _evar_0_9 __}} in - case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { + 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 b2 -> 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 + 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; - Transfer 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 x1 -> unsafeCoerce _evar_0_7 x x0 x1; - FreeReg x x0 x1 -> _evar_0_8 x x0 x1; - AllocStack x -> _evar_0_9 x; - FreeStack x -> _evar_0_10 x; - Looped x -> _evar_0_11 x}} + Spill x x0 x1 -> _evar_0_4 x x0 x1; + Restore x x0 x1 -> _evar_0_5 x x0 x1; + AllocReg x x0 x1 -> _evar_0_6 x x0 x1; + FreeReg x x0 x1 -> unsafeCoerce _evar_0_7 x x0 x1; + 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 b1 _top_assumption_0 -> + _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 -> 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 b2 -> 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 b2 -> Ssrbool.ReflectF} in + let {_evar_0_8 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in let { - _evar_0_9 = \fr2 tv2 b2 -> + _evar_0_9 = \fr2 tv2 -> let { _evar_0_9 = \_ -> let { _evar_0_9 = 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 Eqtype.bool_eqType b1 b2 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 Eqtype.bool_eqType b1 b2 of { - Ssrbool.ReflectT -> _evar_0_10 __; - Ssrbool.ReflectF -> _evar_0_11 __}} + let {_evar_0_9 = Ssrbool.ReflectT} in _evar_0_9} in - case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { + 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 @@ -731,148 +724,191 @@ _evar_0_10 = \_ -> let { _evar_0_10 = \_ -> - 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 Eqtype.bool_eqType b1 b2 of { - Ssrbool.ReflectT -> _evar_0_10 __; - Ssrbool.ReflectF -> _evar_0_11 __}} - in - _evar_0_10} - in - let { - _evar_0_11 = \_ -> - let { - _evar_0_11 = \_ -> - let {_evar_0_11 = Ssrbool.ReflectF} in _evar_0_11} - in - let {_evar_0_12 = \_ -> Ssrbool.ReflectF} in - case Eqtype.eqP Eqtype.bool_eqType b1 b2 of { - Ssrbool.ReflectT -> _evar_0_11 __; - Ssrbool.ReflectF -> _evar_0_12 __}} + let {_evar_0_10 = Ssrbool.ReflectF} in _evar_0_10} in - case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { + 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 (Fintype.ordinal_eqType maxReg) fr1 fr2 of { + case Eqtype.eqP Ssrnat.nat_eqType fr1 fr2 of { Ssrbool.ReflectT -> _evar_0_9 __; Ssrbool.ReflectF -> _evar_0_10 __}} 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 + 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; - Transfer x x0 x1 -> _evar_0_5 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 x1 -> _evar_0_7 x x0 x1; + FreeReg x x0 x1 -> _evar_0_8 x x0 x1; + 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 b2 -> Ssrbool.ReflectF} in + let {_evar_0_9 = \fr2 tv2 b2 -> 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 x1 -> _evar_0_8 x x0 x1; - FreeReg x x0 x1 -> unsafeCoerce _evar_0_9 x x0 x1; - AllocStack x -> _evar_0_10 x; - FreeStack x -> _evar_0_11 x; - Looped x -> _evar_0_12 x}} + FreeReg x x0 x1 -> _evar_0_9 x x0 x1; + 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_5 = \tv1 _top_assumption_0 -> - let {_evar_0_5 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in + _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 b2 -> Ssrbool.ReflectF} in let {_evar_0_10 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in + let {_evar_0_11 = \fr2 tv2 -> Ssrbool.ReflectF} in + let {_evar_0_12 = \fr2 tv2 -> Ssrbool.ReflectF} in let { - _evar_0_11 = \tv2 -> + _evar_0_13 = \tv2 -> let { - _evar_0_11 = \_ -> let {_evar_0_11 = Ssrbool.ReflectT} in _evar_0_11} + _evar_0_13 = \_ -> let {_evar_0_13 = Ssrbool.ReflectT} in _evar_0_13} in - let {_evar_0_12 = \_ -> Ssrbool.ReflectF} in + let {_evar_0_14 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Ssrnat.nat_eqType tv1 tv2 of { - Ssrbool.ReflectT -> _evar_0_11 __; - Ssrbool.ReflectF -> _evar_0_12 __}} + Ssrbool.ReflectT -> _evar_0_13 __; + Ssrbool.ReflectF -> _evar_0_14 __}} in - let {_evar_0_12 = \fv2 -> Ssrbool.ReflectF} in - let {_evar_0_13 = \y -> Ssrbool.ReflectF} 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_5 x x0 x1; - Transfer x x0 x1 -> _evar_0_6 x x0 x1; + 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 x1 -> _evar_0_9 x x0 x1; FreeReg x x0 x1 -> _evar_0_10 x x0 x1; - AllocStack x -> unsafeCoerce _evar_0_11 x; - FreeStack x -> _evar_0_12 x; - Looped x -> _evar_0_13 x}} + 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_6 = \fv1 _top_assumption_0 -> - let {_evar_0_6 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in + _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 b2 -> Ssrbool.ReflectF} in let {_evar_0_11 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in - let {_evar_0_12 = \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_13 = \fv2 -> + _evar_0_15 = \fv2 -> let { - _evar_0_13 = \_ -> let {_evar_0_13 = Ssrbool.ReflectT} in _evar_0_13} + _evar_0_15 = \_ -> let {_evar_0_15 = Ssrbool.ReflectT} in _evar_0_15} in - let {_evar_0_14 = \_ -> Ssrbool.ReflectF} in + let {_evar_0_16 = \_ -> Ssrbool.ReflectF} in case Eqtype.eqP Ssrnat.nat_eqType fv1 fv2 of { - Ssrbool.ReflectT -> _evar_0_13 __; - Ssrbool.ReflectF -> _evar_0_14 __}} + Ssrbool.ReflectT -> _evar_0_15 __; + Ssrbool.ReflectF -> _evar_0_16 __}} in - let {_evar_0_14 = \y -> Ssrbool.ReflectF} in + let {_evar_0_16 = \y -> Ssrbool.ReflectF} in case _top_assumption_0 of { - Move x x0 x1 -> _evar_0_6 x x0 x1; - Transfer x x0 x1 -> _evar_0_7 x x0 x1; + 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 x1 -> _evar_0_10 x x0 x1; FreeReg x x0 x1 -> _evar_0_11 x x0 x1; - AllocStack x -> _evar_0_12 x; - FreeStack x -> unsafeCoerce _evar_0_13 x; - Looped x -> _evar_0_14 x}} + 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_7 = \x iHx _top_assumption_0 -> - let {_evar_0_7 = \fr2 fv2 tr2 -> Ssrbool.ReflectF} in + _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 b2 -> Ssrbool.ReflectF} in let {_evar_0_12 = \fr2 tv2 b2 -> Ssrbool.ReflectF} in - let {_evar_0_13 = \tv2 -> Ssrbool.ReflectF} in - let {_evar_0_14 = \fv2 -> 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_15 = \y -> + _evar_0_17 = \y -> let {iHx0 = iHx y} in - let {_evar_0_15 = \_ -> Ssrbool.ReflectT} in - let {_evar_0_16 = \_ -> Ssrbool.ReflectF} in + let {_evar_0_17 = \_ -> Ssrbool.ReflectT} in + let {_evar_0_18 = \_ -> Ssrbool.ReflectF} in case iHx0 of { - Ssrbool.ReflectT -> _evar_0_15 __; - Ssrbool.ReflectF -> _evar_0_16 __}} + Ssrbool.ReflectT -> _evar_0_17 __; + Ssrbool.ReflectF -> _evar_0_18 __}} in case _top_assumption_0 of { - Move x0 x1 x2 -> _evar_0_7 x0 x1 x2; - Transfer x0 x1 x2 -> _evar_0_8 x0 x1 x2; + 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 x2 -> _evar_0_11 x0 x1 x2; FreeReg x0 x1 x2 -> _evar_0_12 x0 x1 x2; - AllocStack x0 -> _evar_0_13 x0; - FreeStack x0 -> _evar_0_14 x0; - Looped x0 -> _evar_0_15 x0}} + 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) _evar_0_7 _top_assumption_ + (unsafeCoerce _evar_0_6) (unsafeCoerce _evar_0_7) _evar_0_8 + _top_assumption_ coq_ResolvingMove_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of ResolvingMove @@ -883,142 +919,155 @@ coq_ResolvingMove_eqType maxReg = unsafeCoerce (coq_ResolvingMove_eqMixin maxReg) -data ResGraphNode = - RegNode PhysReg - | VarNode Blocks.VarId - | VirtNode ResGraphNode - -coq_ResGraphNode_rect :: Prelude.Int -> (PhysReg -> a1) -> (Blocks.VarId -> - a1) -> (ResGraphNode -> a1 -> a1) -> ResGraphNode -> - a1 -coq_ResGraphNode_rect maxReg f f0 f1 r = - case r of { - RegNode p -> f p; - VarNode v -> f0 v; - VirtNode r0 -> f1 r0 (coq_ResGraphNode_rect maxReg f f0 f1 r0)} - -eqResGraphNode :: Prelude.Int -> ResGraphNode -> ResGraphNode -> Prelude.Bool -eqResGraphNode maxReg s1 s2 = - case s1 of { - RegNode r1 -> - case s2 of { - RegNode r2 -> - Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce r1) - (unsafeCoerce r2); +addResolvingEdge :: Prelude.Int -> ResolvingMove -> ResolvingMove -> + Prelude.Bool +addResolvingEdge 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 b -> + (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}; - VarNode v1 -> - case s2 of { - VarNode v2 -> - Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce v1) (unsafeCoerce v2); + 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 b0 -> + Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) + (unsafeCoerce tr2); + FreeReg fr2 tv2 b0 -> + (Prelude.&&) + (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce fv1) + (unsafeCoerce tv2)) + (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) + (unsafeCoerce fr2)); _ -> Prelude.False}; - VirtNode n1 -> - case s2 of { - VirtNode n2 -> eqResGraphNode maxReg n1 n2; - _ -> 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 b -> + 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 b0 -> + (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 b0 -> + (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 b -> + case y of { + Restore v0 tr2 b0 -> + Eqtype.eq_op (Fintype.ordinal_eqType maxReg) (unsafeCoerce fr1) + (unsafeCoerce tr2); + AllocReg v0 tr2 b0 -> + 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} -eqResGraphNodeP :: Prelude.Int -> Eqtype.Equality__Coq_axiom ResGraphNode -eqResGraphNodeP maxReg _top_assumption_ = - let { - _evar_0_ = \r1 _top_assumption_0 -> - let { - _evar_0_ = \r2 -> - 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) r1 r2 of { - Ssrbool.ReflectT -> _evar_0_ __; - Ssrbool.ReflectF -> _evar_0_0 __}} - in - let {_evar_0_0 = \v2 -> Ssrbool.ReflectF} in - let {_evar_0_1 = \n2 -> Ssrbool.ReflectF} in - case _top_assumption_0 of { - RegNode x -> unsafeCoerce _evar_0_ x; - VarNode x -> _evar_0_0 x; - VirtNode x -> _evar_0_1 x}} - in - let { - _evar_0_0 = \v1 _top_assumption_0 -> - let {_evar_0_0 = \r2 -> Ssrbool.ReflectF} in - let { - _evar_0_1 = \v2 -> - 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 v1 v2 of { - Ssrbool.ReflectT -> _evar_0_1 __; - Ssrbool.ReflectF -> _evar_0_2 __}} - in - let {_evar_0_2 = \n2 -> Ssrbool.ReflectF} in - case _top_assumption_0 of { - RegNode x -> _evar_0_0 x; - VarNode x -> unsafeCoerce _evar_0_1 x; - VirtNode x -> _evar_0_2 x}} - in +addResolution :: Prelude.Int -> ResolvingMove -> Graph.Graph -> Graph.Graph +addResolution maxReg x g = let { - _evar_0_1 = \n1 iHn _top_assumption_0 -> - let {_evar_0_1 = \r2 -> Ssrbool.ReflectF} in - let {_evar_0_2 = \v2 -> Ssrbool.ReflectF} in - let { - _evar_0_3 = \n2 -> - let {iHn0 = iHn n2} in - let {_evar_0_3 = \_ -> Ssrbool.ReflectT} in - let {_evar_0_4 = \_ -> Ssrbool.ReflectF} in - case iHn0 of { - Ssrbool.ReflectT -> _evar_0_3 __; - Ssrbool.ReflectF -> _evar_0_4 __}} - in - case _top_assumption_0 of { - RegNode x -> _evar_0_1 x; - VarNode x -> _evar_0_2 x; - VirtNode x -> _evar_0_3 x}} + f = \x0 y z -> + case addResolvingEdge maxReg x0 y of { + Prelude.True -> + Graph.addEdge (coq_ResolvingMove_eqType maxReg) + (unsafeCoerce ((,) x0 y)) z; + Prelude.False -> z}} in - coq_ResGraphNode_rect maxReg (unsafeCoerce _evar_0_) - (unsafeCoerce _evar_0_0) _evar_0_1 _top_assumption_ - -coq_ResGraphNode_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of - ResGraphNode -coq_ResGraphNode_eqMixin maxReg = - Eqtype.Equality__Mixin (eqResGraphNode maxReg) (eqResGraphNodeP maxReg) - -coq_ResGraphNode_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type -coq_ResGraphNode_eqType maxReg = - unsafeCoerce (coq_ResGraphNode_eqMixin maxReg) + 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) -determineNodes :: Prelude.Int -> ResolvingMove -> (,) ResGraphNode - ResGraphNode -determineNodes maxReg x = - case x of { - Move fr fv tr -> (,) (RegNode tr) (RegNode fr); - Transfer fr fv tr -> (,) (RegNode tr) (RegNode fr); - Spill fr tv b -> (,) (VirtNode (VarNode tv)) (RegNode fr); - Restore fv tr b -> (,) (RegNode tr) (VarNode fv); - AllocReg fv tr b -> (,) (RegNode tr) (VarNode fv); - FreeReg fr tv b -> (,) (VirtNode (VarNode tv)) (RegNode fr); - AllocStack tv -> (,) (VarNode tv) (VirtNode (VarNode tv)); - FreeStack fv -> (,) (VirtNode (VarNode fv)) (VarNode fv); - Looped x0 -> determineNodes maxReg x0} +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; - Transfer p v p0 -> Prelude.True; _ -> Prelude.False} -splitMove :: Prelude.Int -> ResolvingMove -> [] ResolvingMove -splitMove maxReg x = +splitMove :: Prelude.Int -> ResolvingMove -> Graph.Graph -> Graph.Graph +splitMove maxReg x g = case x of { - Move fr fv tr -> (:) (Spill fr fv Prelude.True) ((:) (Restore fv tr - Prelude.True) []); - Transfer fr fv tr -> (:) (FreeReg fr fv Prelude.True) ((:) (AllocReg fv tr - Prelude.True) []); - Looped r -> (:) x []; - _ -> (:) (Looped x) []} + 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 + IntMap.IntMap ([] ResolvingMove) resolvingMoves maxReg allocs liveIn from to = let { allocsAt = \pos -> @@ -1052,27 +1101,36 @@ Prelude.Just yr -> Prelude.Just (case (Prelude.||) (varNotLive vid) (Prelude.not (Ssrnat.odd to)) of { - Prelude.True -> Transfer xr vid yr; - Prelude.False -> Move xr vid yr}); - Prelude.Nothing -> Prelude.Just (Spill xr vid Prelude.False)}; + Prelude.True -> (:) (FreeReg xr vid Prelude.True) ((:) + (AllocReg vid yr Prelude.True) []); + Prelude.False -> (:) (FreeReg xr vid Prelude.False) ((:) + (AllocReg vid yr Prelude.False) ((:) (Move xr vid yr) ((:) + (AssignReg vid yr) [])))}); + Prelude.Nothing -> Prelude.Just ((:) (FreeReg xr vid + Prelude.False) ((:) (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; - Prelude.False -> Restore vid yr Prelude.False}); + Prelude.True -> (:) (AllocReg vid yr Prelude.False) []; + Prelude.False -> (:) (AllocReg vid yr Prelude.False) ((:) + (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.False); - Prelude.Nothing -> Prelude.Just (FreeStack vid)}}; + Prelude.Just r -> Prelude.Just ((:) (FreeReg r vid Prelude.False) + []); + 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.False); - Prelude.Nothing -> Prelude.Just (AllocStack vid)}; + Prelude.Just r -> Prelude.Just ((:) (AllocReg vid r Prelude.False) + []); + Prelude.Nothing -> Prelude.Just ((:) (AllocStack vid) [])}; Prelude.Nothing -> Prelude.Nothing}}) (allocsAt from) (allocsAt to) determineMoves :: Prelude.Int -> ([] Allocate.Allocation) -> (Prelude.Maybe @@ -1080,22 +1138,13 @@ ResolvingMove determineMoves maxReg allocs liveIn from to = let { - sortMoves = \x -> - Prelude.map (\i -> Prelude.snd i) - (Prelude.snd - (Graph.topsort (coq_ResGraphNode_eqType maxReg) - (coq_ResolvingMove_eqType maxReg) x - (unsafeCoerce (isMoveSplittable maxReg)) - (unsafeCoerce (splitMove maxReg))))} + sortMoves = Graph.topsort (coq_ResolvingMove_eqType maxReg) + (unsafeCoerce (isMoveSplittable maxReg)) + (unsafeCoerce (splitMove maxReg))} in unsafeCoerce sortMoves - (IntMap.coq_IntMap_foldr - (unsafeCoerce - (Graph.addEdge (coq_ResGraphNode_eqType maxReg) - (coq_ResolvingMove_eqType maxReg))) - (Graph.emptyGraph (coq_ResGraphNode_eqType maxReg) - (coq_ResolvingMove_eqType maxReg) - (unsafeCoerce (determineNodes maxReg))) + (IntMap.coq_IntMap_foldr (Prelude0.flip (addResolutions maxReg)) + (Graph.emptyGraph (coq_ResolvingMove_eqType maxReg)) (resolvingMoves maxReg allocs liveIn from to)) type BlockMoves = (,) ([] ResolvingMove) ([] ResolvingMove) diff --git a/LinearScan/Seq.hs b/LinearScan/Seq.hs --- a/LinearScan/Seq.hs +++ b/LinearScan/Seq.hs @@ -241,7 +241,3 @@ (iota ((Prelude.succ) m) n')) n -flatten :: ([] ([] a1)) -> [] a1 -flatten = - Prelude.foldr (Prelude.++) [] - diff --git a/LinearScan/Verify.hs b/LinearScan/Verify.hs --- a/LinearScan/Verify.hs +++ b/LinearScan/Verify.hs @@ -494,6 +494,27 @@ (isResident maxReg mDict reg)) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) +isStackAllocated :: Prelude.Int -> (Monad.Monad a1) -> Blocks.VarId -> + Verified a1 a2 Prelude.Bool +isStackAllocated maxReg mDict var = + Monad.bind (State0.coq_StateT_Monad mDict) (\st -> + Applicative.pure (State0.coq_StateT_Applicative mDict) + (IntSet.coq_IntSet_member var (rsStack maxReg st))) + (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) + +checkStack :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier + -> Blocks.VarId -> Verified a1 a2 () +checkStack maxReg mDict pc useVerifier var = + Monad.bind (State0.coq_StateT_Monad mDict) (\st -> + Monad.bind (State0.coq_StateT_Monad mDict) (\res -> + let {err = errorT maxReg mDict pc (StackNotAllocatedForVar var)} in + case useVerifier of { + VerifyEnabledStrict -> + Monad.unless (State0.coq_StateT_Monad mDict) res err; + _ -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}) + (isStackAllocated maxReg mDict var)) + (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict) + allocStack :: Prelude.Int -> (Monad.Monad a1) -> Blocks.OpId -> UseVerifier -> Blocks.VarId -> Verified a1 a2 () allocStack maxReg mDict pc useVerifier var = @@ -744,71 +765,42 @@ Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> - Monad.bind (State0.coq_StateT_Monad mDict) (\check -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x2 -> - Applicative.pure (State0.coq_StateT_Applicative mDict) - (Seq.rcons acc mv)) - (case useVerifier of { - VerifyEnabledStrict -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x2 -> - assignReg maxReg mDict pc useVerifier toReg fromVar) - (Monad.when (State0.coq_StateT_Monad mDict) - (Maybe.isJust check) - (checkResidency maxReg mDict pc useVerifier - fromReg fromVar)); - _ -> - assignReg maxReg mDict pc useVerifier toReg fromVar})) - (isResident maxReg mDict fromReg)) + Applicative.pure (State0.coq_StateT_Applicative mDict) + (Seq.rcons acc mv)) (addMove maxReg mDict pc (Resolve.weakenResolvingMove maxReg mv))) - (reserveReg maxReg mDict pc toReg fromVar Prelude.False)) - (Monad.unless (State0.coq_StateT_Monad mDict) - (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) - (unsafeCoerce fromReg) (unsafeCoerce toReg)) - (releaseReg maxReg mDict pc fromReg fromVar Prelude.False)); - Resolve.Transfer fromReg fromVar toReg -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> - Applicative.pure (State0.coq_StateT_Applicative mDict) acc) - (reserveReg maxReg mDict pc toReg fromVar Prelude.False)) - (Monad.unless (State0.coq_StateT_Monad mDict) - (Eqtype.eq_op (Fintype.ordinal_eqType maxReg) - (unsafeCoerce fromReg) (unsafeCoerce toReg)) - (releaseReg maxReg mDict pc fromReg fromVar Prelude.False)); + (checkReservation maxReg mDict pc toReg fromVar)) + (checkResidency maxReg mDict pc useVerifier fromReg fromVar); Resolve.Spill fromReg toSpillSlot fromSplit -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.bind (State0.coq_StateT_Monad mDict) (\check -> - case Maybe.isJust check of { + case Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType) + check (unsafeCoerce (Prelude.Just toSpillSlot)) of { Prelude.True -> Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> - Applicative.pure (State0.coq_StateT_Applicative mDict) - (Seq.rcons acc mv)) - (addMove maxReg mDict pc - (Resolve.weakenResolvingMove maxReg mv))) - (allocStack maxReg mDict pc useVerifier toSpillSlot); + Applicative.pure (State0.coq_StateT_Applicative mDict) + (Seq.rcons acc mv)) + (addMove maxReg mDict pc + (Resolve.weakenResolvingMove maxReg mv)); Prelude.False -> - Applicative.pure (State0.coq_StateT_Applicative mDict) acc}) + let {mv' = Resolve.FreeStack toSpillSlot} in + Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> + Applicative.pure (State0.coq_StateT_Applicative mDict) + (Seq.rcons acc mv')) + (addMove maxReg mDict pc + (Resolve.weakenResolvingMove maxReg mv'))}) (isResident maxReg mDict fromReg)) - (releaseReg maxReg mDict pc fromReg toSpillSlot fromSplit); + (checkStack maxReg mDict pc useVerifier toSpillSlot); Resolve.Restore fromSpillSlot toReg fromSplit -> - Monad.bind (State0.coq_StateT_Monad mDict) (\check -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x2 -> - Applicative.pure (State0.coq_StateT_Applicative mDict) - (Seq.rcons acc mv)) - (assignReg maxReg mDict pc useVerifier toReg - fromSpillSlot)) - (freeStack maxReg mDict pc useVerifier fromSpillSlot)) + Monad.bind (State0.coq_StateT_Monad mDict) (\x -> + Monad.bind (State0.coq_StateT_Monad mDict) (\x0 -> + Monad.bind (State0.coq_StateT_Monad mDict) (\x1 -> + Applicative.pure (State0.coq_StateT_Applicative mDict) + (Seq.rcons acc mv)) (addMove maxReg mDict pc (Resolve.weakenResolvingMove maxReg mv))) - (Monad.unless (State0.coq_StateT_Monad mDict) - (Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType) check - (unsafeCoerce (Prelude.Just fromSpillSlot))) - (reserveReg maxReg mDict pc toReg fromSpillSlot fromSplit))) - (isReserved maxReg mDict toReg); + (checkReservation maxReg mDict pc toReg fromSpillSlot)) + (checkStack maxReg mDict pc useVerifier fromSpillSlot); Resolve.AllocReg toVar toReg fromSplit -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc) @@ -817,6 +809,14 @@ Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc) (releaseReg maxReg mDict pc fromReg fromVar fromSplit); + Resolve.AssignReg fromVar toReg -> + Monad.bind (State0.coq_StateT_Monad mDict) (\x -> + Applicative.pure (State0.coq_StateT_Applicative mDict) acc) + (assignReg maxReg mDict pc useVerifier toReg fromVar); + Resolve.ClearReg fromReg toVar -> + Monad.bind (State0.coq_StateT_Monad mDict) (\x -> + Applicative.pure (State0.coq_StateT_Applicative mDict) acc) + (clearReg maxReg mDict pc useVerifier fromReg toVar); Resolve.AllocStack toVar -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Applicative.pure (State0.coq_StateT_Applicative mDict) acc) @@ -857,113 +857,69 @@ (checkAllocation maxReg mDict pc intervals (Prelude.Just (Prelude.Just fromReg)) fromVar from ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0))))); - Resolve.Transfer fromReg fromVar toReg -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x -> - checkAllocation maxReg mDict pc intervals (Prelude.Just - (Prelude.Just toReg)) fromVar to ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) 0)))))))) - (checkAllocation maxReg mDict pc intervals (Prelude.Just - (Prelude.Just fromReg)) fromVar from ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) 0))))))); Resolve.Spill fromReg toSpillSlot fromSplit -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> Monad.unless (State0.coq_StateT_Monad mDict) fromSplit (checkAllocation maxReg mDict pc intervals (Prelude.Just Prelude.Nothing) toSpillSlot to ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) 0))))))))))) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0))))))))) (checkAllocation maxReg mDict pc intervals (Prelude.Just (Prelude.Just fromReg)) toSpillSlot from ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0))))))))); + ((Prelude.succ) 0))))))); Resolve.Restore fromSpillSlot toReg fromSplit -> Monad.bind (State0.coq_StateT_Monad mDict) (\x -> checkAllocation maxReg mDict pc intervals (Prelude.Just (Prelude.Just toReg)) fromSpillSlot to ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) 0)))))))))))) + 0)))))))))) (Monad.unless (State0.coq_StateT_Monad mDict) fromSplit (checkAllocation maxReg mDict pc intervals (Prelude.Just Prelude.Nothing) fromSpillSlot from ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0)))))))))))); + ((Prelude.succ) 0)))))))))); Resolve.AllocReg toVar toReg fromSplit -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x -> - checkAllocation maxReg mDict pc intervals (Prelude.Just - (Prelude.Just toReg)) toVar to ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) 0)))))))))))))) - (Monad.unless (State0.coq_StateT_Monad mDict) fromSplit - (let {alloc = allocationFor maxReg intervals toVar from} in - case alloc of { - Prelude.Just o -> - case o of { - Prelude.Just p -> - errorT maxReg mDict pc (AllocationDoesNotMatch toVar - Prelude.Nothing - (alloc) from - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - 0))))))))))))); - Prelude.Nothing -> - Applicative.pure (State0.coq_StateT_Applicative mDict) ()}; - Prelude.Nothing -> - Applicative.pure (State0.coq_StateT_Applicative mDict) ()})); + checkAllocation maxReg mDict pc intervals (Prelude.Just + (Prelude.Just toReg)) toVar to ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + 0)))))))))); Resolve.FreeReg fromReg fromVar fromSplit -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x -> - Monad.unless (State0.coq_StateT_Monad mDict) fromSplit - (checkAllocation maxReg mDict pc intervals Prelude.Nothing - fromVar to ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - 0))))))))))))))))) - (checkAllocation maxReg mDict pc intervals (Prelude.Just - (Prelude.Just fromReg)) fromVar from ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) 0))))))))))))))); + checkAllocation maxReg mDict pc intervals (Prelude.Just + (Prelude.Just fromReg)) fromVar from ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) 0))))))))))); + Resolve.AssignReg fromVar toReg -> + checkAllocation maxReg mDict pc intervals (Prelude.Just + (Prelude.Just toReg)) fromVar to ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) 0)))))))))))); + Resolve.ClearReg fromReg toVar -> + checkAllocation maxReg mDict pc intervals (Prelude.Just + (Prelude.Just fromReg)) toVar from ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + 0))))))))))))); Resolve.AllocStack toVar -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x -> - checkAllocation maxReg mDict pc intervals (Prelude.Just - Prelude.Nothing) toVar to ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - 0)))))))))))))))))) - (checkAllocation maxReg mDict pc intervals Prelude.Nothing toVar - from ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) 0))))))))))))))))); + checkAllocation maxReg mDict pc intervals (Prelude.Just + Prelude.Nothing) toVar to ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + 0)))))))))))))); Resolve.FreeStack fromVar -> - Monad.bind (State0.coq_StateT_Monad mDict) (\x -> - checkAllocation maxReg mDict pc intervals Prelude.Nothing fromVar - to ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - 0)))))))))))))))))))) - (checkAllocation maxReg mDict pc intervals (Prelude.Just - Prelude.Nothing) fromVar from ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) - 0))))))))))))))))))); + checkAllocation maxReg mDict pc intervals (Prelude.Just + Prelude.Nothing) fromVar from ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) ((Prelude.succ) + ((Prelude.succ) 0))))))))))))))); Resolve.Looped x -> Applicative.pure (State0.coq_StateT_Applicative mDict) ()}) (Lens.use (Lens.stepdowng (\_ -> _verDesc maxReg)) mDict))} diff --git a/linearscan.cabal b/linearscan.cabal --- a/linearscan.cabal +++ b/linearscan.cabal @@ -1,5 +1,5 @@ name: linearscan -version: 0.10.1 +version: 0.10.2 synopsis: Linear scan register allocator, formally verified in Coq homepage: http://github.com/jwiegley/linearscan license: BSD3 @@ -43,6 +43,10 @@ takes a list of information about basic blocks to an equivalent list, with annotations indicating allocation choices. +Source-repository head + type: git + location: https://github.com/jwiegley/linearscan + library default-language: Haskell2010 exposed-modules: @@ -105,11 +109,11 @@ LinearScan.Vector0 LinearScan.Verify Hask.Utils - cpp-options: -DMAX_REG=4 -DREG_SIZE=8 - ghc-options: -fno-warn-deprecated-flags + ghc-options: -fno-warn-deprecated-flags other-extensions: Safe - hs-source-dirs: . Hask/haskell - build-depends: base >=4.7 && <5.0 + hs-source-dirs: . Hask/haskell + build-depends: + base >=4.7 && <5.0 , containers , transformers , mtl