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

module LinearScan.Seq where


import Debug.Trace (trace, traceShow)
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 LinearScan.Utils

import qualified LinearScan.Datatypes as Datatypes
import qualified LinearScan.Eqtype as Eqtype
import qualified LinearScan.Ssrbool as Ssrbool
import qualified LinearScan.Ssrfun as Ssrfun
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"

nilp :: ([] a1) -> Prelude.Bool
nilp s =
  Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Data.List.length s))
    (unsafeCoerce 0)

head :: a1 -> ([] a1) -> a1
head x0 s =
  case s of {
   [] -> x0;
   (:) x l -> x}

rcons :: ([] a1) -> a1 -> [] a1
rcons s z =
  case s of {
   [] -> (:) z [];
   (:) x s' -> (:) x (rcons s' z)}

last :: a1 -> ([] a1) -> a1
last x s =
  case s of {
   [] -> x;
   (:) x' s' -> last x' s'}

belast :: a1 -> ([] a1) -> [] a1
belast x s =
  case s of {
   [] -> [];
   (:) x' s' -> (:) x (belast x' s')}

data Coq_last_spec t =
   LastNil
 | LastRcons ([] t) t

lastP :: ([] a1) -> Coq_last_spec a1
lastP s =
  let {_evar_0_ = LastNil} in
  let {
   _evar_0_0 = \x s0 ->
    let {_evar_0_0 = LastRcons (belast x s0) (last x s0)} in  _evar_0_0}
  in
  case s of {
   [] -> _evar_0_;
   (:) x x0 -> _evar_0_0 x x0}

last_ind :: a2 -> (([] a1) -> a1 -> a2 -> a2) -> ([] a1) -> a2
last_ind hnil hlast s =
  let {
   _evar_0_ = let {_evar_0_ = \s1 hs1 ->  hs1} in
              let {
               _evar_0_0 = \x s2 iHs s1 hs1 ->
                let {_evar_0_0 = iHs (rcons s1 x) (hlast s1 x hs1)} in
                 _evar_0_0}
              in
              Datatypes.list_rect _evar_0_ _evar_0_0 s [] hnil}
  in
   _evar_0_

find :: (Ssrbool.Coq_pred a1) -> ([] a1) -> Prelude.Int
find a s =
  case s of {
   [] -> 0;
   (:) x s' ->
    case a x of {
     Prelude.True -> 0;
     Prelude.False -> (Prelude.succ) (find a s')}}

count :: (Ssrbool.Coq_pred a1) -> ([] a1) -> Prelude.Int
count a s =
  case s of {
   [] -> 0;
   (:) x s' -> (Prelude.+) (Ssrnat.nat_of_bool (a x)) (count a s')}

catrev :: ([] a1) -> ([] a1) -> [] a1
catrev s1 s2 =
  case s1 of {
   [] -> s2;
   (:) x s1' -> catrev s1' ((:) x s2)}

rev :: ([] a1) -> [] a1
rev s =
  catrev s []

eqseq :: Eqtype.Equality__Coq_type -> ([] Eqtype.Equality__Coq_sort) -> ([]
         Eqtype.Equality__Coq_sort) -> Prelude.Bool
eqseq t s1 s2 =
  case s1 of {
   [] ->
    case s2 of {
     [] -> Prelude.True;
     (:) s l -> Prelude.False};
   (:) x1 s1' ->
    case s2 of {
     [] -> Prelude.False;
     (:) x2 s2' -> (Prelude.&&) (Eqtype.eq_op t x1 x2) (eqseq t s1' s2')}}

eqseqP :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_axiom
          ([] Eqtype.Equality__Coq_sort)
eqseqP t _top_assumption_ =
  let {
   _evar_0_ = \_top_assumption_0 ->
    let {_evar_0_ = Ssrbool.ReflectT} in
    let {_evar_0_0 = \x2 s2 -> Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     [] -> _evar_0_;
     (:) x x0 -> _evar_0_0 x x0}}
  in
  let {
   _evar_0_0 = \x1 s1 iHs _top_assumption_0 ->
    let {_evar_0_0 = Ssrbool.ReflectF} in
    let {
     _evar_0_1 = \x2 s2 ->
      let {
       _evar_0_1 = \_ ->
        let {_evar_0_1 = Ssrbool.iffP (eqseq t s1 s2) (iHs s2)} in  _evar_0_1}
      in
      let {_evar_0_2 = \_ -> Ssrbool.ReflectF} in
      case Eqtype.eqP t x1 x2 of {
       Ssrbool.ReflectT -> _evar_0_1 __;
       Ssrbool.ReflectF -> _evar_0_2 __}}
    in
    case _top_assumption_0 of {
     [] -> _evar_0_0;
     (:) x x0 -> _evar_0_1 x x0}}
  in
  Datatypes.list_rect _evar_0_ _evar_0_0 _top_assumption_

seq_eqMixin :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_mixin_of
               ([] Eqtype.Equality__Coq_sort)
seq_eqMixin t =
  Eqtype.Equality__Mixin (eqseq t) (eqseqP t)

seq_eqType :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type
seq_eqType t =
  unsafeCoerce (seq_eqMixin t)

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))

undup :: Eqtype.Equality__Coq_type -> ([] Eqtype.Equality__Coq_sort) -> []
         Eqtype.Equality__Coq_sort
undup t s =
  case s of {
   [] -> [];
   (:) x s' ->
    case Ssrbool.in_mem x (Ssrbool.mem (seq_predType t) (unsafeCoerce s')) of {
     Prelude.True -> undup t s';
     Prelude.False -> (:) x (undup t s')}}

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)}}

pmap :: (a1 -> Prelude.Maybe a2) -> ([] a1) -> [] a2
pmap f s =
  case s of {
   [] -> [];
   (:) x s' ->
    let {r = pmap f s'} in Ssrfun._Option__apply (\x0 -> (:) x0 r) r (f x)}

iota :: Prelude.Int -> Prelude.Int -> [] Prelude.Int
iota m n =
  (\fO fS n -> if n Prelude.<= 0 then fO () else fS (n Prelude.- 1))
    (\_ ->
    [])
    (\n' -> (:) m
    (iota ((Prelude.succ) m) n'))
    n