diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/LinearScan.hs b/LinearScan.hs new file mode 100644 --- /dev/null +++ b/LinearScan.hs @@ -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) diff --git a/LinearScan/Datatypes.hs b/LinearScan/Datatypes.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Datatypes.hs @@ -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)} + diff --git a/LinearScan/Eqtype.hs b/LinearScan/Eqtype.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Eqtype.hs @@ -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) + diff --git a/LinearScan/Fintype.hs b/LinearScan/Fintype.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Fintype.hs @@ -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) + diff --git a/LinearScan/IApplicative.hs b/LinearScan/IApplicative.hs new file mode 100644 --- /dev/null +++ b/LinearScan/IApplicative.hs @@ -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} + diff --git a/LinearScan/IEndo.hs b/LinearScan/IEndo.hs new file mode 100644 --- /dev/null +++ b/LinearScan/IEndo.hs @@ -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 + diff --git a/LinearScan/IMonad.hs b/LinearScan/IMonad.hs new file mode 100644 --- /dev/null +++ b/LinearScan/IMonad.hs @@ -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} + diff --git a/LinearScan/IState.hs b/LinearScan/IState.hs new file mode 100644 --- /dev/null +++ b/LinearScan/IState.hs @@ -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' __}}) + diff --git a/LinearScan/Interval.hs b/LinearScan/Interval.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Interval.hs @@ -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} + diff --git a/LinearScan/Lib.hs b/LinearScan/Lib.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Lib.hs @@ -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}} + diff --git a/LinearScan/Logic.hs b/LinearScan/Logic.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Logic.hs @@ -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 + diff --git a/LinearScan/Main.hs b/LinearScan/Main.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Main.hs @@ -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}} + diff --git a/LinearScan/NonEmpty0.hs b/LinearScan/NonEmpty0.hs new file mode 100644 --- /dev/null +++ b/LinearScan/NonEmpty0.hs @@ -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 + diff --git a/LinearScan/Range.hs b/LinearScan/Range.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Range.hs @@ -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}}} + diff --git a/LinearScan/Seq.hs b/LinearScan/Seq.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Seq.hs @@ -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)}} + diff --git a/LinearScan/Specif.hs b/LinearScan/Specif.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Specif.hs @@ -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 + diff --git a/LinearScan/Ssrbool.hs b/LinearScan/Ssrbool.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Ssrbool.hs @@ -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 + diff --git a/LinearScan/Ssrfun.hs b/LinearScan/Ssrfun.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Ssrfun.hs @@ -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)) + diff --git a/LinearScan/Ssrnat.hs b/LinearScan/Ssrnat.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Ssrnat.hs @@ -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 + diff --git a/LinearScan/Utils.hs b/LinearScan/Utils.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Utils.hs @@ -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) diff --git a/LinearScan/Vector0.hs b/LinearScan/Vector0.hs new file mode 100644 --- /dev/null +++ b/LinearScan/Vector0.hs @@ -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 + diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/linearscan.cabal b/linearscan.cabal new file mode 100644 --- /dev/null +++ b/linearscan.cabal @@ -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 + . 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 (), 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 diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -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