packages feed

linearscan (empty) → 0.1.0.0

raw patch · 25 files changed

+3682/−0 lines, 25 filesdep +HUnitdep +basedep +containerssetup-changed

Dependencies added: HUnit, base, containers, free, hoopl, hspec, hspec-expectations, linearscan, transformers

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2014, John Wiegley++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of John Wiegley nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ LinearScan.hs view
@@ -0,0 +1,149 @@+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE StandaloneDeriving #-}++{-# OPTIONS_GHC -Wall -Werror -fno-warn-orphans #-}++module LinearScan+    ( -- * Main entry point+      allocate+      -- * Blocks+    , BlockInfo(..)+    , defaultBlockInfo+      -- * Operations+    , OpInfo(..)+    , OpKind(..)+    , defaultOpInfo+      -- * Variables+    , VarInfo(..)+    , VarKind(..)+    , Allocation(..)+    , PhysReg+    , defaultVarInfo+    ) where++import qualified LinearScan.Main as LS+import LinearScan.Main+    ( VarKind(..)+    , Allocation(..)+    , OpKind(..)+    , PhysReg+    )++-- | Each variable has associated allocation details, and a flag to indicate+--   whether it must be loaded into a register at its point of use.  Variables+--   are also distinguished by their kind, which allows for restricting the+--   scope of their lifetime.  For example, output variables are not needed in a+--   basic block until the first point of use, while the lifetime of input+--   variables extends until their final use.+data VarInfo = VarInfo+    { varId       :: Int+    , varKind     :: VarKind+    , varAlloc    :: Allocation+    , regRequired :: Bool+    }+    deriving (Eq, Show)++deriving instance Eq VarKind+deriving instance Show VarKind++defaultVarInfo :: VarInfo+defaultVarInfo = VarInfo+    { varId       = 0+    , varKind     = Temp+    , varAlloc    = Unallocated+    , regRequired = False+    }++toVarInfo :: LS.VarInfo -> VarInfo+toVarInfo (LS.Build_VarInfo a b c d) = VarInfo a b c d++fromVarInfo :: VarInfo -> LS.VarInfo+fromVarInfo (VarInfo a b c d) = LS.Build_VarInfo a b c d++-- | Every operation may reference multiple variables and/or specific physical+--   registers.  If a physical register is referenced, then that register is+--   considered unavailable for allocation over the range of such references.+--+--   Certain operations have special significance as to how basic blocks are+--   organized, and the lifetime of allocations.  Thus, if an operation begins+--   or ends a loop, or represents a method call, it should be indicated using+--   the 'OpKind' field.  Indication of calls is necessary in order to save+--   and restore all registers around a call, but indication of loops is+--   optional, as it's merely avoids reloading of spilled variables inside+--   loop bodies.+data OpInfo = OpInfo+    { opId    :: Int+    , opMeta  :: Int+    , opKind  :: OpKind+    , varRefs :: [VarInfo]+    , regRefs :: [PhysReg]+    }+    deriving (Eq, Show)++deriving instance Eq OpKind+deriving instance Show OpKind++defaultOpInfo :: OpInfo+defaultOpInfo = OpInfo+    { opId    = 0+    , opMeta  = 0+    , opKind  = Normal+    , varRefs = []+    , regRefs = []+    }++toOpInfo :: LS.OpInfo -> OpInfo+toOpInfo (LS.Build_OpInfo a b c d e) = OpInfo a b c (map toVarInfo d) e++fromOpInfo :: OpInfo -> LS.OpInfo+fromOpInfo (OpInfo a b c d e) = LS.Build_OpInfo a b c (map fromVarInfo d) e++-- | From the point of view of this library, a basic block is nothing more+--   than an ordered sequence of operations.+data BlockInfo = BlockInfo+    { blockId  :: Int+    , blockOps :: [OpInfo]+    }+    deriving (Eq, Show)++defaultBlockInfo :: BlockInfo+defaultBlockInfo = BlockInfo+    { blockId  = 0+    , blockOps = []+    }++toBlockInfo :: LS.BlockInfo -> BlockInfo+toBlockInfo (LS.Build_BlockInfo a b) = BlockInfo a (map toOpInfo b)++fromBlockInfo :: BlockInfo -> LS.BlockInfo+fromBlockInfo (BlockInfo a b) = LS.Build_BlockInfo a (map fromOpInfo b)++-- | Transform a list of basic blocks containing variable references, into an+--   equivalent list where each reference is associated with a register+--   allocation.  Artificial save and restore instructions may also be+--   inserted into blocks to indicate spilling and reloading of variables.+--+--   In order to call this function, the caller must transform their own basic+--   block representation into a linear series of 'BlockInfo' structures.+--   Each of these structures may be associated with a unique identifier, to+--   assist with processing allocation info afterward.+--+--   If allocation is found to be impossible -- for example if there are+--   simply not enough registers -- a 'Left' value is returned, with a string+--   describing the error.+allocate :: [BlockInfo] -> Either String [BlockInfo]+allocate [] = Left "No basic blocks were provided"+allocate blocks =+    case LS.linearScan (map fromBlockInfo blocks) of+        Left x -> Left $ case x of+            LS.ECannotSplitSingleton n ->+                "Current interval is a singleton (" ++ show n ++ ")"+            LS.ECannotSplitAssignedSingleton n ->+                "Current interval is an assigned singleton (" ++ show n ++ ")"+            LS.ENoIntervalsToSplit ->+                "There are no intervals to split"+            LS.ERegisterAlreadyAssigned n ->+                "Register is already assigned (" ++ show n ++ ")"+            LS.ERegisterAssignmentsOverlap n ->+                "Register assignments overlap (" ++ show n ++ ")"+        Right z -> Right (map toBlockInfo z)
+ LinearScan/Datatypes.hs view
@@ -0,0 +1,16 @@+module LinearScan.Datatypes where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils+++list_rect :: a2 -> (a1 -> ([] a1) -> a2 -> a2) -> ([] a1) -> a2+list_rect f f0 l =+  case l of {+   [] -> f;+   (:) y l0 -> f0 y l0 (list_rect f f0 l0)}+
+ LinearScan/Eqtype.hs view
@@ -0,0 +1,184 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Eqtype where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Ssrbool as Ssrbool+import qualified LinearScan.Ssrfun as Ssrfun++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++__ :: any+__ = Prelude.error "Logical or arity value used"++type Equality__Coq_axiom t = t -> t -> Ssrbool.Coq_reflect++data Equality__Coq_mixin_of t =+   Equality__Mixin (Ssrbool.Coq_rel t) (Equality__Coq_axiom t)++_Equality__mixin_of_rect :: ((Ssrbool.Coq_rel a1) -> (Equality__Coq_axiom +                            a1) -> a2) -> (Equality__Coq_mixin_of a1) -> a2+_Equality__mixin_of_rect f m =+  case m of {+   Equality__Mixin x x0 -> f x x0}++_Equality__mixin_of_rec :: ((Ssrbool.Coq_rel a1) -> (Equality__Coq_axiom +                           a1) -> a2) -> (Equality__Coq_mixin_of a1) -> a2+_Equality__mixin_of_rec =+  _Equality__mixin_of_rect++_Equality__op :: (Equality__Coq_mixin_of a1) -> Ssrbool.Coq_rel a1+_Equality__op m =+  case m of {+   Equality__Mixin op0 x -> op0}++type Equality__Coq_type =+  Equality__Coq_mixin_of ()+  -- singleton inductive, whose constructor was Pack+  +_Equality__type_rect :: (() -> (Equality__Coq_mixin_of ()) -> () -> a1) ->+                        Equality__Coq_type -> a1+_Equality__type_rect f t =+  f __ t __++_Equality__type_rec :: (() -> (Equality__Coq_mixin_of ()) -> () -> a1) ->+                       Equality__Coq_type -> a1+_Equality__type_rec =+  _Equality__type_rect++type Equality__Coq_sort = ()++_Equality__coq_class :: Equality__Coq_type -> Equality__Coq_mixin_of+                        Equality__Coq_sort+_Equality__coq_class cT =+  cT++_Equality__pack :: (Equality__Coq_mixin_of a1) -> Equality__Coq_type+_Equality__pack c =+  unsafeCoerce c++_Equality__clone :: Equality__Coq_type -> (Equality__Coq_mixin_of a1) ->+                    (Equality__Coq_sort -> a1) -> Equality__Coq_type+_Equality__clone cT c x =+  _Equality__pack c++eq_op :: Equality__Coq_type -> Ssrbool.Coq_rel Equality__Coq_sort+eq_op t =+  _Equality__op (_Equality__coq_class t)++eqP :: Equality__Coq_type -> Equality__Coq_axiom Equality__Coq_sort+eqP t =+  let {_evar_0_ = \op0 a -> a} in+  case t of {+   Equality__Mixin x x0 -> _evar_0_ x x0}++data Coq_subType t =+   SubType (() -> t) (t -> () -> ()) (() -> (t -> () -> ()) -> () -> ())++type Coq_sub_sort t = ()++val :: (Ssrbool.Coq_pred a1) -> (Coq_subType a1) -> (Coq_sub_sort a1) -> a1+val p s =+  case s of {+   SubType val0 sub x -> val0}++inj_eqAxiom :: Equality__Coq_type -> (a1 -> Equality__Coq_sort) ->+               Equality__Coq_axiom a1+inj_eqAxiom eT f x y =+  Ssrbool.iffP (eq_op eT (f x) (f y)) (eqP eT (f x) (f y))++val_eqP :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->+           (Coq_subType Equality__Coq_sort) -> Equality__Coq_axiom+           (Coq_sub_sort Equality__Coq_sort)+val_eqP t p sT =+  inj_eqAxiom t (val p sT)++pair_eq :: Equality__Coq_type -> Equality__Coq_type -> Ssrbool.Coq_simpl_rel+           ((,) Equality__Coq_sort Equality__Coq_sort)+pair_eq t1 t2 =+   (\u v ->+    (Prelude.&&) (eq_op t1 (Prelude.fst u) (Prelude.fst v))+      (eq_op t2 (Prelude.snd u) (Prelude.snd v)))++pair_eqP :: Equality__Coq_type -> Equality__Coq_type -> Equality__Coq_axiom+            ((,) Equality__Coq_sort Equality__Coq_sort)+pair_eqP t1 t2 _top_assumption_ =+  let {+   _evar_0_ = \x1 x2 _top_assumption_0 ->+    let {+     _evar_0_ = \y1 y2 ->+      Ssrbool.iffP ((Prelude.&&) (eq_op t1 x1 y1) (eq_op t2 x2 y2))+        (Ssrbool.andP (eq_op t1 x1 y1) (eq_op t2 x2 y2))}+    in+    case _top_assumption_0 of {+     (,) x x0 -> _evar_0_ x x0}}+  in+  case _top_assumption_ of {+   (,) x x0 -> _evar_0_ x x0}++prod_eqMixin :: Equality__Coq_type -> Equality__Coq_type ->+                Equality__Coq_mixin_of+                ((,) Equality__Coq_sort Equality__Coq_sort)+prod_eqMixin t1 t2 =+  Equality__Mixin (Ssrbool.rel_of_simpl_rel (pair_eq t1 t2)) (pair_eqP t1 t2)++prod_eqType :: Equality__Coq_type -> Equality__Coq_type -> Equality__Coq_type+prod_eqType t1 t2 =+  unsafeCoerce (prod_eqMixin t1 t2)++opt_eq :: Equality__Coq_type -> (Prelude.Maybe Equality__Coq_sort) ->+          (Prelude.Maybe Equality__Coq_sort) -> Prelude.Bool+opt_eq t u v =+  Ssrfun._Option__apply (\x ->+    Ssrfun._Option__apply (eq_op t x) Prelude.False v)+    (Prelude.not (Ssrbool.isSome v)) u++opt_eqP :: Equality__Coq_type -> Equality__Coq_axiom+           (Prelude.Maybe Equality__Coq_sort)+opt_eqP t _top_assumption_ =+  let {+   _evar_0_ = \x _top_assumption_0 ->+    let {_evar_0_ = \y -> Ssrbool.iffP (eq_op t x y) (eqP t x y)} in+    let {_evar_0_0 = Ssrbool.ReflectF} in+    case _top_assumption_0 of {+     Prelude.Just x0 -> _evar_0_ x0;+     Prelude.Nothing -> _evar_0_0}}+  in+  let {+   _evar_0_0 = \_top_assumption_0 ->+    let {_evar_0_0 = \y -> Ssrbool.ReflectF} in+    let {_evar_0_1 = Ssrbool.ReflectT} in+    case _top_assumption_0 of {+     Prelude.Just x -> _evar_0_0 x;+     Prelude.Nothing -> _evar_0_1}}+  in+  case _top_assumption_ of {+   Prelude.Just x -> _evar_0_ x;+   Prelude.Nothing -> _evar_0_0}++option_eqMixin :: Equality__Coq_type -> Equality__Coq_mixin_of+                  (Prelude.Maybe Equality__Coq_sort)+option_eqMixin t =+  Equality__Mixin (opt_eq t) (opt_eqP t)++option_eqType :: Equality__Coq_type -> Equality__Coq_type+option_eqType t =+  unsafeCoerce (option_eqMixin t)+
+ LinearScan/Fintype.hs view
@@ -0,0 +1,49 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Fintype where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Ssrnat as Ssrnat++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++__ :: any+__ = Prelude.error "Logical or arity value used"++ordinal_subType :: Prelude.Int -> Eqtype.Coq_subType Prelude.Int+ordinal_subType n =+  Eqtype.SubType (unsafeCoerce ) (unsafeCoerce (\x _ ->  x)) (\_ k_S u ->+    case unsafeCoerce u of {+      x -> k_S x __})++ordinal_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of Prelude.Int+ordinal_eqMixin n =+  Eqtype.Equality__Mixin (\x y ->+    Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce ( x)) (unsafeCoerce ( y)))+    (unsafeCoerce+      (Eqtype.val_eqP Ssrnat.nat_eqType (\x ->+        (Prelude.<=) ((Prelude.succ) (unsafeCoerce x)) n)+        (unsafeCoerce (ordinal_subType n))))++ordinal_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type+ordinal_eqType n =+  unsafeCoerce (ordinal_eqMixin n)+
+ LinearScan/IApplicative.hs view
@@ -0,0 +1,40 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.IApplicative where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.IEndo as IEndo++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++__ :: any+__ = Prelude.error "Logical or arity value used"++data IApplicative f =+   Build_IApplicative (IEndo.IFunctor f) (() -> () -> () -> f) (() -> () ->+                                                               () -> () -> ()+                                                               -> f -> f ->+                                                               f)++ipure :: (IApplicative a1) -> a3 -> a1+ipure iApplicative x =+  case iApplicative of {+   Build_IApplicative is_ifunctor ipure0 iap -> unsafeCoerce ipure0 __ __ x}+
+ LinearScan/IEndo.hs view
@@ -0,0 +1,35 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.IEndo where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++__ :: any+__ = Prelude.error "Logical or arity value used"++type IFunctor f =+  () -> () -> () -> () -> (() -> ()) -> f -> f+  -- singleton inductive, whose constructor was Build_IFunctor+  +imap :: (IFunctor a1) -> (a4 -> a5) -> a1 -> a1+imap iFunctor x x0 =+  unsafeCoerce iFunctor __ __ __ __ x x0+
+ LinearScan/IMonad.hs view
@@ -0,0 +1,24 @@+module LinearScan.IMonad where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.IApplicative as IApplicative+++__ :: any+__ = Prelude.error "Logical or arity value used"++data IMonad m =+   Build_IMonad (IApplicative.IApplicative m) (() -> () -> () -> () -> m ->+                                              m)++ijoin :: (IMonad a1) -> a1 -> a1+ijoin iMonad x =+  case iMonad of {+   Build_IMonad is_iapplicative ijoin0 -> ijoin0 __ __ __ __ x}+
+ LinearScan/IState.hs view
@@ -0,0 +1,99 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.IState where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.IApplicative as IApplicative+import qualified LinearScan.IEndo as IEndo+import qualified LinearScan.IMonad as IMonad++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++__ :: any+__ = Prelude.error "Logical or arity value used"++type IState errType i o a =+  i -> Prelude.Either errType ((,) a o)+  -- singleton inductive, whose constructor was mkIState+  +runIState :: (IState a1 a2 a3 a4) -> a2 -> Prelude.Either a1 ((,) a4 a3)+runIState x =+  x++coq_IState_IFunctor :: IEndo.IFunctor (IState a1 () () ())+coq_IState_IFunctor _ _ _ _ f x st =+  let {filtered_var = runIState x st} in+  case filtered_var of {+   Prelude.Left err -> Prelude.Left err;+   Prelude.Right p ->+    case p of {+     (,) a st' -> Prelude.Right ((,) (f a) st')}}++ierr :: a1 -> IState a1 a2 a2 ()+ierr err i =+  Prelude.Left err++iget :: IState a1 a2 a2 a2+iget i =+  Prelude.Right ((,) i i)++iput :: a3 -> IState a1 a2 a3 ()+iput x s =+  Prelude.Right ((,) () x)++imodify :: (a2 -> a3) -> IState a1 a2 a3 ()+imodify f i =+  Prelude.Right ((,) () (f i))++coq_IState_IApplicative :: IApplicative.IApplicative (IState a1 () () ())+coq_IState_IApplicative =+  IApplicative.Build_IApplicative coq_IState_IFunctor (\_ _ x st ->+    Prelude.Right ((,) x st)) (\_ _ _ _ _ f x st ->+    let {filtered_var = runIState f st} in+    case filtered_var of {+     Prelude.Left err -> Prelude.Left err;+     Prelude.Right p ->+      case p of {+       (,) f' st' ->+        unsafeCoerce (\f'0 st'0 _ ->+          let {filtered_var0 = runIState x st'0} in+          case filtered_var0 of {+           Prelude.Left err -> Prelude.Left err;+           Prelude.Right p0 ->+            case p0 of {+             (,) x' st'' -> Prelude.Right ((,) (f'0 x') st'')}}) f' st' __}})++coq_IState_IMonad :: IMonad.IMonad (IState a1 () () ())+coq_IState_IMonad =+  IMonad.Build_IMonad coq_IState_IApplicative (\_ _ _ _ x st ->+    let {filtered_var = runIState x st} in+    case filtered_var of {+     Prelude.Left err -> Prelude.Left err;+     Prelude.Right p ->+      case p of {+       (,) y st' ->+        unsafeCoerce (\y0 st'0 _ ->+          let {filtered_var0 = runIState y0 st'0} in+          case filtered_var0 of {+           Prelude.Left err -> Prelude.Left err;+           Prelude.Right p0 ->+            case p0 of {+             (,) a st'' -> Prelude.Right ((,) a st'')}}) y st' __}})+
+ LinearScan/Interval.hs view
@@ -0,0 +1,400 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Interval where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Lib as Lib+import qualified LinearScan.Logic as Logic+import qualified LinearScan.Range as Range+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Ssrnat as Ssrnat++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++__ :: any+__ = Prelude.error "Logical or arity value used"++data IntervalDesc =+   Build_IntervalDesc Prelude.Int Prelude.Int Prelude.Int ([]+                                                          Range.RangeDesc)++ivar :: IntervalDesc -> Prelude.Int+ivar i =+  case i of {+   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> ivar0}++ibeg :: IntervalDesc -> Prelude.Int+ibeg i =+  case i of {+   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> ibeg0}++iend :: IntervalDesc -> Prelude.Int+iend i =+  case i of {+   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> iend0}++rds :: IntervalDesc -> [] Range.RangeDesc+rds i =+  case i of {+   Build_IntervalDesc ivar0 ibeg0 iend0 rds0 -> rds0}++getIntervalDesc :: IntervalDesc -> IntervalDesc+getIntervalDesc d =+  d++packInterval :: IntervalDesc -> IntervalDesc+packInterval d =+  d++intervalStart :: IntervalDesc -> Prelude.Int+intervalStart i =+  ibeg i++intervalEnd :: IntervalDesc -> Prelude.Int+intervalEnd i =+  iend i++intervalCoversPos :: IntervalDesc -> Prelude.Int -> Prelude.Bool+intervalCoversPos d pos =+  (Prelude.&&) ((Prelude.<=) (intervalStart d) pos)+    ((Prelude.<=) ((Prelude.succ) pos) (intervalEnd d))++intervalExtent :: IntervalDesc -> Prelude.Int+intervalExtent d =+  (Prelude.-) (intervalEnd d) (intervalStart d)++coq_Interval_is_singleton :: IntervalDesc -> Prelude.Bool+coq_Interval_is_singleton d =+  (Prelude.&&)+    (Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Prelude.length (rds d)))+      (unsafeCoerce ((Prelude.succ) 0)))+    (Eqtype.eq_op Ssrnat.nat_eqType+      (unsafeCoerce (Prelude.length (Range.ups ( (Prelude.head (rds d))))))+      (unsafeCoerce ((Prelude.succ) 0)))++intervalsIntersect :: IntervalDesc -> IntervalDesc -> Prelude.Bool+intervalsIntersect i j =+  let {f = \x y -> Range.rangesIntersect ( x) ( y)} in+  Data.List.any (\x -> Data.List.any (f x) ( (rds j))) ( (rds i))++intervalIntersectionPoint :: IntervalDesc -> IntervalDesc -> Prelude.Maybe+                             Prelude.Int+intervalIntersectionPoint i j =+  Data.List.foldl' (\acc rd ->+    case acc of {+     Prelude.Just x -> Prelude.Just x;+     Prelude.Nothing ->+      Data.List.foldl' (\acc' rd' ->+        case acc' of {+         Prelude.Just x -> Prelude.Just x;+         Prelude.Nothing -> Range.rangeIntersectionPoint ( rd) ( rd')})+        Prelude.Nothing (rds j)}) Prelude.Nothing (rds i)++findIntervalUsePos :: IntervalDesc -> (Range.UsePos -> Prelude.Bool) ->+                      Prelude.Maybe ((,) Range.RangeDesc Range.UsePos)+findIntervalUsePos i f =+  let {+   f0 = \r ->+    case Range.findRangeUsePos r f of {+     Prelude.Just pos -> Prelude.Just ((,) r pos);+     Prelude.Nothing -> Prelude.Nothing}}+  in+  let {+   go rs =+     (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+       (\r ->+       f0 r)+       (\r rs' ->+       Lib.option_choose (f0 r) (go rs'))+       rs}+  in go (rds i)++nextUseAfter :: IntervalDesc -> Prelude.Int -> Prelude.Maybe Prelude.Int+nextUseAfter d pos =+  Lib.option_map ((Prelude..) Range.uloc Prelude.snd)+    (findIntervalUsePos d (\u ->+      (Prelude.<=) ((Prelude.succ) pos) (Range.uloc u)))++firstUsePos :: IntervalDesc -> Prelude.Int+firstUsePos d =+  Range.uloc (Prelude.head (Range.ups ( (Prelude.head (rds d)))))++firstUseReqReg :: IntervalDesc -> Prelude.Maybe Prelude.Int+firstUseReqReg d =+  Lib.option_map ((Prelude..) Range.uloc Prelude.snd)+    (findIntervalUsePos d Range.regReq)++lastUsePos :: IntervalDesc -> Prelude.Int+lastUsePos d =+  Range.uloc (Prelude.last (Range.ups ( (Prelude.last (rds d)))))++splitPosition :: IntervalDesc -> (Prelude.Maybe Prelude.Int) -> Prelude.Bool+                 -> Prelude.Int+splitPosition d before splitBeforeLifetimeHole =+  let {initial = firstUsePos d} in+  let {final = lastUsePos d} in+  Prelude.max ((Prelude.succ) initial)+    (Prelude.min final+      (Lib.fromMaybe final (Lib.option_choose before (firstUseReqReg d))))++intervalSpan :: ([] Range.RangeDesc) -> Prelude.Int -> Prelude.Int ->+                Prelude.Int -> Prelude.Int ->+                ((,) (Prelude.Maybe IntervalDesc)+                (Prelude.Maybe IntervalDesc))+intervalSpan rs before iv ib ie =+  let {f = \u -> (Prelude.<=) ((Prelude.succ) (Range.uloc u)) before} in+  (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+    (\r ->+    let {_top_assumption_ = Range.rangeSpan f ( r)} in+    let {+     _evar_0_ = \_top_assumption_0 ->+      let {+       _evar_0_ = \r0 _top_assumption_1 ->+        let {+         _evar_0_ = \r1 ->+          let {+           _evar_0_ = let {+                       _evar_0_ = \_ _ -> (,) (Prelude.Just+                        (Build_IntervalDesc iv (Range.rbeg ( r0))+                        (Range.rend ( r0)) ((:[]) ( r0)))) (Prelude.Just+                        (Build_IntervalDesc iv (Range.rbeg ( r1))+                        (Range.rend ( r1)) ((:[]) ( r1))))}+                      in+                       _evar_0_}+          in+           _evar_0_ __ __}+        in+        let {+         _evar_0_0 = \_ ->+          let {+           _evar_0_0 = \_ -> (,) (Prelude.Just (Build_IntervalDesc iv ib ie+            ((:[]) r))) Prelude.Nothing}+          in+           _evar_0_0 __}+        in+        case _top_assumption_1 of {+         Prelude.Just x -> (\_ -> _evar_0_ x);+         Prelude.Nothing -> _evar_0_0}}+      in+      let {+       _evar_0_0 = \_top_assumption_1 ->+        let {+         _evar_0_0 = \r1 ->+          let {+           _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just+            (Build_IntervalDesc iv ib ie ((:[]) r)))}+          in+           _evar_0_0 __}+        in+        let {_evar_0_1 = \_ -> Logic.coq_False_rec} in+        case _top_assumption_1 of {+         Prelude.Just x -> (\_ -> _evar_0_0 x);+         Prelude.Nothing -> _evar_0_1}}+      in+      case _top_assumption_0 of {+       Prelude.Just x -> _evar_0_ x;+       Prelude.Nothing -> _evar_0_0}}+    in+    case _top_assumption_ of {+     (,) x x0 -> _evar_0_ x x0 __})+    (\r rs0 ->+    let {_top_assumption_ = Range.rangeSpan f ( r)} in+    let {+     _evar_0_ = \_top_assumption_0 ->+      let {+       _evar_0_ = \r0 _top_assumption_1 ->+        let {+         _evar_0_ = \r1 ->+          let {+           _evar_0_ = \_ ->+            let {+             _evar_0_ = \_ _ ->+              (Prelude.flip (Prelude.$)) __ (\_ -> (,) (Prelude.Just+                (Build_IntervalDesc iv (Range.rbeg ( r0)) (Range.rend ( r0))+                ((:[]) ( r0)))) (Prelude.Just (Build_IntervalDesc iv+                (Range.rbeg ( r1)) (Range.rend ( (Prelude.last rs0))) ((:) r1+                rs0))))}+            in+             _evar_0_ __ __}+          in+           _evar_0_ __}+        in+        let {+         _evar_0_0 = \_ ->+          let {+           _evar_0_0 = \_ ->+            let {+             _evar_0_0 = \_ ->+              let {+               _top_assumption_2 = intervalSpan rs0 before iv+                                     (Range.rbeg ( (Prelude.head rs0)))+                                     (Range.rend ( (Prelude.last rs0)))}+              in+              let {+               _evar_0_0 = \_top_assumption_3 ->+                let {+                 _evar_0_0 = \i1_1 _top_assumption_4 ->+                  let {+                   _evar_0_0 = \i1_2 ->+                    case i1_1 of {+                     Build_IntervalDesc ivar0 ibeg0 iend0 rds0 ->+                      let {+                       _evar_0_0 = let {+                                    _evar_0_0 = \_ _ ->+                                     let {+                                      _evar_0_0 = \_ ->+                                       let {+                                        _evar_0_0 = \_ ->+                                         let {+                                          _evar_0_0 = (Prelude.flip (Prelude.$))+                                                        __ (\_ ->+                                                        let {+                                                         _evar_0_0 = \_ _ ->+                                                          (,) (Prelude.Just+                                                          (Build_IntervalDesc+                                                          ivar0+                                                          (Range.rbeg ( r))+                                                          iend0 ((:) r+                                                          rds0)))+                                                          (Prelude.Just+                                                          i1_2)}+                                                        in+                                                         _evar_0_0 __)}+                                         in+                                          _evar_0_0}+                                       in+                                        _evar_0_0 __}+                                     in+                                      _evar_0_0 __}+                                   in+                                    _evar_0_0}+                      in+                       _evar_0_0 __ __}}+                  in+                  let {+                   _evar_0_1 = \_ ->+                    let {+                     _evar_0_1 = \_ _ _ -> (,) (Prelude.Just+                      (Build_IntervalDesc iv (Range.rbeg ( r))+                      (Range.rend ( (Prelude.last rs0))) ((:) r rs0)))+                      Prelude.Nothing}+                    in+                     _evar_0_1 __}+                  in+                  case _top_assumption_4 of {+                   Prelude.Just x -> (\_ _ -> _evar_0_0 x);+                   Prelude.Nothing -> _evar_0_1}}+                in+                let {+                 _evar_0_1 = \_top_assumption_4 ->+                  let {+                   _evar_0_1 = \i1_2 ->+                    let {+                     _evar_0_1 = \_ _ _ -> (,) (Prelude.Just+                      (Build_IntervalDesc iv ib (Range.rend ( r)) ((:[]) r)))+                      (Prelude.Just (Build_IntervalDesc iv+                      (Range.rbeg ( (Prelude.head rs0)))+                      (Range.rend ( (Prelude.last rs0))) rs0))}+                    in+                     _evar_0_1 __}+                  in+                  let {_evar_0_2 = \_ _ _ -> Logic.coq_False_rec} in+                  case _top_assumption_4 of {+                   Prelude.Just x -> (\_ -> _evar_0_1 x);+                   Prelude.Nothing -> _evar_0_2}}+                in+                case _top_assumption_3 of {+                 Prelude.Just x -> _evar_0_0 x;+                 Prelude.Nothing -> _evar_0_1}}+              in+              case _top_assumption_2 of {+               (,) x x0 -> _evar_0_0 x x0 __ __ __}}+            in+             _evar_0_0 __}+          in+           _evar_0_0 __}+        in+        case _top_assumption_1 of {+         Prelude.Just x -> (\_ -> _evar_0_ x);+         Prelude.Nothing -> _evar_0_0}}+      in+      let {+       _evar_0_0 = \_top_assumption_1 ->+        let {+         _evar_0_0 = \r1 ->+          let {+           _evar_0_0 = \_ -> (,) Prelude.Nothing (Prelude.Just+            (Build_IntervalDesc iv ib ie ((:) r rs0)))}+          in+           _evar_0_0 __}+        in+        let {_evar_0_1 = \_ -> Logic.coq_False_rec} in+        case _top_assumption_1 of {+         Prelude.Just x -> (\_ -> _evar_0_0 x);+         Prelude.Nothing -> _evar_0_1}}+      in+      case _top_assumption_0 of {+       Prelude.Just x -> _evar_0_ x;+       Prelude.Nothing -> _evar_0_0}}+    in+    case _top_assumption_ of {+     (,) x x0 -> _evar_0_ x x0 __})+    rs++splitInterval :: Prelude.Int -> IntervalDesc ->+                 ((,) IntervalDesc IntervalDesc)+splitInterval before d =+  let {+   _evar_0_ = \iv ib ie rds0 ->+    let {_top_assumption_ = intervalSpan rds0 before iv ib ie} in+    let {+     _evar_0_ = \_top_assumption_0 ->+      let {+       _evar_0_ = \i0 _top_assumption_1 ->+        let {_evar_0_ = \i1 -> (,) i0 i1} in+        let {+         _evar_0_0 = \_ ->+          let {_evar_0_0 = \_ -> Logic.coq_False_rec} in  _evar_0_0 __}+        in+        case _top_assumption_1 of {+         Prelude.Just x -> (\_ -> _evar_0_ x);+         Prelude.Nothing -> _evar_0_0}}+      in+      let {+       _evar_0_0 = \_top_assumption_1 ->+        let {+         _evar_0_0 = \i1 ->+          let {_evar_0_0 = \_ -> Logic.coq_False_rec} in  _evar_0_0 __}+        in+        let {_evar_0_1 = \_ -> Logic.coq_False_rec} in+        case _top_assumption_1 of {+         Prelude.Just x -> (\_ -> _evar_0_0 x);+         Prelude.Nothing -> _evar_0_1}}+      in+      case _top_assumption_0 of {+       Prelude.Just x -> _evar_0_ x;+       Prelude.Nothing -> _evar_0_0}}+    in+    case _top_assumption_ of {+     (,) x x0 -> _evar_0_ x x0 __}}+  in+  case d of {+   Build_IntervalDesc x x0 x1 x2 -> _evar_0_ x x0 x1 x2}+
+ LinearScan/Lib.hs view
@@ -0,0 +1,107 @@+module LinearScan.Lib where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Logic as Logic+import qualified LinearScan.Specif as Specif+import qualified LinearScan.Eqtype as Eqtype+++__ :: any+__ = Prelude.error "Logical or arity value used"++ex_falso_quodlibet :: a1+ex_falso_quodlibet =+  Logic.coq_False_rect++fromMaybe :: a1 -> (Prelude.Maybe a1) -> a1+fromMaybe d mx =+  case mx of {+   Prelude.Just x -> x;+   Prelude.Nothing -> d}++option_map :: (a1 -> a2) -> (Prelude.Maybe a1) -> Prelude.Maybe a2+option_map f x =+  case x of {+   Prelude.Just x0 -> Prelude.Just (f x0);+   Prelude.Nothing -> Prelude.Nothing}++option_choose :: (Prelude.Maybe a1) -> (Prelude.Maybe a1) -> Prelude.Maybe a1+option_choose x y =+  case x of {+   Prelude.Just a -> x;+   Prelude.Nothing -> y}++foldl_with_index :: (Prelude.Int -> a2 -> a1 -> a2) -> a2 -> ([] a1) -> a2+foldl_with_index f b v =+  let {+   go n xs z =+     case xs of {+      [] -> z;+      (:) y ys -> go ((Prelude.succ) n) ys (f n z y)}}+  in go 0 v b++mapAccumL :: (a1 -> a2 -> (,) a1 a3) -> a1 -> ([] a2) -> (,) a1 ([] a3)+mapAccumL f s v =+  case v of {+   [] -> (,) s [];+   (:) x xs ->+    case f s x of {+     (,) s' y ->+      case mapAccumL f s' xs of {+       (,) s'' ys -> (,) s'' ((:) y ys)}}}++dep_foldl_inv :: (a1 -> Eqtype.Equality__Coq_type) -> a1 -> ([]+                 Eqtype.Equality__Coq_sort) -> Prelude.Int -> (a1 -> []+                 Eqtype.Equality__Coq_sort) -> (a1 -> a1 -> () ->+                 Eqtype.Equality__Coq_sort -> Eqtype.Equality__Coq_sort) ->+                 (a1 -> () -> Eqtype.Equality__Coq_sort -> ([]+                 Eqtype.Equality__Coq_sort) -> () -> Specif.Coq_sig2 +                 a1) -> a1+dep_foldl_inv e b v n q f f0 =+  let {filtered_var = (,) v n} in+  case filtered_var of {+   (,) l n0 ->+    case l of {+     [] -> b;+     (:) y ys ->+      (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))+        (\_ ->+        b)+        (\n' ->+        let {filtered_var0 = f0 b __ y ys __} in+        let {ys' = Prelude.map (f b filtered_var0 __) ys} in+        dep_foldl_inv e filtered_var0 ys' n' q f f0)+        n0}}++dep_foldl_invE :: (a2 -> Eqtype.Equality__Coq_type) -> a2 -> ([]+                  Eqtype.Equality__Coq_sort) -> Prelude.Int -> (a2 -> []+                  Eqtype.Equality__Coq_sort) -> (a2 -> a2 -> () ->+                  Eqtype.Equality__Coq_sort -> Eqtype.Equality__Coq_sort) ->+                  (a2 -> () -> Eqtype.Equality__Coq_sort -> ([]+                  Eqtype.Equality__Coq_sort) -> () -> Prelude.Either +                  a1 (Specif.Coq_sig2 a2)) -> Prelude.Either a1 a2+dep_foldl_invE e b v n q f f0 =+  let {filtered_var = (,) v n} in+  case filtered_var of {+   (,) l n0 ->+    case l of {+     [] -> Prelude.Right b;+     (:) y ys ->+      (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))+        (\_ -> Prelude.Right+        b)+        (\n' ->+        let {filtered_var0 = f0 b __ y ys __} in+        case filtered_var0 of {+         Prelude.Left err -> Prelude.Left err;+         Prelude.Right s ->+          let {ys' = Prelude.map (f b s __) ys} in+          dep_foldl_invE e s ys' n' q f f0})+        n0}}+
+ LinearScan/Logic.hs view
@@ -0,0 +1,18 @@+module LinearScan.Logic where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils+++coq_False_rect :: a1+coq_False_rect =+  Prelude.error "absurd case"++coq_False_rec :: a1+coq_False_rec =+  coq_False_rect+
+ LinearScan/Main.hs view
@@ -0,0 +1,1700 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Main where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Datatypes as Datatypes+import qualified LinearScan.IApplicative as IApplicative+import qualified LinearScan.IEndo as IEndo+import qualified LinearScan.IMonad as IMonad+import qualified LinearScan.IState as IState+import qualified LinearScan.Interval as Interval+import qualified LinearScan.Lib as Lib+import qualified LinearScan.Logic as Logic+import qualified LinearScan.NonEmpty0 as NonEmpty0+import qualified LinearScan.Range as Range+import qualified LinearScan.Specif as Specif+import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Fintype as Fintype+import qualified LinearScan.Seq as Seq+import qualified LinearScan.Ssrbool as Ssrbool+import qualified LinearScan.Ssrnat as Ssrnat++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++__ :: any+__ = Prelude.error "Logical or arity value used"++_MyMachine__maxReg :: Prelude.Int+_MyMachine__maxReg = 32++type MyMachine__PhysReg = Prelude.Int++maxReg :: Prelude.Int+maxReg =+  _MyMachine__maxReg++type PhysReg = Prelude.Int++data SSError =+   ECannotSplitSingleton Prelude.Int+ | ECannotSplitAssignedSingleton Prelude.Int+ | ENoIntervalsToSplit+ | ERegisterAlreadyAssigned Prelude.Int+ | ERegisterAssignmentsOverlap Prelude.Int++coq_SSError_rect :: (Prelude.Int -> a1) -> (Prelude.Int -> a1) ->+                               a1 -> (Prelude.Int -> a1) -> (Prelude.Int ->+                               a1) -> SSError -> a1+coq_SSError_rect f f0 f1 f2 f3 s =+  case s of {+   ECannotSplitSingleton x -> f x;+   ECannotSplitAssignedSingleton x -> f0 x;+   ENoIntervalsToSplit -> f1;+   ERegisterAlreadyAssigned x -> f2 x;+   ERegisterAssignmentsOverlap x -> f3 x}++coq_SSError_rec :: (Prelude.Int -> a1) -> (Prelude.Int -> a1) ->+                              a1 -> (Prelude.Int -> a1) -> (Prelude.Int ->+                              a1) -> SSError -> a1+coq_SSError_rec =+  coq_SSError_rect++stbind :: (a4 -> IState.IState SSError a2 a3 a5) ->+                     (IState.IState SSError a1 a2 a4) ->+                     IState.IState SSError a1 a3 a5+stbind f x =+  IMonad.ijoin (unsafeCoerce IState.coq_IState_IMonad)+    (IEndo.imap (unsafeCoerce IState.coq_IState_IFunctor) f (unsafeCoerce x))++error_ :: SSError -> IState.IState SSError +                     a1 a1 a2+error_ err x =+  Prelude.Left err++return_ :: a2 -> IState.IState SSError a1 a1 a2+return_ =+  IApplicative.ipure (unsafeCoerce IState.coq_IState_IApplicative)++type Coq_fixedIntervalsType =+  [] (Prelude.Maybe Interval.IntervalDesc)++data ScanStateDesc =+   Build_ScanStateDesc Prelude.Int ([] Interval.IntervalDesc) + Coq_fixedIntervalsType ([] ((,) Prelude.Int Prelude.Int)) + ([] ((,) Prelude.Int PhysReg)) ([]+                                          ((,) Prelude.Int PhysReg)) + ([] ((,) Prelude.Int PhysReg))++coq_ScanStateDesc_rect :: (Prelude.Int -> ([]+                                     Interval.IntervalDesc) ->+                                     Coq_fixedIntervalsType -> ([]+                                     ((,) Prelude.Int Prelude.Int)) -> ([]+                                     ((,) Prelude.Int PhysReg)) ->+                                     ([] ((,) Prelude.Int PhysReg))+                                     -> ([]+                                     ((,) Prelude.Int PhysReg)) ->+                                     a1) -> ScanStateDesc -> a1+coq_ScanStateDesc_rect f s =+  case s of {+   Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 -> f x x0 x1 x2 x3 x4 x5}++coq_ScanStateDesc_rec :: (Prelude.Int -> ([]+                                    Interval.IntervalDesc) ->+                                    Coq_fixedIntervalsType -> ([]+                                    ((,) Prelude.Int Prelude.Int)) -> ([]+                                    ((,) Prelude.Int PhysReg)) ->+                                    ([] ((,) Prelude.Int PhysReg))+                                    -> ([]+                                    ((,) Prelude.Int PhysReg)) ->+                                    a1) -> ScanStateDesc -> a1+coq_ScanStateDesc_rec =+  coq_ScanStateDesc_rect++nextInterval :: ScanStateDesc -> Prelude.Int+nextInterval s =+  case s of {+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0+    unhandled0 active0 inactive0 handled0 -> nextInterval0}++type IntervalId = Prelude.Int++intervals :: ScanStateDesc -> [] Interval.IntervalDesc+intervals s =+  case s of {+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0+    unhandled0 active0 inactive0 handled0 -> intervals0}++fixedIntervals :: ScanStateDesc ->+                             Coq_fixedIntervalsType+fixedIntervals s =+  case s of {+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0+    unhandled0 active0 inactive0 handled0 -> fixedIntervals0}++unhandled :: ScanStateDesc -> []+                        ((,) IntervalId Prelude.Int)+unhandled s =+  case s of {+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0+    unhandled0 active0 inactive0 handled0 -> unhandled0}++active :: ScanStateDesc -> []+                     ((,) IntervalId PhysReg)+active s =+  case s of {+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0+    unhandled0 active0 inactive0 handled0 -> active0}++inactive :: ScanStateDesc -> []+                       ((,) IntervalId PhysReg)+inactive s =+  case s of {+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0+    unhandled0 active0 inactive0 handled0 -> inactive0}++handled :: ScanStateDesc -> []+                      ((,) IntervalId PhysReg)+handled s =+  case s of {+   Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0+    unhandled0 active0 inactive0 handled0 -> handled0}++unhandledIds :: ScanStateDesc -> [] IntervalId+unhandledIds s =+  Prelude.map (\i -> Prelude.fst i) (unhandled s)++activeIds :: ScanStateDesc -> [] IntervalId+activeIds s =+  Prelude.map (\i -> Prelude.fst i) (active s)++inactiveIds :: ScanStateDesc -> [] IntervalId+inactiveIds s =+  Prelude.map (\i -> Prelude.fst i) (inactive s)++handledIds :: ScanStateDesc -> [] IntervalId+handledIds s =+  Prelude.map (\i -> Prelude.fst i) (handled s)++all_state_lists :: ScanStateDesc -> []+                              IntervalId+all_state_lists s =+  (Prelude.++) (unhandledIds s)+    ((Prelude.++) (activeIds s)+      ((Prelude.++) (inactiveIds s) (handledIds s)))++totalExtent :: ScanStateDesc -> ([]+                          IntervalId) -> Prelude.Int+totalExtent sd xs =+  Data.List.sum+    (Prelude.map (\i ->+      Interval.intervalExtent+        (+          (LinearScan.Utils.nth (nextInterval sd)+            (intervals sd) i))) xs)++unhandledExtent :: ScanStateDesc -> Prelude.Int+unhandledExtent sd =+  totalExtent sd+    (Prelude.map (\i -> Prelude.fst i) (unhandled sd))++registerWithHighestPos :: ([] (Prelude.Maybe Prelude.Int)) -> (,)+                                     Prelude.Int (Prelude.Maybe Prelude.Int)+registerWithHighestPos =+  (LinearScan.Utils.vfoldl'_with_index) maxReg (\reg res x ->+    case res of {+     (,) r o ->+      case o of {+       Prelude.Just n ->+        case x of {+         Prelude.Just m ->+          case (Prelude.<=) ((Prelude.succ) n) m of {+           Prelude.True -> (,) reg (Prelude.Just m);+           Prelude.False -> (,) r (Prelude.Just n)};+         Prelude.Nothing -> (,) reg Prelude.Nothing};+       Prelude.Nothing -> (,) r Prelude.Nothing}}) ((,) ( 0) (Prelude.Just+    0))++getScanStateDesc :: ScanStateDesc ->+                               ScanStateDesc+getScanStateDesc sd =+  sd++packScanState :: ScanStateDesc ->+                            ScanStateDesc+packScanState sd =+  sd++coq_ScanStateCursor_rect :: ScanStateDesc -> (() -> ()+                                       -> a1) -> a1+coq_ScanStateCursor_rect sd f =+  f __ __++coq_ScanStateCursor_rec :: ScanStateDesc -> (() -> () ->+                                      a1) -> a1+coq_ScanStateCursor_rec sd f =+  coq_ScanStateCursor_rect sd f++curId :: ScanStateDesc -> (,) IntervalId+                    Prelude.Int+curId sd =+  Prelude.head (unhandled sd)++curIntDetails :: ScanStateDesc -> Interval.IntervalDesc+curIntDetails sd =+  LinearScan.Utils.nth (nextInterval sd) (intervals sd)+    (Prelude.fst (curId sd))++curPosition :: ScanStateDesc -> Prelude.Int+curPosition sd =+  Interval.intervalStart ( (curIntDetails sd))++data VarKind =+   Input+ | Temp+ | Output++coq_VarKind_rect :: a1 -> a1 -> a1 -> VarKind -> a1+coq_VarKind_rect f f0 f1 v =+  case v of {+   Input -> f;+   Temp -> f0;+   Output -> f1}++coq_VarKind_rec :: a1 -> a1 -> a1 -> VarKind -> a1+coq_VarKind_rec =+  coq_VarKind_rect++data Allocation =+   Unallocated+ | Register PhysReg+ | Spill deriving (Prelude.Show, Prelude.Eq)++coq_Allocation_rect :: a1 -> (PhysReg -> a1) -> a1 ->+                                  Allocation -> a1+coq_Allocation_rect f f0 f1 a =+  case a of {+   Unallocated -> f;+   Register x -> f0 x;+   Spill -> f1}++coq_Allocation_rec :: a1 -> (PhysReg -> a1) -> a1 ->+                                 Allocation -> a1+coq_Allocation_rec =+  coq_Allocation_rect++data VarInfo =+   Build_VarInfo Prelude.Int VarKind Allocation + Prelude.Bool++coq_VarInfo_rect :: (Prelude.Int -> VarKind ->+                               Allocation -> Prelude.Bool -> a1) ->+                               VarInfo -> a1+coq_VarInfo_rect f v =+  case v of {+   Build_VarInfo x x0 x1 x2 -> f x x0 x1 x2}++coq_VarInfo_rec :: (Prelude.Int -> VarKind ->+                              Allocation -> Prelude.Bool -> a1) ->+                              VarInfo -> a1+coq_VarInfo_rec =+  coq_VarInfo_rect++varId :: VarInfo -> Prelude.Int+varId v =+  case v of {+   Build_VarInfo varId0 varKind0 varAlloc0 regRequired0 -> varId0}++varKind :: VarInfo -> VarKind+varKind v =+  case v of {+   Build_VarInfo varId0 varKind0 varAlloc0 regRequired0 -> varKind0}++varAlloc :: VarInfo -> Allocation+varAlloc v =+  case v of {+   Build_VarInfo varId0 varKind0 varAlloc0 regRequired0 ->+    varAlloc0}++regRequired :: VarInfo -> Prelude.Bool+regRequired v =+  case v of {+   Build_VarInfo varId0 varKind0 varAlloc0 regRequired0 ->+    regRequired0}++data OpKind =+   Normal+ | LoopBegin+ | LoopEnd+ | Call++coq_OpKind_rect :: a1 -> a1 -> a1 -> a1 -> OpKind -> a1+coq_OpKind_rect f f0 f1 f2 o =+  case o of {+   Normal -> f;+   LoopBegin -> f0;+   LoopEnd -> f1;+   Call -> f2}++coq_OpKind_rec :: a1 -> a1 -> a1 -> a1 -> OpKind -> a1+coq_OpKind_rec =+  coq_OpKind_rect++data OpInfo =+   Build_OpInfo Prelude.Int Prelude.Int OpKind ([]+                                                                   VarInfo) + ([] PhysReg)++coq_OpInfo_rect :: (Prelude.Int -> Prelude.Int -> OpKind+                              -> ([] VarInfo) -> ([]+                              PhysReg) -> a1) -> OpInfo+                              -> a1+coq_OpInfo_rect f o =+  case o of {+   Build_OpInfo x x0 x1 x2 x3 -> f x x0 x1 x2 x3}++coq_OpInfo_rec :: (Prelude.Int -> Prelude.Int -> OpKind+                             -> ([] VarInfo) -> ([]+                             PhysReg) -> a1) -> OpInfo ->+                             a1+coq_OpInfo_rec =+  coq_OpInfo_rect++opId :: OpInfo -> Prelude.Int+opId o =+  case o of {+   Build_OpInfo opId0 opMeta0 opKind0 varRefs0 regRefs0 -> opId0}++opMeta :: OpInfo -> Prelude.Int+opMeta o =+  case o of {+   Build_OpInfo opId0 opMeta0 opKind0 varRefs0 regRefs0 -> opMeta0}++opKind :: OpInfo -> OpKind+opKind o =+  case o of {+   Build_OpInfo opId0 opMeta0 opKind0 varRefs0 regRefs0 -> opKind0}++varRefs :: OpInfo -> [] VarInfo+varRefs o =+  case o of {+   Build_OpInfo opId0 opMeta0 opKind0 varRefs0 regRefs0 -> varRefs0}++regRefs :: OpInfo -> [] PhysReg+regRefs o =+  case o of {+   Build_OpInfo opId0 opMeta0 opKind0 varRefs0 regRefs0 -> regRefs0}++data BlockInfo =+   Build_BlockInfo Prelude.Int ([] OpInfo)++coq_BlockInfo_rect :: (Prelude.Int -> ([] OpInfo) -> a1)+                                 -> BlockInfo -> a1+coq_BlockInfo_rect f b =+  case b of {+   Build_BlockInfo x x0 -> f x x0}++coq_BlockInfo_rec :: (Prelude.Int -> ([] OpInfo) -> a1)+                                -> BlockInfo -> a1+coq_BlockInfo_rec =+  coq_BlockInfo_rect++blockId :: BlockInfo -> Prelude.Int+blockId b =+  case b of {+   Build_BlockInfo blockId0 blockOps0 -> blockId0}++blockOps :: BlockInfo -> [] OpInfo+blockOps b =+  case b of {+   Build_BlockInfo blockId0 blockOps0 -> blockOps0}++type BlockList = [] BlockInfo++type BoundedRange = Range.RangeDesc++transportBoundedRange :: Prelude.Int -> Prelude.Int ->+                                    BoundedRange ->+                                    BoundedRange+transportBoundedRange base prev x =+  x++data BuildState =+   Build_BuildState Prelude.Int ([]+                                          (Prelude.Maybe+                                          BoundedRange)) ([]+                                                                   (Prelude.Maybe+                                                                   BoundedRange))++coq_BuildState_rect :: (Prelude.Int -> ([]+                                  (Prelude.Maybe BoundedRange)) ->+                                  ([] (Prelude.Maybe BoundedRange))+                                  -> a1) -> BuildState -> a1+coq_BuildState_rect f b =+  case b of {+   Build_BuildState x x0 x1 -> f x x0 x1}++coq_BuildState_rec :: (Prelude.Int -> ([]+                                 (Prelude.Maybe BoundedRange)) ->+                                 ([] (Prelude.Maybe BoundedRange))+                                 -> a1) -> BuildState -> a1+coq_BuildState_rec =+  coq_BuildState_rect++bsPos :: BuildState -> Prelude.Int+bsPos b =+  case b of {+   Build_BuildState bsPos0 bsVars0 bsRegs0 -> bsPos0}++bsVars :: BuildState -> []+                     (Prelude.Maybe BoundedRange)+bsVars b =+  case b of {+   Build_BuildState bsPos0 bsVars0 bsRegs0 -> bsVars0}++bsRegs :: BuildState -> []+                     (Prelude.Maybe BoundedRange)+bsRegs b =+  case b of {+   Build_BuildState bsPos0 bsVars0 bsRegs0 -> bsRegs0}++foldOps :: (a1 -> OpInfo -> a1) -> a1 ->+                      BlockList -> a1+foldOps f z =+  Data.List.foldl' (\bacc blk ->+    Data.List.foldl' f bacc (blockOps blk)) z++foldOpsRev :: (a1 -> OpInfo -> a1) -> a1 ->+                         BlockList -> a1+foldOpsRev f z blocks =+  Data.List.foldl' (\bacc blk ->+    Data.List.foldl' f bacc (Seq.rev (blockOps blk))) z+    (Seq.rev ( blocks))++mapAccumLOps :: (a1 -> OpInfo -> (,) a1+                           OpInfo) -> a1 -> BlockList ->+                           (,) a1 BlockList+mapAccumLOps f =+  NonEmpty0.coq_NE_mapAccumL (\z blk ->+    case Lib.mapAccumL f z (blockOps blk) of {+     (,) z' ops -> (,) z' (Build_BlockInfo (blockId blk)+      ops)})++processOperations :: BlockList -> BuildState+processOperations blocks =+  (Prelude.flip (Prelude.$))+    (foldOps (\x op ->+      case x of {+       (,) n m -> (,) ((Prelude.succ) n)+        (Data.List.foldl' (\m0 v -> Prelude.max m0 (varId v)) m+          (varRefs op))}) ((,) 0 0) blocks) (\_top_assumption_ ->+    let {+     _evar_0_ = \opCount highestVar ->+      let {+       z = Build_BuildState opCount+        (Seq.nseq ((Prelude.succ) highestVar) Prelude.Nothing)+        (Data.List.replicate maxReg Prelude.Nothing)}+      in+      foldOpsRev (\_top_assumption_0 ->+        let {+         _evar_0_ = \pos vars regs op ->+          (Prelude.flip (Prelude.$)) __ (\_ ->+            let {+             _evar_0_ = \vars0 regs0 -> Build_BuildState 0 vars0+              regs0}+            in+            let {+             _evar_0_0 = \pos0 vars0 regs0 -> Build_BuildState pos0+              ((Prelude.flip (Prelude.$))+                ((Prelude.flip (Prelude.$)) vars0 (\vars' ->+                  let {+                   vars'0 = Prelude.map+                              (Lib.option_map+                                (transportBoundedRange+                                  ((Prelude.succ) (Ssrnat.double pos0))+                                  ((Prelude.succ)+                                  (Ssrnat.double ((Prelude.succ) pos0)))))+                              vars'}+                  in+                  Data.List.foldl' (\vars'1 v ->+                    let {+                     upos = Range.Build_UsePos ((Prelude.succ)+                      (Ssrnat.double pos0)) (regRequired v)}+                    in+                    (Prelude.flip (Prelude.$)) __ (\_ ->+                      Seq.set_nth Prelude.Nothing vars'1 (varId v)+                        (Prelude.Just+                        (let {+                          _evar_0_0 = \_top_assumption_1 ->+                           Range.Build_RangeDesc (Range.uloc upos)+                           (Range.rend ( _top_assumption_1)) ((:) upos+                           (Range.ups ( _top_assumption_1)))}+                         in+                         let {+                          _evar_0_1 = Range.Build_RangeDesc (Range.uloc upos)+                           ((Prelude.succ) (Range.uloc upos)) ((:[]) upos)}+                         in+                         case Seq.nth Prelude.Nothing vars0+                                (varId v) of {+                          Prelude.Just x -> _evar_0_0 x;+                          Prelude.Nothing -> _evar_0_1})))) vars'0+                    (varRefs op))) (\x -> x))+              ((Prelude.flip (Prelude.$))+                ((Prelude.flip (Prelude.$)) regs0 (\regs' ->+                  let {+                   regs'0 = LinearScan.Utils.vmap maxReg+                              (Lib.option_map+                                (transportBoundedRange+                                  ((Prelude.succ) (Ssrnat.double pos0))+                                  ((Prelude.succ)+                                  (Ssrnat.double ((Prelude.succ) pos0)))))+                              regs'}+                  in+                  Data.List.foldl' (\regs'1 reg ->+                    let {+                     upos = Range.Build_UsePos ((Prelude.succ)+                      (Ssrnat.double pos0)) Prelude.True}+                    in+                    (Prelude.flip (Prelude.$)) __ (\_ ->+                      LinearScan.Utils.set_nth maxReg regs'1 reg+                        (Prelude.Just+                        (let {+                          _evar_0_0 = \_top_assumption_1 ->+                           Range.Build_RangeDesc (Range.uloc upos)+                           (Range.rend ( _top_assumption_1)) ((:) upos+                           (Range.ups ( _top_assumption_1)))}+                         in+                         let {+                          _evar_0_1 = Range.Build_RangeDesc (Range.uloc upos)+                           ((Prelude.succ) (Range.uloc upos)) ((:[]) upos)}+                         in+                         case LinearScan.Utils.nth maxReg regs0+                                reg of {+                          Prelude.Just x -> _evar_0_0 x;+                          Prelude.Nothing -> _evar_0_1})))) regs'0+                    (regRefs op))) (\x -> x))}+            in+            (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))+              (\_ ->+              _evar_0_ vars regs)+              (\x ->+              _evar_0_0 x vars regs)+              pos)}+        in+        case _top_assumption_0 of {+         Build_BuildState x x0 x1 -> _evar_0_ x x0 x1}) z blocks}+    in+    case _top_assumption_ of {+     (,) x x0 -> _evar_0_ x x0})++computeBlockOrder :: IState.IState SSError+                                BlockList BlockList +                                ()+computeBlockOrder =+  return_ ()++numberOperations :: IState.IState SSError+                               BlockList BlockList +                               ()+numberOperations =+  let {+   f = \n op -> (,) ((Prelude.succ) ((Prelude.succ) n))+    (Build_OpInfo n (opMeta op) (opKind op)+    (varRefs op) (regRefs op))}+  in+  IState.imodify+    ((Prelude..) Prelude.snd (mapAccumLOps f ((Prelude.succ) 0)))++type BlockState a =+  IState.IState SSError BlockList BlockList a++computeLocalLiveSets :: BlockState ()+computeLocalLiveSets =+  return_ ()++computeGlobalLiveSets :: BlockState ()+computeGlobalLiveSets =+  return_ ()++buildIntervals :: IState.IState SSError+                             BlockList BlockList+                             ScanStateDesc+buildIntervals =+  let {+   mkint = \vid ss pos mx f ->+    case mx of {+     Prelude.Just b ->+      f ss __ (Interval.Build_IntervalDesc vid (Range.rbeg ( b))+        (Range.rend ( b)) ((:[]) ( b))) __;+     Prelude.Nothing -> ss}}+  in+  let {+   handleVar = \pos vid ss mx ->+    (Prelude.$) (mkint vid ss pos mx) (\sd _ d _ ->+      packScanState (Build_ScanStateDesc ((Prelude.succ)+        (nextInterval sd))+        (LinearScan.Utils.snoc (nextInterval sd)+          (intervals sd) d) (fixedIntervals sd)+        (Data.List.insertBy (Data.Ord.comparing Prelude.snd) ((,)+          ( (nextInterval sd)) (Interval.ibeg d))+          (Prelude.map Prelude.id (unhandled sd)))+        (Prelude.map Prelude.id (active sd))+        (Prelude.map Prelude.id (inactive sd))+        (Prelude.map Prelude.id (handled sd))))}+  in+  stbind (\blocks ->+    let {bs = processOperations blocks} in+    let {+     regs = LinearScan.Utils.vmap maxReg (\mr ->+              case mr of {+               Prelude.Just y -> Prelude.Just+                (Interval.packInterval (Interval.Build_IntervalDesc 0+                  (Range.rbeg ( y)) (Range.rend ( y)) ((:[]) ( y))));+               Prelude.Nothing -> Prelude.Nothing}) (bsRegs bs)}+    in+    let {+     s2 = packScanState (Build_ScanStateDesc+            (nextInterval (Build_ScanStateDesc 0 []+              (Data.List.replicate maxReg Prelude.Nothing) [] []+              [] []))+            (intervals (Build_ScanStateDesc 0 []+              (Data.List.replicate maxReg Prelude.Nothing) [] []+              [] [])) regs+            (unhandled (Build_ScanStateDesc 0 []+              (Data.List.replicate maxReg Prelude.Nothing) [] []+              [] []))+            (active (Build_ScanStateDesc 0 []+              (Data.List.replicate maxReg Prelude.Nothing) [] []+              [] []))+            (inactive (Build_ScanStateDesc 0 []+              (Data.List.replicate maxReg Prelude.Nothing) [] []+              [] []))+            (handled (Build_ScanStateDesc 0 []+              (Data.List.replicate maxReg Prelude.Nothing) [] []+              [] [])))}+    in+    (Prelude.$) return_+      (Lib.foldl_with_index (handleVar (bsPos bs)) s2+        (bsVars bs))) IState.iget++resolveDataFlow :: BlockState ()+resolveDataFlow =+  return_ ()++mapOps :: (OpInfo -> OpInfo) ->+                     BlockList -> BlockList+mapOps f =+  Prelude.map (\blk -> Build_BlockInfo (blockId blk)+    (Prelude.map f (blockOps blk)))++assignRegNum :: ScanStateDesc -> IState.IState+                           SSError BlockList+                           BlockList ()+assignRegNum sd =+  let {+   ints = (Prelude.++) (handled sd)+            ((Prelude.++) (active sd) (inactive sd))}+  in+  let {+   f = \op ->+    let {+     k = \v ->+      let {vid = varId v} in+      let {+       h = \acc x ->+        case x of {+         (,) xid reg ->+          let {+           int = Interval.getIntervalDesc+                   (+                     (LinearScan.Utils.nth (nextInterval sd)+                       (intervals sd) xid))}+          in+          case (Prelude.&&)+                 (Eqtype.eq_op Ssrnat.nat_eqType+                   (unsafeCoerce (Interval.ivar int)) (unsafeCoerce vid))+                 ((Prelude.&&)+                   ((Prelude.<=) (Interval.ibeg int) (opId op))+                   ((Prelude.<=) ((Prelude.succ) (opId op))+                     (Interval.iend int))) of {+           Prelude.True -> Build_VarInfo (varId v)+            (varKind v) (Register reg)+            (regRequired v);+           Prelude.False -> acc}}}+      in+      Data.List.foldl' h v ints}+    in+    Build_OpInfo (opId op) (opMeta op)+    (opKind op) (Prelude.map k (varRefs op))+    (regRefs op)}+  in+  IState.imodify (mapOps f)++coq_SSMorph_rect :: ScanStateDesc ->+                               ScanStateDesc -> (() -> () -> () ->+                               a1) -> a1+coq_SSMorph_rect sd1 sd2 f =+  f __ __ __++coq_SSMorph_rec :: ScanStateDesc ->+                              ScanStateDesc -> (() -> () -> () ->+                              a1) -> a1+coq_SSMorph_rec sd1 sd2 f =+  coq_SSMorph_rect sd1 sd2 f++coq_SSMorphSt_rect :: ScanStateDesc ->+                                 ScanStateDesc -> (() -> () -> a1)+                                 -> a1+coq_SSMorphSt_rect sd1 sd2 f =+  f __ __++coq_SSMorphSt_rec :: ScanStateDesc ->+                                ScanStateDesc -> (() -> () -> a1)+                                -> a1+coq_SSMorphSt_rec sd1 sd2 f =+  coq_SSMorphSt_rect sd1 sd2 f++coq_SSMorphLen_rect :: ScanStateDesc ->+                                  ScanStateDesc -> (() -> () -> a1)+                                  -> a1+coq_SSMorphLen_rect sd1 sd2 f =+  f __ __++coq_SSMorphLen_rec :: ScanStateDesc ->+                                 ScanStateDesc -> (() -> () -> a1)+                                 -> a1+coq_SSMorphLen_rec sd1 sd2 f =+  coq_SSMorphLen_rect sd1 sd2 f++transportation :: ScanStateDesc ->+                             ScanStateDesc -> IntervalId+                             -> IntervalId+transportation sd1 sd2 x =+   x++data HasBase p =+   Build_HasBase++coq_HasBase_rect :: (() -> a2) -> a2+coq_HasBase_rect f =+  f __++coq_HasBase_rec :: (() -> a2) -> a2+coq_HasBase_rec f =+  coq_HasBase_rect f++coq_SSMorphStLen_rect :: ScanStateDesc ->+                                    ScanStateDesc -> (() -> () ->+                                    a1) -> a1+coq_SSMorphStLen_rect sd1 sd2 f =+  f __ __++coq_SSMorphStLen_rec :: ScanStateDesc ->+                                   ScanStateDesc -> (() -> () ->+                                   a1) -> a1+coq_SSMorphStLen_rec sd1 sd2 f =+  coq_SSMorphStLen_rect sd1 sd2 f++coq_SSMorphHasLen_rect :: ScanStateDesc ->+                                     ScanStateDesc -> (() -> () ->+                                     a1) -> a1+coq_SSMorphHasLen_rect sd1 sd2 f =+  f __ __++coq_SSMorphHasLen_rec :: ScanStateDesc ->+                                    ScanStateDesc -> (() -> () ->+                                    a1) -> a1+coq_SSMorphHasLen_rec sd1 sd2 f =+  coq_SSMorphHasLen_rect sd1 sd2 f++data HasWork p =+   Build_HasWork++coq_HasWork_rect :: (() -> a2) -> a2+coq_HasWork_rect f =+  f __++coq_HasWork_rec :: (() -> a2) -> a2+coq_HasWork_rec f =+  coq_HasWork_rect f++coq_SSMorphStHasLen_rect :: ScanStateDesc ->+                                       ScanStateDesc -> (() -> ()+                                       -> a1) -> a1+coq_SSMorphStHasLen_rect sd1 sd2 f =+  f __ __++coq_SSMorphStHasLen_rec :: ScanStateDesc ->+                                      ScanStateDesc -> (() -> () ->+                                      a1) -> a1+coq_SSMorphStHasLen_rec sd1 sd2 f =+  coq_SSMorphStHasLen_rect sd1 sd2 f++coq_SSMorphSplit_rect :: ScanStateDesc ->+                                    ScanStateDesc -> (() -> () ->+                                    a1) -> a1+coq_SSMorphSplit_rect sd1 sd2 f =+  f __ __++coq_SSMorphSplit_rec :: ScanStateDesc ->+                                   ScanStateDesc -> (() -> () ->+                                   a1) -> a1+coq_SSMorphSplit_rec sd1 sd2 f =+  coq_SSMorphSplit_rect sd1 sd2 f++data IsSplittable p =+   Build_IsSplittable++coq_IsSplittable_rect :: (() -> a2) -> a2+coq_IsSplittable_rect f =+  f __++coq_IsSplittable_rec :: (() -> a2) -> a2+coq_IsSplittable_rec f =+  coq_IsSplittable_rect f++coq_SSMorphStSplit_rect :: ScanStateDesc ->+                                      ScanStateDesc -> (() -> () ->+                                      a1) -> a1+coq_SSMorphStSplit_rect sd1 sd2 f =+  f __ __++coq_SSMorphStSplit_rec :: ScanStateDesc ->+                                     ScanStateDesc -> (() -> () ->+                                     a1) -> a1+coq_SSMorphStSplit_rec sd1 sd2 f =+  coq_SSMorphStSplit_rect sd1 sd2 f++data SSInfo p =+   Build_SSInfo ScanStateDesc p++coq_SSInfo_rect :: ScanStateDesc ->+                              (ScanStateDesc -> a1 -> () -> a2) ->+                              (SSInfo a1) -> a2+coq_SSInfo_rect startDesc f s =+  case s of {+   Build_SSInfo x x0 -> f x x0 __}++coq_SSInfo_rec :: ScanStateDesc ->+                             (ScanStateDesc -> a1 -> () -> a2) ->+                             (SSInfo a1) -> a2+coq_SSInfo_rec startDesc =+  coq_SSInfo_rect startDesc++thisDesc :: ScanStateDesc -> (SSInfo a1) ->+                       ScanStateDesc+thisDesc startDesc s =+  case s of {+   Build_SSInfo thisDesc0 thisHolds0 -> thisDesc0}++thisHolds :: ScanStateDesc -> (SSInfo +                        a1) -> a1+thisHolds startDesc s =+  case s of {+   Build_SSInfo thisDesc0 thisHolds0 -> thisHolds0}++type SState p q a =+  IState.IState SSError (SSInfo p) (SSInfo q) a++withScanState :: ScanStateDesc ->+                            (ScanStateDesc -> () ->+                            SState a2 a3 a1) -> SState +                            a2 a3 a1+withScanState pre f =+  stbind (\i -> f (thisDesc pre i) __) IState.iget++withScanStatePO :: ScanStateDesc ->+                              (ScanStateDesc -> () ->+                              SState () () a1) -> SState+                              () () a1+withScanStatePO pre f i =+  case i of {+   Build_SSInfo thisDesc0 _ ->+    let {f0 = f thisDesc0 __} in+    let {x = Build_SSInfo thisDesc0 __} in+    let {x0 = f0 x} in+    case x0 of {+     Prelude.Left s0 -> Prelude.Left s0;+     Prelude.Right p -> Prelude.Right+      (case p of {+        (,) a0 s0 -> (,) a0+         (case s0 of {+           Build_SSInfo thisDesc1 _ -> Build_SSInfo+            thisDesc1 __})})}}++liftLen :: ScanStateDesc -> (ScanStateDesc ->+                      SState () () a1) -> SState +                      () () a1+liftLen pre f _top_assumption_ =+  let {+   _evar_0_ = \sd ->+    let {ss = Build_SSInfo sd __} in+    let {_top_assumption_0 = f sd} in+    let {_top_assumption_1 = _top_assumption_0 ss} in+    let {_evar_0_ = \err -> Prelude.Left err} in+    let {+     _evar_0_0 = \_top_assumption_2 ->+      let {+       _evar_0_0 = \x _top_assumption_3 ->+        let {+         _evar_0_0 = \sd' -> Prelude.Right ((,) x (Build_SSInfo sd'+          __))}+        in+        case _top_assumption_3 of {+         Build_SSInfo x0 x1 -> _evar_0_0 x0}}+      in+      case _top_assumption_2 of {+       (,) x x0 -> _evar_0_0 x x0}}+    in+    case _top_assumption_1 of {+     Prelude.Left x -> _evar_0_ x;+     Prelude.Right x -> _evar_0_0 x}}+  in+  case _top_assumption_ of {+   Build_SSInfo x x0 -> _evar_0_ x}++weakenStHasLenToSt :: ScanStateDesc -> SState+                                 () () ()+weakenStHasLenToSt pre hS =+  Prelude.Right ((,) ()+    (case hS of {+      Build_SSInfo thisDesc0 _ -> Build_SSInfo thisDesc0+       __}))++withCursor :: ScanStateDesc -> (ScanStateDesc+                         -> () -> SState a1 a2 a3) ->+                         SState a1 a2 a3+withCursor pre f x =+  case x of {+   Build_SSInfo thisDesc0 thisHolds0 ->+    f thisDesc0 __ (Build_SSInfo thisDesc0 thisHolds0)}++moveUnhandledToActive :: ScanStateDesc ->+                                    PhysReg -> SState +                                    a1 () ()+moveUnhandledToActive pre reg x =+  case x of {+   Build_SSInfo thisDesc0 thisHolds0 ->+    case thisDesc0 of {+     Build_ScanStateDesc nextInterval0 intervals0 fixedIntervals0+      unhandled0 active0 inactive0 handled0 ->+      case unhandled0 of {+       [] -> Logic.coq_False_rect;+       (:) p unhandled1 ->+        let {+         _evar_0_ = \_ -> Prelude.Right ((,) () (Build_SSInfo+          (Build_ScanStateDesc nextInterval0 intervals0+          fixedIntervals0 unhandled1 ((:) ((,) (Prelude.fst p) reg) active0)+          inactive0 handled0) __))}+        in+        let {+         _evar_0_0 = \_ -> Prelude.Left (ERegisterAlreadyAssigned+          ( reg))}+        in+        case Prelude.not+               (Ssrbool.in_mem (unsafeCoerce reg)+                 (Ssrbool.mem+                   (Seq.seq_predType+                     (Fintype.ordinal_eqType maxReg))+                   (unsafeCoerce (Prelude.map (\i -> Prelude.snd i) active0)))) of {+         Prelude.True -> _evar_0_ __;+         Prelude.False -> _evar_0_0 __}}}}++moveActiveToHandled :: ScanStateDesc ->+                                  Eqtype.Equality__Coq_sort ->+                                  Specif.Coq_sig2 ScanStateDesc+moveActiveToHandled sd x =+  Build_ScanStateDesc (nextInterval sd)+    (intervals sd) (fixedIntervals sd)+    (unhandled sd)+    (unsafeCoerce+      (Seq.rem+        (Eqtype.prod_eqType+          (Fintype.ordinal_eqType (nextInterval sd))+          (Fintype.ordinal_eqType maxReg)) x+        (unsafeCoerce (active sd)))) (inactive sd) ((:)+    (unsafeCoerce x) (handled sd))++moveActiveToInactive :: ScanStateDesc ->+                                   Eqtype.Equality__Coq_sort ->+                                   Specif.Coq_sig2 ScanStateDesc+moveActiveToInactive sd x =+  Build_ScanStateDesc (nextInterval sd)+    (intervals sd) (fixedIntervals sd)+    (unhandled sd)+    (unsafeCoerce+      (Seq.rem+        (Eqtype.prod_eqType+          (Fintype.ordinal_eqType (nextInterval sd))+          (Fintype.ordinal_eqType maxReg)) x+        (unsafeCoerce (active sd)))) ((:) (unsafeCoerce x)+    (inactive sd)) (handled sd)++moveInactiveToActive :: ScanStateDesc ->+                                   Eqtype.Equality__Coq_sort ->+                                   Specif.Coq_sig2 ScanStateDesc+moveInactiveToActive sd x =+  Build_ScanStateDesc (nextInterval sd)+    (intervals sd) (fixedIntervals sd)+    (unhandled sd) ((:) (unsafeCoerce x) (active sd))+    (unsafeCoerce+      (Seq.rem+        (Eqtype.prod_eqType+          (Fintype.ordinal_eqType (nextInterval sd))+          (Fintype.ordinal_eqType maxReg)) x+        (unsafeCoerce (inactive sd)))) (handled sd)++moveInactiveToHandled :: ScanStateDesc ->+                                    Eqtype.Equality__Coq_sort ->+                                    Specif.Coq_sig2 ScanStateDesc+moveInactiveToHandled sd x =+  Build_ScanStateDesc (nextInterval sd)+    (intervals sd) (fixedIntervals sd)+    (unhandled sd) (active sd)+    (unsafeCoerce+      (Seq.rem+        (Eqtype.prod_eqType+          (Fintype.ordinal_eqType (nextInterval sd))+          (Fintype.ordinal_eqType maxReg)) x+        (unsafeCoerce (inactive sd)))) ((:) (unsafeCoerce x)+    (handled sd))++distance :: Prelude.Int -> Prelude.Int -> Prelude.Int+distance n m =+  case (Prelude.<=) ((Prelude.succ) n) m of {+   Prelude.True -> (Prelude.-) m n;+   Prelude.False -> (Prelude.-) n m}++splitCurrentInterval :: ScanStateDesc -> (Prelude.Maybe+                                   Prelude.Int) -> SState a1 +                                   () ()+splitCurrentInterval pre before ssi =+  let {+   _evar_0_ = \desc holds ->+    let {+     _evar_0_ = \_nextInterval_ intervals0 _fixedIntervals_ unhandled0 _active_ _inactive_ _handled_ ->+      let {_evar_0_ = \holds0 -> Logic.coq_False_rect} in+      let {+       _evar_0_0 = \_top_assumption_ ->+        let {+         _evar_0_0 = \uid beg us holds0 ->+          let {int = LinearScan.Utils.nth _nextInterval_ intervals0 uid} in+          let {+           _evar_0_0 = \_ -> Prelude.Left (ECannotSplitSingleton+            ( uid))}+          in+          let {+           _evar_0_1 = \_ -> Prelude.Right ((,) ()+            ((Prelude.flip (Prelude.$)) __ (\_ ->+              let {+               _top_assumption_0 = Interval.splitPosition ( int) before+                                     Prelude.True}+              in+              let {+               _top_assumption_1 = Interval.splitInterval _top_assumption_0+                                     ( int)}+              in+              let {+               _evar_0_1 = \_top_assumption_2 _top_assumption_3 ->+                let {+                 _evar_0_1 = \_ ->+                  (Prelude.flip (Prelude.$)) __ (\_ ->+                    (Prelude.flip (Prelude.$)) __+                      ((Prelude.flip (Prelude.$)) __+                        ((Prelude.flip (Prelude.$)) __ (\_ _ _ ->+                          (Prelude.flip (Prelude.$)) __+                            ((Prelude.flip (Prelude.$)) __+                              (let {+                                new_unhandled_added = Build_ScanStateDesc+                                 ((Prelude.succ) _nextInterval_)+                                 (LinearScan.Utils.snoc _nextInterval_+                                   (LinearScan.Utils.set_nth _nextInterval_+                                     intervals0 uid _top_assumption_2)+                                   _top_assumption_3) _fixedIntervals_+                                 (Data.List.insertBy+                                   (Data.Ord.comparing Prelude.snd) ((,)+                                   ( _nextInterval_)+                                   (Interval.ibeg _top_assumption_3)) ((:)+                                   (Prelude.id ((,) uid beg))+                                   (Prelude.map Prelude.id us)))+                                 (Prelude.map Prelude.id _active_)+                                 (Prelude.map Prelude.id _inactive_)+                                 (Prelude.map Prelude.id _handled_)}+                               in+                               \_ _ -> Build_SSInfo+                               new_unhandled_added __))))))}+                in+                 _evar_0_1 __}+              in+              case _top_assumption_1 of {+               (,) x x0 -> _evar_0_1 x x0})))}+          in+          case Interval.coq_Interval_is_singleton ( int) of {+           Prelude.True -> _evar_0_0 __;+           Prelude.False -> _evar_0_1 __}}+        in+        (\us _ _ _ _ _ holds0 _ _ ->+        case _top_assumption_ of {+         (,) x x0 -> _evar_0_0 x x0 us holds0})}+      in+      case unhandled0 of {+       [] -> (\_ _ _ _ holds0 _ _ -> _evar_0_ holds0);+       (:) x x0 -> _evar_0_0 x x0 __}}+    in+    case desc of {+     Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->+      _evar_0_ x x0 x1 x2 x3 x4 x5 __ __ __ __ holds __}}+  in+  case ssi of {+   Build_SSInfo x x0 -> _evar_0_ x x0 __}++create_ssinfo :: Prelude.Int -> ([] Interval.IntervalDesc) ->+                            Coq_fixedIntervalsType -> ([]+                            ((,) Prelude.Int Prelude.Int)) -> ([]+                            ((,) Prelude.Int PhysReg)) -> ([]+                            ((,) Prelude.Int PhysReg)) -> ([]+                            ((,) Prelude.Int PhysReg)) ->+                            ScanStateDesc -> Prelude.Int ->+                            Prelude.Int -> Interval.IntervalDesc ->+                            Interval.IntervalDesc -> ([]+                            ((,) Prelude.Int PhysReg)) -> ([]+                            ((,) Prelude.Int PhysReg)) ->+                            SSInfo ()+create_ssinfo ni intervals0 fixedIntervals0 unh active0 inactive0 handled0 pre aid pos' id0 id1 active1 inactive1 =+  let {+   new_inactive_added = Build_ScanStateDesc ((Prelude.succ) ni)+    (LinearScan.Utils.snoc ni+      (LinearScan.Utils.set_nth ni intervals0 aid id0) id1) fixedIntervals0+    (Prelude.map (\i -> Prelude.id i) unh) active1 inactive1+    (Prelude.map (\i -> Prelude.id i) handled0)}+  in+  Build_SSInfo new_inactive_added __++splitAssignedIntervalForReg :: ScanStateDesc ->+                                          PhysReg -> (Prelude.Maybe+                                          Prelude.Int) -> Prelude.Bool ->+                                          SState a1 () ()+splitAssignedIntervalForReg pre reg pos trueForActives ssi =+  let {+   _evar_0_ = \desc holds ->+    let {+     intlist = case trueForActives of {+                Prelude.True -> active desc;+                Prelude.False -> inactive desc}}+    in+    (Prelude.flip (Prelude.$)) __ (\_ ->+      let {+       intids = Prelude.map (\i -> Prelude.fst i)+                  (Prelude.filter (\i ->+                    Eqtype.eq_op (Fintype.ordinal_eqType maxReg)+                      (Prelude.snd (unsafeCoerce i)) (unsafeCoerce reg))+                    intlist)}+      in+      (Prelude.flip (Prelude.$)) __ (\_ ->+        let {+         _evar_0_ = \_ ->+          let {+           _evar_0_ = \ni intervals0 _fixedIntervals_ unh active0 _inactive_ _handled_ holds0 intlist0 intids0 ->+            let {_evar_0_ = \_ -> Prelude.Left ENoIntervalsToSplit}+            in+            let {+             _evar_0_0 = \aid aids iHaids ->+              let {int = LinearScan.Utils.nth ni intervals0 aid} in+              let {_evar_0_0 = \_ -> iHaids __} in+              let {+               _evar_0_1 = \_ ->+                (Prelude.flip (Prelude.$)) __ (\_ ->+                  let {+                   _top_assumption_ = Interval.splitPosition ( int) pos+                                        Prelude.False}+                  in+                  let {_evar_0_1 = iHaids __} in+                  let {+                   _evar_0_2 = Prelude.Right ((,) ()+                    (let {+                      _top_assumption_0 = Interval.splitInterval+                                            _top_assumption_ ( int)}+                     in+                     let {+                      _evar_0_2 = \_top_assumption_1 _top_assumption_2 ->+                       let {+                        _evar_0_2 = \_ ->+                         (Prelude.flip (Prelude.$)) __ (\_ ->+                           let {+                            _evar_0_2 = \_ _ ->+                             (Prelude.flip (Prelude.$)) __+                               (let {+                                 _evar_0_2 = \_ ->+                                  (Prelude.flip (Prelude.$)) __ (\_ ->+                                    create_ssinfo ni intervals0+                                      _fixedIntervals_ unh active0 _inactive_+                                      _handled_ pre aid _top_assumption_+                                      _top_assumption_1 _top_assumption_2+                                      (Prelude.map (unsafeCoerce Prelude.id)+                                        (Seq.rem+                                          (Eqtype.prod_eqType+                                            (Fintype.ordinal_eqType ni)+                                            (Fintype.ordinal_eqType+                                              maxReg))+                                          (unsafeCoerce ((,) aid reg))+                                          intlist0)) ((:) ((,) ( ni) reg)+                                      ((:) (Prelude.id ((,) aid reg))+                                      (Prelude.map Prelude.id _inactive_))))}+                                in+                                 _evar_0_2)}+                           in+                           let {+                            _evar_0_3 = \_ _ ->+                             (Prelude.flip (Prelude.$)) __ (\_ ->+                               create_ssinfo ni intervals0+                                 _fixedIntervals_ unh active0 _inactive_+                                 _handled_ pre aid _top_assumption_+                                 _top_assumption_1 _top_assumption_2+                                 (Prelude.map Prelude.id active0) ((:) ((,)+                                 ( ni) reg)+                                 (Prelude.map Prelude.id _inactive_)))}+                           in+                           case trueForActives of {+                            Prelude.True -> _evar_0_2 __ __;+                            Prelude.False -> _evar_0_3 __ __})}+                       in+                        _evar_0_2 __}+                     in+                     case _top_assumption_0 of {+                      (,) x x0 -> _evar_0_2 x x0}))}+                  in+                  case Eqtype.eq_op (Eqtype.option_eqType Ssrnat.nat_eqType)+                         (unsafeCoerce pos)+                         (unsafeCoerce (Prelude.Just+                           (Prelude.pred _top_assumption_))) of {+                   Prelude.True -> _evar_0_1;+                   Prelude.False -> _evar_0_2})}+              in+              case Interval.coq_Interval_is_singleton ( int) of {+               Prelude.True -> _evar_0_0 __;+               Prelude.False -> _evar_0_1 __}}+            in+            Datatypes.list_rect _evar_0_ (\aid aids iHaids _ ->+              _evar_0_0 aid aids iHaids) intids0 __}+          in+          (\intlist0 _ intids0 _ ->+          case desc of {+           Build_ScanStateDesc x x0 x1 x2 x3 x4 x5 ->+            _evar_0_ x x0 x1 x2 x3 x4 x5 holds intlist0 intids0})}+        in+        unsafeCoerce _evar_0_ __ intlist __ intids __))}+  in+  case ssi of {+   Build_SSInfo x x0 -> _evar_0_ x x0}++splitActiveIntervalForReg :: ScanStateDesc ->+                                        PhysReg -> Prelude.Int ->+                                        SState a1 () ()+splitActiveIntervalForReg pre reg pos =+  splitAssignedIntervalForReg pre reg (Prelude.Just pos)+    Prelude.True++splitAnyInactiveIntervalForReg :: ScanStateDesc ->+                                             PhysReg ->+                                             SState a1 () ()+splitAnyInactiveIntervalForReg pre reg ss =+  (Prelude.flip (Prelude.$)) (\s _ _ ->+    splitAssignedIntervalForReg s reg Prelude.Nothing+      Prelude.False) (\_top_assumption_ ->+    let {_top_assumption_0 = _top_assumption_ pre __ __} in+    let {_top_assumption_1 = _top_assumption_0 ss} in+    let {+     _evar_0_ = \err -> Prelude.Right ((,) () (Build_SSInfo+      (thisDesc pre ss) __))}+    in+    let {+     _evar_0_0 = \_top_assumption_2 ->+      let {_evar_0_0 = \_the_1st_wildcard_ ss' -> Prelude.Right ((,) () ss')}+      in+      case _top_assumption_2 of {+       (,) x x0 -> _evar_0_0 x x0}}+    in+    case _top_assumption_1 of {+     Prelude.Left x -> _evar_0_ x;+     Prelude.Right x -> _evar_0_0 x})++intersectsWithFixedInterval :: ScanStateDesc ->+                                          PhysReg ->+                                          SState a1 a1+                                          (Prelude.Maybe Prelude.Int)+intersectsWithFixedInterval pre reg =+  (Prelude.$) (withCursor pre) (\sd _ ->+    let {int = curIntDetails sd} in+    (Prelude.$) return_+      (LinearScan.Utils.vfoldl' maxReg (\mx v ->+        Lib.option_choose mx+          (case v of {+            Prelude.Just i -> Interval.intervalIntersectionPoint ( int) ( i);+            Prelude.Nothing -> Prelude.Nothing})) Prelude.Nothing+        (fixedIntervals sd)))++tryAllocateFreeReg :: ScanStateDesc -> SState+                                 a1 a1+                                 (Prelude.Maybe+                                 (SState a1 () PhysReg))+tryAllocateFreeReg pre =+  (Prelude.$) (withCursor pre) (\sd _ ->+    let {+     go = \n ->+      Data.List.foldl' (\v p ->+        case p of {+         (,) i r -> LinearScan.Utils.set_nth maxReg v r (n i)})}+    in+    let {+     freeUntilPos' = go (\x -> Prelude.Just 0)+                       (Data.List.replicate maxReg+                         Prelude.Nothing) (active sd)}+    in+    let {+     intersectingIntervals = Prelude.filter (\x ->+                               Interval.intervalsIntersect+                                 ( (curIntDetails sd))+                                 (+                                   (LinearScan.Utils.nth+                                     (nextInterval sd)+                                     (intervals sd)+                                     (Prelude.fst x))))+                               (inactive sd)}+    in+    let {+     freeUntilPos = go (\i ->+                      Interval.intervalIntersectionPoint+                        (+                          (LinearScan.Utils.nth (nextInterval sd)+                            (intervals sd) i))+                        ( (curIntDetails sd))) freeUntilPos'+                      intersectingIntervals}+    in+    case registerWithHighestPos freeUntilPos of {+     (,) reg mres ->+      let {+       success = stbind (\x -> return_ reg)+                   (moveUnhandledToActive pre reg)}+      in+      let {+       maction = case mres of {+                  Prelude.Just n ->+                   case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce n)+                          (unsafeCoerce 0) of {+                    Prelude.True -> Prelude.Nothing;+                    Prelude.False -> Prelude.Just+                     (case (Prelude.<=) ((Prelude.succ)+                             (Interval.intervalEnd+                               ( (curIntDetails sd)))) n of {+                       Prelude.True -> success;+                       Prelude.False ->+                        stbind (\x ->+                          stbind (\x0 -> return_ reg)+                            (moveUnhandledToActive pre reg))+                          (splitCurrentInterval pre (Prelude.Just+                            n))})};+                  Prelude.Nothing -> Prelude.Just success}}+      in+      return_ maction})++allocateBlockedReg :: ScanStateDesc -> SState+                                 a1 () (Prelude.Maybe PhysReg)+allocateBlockedReg pre =+  (Prelude.$) (withCursor pre) (\sd _ ->+    let {start = Interval.intervalStart ( (curIntDetails sd))} in+    let {pos = curPosition sd} in+    let {+     go = \v p ->+      case p of {+       (,) i r ->+        let {+         atPos = \u ->+          Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce pos)+            (unsafeCoerce (Range.uloc u))}+        in+        let {+         pos' = case Interval.findIntervalUsePos+                       (+                         (LinearScan.Utils.nth (nextInterval sd)+                           (intervals sd) i)) atPos of {+                 Prelude.Just p0 -> Prelude.Just 0;+                 Prelude.Nothing ->+                  Interval.nextUseAfter+                    (+                      (LinearScan.Utils.nth (nextInterval sd)+                        (intervals sd) i)) start}}+        in+        LinearScan.Utils.set_nth maxReg v r pos'}}+    in+    let {+     nextUsePos' = Data.List.foldl' go+                     (Data.List.replicate maxReg Prelude.Nothing)+                     (active sd)}+    in+    let {+     intersectingIntervals = Prelude.filter (\x ->+                               Interval.intervalsIntersect+                                 ( (curIntDetails sd))+                                 (+                                   (LinearScan.Utils.nth+                                     (nextInterval sd)+                                     (intervals sd)+                                     (Prelude.fst x))))+                               (inactive sd)}+    in+    let {nextUsePos = Data.List.foldl' go nextUsePos' intersectingIntervals}+    in+    case registerWithHighestPos nextUsePos of {+     (,) reg mres ->+      case case mres of {+            Prelude.Just n -> (Prelude.<=) ((Prelude.succ) n) start;+            Prelude.Nothing -> Prelude.False} of {+       Prelude.True ->+        stbind (\x ->+          stbind (\mloc ->+            stbind (\x0 ->+              stbind (\x1 -> return_ Prelude.Nothing)+                (weakenStHasLenToSt pre))+              (case mloc of {+                Prelude.Just n ->+                 splitCurrentInterval pre (Prelude.Just n);+                Prelude.Nothing -> return_ ()}))+            (intersectsWithFixedInterval pre reg))+          (splitCurrentInterval pre+            (Interval.firstUseReqReg ( (curIntDetails sd))));+       Prelude.False ->+        stbind (\x ->+          stbind (\x0 ->+            stbind (\mloc ->+              stbind (\x1 ->+                return_ (Prelude.Just reg))+                (case mloc of {+                  Prelude.Just n ->+                   stbind (\x1 ->+                     moveUnhandledToActive pre reg)+                     (splitCurrentInterval pre (Prelude.Just n));+                  Prelude.Nothing -> moveUnhandledToActive pre reg}))+              (intersectsWithFixedInterval pre reg))+            (splitActiveIntervalForReg pre reg pos))+          (splitAnyInactiveIntervalForReg pre reg)}})++morphlen_transport :: ScanStateDesc ->+                                 ScanStateDesc ->+                                 IntervalId -> IntervalId+morphlen_transport b b' = GHC.Base.id+  ++mt_fst :: ScanStateDesc -> ScanStateDesc ->+                     ((,) IntervalId PhysReg) -> (,)+                     IntervalId PhysReg+mt_fst b b' x =+  case x of {+   (,) xid reg -> (,) (morphlen_transport b b' xid) reg}++type Coq_int_reg_seq =+  [] ((,) IntervalId PhysReg)++type Coq_intermediate_result =+  Specif.Coq_sig2 ScanStateDesc++goActive :: Prelude.Int -> ScanStateDesc ->+                       ScanStateDesc -> ((,) IntervalId+                       PhysReg) -> Coq_int_reg_seq ->+                       Coq_intermediate_result+goActive pos sd z x xs =+  case (Prelude.<=) ((Prelude.succ)+         (Interval.intervalEnd+           (+             (LinearScan.Utils.nth (nextInterval z)+               (intervals z) (Prelude.fst x))))) pos of {+   Prelude.True -> moveActiveToHandled z (unsafeCoerce x);+   Prelude.False ->+    case Prelude.not+           (Interval.intervalCoversPos+             (+               (LinearScan.Utils.nth (nextInterval z)+                 (intervals z) (Prelude.fst x))) pos) of {+     Prelude.True -> moveActiveToInactive z (unsafeCoerce x);+     Prelude.False -> z}}++checkActiveIntervals :: ScanStateDesc -> Prelude.Int ->+                                   SState () () ()+checkActiveIntervals pre pos =+  (Prelude.$) (withScanStatePO pre) (\sd _ ->+    let {+     res = Lib.dep_foldl_inv (\s ->+             Eqtype.prod_eqType+               (Fintype.ordinal_eqType (nextInterval s))+               (Fintype.ordinal_eqType maxReg)) sd+             (unsafeCoerce (active sd))+             (Data.List.length (active sd))+             (unsafeCoerce active)+             (unsafeCoerce (\x x0 _ -> mt_fst x x0))+             (unsafeCoerce (\x _ x0 x1 _ ->+               goActive pos sd x x0 x1))}+    in+    IState.iput (Build_SSInfo res __))++moveInactiveToActive' :: ScanStateDesc -> ((,)+                                    IntervalId PhysReg)+                                    -> Coq_int_reg_seq ->+                                    Prelude.Either SSError+                                    (Specif.Coq_sig2 ScanStateDesc)+moveInactiveToActive' z x xs =+  let {+   filtered_var = Prelude.not+                    (Ssrbool.in_mem (Prelude.snd (unsafeCoerce x))+                      (Ssrbool.mem+                        (Seq.seq_predType+                          (Fintype.ordinal_eqType maxReg))+                        (unsafeCoerce+                          (Prelude.map (\i -> Prelude.snd i)+                            (active z)))))}+  in+  case filtered_var of {+   Prelude.True ->+    let {filtered_var0 = moveInactiveToActive z (unsafeCoerce x)}+    in+    Prelude.Right filtered_var0;+   Prelude.False -> Prelude.Left (ERegisterAssignmentsOverlap+    ( (Prelude.snd x)))}++goInactive :: Prelude.Int -> ScanStateDesc ->+                         ScanStateDesc -> ((,) IntervalId+                         PhysReg) -> Coq_int_reg_seq ->+                         Prelude.Either SSError+                         Coq_intermediate_result+goInactive pos sd z x xs =+  let {f = \sd' -> Prelude.Right sd'} in+  case (Prelude.<=) ((Prelude.succ)+         (Interval.intervalEnd+           (+             (LinearScan.Utils.nth (nextInterval z)+               (intervals z) (Prelude.fst x))))) pos of {+   Prelude.True ->+    let {filtered_var = moveInactiveToHandled z (unsafeCoerce x)}+    in+    f filtered_var;+   Prelude.False ->+    case Interval.intervalCoversPos+           (+             (LinearScan.Utils.nth (nextInterval z)+               (intervals z) (Prelude.fst x))) pos of {+     Prelude.True ->+      let {filtered_var = moveInactiveToActive' z x xs} in+      case filtered_var of {+       Prelude.Left err -> Prelude.Left err;+       Prelude.Right s -> f s};+     Prelude.False -> f z}}++checkInactiveIntervals :: ScanStateDesc -> Prelude.Int+                                     -> SState () () ()+checkInactiveIntervals pre pos =+  (Prelude.$) (withScanStatePO pre) (\sd _ ->+    let {+     eres = Lib.dep_foldl_invE (\s ->+              Eqtype.prod_eqType+                (Fintype.ordinal_eqType (nextInterval s))+                (Fintype.ordinal_eqType maxReg)) sd+              (unsafeCoerce (inactive sd))+              (Data.List.length (inactive sd))+              (unsafeCoerce inactive)+              (unsafeCoerce (\x x0 _ -> mt_fst x x0))+              (unsafeCoerce (\x _ x0 x1 _ ->+                goInactive pos sd x x0 x1))}+    in+    case eres of {+     Prelude.Left err -> IState.ierr err;+     Prelude.Right s -> IState.iput (Build_SSInfo s __)})++handleInterval :: ScanStateDesc -> SState +                             () () (Prelude.Maybe PhysReg)+handleInterval pre =+  (Prelude.$) (unsafeCoerce (withCursor pre)) (\sd _ ->+    let {position = curPosition sd} in+    stbind (\x ->+      stbind (\x0 ->+        stbind (\mres ->+          case mres of {+           Prelude.Just x1 ->+            IEndo.imap (unsafeCoerce IState.coq_IState_IFunctor) (\x2 ->+              Prelude.Just x2) x1;+           Prelude.Nothing ->+            unsafeCoerce (allocateBlockedReg pre)})+          (tryAllocateFreeReg pre))+        (liftLen pre (\sd0 ->+          checkInactiveIntervals sd0 position)))+      (liftLen pre (\sd0 ->+        checkActiveIntervals sd0 position)))++walkIntervals_func :: ((,) ScanStateDesc ()) ->+                                 Prelude.Either SSError+                                 ScanStateDesc+walkIntervals_func x =+  let {sd = Prelude.fst x} in+  let {+   walkIntervals0 = \sd0 ->+    let {y = (,) sd0 __} in walkIntervals_func ( y)}+  in+  let {filtered_var = LinearScan.Utils.uncons (unhandled sd)} in+  case filtered_var of {+   Prelude.Just s ->+    let {ssinfo = Build_SSInfo sd __} in+    let {+     filtered_var0 = IState.runIState (handleInterval sd) ssinfo}+    in+    case filtered_var0 of {+     Prelude.Left err -> Prelude.Left err;+     Prelude.Right p ->+      case p of {+       (,) wildcard' ssinfo' ->+        walkIntervals0 (thisDesc sd ssinfo')}};+   Prelude.Nothing -> Prelude.Right (packScanState sd)}++walkIntervals :: ScanStateDesc -> Prelude.Either+                            SSError ScanStateDesc+walkIntervals sd =+  walkIntervals_func ((,) sd __)++mainAlgorithm :: IState.IState SSError BlockList+                 BlockList ()+mainAlgorithm =+  stbind (\x ->+    stbind (\x0 ->+      stbind (\x1 ->+        stbind (\x2 ->+          stbind (\ssig ->+            case walkIntervals ( ssig) of {+             Prelude.Left err -> error_ err;+             Prelude.Right ssig' ->+              stbind (\x3 -> assignRegNum ( ssig'))+                resolveDataFlow}) buildIntervals)+          computeGlobalLiveSets) computeLocalLiveSets)+      numberOperations) computeBlockOrder++linearScan :: BlockList -> Prelude.Either SSError+              BlockList+linearScan blocks =+  case IState.runIState mainAlgorithm blocks of {+   Prelude.Left err -> Prelude.Left err;+   Prelude.Right p ->+    case p of {+     (,) u res -> Prelude.Right res}}+
+ LinearScan/NonEmpty0.hs view
@@ -0,0 +1,24 @@+module LinearScan.NonEmpty0 where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils+++coq_NE_mapAccumL :: (a1 -> a2 -> (,) a1 a3) -> a1 -> ([] a2) -> (,) a1+                    ([] a3)+coq_NE_mapAccumL f s v =+  (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+    (\x ->+    case f s x of {+     (,) s' y -> (,) s' ((:[]) y)})+    (\x xs ->+    case f s x of {+     (,) s' y ->+      case coq_NE_mapAccumL f s' xs of {+       (,) s'' ys -> (,) s'' ((:) y ys)}})+    v+
+ LinearScan/Range.hs view
@@ -0,0 +1,130 @@+module LinearScan.Range where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Lib as Lib+++__ :: any+__ = Prelude.error "Logical or arity value used"++data UsePos =+   Build_UsePos Prelude.Int Prelude.Bool++uloc :: UsePos -> Prelude.Int+uloc u =+  case u of {+   Build_UsePos uloc0 regReq0 -> uloc0}++regReq :: UsePos -> Prelude.Bool+regReq u =+  case u of {+   Build_UsePos uloc0 regReq0 -> regReq0}++type UsePosSublistsOf =+  ((,) (Prelude.Maybe ([] UsePos)) (Prelude.Maybe ([] UsePos)))++usePosSpan :: (UsePos -> Prelude.Bool) -> ([] UsePos) -> UsePosSublistsOf+usePosSpan f l =+  (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+    (\x ->+    let {b = f x} in+    case b of {+     Prelude.True -> (,) (Prelude.Just ((:[]) x)) Prelude.Nothing;+     Prelude.False -> (,) Prelude.Nothing (Prelude.Just ((:[]) x))})+    (\x xs ->+    let {b = f x} in+    case b of {+     Prelude.True ->+      let {u = usePosSpan f xs} in+      case u of {+       (,) o x0 ->+        case o of {+         Prelude.Just l1 ->+          case x0 of {+           Prelude.Just l2 -> (,) (Prelude.Just ((:) x l1)) (Prelude.Just l2);+           Prelude.Nothing -> (,) (Prelude.Just ((:) x l1)) Prelude.Nothing};+         Prelude.Nothing ->+          case x0 of {+           Prelude.Just l2 -> (,) (Prelude.Just ((:[]) x)) (Prelude.Just l2);+           Prelude.Nothing -> Prelude.error "absurd case"}}};+     Prelude.False -> (,) Prelude.Nothing (Prelude.Just ((:) x xs))})+    l++data RangeDesc =+   Build_RangeDesc Prelude.Int Prelude.Int ([] UsePos)++rbeg :: RangeDesc -> Prelude.Int+rbeg r =+  case r of {+   Build_RangeDesc rbeg0 rend0 ups0 -> rbeg0}++rend :: RangeDesc -> Prelude.Int+rend r =+  case r of {+   Build_RangeDesc rbeg0 rend0 ups0 -> rend0}++ups :: RangeDesc -> [] UsePos+ups r =+  case r of {+   Build_RangeDesc rbeg0 rend0 ups0 -> ups0}++rangesIntersect :: RangeDesc -> RangeDesc -> Prelude.Bool+rangesIntersect x y =+  case (Prelude.<=) ((Prelude.succ) (rbeg x)) (rbeg y) of {+   Prelude.True -> (Prelude.<=) ((Prelude.succ) (rbeg y)) (rend x);+   Prelude.False -> (Prelude.<=) ((Prelude.succ) (rbeg x)) (rend y)}++rangeIntersectionPoint :: RangeDesc -> RangeDesc -> Prelude.Maybe Prelude.Int+rangeIntersectionPoint x y =+  case rangesIntersect x y of {+   Prelude.True -> Prelude.Just (Prelude.min (rbeg x) (rbeg y));+   Prelude.False -> Prelude.Nothing}++findRangeUsePos :: RangeDesc -> (UsePos -> Prelude.Bool) -> Prelude.Maybe+                   UsePos+findRangeUsePos r f =+  let {+   go xs =+     (\ns nc l -> case l of [x] -> ns x; (x:xs) -> nc x xs)+       (\x ->+       case f x of {+        Prelude.True -> Prelude.Just x;+        Prelude.False -> Prelude.Nothing})+       (\x xs0 ->+       case f x of {+        Prelude.True -> Prelude.Just x;+        Prelude.False -> go xs0})+       xs}+  in go (ups r)++makeDividedRange :: (UsePos -> Prelude.Bool) -> RangeDesc -> ([] UsePos) ->+                    ([] UsePos) ->+                    ((,) (Prelude.Maybe RangeDesc) (Prelude.Maybe RangeDesc))+makeDividedRange f rd l1 l2 =+  case rd of {+   Build_RangeDesc rbeg0 rend0 ups0 ->+     (\_ -> (,) (Prelude.Just (Build_RangeDesc rbeg0 ((Prelude.succ)+      (uloc (Prelude.last l1))) l1)) (Prelude.Just (Build_RangeDesc+      (uloc (Prelude.head l2)) rend0 l2))) __}++rangeSpan :: (UsePos -> Prelude.Bool) -> RangeDesc ->+             ((,) (Prelude.Maybe RangeDesc) (Prelude.Maybe RangeDesc))+rangeSpan f rd =+  case usePosSpan f (ups rd) of {+   (,) o o0 ->+    case o of {+     Prelude.Just l1 ->+      case o0 of {+       Prelude.Just l2 -> makeDividedRange f rd l1 l2;+       Prelude.Nothing -> (,) (Prelude.Just rd) Prelude.Nothing};+     Prelude.Nothing ->+      case o0 of {+       Prelude.Just n -> (,) Prelude.Nothing (Prelude.Just rd);+       Prelude.Nothing -> Lib.ex_falso_quodlibet}}}+
+ LinearScan/Seq.hs view
@@ -0,0 +1,100 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Seq where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Ssrbool as Ssrbool+import qualified LinearScan.Ssrnat as Ssrnat++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++ncons :: Prelude.Int -> a1 -> ([] a1) -> [] a1+ncons n x =+  Ssrnat.iter n (\x0 -> (:) x x0)++nseq :: Prelude.Int -> a1 -> [] a1+nseq n x =+  ncons n x []++nth :: a1 -> ([] a1) -> Prelude.Int -> a1+nth x0 s n =+  case s of {+   [] -> x0;+   (:) x s' ->+    (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))+      (\_ ->+      x)+      (\n' ->+      nth x0 s' n')+      n}++set_nth :: a1 -> ([] a1) -> Prelude.Int -> a1 -> [] a1+set_nth x0 s n y =+  case s of {+   [] -> ncons n x0 ((:) y []);+   (:) x s' ->+    (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))+      (\_ -> (:) y+      s')+      (\n' -> (:) x+      (set_nth x0 s' n' y))+      n}++catrev :: ([] a1) -> ([] a1) -> [] a1+catrev s1 s2 =+  case s1 of {+   [] -> s2;+   (:) x s1' -> catrev s1' ((:) x s2)}++rev :: ([] a1) -> [] a1+rev s =+  catrev s []++mem_seq :: Eqtype.Equality__Coq_type -> ([] Eqtype.Equality__Coq_sort) ->+           Eqtype.Equality__Coq_sort -> Prelude.Bool+mem_seq t s =+  case s of {+   [] -> (\x -> Prelude.False);+   (:) y s' ->+    let {p = mem_seq t s'} in (\x -> (Prelude.||) (Eqtype.eq_op t x y) (p x))}++type Coq_eqseq_class = [] Eqtype.Equality__Coq_sort++pred_of_eq_seq :: Eqtype.Equality__Coq_type -> Coq_eqseq_class ->+                  Ssrbool.Coq_pred_sort Eqtype.Equality__Coq_sort+pred_of_eq_seq t s =+  unsafeCoerce (\x -> mem_seq t s x)++seq_predType :: Eqtype.Equality__Coq_type -> Ssrbool.Coq_predType+                Eqtype.Equality__Coq_sort+seq_predType t =+  Ssrbool.mkPredType (unsafeCoerce (pred_of_eq_seq t))++rem :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> ([]+       Eqtype.Equality__Coq_sort) -> [] Eqtype.Equality__Coq_sort+rem t x s =+  case s of {+   [] -> s;+   (:) y t0 ->+    case Eqtype.eq_op t y x of {+     Prelude.True -> t0;+     Prelude.False -> (:) y (rem t x t0)}}+
+ LinearScan/Specif.hs view
@@ -0,0 +1,18 @@+module LinearScan.Specif where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils+++type Coq_sig a =+  a+  -- singleton inductive, whose constructor was exist+  +type Coq_sig2 a =+  a+  -- singleton inductive, whose constructor was exist2+
+ LinearScan/Ssrbool.hs view
@@ -0,0 +1,96 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Ssrbool where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++__ :: any+__ = Prelude.error "Logical or arity value used"++isSome :: (Prelude.Maybe a1) -> Prelude.Bool+isSome u =+  case u of {+   Prelude.Just t -> Prelude.True;+   Prelude.Nothing -> Prelude.False}++data Coq_reflect =+   ReflectT+ | ReflectF++iffP :: Prelude.Bool -> Coq_reflect -> Coq_reflect+iffP b pb =+  let {_evar_0_ = \_ _ _ -> ReflectT} in+  let {_evar_0_0 = \_ _ _ -> ReflectF} in+  case pb of {+   ReflectT -> _evar_0_ __ __ __;+   ReflectF -> _evar_0_0 __ __ __}++idP :: Prelude.Bool -> Coq_reflect+idP b1 =+  case b1 of {+   Prelude.True -> ReflectT;+   Prelude.False -> ReflectF}++andP :: Prelude.Bool -> Prelude.Bool -> Coq_reflect+andP b1 b2 =+  case b1 of {+   Prelude.True ->+    case b2 of {+     Prelude.True -> ReflectT;+     Prelude.False -> ReflectF};+   Prelude.False -> ReflectF}++type Coq_pred t = t -> Prelude.Bool++type Coq_rel t = t -> Coq_pred t++type Coq_simpl_rel t = (->) t (Coq_pred t)++rel_of_simpl_rel :: (Coq_simpl_rel a1) -> Coq_rel a1+rel_of_simpl_rel r x y =+  (Prelude.$) r x y++data Coq_mem_pred t =+   Mem (Coq_pred t)++data Coq_predType t =+   PredType (() -> Coq_pred t) (() -> Coq_mem_pred t)++type Coq_pred_sort t = ()++mkPredType :: (a2 -> a1 -> Prelude.Bool) -> Coq_predType a1+mkPredType toP =+  PredType (unsafeCoerce toP) (\p -> Mem (\x -> unsafeCoerce toP p x))++pred_of_mem :: (Coq_mem_pred a1) -> Coq_pred_sort a1+pred_of_mem mp =+  case mp of {+   Mem p -> unsafeCoerce (\x -> p x)}++mem :: (Coq_predType a1) -> (Coq_pred_sort a1) -> Coq_mem_pred a1+mem pT =+  case pT of {+   PredType topred s -> s}++in_mem :: a1 -> (Coq_mem_pred a1) -> Prelude.Bool+in_mem x mp =+  unsafeCoerce (\_ -> pred_of_mem) __ mp x+
+ LinearScan/Ssrfun.hs view
@@ -0,0 +1,29 @@+module LinearScan.Ssrfun where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils+++_Option__apply :: (a1 -> a2) -> a2 -> (Prelude.Maybe a1) -> a2+_Option__apply f x u =+  case u of {+   Prelude.Just y -> f y;+   Prelude.Nothing -> x}++_Option__coq_default :: a1 -> (Prelude.Maybe a1) -> a1+_Option__coq_default =+  _Option__apply (\x -> x)++_Option__bind :: (a1 -> Prelude.Maybe a2) -> (Prelude.Maybe a1) ->+                 Prelude.Maybe a2+_Option__bind f =+  _Option__apply f Prelude.Nothing++_Option__map :: (a1 -> a2) -> (Prelude.Maybe a1) -> Prelude.Maybe a2+_Option__map f =+  _Option__bind (\x -> Prelude.Just (f x))+
+ LinearScan/Ssrnat.hs view
@@ -0,0 +1,61 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Ssrnat where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++import qualified LinearScan.Eqtype as Eqtype+import qualified LinearScan.Ssrbool as Ssrbool++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif++eqnP :: Eqtype.Equality__Coq_axiom Prelude.Int+eqnP n m =+  Ssrbool.iffP ((Prelude.==) n m) (Ssrbool.idP ((Prelude.==) n m))++nat_eqMixin :: Eqtype.Equality__Coq_mixin_of Prelude.Int+nat_eqMixin =+  Eqtype.Equality__Mixin (Prelude.==) eqnP++nat_eqType :: Eqtype.Equality__Coq_type+nat_eqType =+  unsafeCoerce nat_eqMixin++iter :: Prelude.Int -> (a1 -> a1) -> a1 -> a1+iter n f x =+  (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))+    (\_ ->+    x)+    (\i ->+    f (iter i f x))+    n++double_rec :: Prelude.Int -> Prelude.Int+double_rec n =+  (\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))+    (\_ ->+    0)+    (\n' -> (Prelude.succ) ((Prelude.succ)+    (double_rec n')))+    n++double :: Prelude.Int -> Prelude.Int+double =+  double_rec+
+ LinearScan/Utils.hs view
@@ -0,0 +1,32 @@+module LinearScan.Utils where++import Data.List++boundedTransport' pos n _top_assumption_ = _top_assumption_++snoc _ xs x = xs ++ [x]++set_nth _ xs n x = take n xs ++ x : drop (n+1) xs++vmap _ = Data.List.map++vfoldl' _ = Data.List.foldl'++vfoldl'_with_index _ f = go 0+  where+    go _ z [] = z+    go n z (x:xs) = go (n+1) (f n z x) xs++nth _ = (!!)++list_rect :: b -> (Int -> a -> [a] -> b -> b) -> Int -> [a] -> b+list_rect z f _ = go z+  where+    go z [] = z+    go z (x:xs) = go (f err x xs z) xs++    err = error "list_rect: attempt to use size"++uncons :: [a] -> Maybe (a, [a])+uncons [] = Nothing+uncons (x:xs) = Just (x, xs)
+ LinearScan/Vector0.hs view
@@ -0,0 +1,24 @@+{-# OPTIONS_GHC -cpp -fglasgow-exts #-}+{- For Hugs, use the option -F"cpp -P -traditional" -}++module LinearScan.Vector0 where+++import qualified Prelude+import qualified Data.List+import qualified Data.Ord+import qualified Data.Functor.Identity+import qualified LinearScan.Utils++++--unsafeCoerce :: a -> b+#ifdef __GLASGOW_HASKELL__+import qualified GHC.Base as GHC.Base+unsafeCoerce = GHC.Base.unsafeCoerce#+#else+-- HUGS+import qualified LinearScan.IOExts as IOExts+unsafeCoerce = IOExts.unsafeCoerce+#endif+
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ linearscan.cabal view
@@ -0,0 +1,97 @@+name:          linearscan+version:       0.1.0.0+synopsis:      Linear scan register allocator, formally verified in Coq+homepage:      http://github.com/jwiegley/linearscan+license:       BSD3+license-file:  LICENSE+author:        John Wiegley+maintainer:    johnw@newartisans.com+category:      Development+build-type:    Simple+cabal-version: >=1.10++description:+  The @linearscan@ library is an implementation -- in Coq, extracted to+  Haskell -- of a register allocation algorithm developed by Christian Wimmer.+  It is described in detail in his Masters thesis, which can be found at+  <http://www.christianwimmer.at/Publications/Wimmer04a/Wimmer04a.pdf>.  A+  Java implementation of this same algorithm, by that author, is used in+  Oracle's Graal project.+  .+  This version of the algorithm was written and verified in Coq, containing+  over 130 proved lemmas, at over 5K LOC.  It was funded as a research project+  by BAE Systems (<http://www.baesystems.com>), to be used in an in-house+  compiler written in Haskell.+  .+  In order for the Coq code to be usable from Haskell, it is first extracted+  from Coq as a Haskell library, during which many of Coq's fundamental types+  are mapped directly onto counterparts in the Haskell Prelude.  Thus, it+  should be within the performance range of an equivalent implementation+  written directly in Haskell.+  .+  Note that not every conceivable property of this library has been proven.+  For some of the lower layers this is true, because the algebraic constraints+  on these components could be exhaustively described in the context of their+  use.  However, higher-level components represent a great variety of use+  cases, and not every one of these cases has been proven correct.  This+  represents an ongoing effort, with the hope that proofs will entirely+  replace the necessity for ad hoc unit testing, and that at some point we can+  know that any allocation produced by this library must either fail, or be+  mathematically sound.+  .+  This library's sole entry point is the 'LinearScan.allocate' function, which+  takes a list of information about basic blocks to an equivalent list, with+  annotations indicating allocation choices.  In order to use this function+  you must first convert from your own basic block representation to that of+  the @BlockInfo@, @OpInfo@ and @VarInfo@ structures used by this library.+  For example of such a transformation from a Hoopl Graph, see the file+  @Tempest.hs@ in the tests directory.++library+  default-language: Haskell2010+  exposed-modules:+    LinearScan+  other-modules:+    LinearScan.Datatypes+    LinearScan.IApplicative+    LinearScan.IEndo+    LinearScan.IMonad+    LinearScan.IState+    LinearScan.Interval+    LinearScan.Lib+    -- LinearScan.List0+    LinearScan.Logic+    LinearScan.Main+    LinearScan.NonEmpty0+    -- LinearScan.Peano+    LinearScan.Range+    LinearScan.Specif+    LinearScan.Utils+    LinearScan.Vector0+    LinearScan.Eqtype+    LinearScan.Fintype+    LinearScan.Seq+    LinearScan.Ssrbool+    -- LinearScan.Ssreflect+    LinearScan.Ssrfun+    LinearScan.Ssrnat+  ghc-options:      -fno-warn-deprecated-flags+  build-depends:    base >=4.7 && <4.8+                  , transformers++test-suite test+  default-language: Haskell2010+  type:             exitcode-stdio-1.0+  ghc-options:      -fno-warn-deprecated-flags+  hs-source-dirs:   test+  main-is:          Main.hs+  build-depends: +        base >=3+      , linearscan+      , HUnit              >= 1.2.5+      , hspec              >= 1.4.4+      , hspec-expectations >= 0.3+      , hoopl              >= 3.10+      , containers         >= 0.5.5+      , transformers       >= 0.3.0.0+      , free
+ test/Main.hs view
@@ -0,0 +1,218 @@+{-# OPTIONS_GHC -Wall -Werror #-}++module Main where++{-+The objective of these tests is to present a real world instruction stream to+the register allocator algorithm, and verify that for certain inputs we get+the expected outputs.  I've extracted several of the types from the Tempest+compiler for which this algorithm was originally developed.  We link from this+module to the Haskell interface code (LinearScan), which calls into the+Haskell code that was extracted from Coq.+-}++import Tempest+import Test.Hspec++main :: IO ()+main = hspec $ do+  let basicAlloc = op $ alloc 0 2 >> alloc 1 1 >> alloc 2 0++  describe "Sanity tests" $ do+    it "Single instruction" $ asmTest+        (add v0 v1 v2)++        (block basicAlloc)++    it "Single, repeated instruction" $ asmTest+        (do add v0 v1 v2+            add v0 v1 v2+            add v0 v1 v2) $++        block $ do+            basicAlloc+            basicAlloc+            basicAlloc++    it "Multiple instructions" $ asmTest+        (do add v0 v1 v2+            add v0 v1 v3+            add v0 v1 v2) $++        block $ do+            basicAlloc+            op $ alloc 0 2 >> alloc 1 1 >> alloc 3 3+            basicAlloc++    it "More variables used than registers" $ asmTest+        (do add v0 v1 v2+            add v3 v4 v5+            add v6 v7 v8+            add v9 v10 v11+            add v12 v13 v14+            add v15 v16 v17+            add v18 v19 v20+            add v21 v22 v23+            add v24 v25 v26+            add v27 v28 v29+            add v30 v31 v32+            add v33 v34 v35) $++        block $ do+            op $ alloc  0 2 >> alloc  1 1 >> alloc  2 0+            op $ alloc  3 2 >> alloc  4 1 >> alloc  5 0+            op $ alloc  6 2 >> alloc  7 1 >> alloc  8 0+            op $ alloc  9 2 >> alloc 10 1 >> alloc 11 0+            op $ alloc 12 2 >> alloc 13 1 >> alloc 14 0+            op $ alloc 15 2 >> alloc 16 1 >> alloc 17 0+            op $ alloc 18 2 >> alloc 19 1 >> alloc 20 0+            op $ alloc 21 2 >> alloc 22 1 >> alloc 23 0+            op $ alloc 24 2 >> alloc 25 1 >> alloc 26 0+            op $ alloc 27 2 >> alloc 28 1 >> alloc 29 0+            op $ alloc 30 2 >> alloc 31 1 >> alloc 32 0+            op $ alloc 33 2 >> alloc 34 1 >> alloc 35 0++    it "Single long-lived variable" $ asmTest+        (do add v0 v1 v2+            add v0 v4 v5+            add v0 v7 v8+            add v0 v10 v11) $++        block $ do+            op $ alloc  0 2 >> alloc  1 1 >> alloc  2 0+            op $ alloc  0 2 >> alloc  4 1 >> alloc  5 0+            op $ alloc  0 2 >> alloc  7 1 >> alloc  8 0+            op $ alloc  0 2 >> alloc 10 1 >> alloc 11 0++    it "Two long-lived variables" $ asmTest+        (do add v0 v1 v2+            add v0 v4 v5+            add v0 v4 v8+            add v0 v4 v11) $++        block $ do+            op $ alloc  0 2 >> alloc  1 1 >> alloc  2 0+            op $ alloc  0 2 >> alloc  4 1 >> alloc  5 0+            op $ alloc  0 2 >> alloc  4 1 >> alloc  8 0+            op $ alloc  0 2 >> alloc  4 1 >> alloc 11 0++    it "One variable with a long interval" $ asmTest+        (do add v0   v1  v2+            add v3   v4  v5+            add v6   v7  v8+            add v9  v10 v11+            add v12 v13 v14+            add v15 v16 v17+            add v18 v19 v20+            add v21 v22 v23+            add v24 v25 v26+            add v27 v28 v29+            add v30 v31 v32+            add v0  v34 v35) $++        block $ do+            op $ alloc  0 2 >> alloc  1 1 >> alloc  2 0+            op $ alloc  3 3 >> alloc  4 1 >> alloc  5 0+            op $ alloc  6 3 >> alloc  7 1 >> alloc  8 0+            op $ alloc  9 3 >> alloc 10 1 >> alloc 11 0+            op $ alloc 12 3 >> alloc 13 1 >> alloc 14 0+            op $ alloc 15 3 >> alloc 16 1 >> alloc 17 0+            op $ alloc 18 3 >> alloc 19 1 >> alloc 20 0+            op $ alloc 21 3 >> alloc 22 1 >> alloc 23 0+            op $ alloc 24 3 >> alloc 25 1 >> alloc 26 0+            op $ alloc 27 3 >> alloc 28 1 >> alloc 29 0+            op $ alloc 30 3 >> alloc 31 1 >> alloc 32 0+            op $ alloc  0 2 >> alloc 34 1 >> alloc 35 0++    it "Many variables with long intervals" $ asmTest+        (do add v0   v1  v2+            add v3   v4  v5+            add v6   v7  v8+            add v9  v10 v11+            add v12 v13 v14+            add v15 v16 v17+            add v18 v19 v20+            add v21 v22 v23+            add v24 v25 v26+            add v27 v28 v29+            add v0   v1  v2+            add v3   v4  v5+            add v6   v7  v8+            add v9  v10 v11+            add v12 v13 v14+            add v15 v16 v17+            add v18 v19 v20+            add v21 v22 v23+            add v24 v25 v26+            add v27 v28 v29+        ) $++        block $ do+            op $ alloc  0  2 >> alloc  1  1 >> alloc  2  0+            op $ alloc  3  5 >> alloc  4  4 >> alloc  5  3+            op $ alloc  6  8 >> alloc  7  7 >> alloc  8  6+            op $ alloc  9 11 >> alloc 10 10 >> alloc 11  9+            op $ alloc 12 14 >> alloc 13 13 >> alloc 14 12+            op $ alloc 15 17 >> alloc 16 16 >> alloc 17 15+            op $ alloc 18 20 >> alloc 19 19 >> alloc 20 18+            op $ alloc 21 23 >> alloc 22 22 >> alloc 23 21+            op $ alloc 24 26 >> alloc 25 25 >> alloc 26 24+            op $ alloc 27 29 >> alloc 28 28 >> alloc 29 27+            op $ alloc  0  2 >> alloc  1  1 >> alloc  2  0+            op $ alloc  3  5 >> alloc  4  4 >> alloc  5  3+            op $ alloc  6  8 >> alloc  7  7 >> alloc  8  6+            op $ alloc  9 11 >> alloc 10 10 >> alloc 11  9+            op $ alloc 12 14 >> alloc 13 13 >> alloc 14 12+            op $ alloc 15 17 >> alloc 16 16 >> alloc 17 15+            op $ alloc 18 20 >> alloc 19 19 >> alloc 20 18+            op $ alloc 21 23 >> alloc 22 22 >> alloc 23 21+            op $ alloc 24 26 >> alloc 25 25 >> alloc 26 24+            op $ alloc 27 29 >> alloc 28 28 >> alloc 29 27++    it "Spilling one variable" $ asmTest+        (do {-  1 -} add v0   v1  v2+            {-  3 -} add v3   v4  v5+            {-  5 -} add v6   v7  v8+            {-  7 -} add v9  v10 v11+            {-  9 -} add v12 v13 v14+            {- 11 -} add v15 v16 v17+            {- 13 -} add v18 v19 v20+            {- 15 -} add v21 v22 v23+            {- 17 -} add v24 v25 v26+            {- 19 -} add v27 v28 v29+            {- 21 -} add v30 v31 v32+            {- 23 -} add v0   v1  v2+            {- 25 -} add v3   v4  v5+            {- 27 -} add v6   v7  v8+            {- 29 -} add v9  v10 v11+            {- 31 -} add v12 v13 v14+            {- 33 -} add v15 v16 v17+            {- 35 -} add v18 v19 v20+            {- 37 -} add v21 v22 v23+            {- 39 -} add v24 v25 v26+            {- 41 -} add v27 v28 v29+            {- 43 -} add v30 v31 v32) $++        block $ do+            op $ alloc  0  2 >> alloc  1  1 >> alloc  2  0+            op $ alloc  3  5 >> alloc  4  4 >> alloc  5  3+            op $ alloc  6  8 >> alloc  7  7 >> alloc  8  6+            op $ alloc  9 11 >> alloc 10 10 >> alloc 11  9+            op $ alloc 12 14 >> alloc 13 13 >> alloc 14 12+            op $ alloc 15 17 >> alloc 16 16 >> alloc 17 15+            op $ alloc 18 20 >> alloc 19 19 >> alloc 20 18+            op $ alloc 21 23 >> alloc 22 22 >> alloc 23 21+            op $ alloc 24 26 >> alloc 25 25 >> alloc 26 24+            op $ alloc 27 29 >> alloc 28 28 >> alloc 29 27+            op $ alloc 30 27 >> alloc 31 31 >> alloc 32 30+            op $ alloc  0  2 >> alloc  1  1 >> alloc  2  0+            op $ alloc  3  5 >> alloc  4  4 >> alloc  5  3+            op $ alloc  6  8 >> alloc  7  7 >> alloc  8  6+            op $ alloc  9 11 >> alloc 10 10 >> alloc 11  9+            op $ alloc 12 14 >> alloc 13 13 >> alloc 14 12+            op $ alloc 15 17 >> alloc 16 16 >> alloc 17 15+            op $ alloc 18 20 >> alloc 19 19 >> alloc 20 18+            op $ alloc 21 23 >> alloc 22 22 >> alloc 23 21+            op $ alloc 24 26 >> alloc 25 25 >> alloc 26 24+            op $ alloc 27 29 >> alloc 28 28 >> alloc 29 27+            op $ alloc 30 27 >> alloc 31 31 >> alloc 32 30