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

module LinearScan.IntMap 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.Lib as Lib
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 IntMap a =
  [] ((,) Prelude.Int a)
  -- singleton inductive, whose constructor was getIntMap
  
emptyIntMap :: IntMap a1
emptyIntMap =
  []

coq_IntMap_fromList :: ([] ((,) Prelude.Int a1)) -> IntMap a1
coq_IntMap_fromList x =
  x

coq_IntMap_size :: (IntMap a1) -> Prelude.Int
coq_IntMap_size m =
  Data.List.length m

coq_IntMap_lookup :: Prelude.Int -> (IntMap a1) -> Prelude.Maybe a1
coq_IntMap_lookup k m =
  Lib.maybeLookup Ssrnat.nat_eqType (unsafeCoerce m) (unsafeCoerce k)

coq_IntMap_alter :: ((Prelude.Maybe a1) -> Prelude.Maybe a1) -> Prelude.Int
                    -> (IntMap a1) -> IntMap a1
coq_IntMap_alter f k m =
  case coq_IntMap_lookup k m of {
   Prelude.Just x ->
    Prelude.foldr (\z acc ->
      case z of {
       (,) a b ->
        case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce a) (unsafeCoerce k) of {
         Prelude.True ->
          case f (Prelude.Just x) of {
           Prelude.Just x' -> Seq.rcons acc ((,) k x');
           Prelude.Nothing -> acc};
         Prelude.False -> (:) z acc}}) [] m;
   Prelude.Nothing ->
    case f Prelude.Nothing of {
     Prelude.Just x -> Seq.rcons m ((,) k x);
     Prelude.Nothing -> m}}

coq_IntMap_insert :: Prelude.Int -> a1 -> (IntMap a1) -> IntMap a1
coq_IntMap_insert k x m =
  coq_IntMap_alter (\x0 -> Prelude.Just x) k m

coq_IntMap_map :: (a1 -> a2) -> (IntMap a1) -> IntMap a2
coq_IntMap_map f m =
  Prelude.map (\x -> (,) (Prelude.fst x) (f (Prelude.snd x))) m

coq_IntMap_mergeWithKey :: (Prelude.Int -> a1 -> a2 -> Prelude.Maybe 
                           a3) -> ((IntMap a1) -> IntMap a3) -> ((IntMap 
                           a2) -> IntMap a3) -> (IntMap a1) -> (IntMap 
                           a2) -> IntMap a3
coq_IntMap_mergeWithKey combine only1 only2 m1 m2 =
  let {only1' = \xs -> only1 xs} in
  let {only2' = \xs -> only2 xs} in
  LinearScan.Utils.intMap_mergeWithKey' combine only1' only2' m1 m2

coq_IntMap_foldl :: (a1 -> a2 -> a1) -> a1 -> (IntMap a2) -> a1
coq_IntMap_foldl f z m =
  Data.List.foldl' (\acc x -> f acc (Prelude.snd x)) z m

coq_IntMap_foldlWithKey :: (a1 -> Prelude.Int -> a2 -> a1) -> a1 -> (IntMap
                           a2) -> a1
coq_IntMap_foldlWithKey f z m =
  Data.List.foldl' (\acc x -> f acc (Prelude.fst x) (Prelude.snd x)) z m

coq_IntMap_toList :: (IntMap a1) -> [] ((,) Prelude.Int a1)
coq_IntMap_toList m =
  m

eqIntMap :: Eqtype.Equality__Coq_type -> (IntMap Eqtype.Equality__Coq_sort)
            -> (IntMap Eqtype.Equality__Coq_sort) -> Prelude.Bool
eqIntMap a s1 s2 =
  Eqtype.eq_op (Seq.seq_eqType (Eqtype.prod_eqType Ssrnat.nat_eqType a))
    (unsafeCoerce s1) (unsafeCoerce s2)

eqIntMapP :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_axiom
             (IntMap Eqtype.Equality__Coq_sort)
eqIntMapP a _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 (Eqtype.prod_eqType Ssrnat.nat_eqType a)) 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_IntMap_eqMixin :: Eqtype.Equality__Coq_type ->
                      Eqtype.Equality__Coq_mixin_of
                      (IntMap Eqtype.Equality__Coq_sort)
coq_IntMap_eqMixin a =
  Eqtype.Equality__Mixin (eqIntMap a) (eqIntMapP a)

coq_IntMap_eqType :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_type
coq_IntMap_eqType a =
  unsafeCoerce (coq_IntMap_eqMixin a)

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

coq_IntMap_groupOn :: (a1 -> Prelude.Int) -> ([] a1) -> IntMap ([] a1)
coq_IntMap_groupOn p l =
  Lib.forFold emptyIntMap l (\acc x ->
    let {n = p x} in
    coq_IntMap_alter (\mxs ->
      case mxs of {
       Prelude.Just xs -> Prelude.Just ((:) x xs);
       Prelude.Nothing -> Prelude.Just ((:[]) x)}) n acc)