{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}

module LinearScan.UsePos where


import Debug.Trace (trace, traceShow, traceShowId)
import qualified Prelude
import qualified Data.IntMap
import qualified Data.IntSet
import qualified Data.List
import qualified Data.Ord
import qualified Data.Functor.Identity
import qualified Hask.Utils

import qualified LinearScan.Eqtype as Eqtype
import qualified LinearScan.Seq as Seq
import qualified LinearScan.Ssrbool as Ssrbool



#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base as GHC.Base
import qualified GHC.Prim as GHC.Prim
#else
-- HUGS
import qualified LinearScan.IOExts as IOExts
#endif


#ifdef __GLASGOW_HASKELL__
--unsafeCoerce :: a -> b
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
--unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif

data VarKind =
   Input
 | InputOutput
 | Temp
 | Output

eqVarKind :: VarKind -> VarKind -> Prelude.Bool
eqVarKind s1 s2 =
  case s1 of {
   Input ->
    case s2 of {
     Input -> Prelude.True;
     _ -> Prelude.False};
   InputOutput ->
    case s2 of {
     InputOutput -> Prelude.True;
     _ -> Prelude.False};
   Temp ->
    case s2 of {
     Temp -> Prelude.True;
     _ -> Prelude.False};
   Output ->
    case s2 of {
     Output -> Prelude.True;
     _ -> Prelude.False}}

eqVarKindP :: Eqtype.Equality__Coq_axiom VarKind
eqVarKindP _top_assumption_ =
  let {
   _evar_0_ = \_top_assumption_0 ->
    let {_evar_0_ = Ssrbool.ReflectT} in
    let {_evar_0_0 = Ssrbool.ReflectF} in
    let {_evar_0_1 = Ssrbool.ReflectF} in
    let {_evar_0_2 = Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     Input -> _evar_0_;
     InputOutput -> _evar_0_0;
     Temp -> _evar_0_1;
     Output -> _evar_0_2}}
  in
  let {
   _evar_0_0 = \_top_assumption_0 ->
    let {_evar_0_0 = Ssrbool.ReflectF} in
    let {_evar_0_1 = Ssrbool.ReflectT} in
    let {_evar_0_2 = Ssrbool.ReflectF} in
    let {_evar_0_3 = Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     Input -> _evar_0_0;
     InputOutput -> _evar_0_1;
     Temp -> _evar_0_2;
     Output -> _evar_0_3}}
  in
  let {
   _evar_0_1 = \_top_assumption_0 ->
    let {_evar_0_1 = Ssrbool.ReflectF} in
    let {_evar_0_2 = Ssrbool.ReflectF} in
    let {_evar_0_3 = Ssrbool.ReflectT} in
    let {_evar_0_4 = Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     Input -> _evar_0_1;
     InputOutput -> _evar_0_2;
     Temp -> _evar_0_3;
     Output -> _evar_0_4}}
  in
  let {
   _evar_0_2 = \_top_assumption_0 ->
    let {_evar_0_2 = Ssrbool.ReflectF} in
    let {_evar_0_3 = Ssrbool.ReflectF} in
    let {_evar_0_4 = Ssrbool.ReflectF} in
    let {_evar_0_5 = Ssrbool.ReflectT} in
    case _top_assumption_0 of {
     Input -> _evar_0_2;
     InputOutput -> _evar_0_3;
     Temp -> _evar_0_4;
     Output -> _evar_0_5}}
  in
  case _top_assumption_ of {
   Input -> _evar_0_;
   InputOutput -> _evar_0_0;
   Temp -> _evar_0_1;
   Output -> _evar_0_2}

coq_VarKind_eqMixin :: Eqtype.Equality__Coq_mixin_of VarKind
coq_VarKind_eqMixin =
  Eqtype.Equality__Mixin eqVarKind eqVarKindP

coq_VarKind_eqType :: Eqtype.Equality__Coq_type
coq_VarKind_eqType =
  unsafeCoerce coq_VarKind_eqMixin

data UsePos =
   Build_UsePos Prelude.Int Prelude.Bool VarKind

uloc :: UsePos -> Prelude.Int
uloc u =
  case u of {
   Build_UsePos uloc0 regReq0 uvar0 -> uloc0}

regReq :: UsePos -> Prelude.Bool
regReq u =
  case u of {
   Build_UsePos uloc0 regReq0 uvar0 -> regReq0}

uvar :: UsePos -> VarKind
uvar u =
  case u of {
   Build_UsePos uloc0 regReq0 uvar0 -> uvar0}

upos_le :: Ssrbool.Coq_rel UsePos
upos_le m n =
  (Prelude.<=) (uloc m) (uloc n)

head_or :: Prelude.Int -> ([] UsePos) -> Prelude.Int
head_or x xs =
  Seq.head x (Prelude.map (\u -> uloc u) xs)