linearscan 0.10.1 → 0.10.2
raw patch · 10 files changed
+610/−637 lines, 10 files
Files
- LinearScan.hs +0/−3
- LinearScan/Allocate.hs +6/−6
- LinearScan/Assign.hs +4/−2
- LinearScan/Graph.hs +67/−97
- LinearScan/Main.hs +2/−2
- LinearScan/Morph.hs +2/−3
- LinearScan/Resolve.hs +428/−379
- LinearScan/Seq.hs +0/−4
- LinearScan/Verify.hs +92/−136
- linearscan.cabal +9/−5
LinearScan.hs view
@@ -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) =- "<xfer> (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) =
LinearScan/Allocate.hs view
@@ -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
LinearScan/Assign.hs view
@@ -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;
LinearScan/Graph.hs view
@@ -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
LinearScan/Main.hs view
@@ -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' ->
LinearScan/Morph.hs view
@@ -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}
LinearScan/Resolve.hs view
@@ -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)
LinearScan/Seq.hs view
@@ -241,7 +241,3 @@ (iota ((Prelude.succ) m) n')) n -flatten :: ([] ([] a1)) -> [] a1-flatten =- Prelude.foldr (Prelude.++) []-
LinearScan/Verify.hs view
@@ -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))}
linearscan.cabal view
@@ -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