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

module LinearScan.IntMap 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.List1 as List1
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 =
  List1.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
  Hask.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_foldr :: (a2 -> a1 -> a1) -> a1 -> (IntMap a2) -> a1
coq_IntMap_foldr f z m =
  Prelude.foldr (\x -> f (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_foldrWithKey :: (a2 -> Prelude.Int -> a1 -> a1) -> a1 -> (IntMap
                           a2) -> a1
coq_IntMap_foldrWithKey f z m =
  Prelude.foldr (\x -> f (Prelude.snd x) (Prelude.fst x)) z m

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

coq_IntMap_combine :: (Prelude.Int -> (Prelude.Maybe a1) -> (Prelude.Maybe
                      a2) -> Prelude.Maybe a3) -> (IntMap a1) -> (IntMap 
                      a2) -> IntMap a3
coq_IntMap_combine f =
  coq_IntMap_mergeWithKey (\idx x y ->
    f idx (Prelude.Just x) (Prelude.Just y))
    (coq_IntMap_foldrWithKey (\x idx rest ->
      let {mres = f idx (Prelude.Just x) Prelude.Nothing} in
      case mres of {
       Prelude.Just res -> coq_IntMap_insert idx res rest;
       Prelude.Nothing -> rest}) emptyIntMap)
    (coq_IntMap_foldrWithKey (\y idx rest ->
      let {mres = f idx Prelude.Nothing (Prelude.Just y)} in
      case mres of {
       Prelude.Just res -> coq_IntMap_insert idx res rest;
       Prelude.Nothing -> rest}) emptyIntMap)

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)

coq_IntMap_groupOn :: (a1 -> Prelude.Int) -> ([] a1) -> IntMap ([] a1)
coq_IntMap_groupOn p l =
  List1.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)