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

module LinearScan.Choice 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.Ssrbool as Ssrbool
import qualified LinearScan.Ssrfun as Ssrfun
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


#ifdef __GLASGOW_HASKELL__
type Any = GHC.Prim.Any
#else
-- HUGS
type Any = ()
#endif

type Choice__Coq_mixin_of t =
  (Ssrbool.Coq_pred t) -> Prelude.Int -> Prelude.Maybe t
  -- singleton inductive, whose constructor was Mixin
  
_Choice__find :: (Choice__Coq_mixin_of a1) -> (Ssrbool.Coq_pred a1) ->
                 Prelude.Int -> Prelude.Maybe a1
_Choice__find m =
  m

data Choice__Coq_class_of t =
   Choice__Class (Eqtype.Equality__Coq_mixin_of t) (Choice__Coq_mixin_of t)

_Choice__base :: (Choice__Coq_class_of a1) -> Eqtype.Equality__Coq_mixin_of
                 a1
_Choice__base c =
  case c of {
   Choice__Class base0 mixin0 -> base0}

_Choice__mixin :: (Choice__Coq_class_of a1) -> Choice__Coq_mixin_of a1
_Choice__mixin c =
  case c of {
   Choice__Class base0 mixin0 -> mixin0}

type Choice__Coq_type =
  Choice__Coq_class_of Any
  -- singleton inductive, whose constructor was Pack
  
type Choice__Coq_sort = Any

_Choice__coq_class :: Choice__Coq_type -> Choice__Coq_class_of
                      Choice__Coq_sort
_Choice__coq_class cT =
  cT

_Choice__InternalTheory__find :: Choice__Coq_type -> (Ssrbool.Coq_pred
                                 Choice__Coq_sort) -> Prelude.Int ->
                                 Prelude.Maybe Choice__Coq_sort
_Choice__InternalTheory__find t =
  _Choice__find (_Choice__mixin (_Choice__coq_class t))

coq_PcanChoiceMixin :: Choice__Coq_type -> (a1 -> Choice__Coq_sort) ->
                       (Choice__Coq_sort -> Prelude.Maybe a1) ->
                       Choice__Coq_mixin_of a1
coq_PcanChoiceMixin t f f' =
  let {
   liftP = \sP ->
    Ssrbool.coq_SimplPred (\x ->
      Ssrfun._Option__apply sP Prelude.False (f' x))}
  in
  let {
   sf = \sP ->  (\n ->
    Ssrfun._Option__bind f'
      (_Choice__InternalTheory__find t (Ssrbool.pred_of_simpl (liftP sP)) n))}
  in
  (\sP -> (Prelude.$) (sf sP))

sub_choiceMixin :: Choice__Coq_type -> (Ssrbool.Coq_pred Choice__Coq_sort) ->
                   (Eqtype.Coq_subType Choice__Coq_sort) ->
                   Choice__Coq_mixin_of
                   (Eqtype.Coq_sub_sort Choice__Coq_sort)
sub_choiceMixin t p sT =
  coq_PcanChoiceMixin t (Eqtype.val p sT) (Eqtype.insub p sT)

nat_choiceMixin :: Choice__Coq_mixin_of Prelude.Int
nat_choiceMixin =
  let {
   f = \p ->  (\n ->
    case p n of {
     Prelude.True -> Prelude.Just n;
     Prelude.False -> Prelude.Nothing})}
  in
  (\p -> (Prelude.$) (f p))

nat_choiceType :: Choice__Coq_type
nat_choiceType =
  Choice__Class (Eqtype._Equality__coq_class Ssrnat.nat_eqType)
    (unsafeCoerce nat_choiceMixin)

data Countable__Coq_mixin_of t =
   Countable__Mixin (t -> Prelude.Int) (Prelude.Int -> Prelude.Maybe t)

_Countable__pickle :: (Countable__Coq_mixin_of a1) -> a1 -> Prelude.Int
_Countable__pickle m =
  case m of {
   Countable__Mixin pickle0 unpickle0 -> pickle0}

_Countable__unpickle :: (Countable__Coq_mixin_of a1) -> Prelude.Int ->
                        Prelude.Maybe a1
_Countable__unpickle m =
  case m of {
   Countable__Mixin pickle0 unpickle0 -> unpickle0}

data Countable__Coq_class_of t =
   Countable__Class (Choice__Coq_class_of t) (Countable__Coq_mixin_of t)

_Countable__mixin :: (Countable__Coq_class_of a1) -> Countable__Coq_mixin_of
                     a1
_Countable__mixin c =
  case c of {
   Countable__Class base0 mixin0 -> mixin0}

type Countable__Coq_type =
  Countable__Coq_class_of Any
  -- singleton inductive, whose constructor was Pack
  
type Countable__Coq_sort = Any

_Countable__coq_class :: Countable__Coq_type -> Countable__Coq_class_of
                         Countable__Coq_sort
_Countable__coq_class cT =
  cT

unpickle :: Countable__Coq_type -> Prelude.Int -> Prelude.Maybe
            Countable__Coq_sort
unpickle t =
  _Countable__unpickle (_Countable__mixin (_Countable__coq_class t))

pickle :: Countable__Coq_type -> Countable__Coq_sort -> Prelude.Int
pickle t =
  _Countable__pickle (_Countable__mixin (_Countable__coq_class t))

coq_PcanCountMixin :: Countable__Coq_type -> (a1 -> Countable__Coq_sort) ->
                      (Countable__Coq_sort -> Prelude.Maybe a1) ->
                      Countable__Coq_mixin_of a1
coq_PcanCountMixin t f f' =
  Countable__Mixin ((Prelude..) (pickle t) f) (Ssrfun.pcomp f' (unpickle t))

sub_countMixin :: Countable__Coq_type -> (Ssrbool.Coq_pred
                  Countable__Coq_sort) -> (Eqtype.Coq_subType
                  Countable__Coq_sort) -> Countable__Coq_mixin_of
                  (Eqtype.Coq_sub_sort Countable__Coq_sort)
sub_countMixin t p sT =
  coq_PcanCountMixin t (Eqtype.val p sT) (Eqtype.insub p sT)

nat_countMixin :: Countable__Coq_mixin_of Prelude.Int
nat_countMixin =
  Countable__Mixin (\x -> x) (\x -> Prelude.Just x)

nat_countType :: Countable__Coq_type
nat_countType =
  Countable__Class (_Choice__coq_class nat_choiceType)
    (unsafeCoerce nat_countMixin)