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

module LinearScan.IntSet 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
import qualified LinearScan.Ssrnat as Ssrnat



#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

__ :: any
__ = Prelude.error "Logical or arity value used"

type IntSet =
  [] Prelude.Int
  -- singleton inductive, whose constructor was getIntSet
  
emptyIntSet :: IntSet
emptyIntSet =
  []

coq_IntSet_singleton :: Prelude.Int -> IntSet
coq_IntSet_singleton x =
  (:) x []

coq_IntSet_member :: Prelude.Int -> IntSet -> Prelude.Bool
coq_IntSet_member k m =
  Ssrbool.in_mem (unsafeCoerce k)
    (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce m))

coq_IntSet_size :: IntSet -> Prelude.Int
coq_IntSet_size m =
  Data.List.length m

coq_IntSet_insert :: Prelude.Int -> IntSet -> IntSet
coq_IntSet_insert k m =
  case Ssrbool.in_mem (unsafeCoerce k)
         (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce m)) of {
   Prelude.True -> m;
   Prelude.False -> (:) k m}

coq_IntSet_delete :: Prelude.Int -> IntSet -> IntSet
coq_IntSet_delete k m =
  unsafeCoerce (Seq.rem Ssrnat.nat_eqType (unsafeCoerce k) (unsafeCoerce m))

coq_IntSet_union :: IntSet -> IntSet -> IntSet
coq_IntSet_union m1 m2 =
  unsafeCoerce
    (Seq.undup Ssrnat.nat_eqType
      ((Prelude.++) (unsafeCoerce m1) (unsafeCoerce m2)))

coq_IntSet_difference :: IntSet -> IntSet -> IntSet
coq_IntSet_difference m1 m2 =
  Prelude.filter (\k ->
    Prelude.not
      (Ssrbool.in_mem (unsafeCoerce k)
        (Ssrbool.mem (Seq.seq_predType Ssrnat.nat_eqType) (unsafeCoerce m2))))
    m1

coq_IntSet_foldl :: (a1 -> Prelude.Int -> a1) -> a1 -> IntSet -> a1
coq_IntSet_foldl f z m =
  Data.List.foldl' f z m

coq_IntSet_forFold :: a1 -> IntSet -> (a1 -> Prelude.Int -> a1) -> a1
coq_IntSet_forFold z m f =
  coq_IntSet_foldl f z m

coq_IntSet_toList :: IntSet -> [] Prelude.Int
coq_IntSet_toList m =
  m

eqIntSet :: IntSet -> IntSet -> Prelude.Bool
eqIntSet s1 s2 =
  Eqtype.eq_op (Seq.seq_eqType Ssrnat.nat_eqType) (unsafeCoerce s1)
    (unsafeCoerce s2)

eqIntSetP :: Eqtype.Equality__Coq_axiom IntSet
eqIntSetP _top_assumption_ =
  let {
   _evar_0_ = \s1 _top_assumption_0 ->
    let {
     _evar_0_ = \s2 ->
      let {_evar_0_ = \_ -> let {_evar_0_ = Ssrbool.ReflectT} in  _evar_0_}
      in
      let {_evar_0_0 = \_ -> Ssrbool.ReflectF} in
      case Eqtype.eqP (Seq.seq_eqType Ssrnat.nat_eqType) s1 s2 of {
       Ssrbool.ReflectT -> _evar_0_ __;
       Ssrbool.ReflectF -> _evar_0_0 __}}
    in
    unsafeCoerce _evar_0_ _top_assumption_0}
  in
  unsafeCoerce _evar_0_ _top_assumption_

coq_IntSet_eqMixin :: Eqtype.Equality__Coq_mixin_of IntSet
coq_IntSet_eqMixin =
  Eqtype.Equality__Mixin eqIntSet eqIntSetP

coq_IntSet_eqType :: Eqtype.Equality__Coq_type
coq_IntSet_eqType =
  unsafeCoerce coq_IntSet_eqMixin