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

module LinearScan.Fintype 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.Choice as Choice
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


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

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

data Finite__Coq_mixin_of =
   Finite__Mixin (Choice.Countable__Coq_mixin_of Eqtype.Equality__Coq_sort) 
 ([] Eqtype.Equality__Coq_sort)

_Finite__mixin_enum :: Eqtype.Equality__Coq_type -> Finite__Coq_mixin_of ->
                       [] Eqtype.Equality__Coq_sort
_Finite__mixin_enum t m =
  case m of {
   Finite__Mixin mixin_base mixin_enum0 -> mixin_enum0}

data Finite__Coq_class_of t =
   Finite__Class (Choice.Choice__Coq_class_of t) Finite__Coq_mixin_of

_Finite__base :: (Finite__Coq_class_of a1) -> Choice.Choice__Coq_class_of a1
_Finite__base c =
  case c of {
   Finite__Class base0 mixin0 -> base0}

_Finite__mixin :: (Finite__Coq_class_of a1) -> Finite__Coq_mixin_of
_Finite__mixin c =
  case c of {
   Finite__Class base0 mixin0 -> mixin0}

type Finite__Coq_type =
  Finite__Coq_class_of Any
  -- singleton inductive, whose constructor was Pack
  
type Finite__Coq_sort = Any

_Finite__coq_class :: Finite__Coq_type -> Finite__Coq_class_of
                      Finite__Coq_sort
_Finite__coq_class cT =
  cT

_Finite__EnumDef__enum :: Finite__Coq_type -> [] Finite__Coq_sort
_Finite__EnumDef__enum cT =
  _Finite__mixin_enum
    (Choice._Choice__base (_Finite__base (_Finite__coq_class cT)))
    (_Finite__mixin (_Finite__coq_class cT))

_Finite__EnumDef__enumDef :: ()
_Finite__EnumDef__enumDef =
  __

enum_mem :: Finite__Coq_type -> (Ssrbool.Coq_mem_pred Finite__Coq_sort) -> []
            Finite__Coq_sort
enum_mem t mA =
  Prelude.filter (Ssrbool.pred_of_simpl (Ssrbool.pred_of_mem_pred mA))
    (_Finite__EnumDef__enum t)

image_mem :: Finite__Coq_type -> (Finite__Coq_sort -> a1) ->
             (Ssrbool.Coq_mem_pred Finite__Coq_sort) -> [] a1
image_mem t f mA =
  Prelude.map f (enum_mem t mA)

ordinal_subType :: Prelude.Int -> Eqtype.Coq_subType Prelude.Int
ordinal_subType n =
  Eqtype.SubType (unsafeCoerce Prelude.id) (unsafeCoerce (\x _ ->  x))
    (\_ k_S u ->
    case unsafeCoerce u of {
      x -> k_S x __})

ordinal_eqMixin :: Prelude.Int -> Eqtype.Equality__Coq_mixin_of Prelude.Int
ordinal_eqMixin n =
  Eqtype.Equality__Mixin (\x y ->
    Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce (Prelude.id x))
      (unsafeCoerce (Prelude.id y)))
    (unsafeCoerce
      (Eqtype.val_eqP Ssrnat.nat_eqType (\x ->
        (Prelude.<=) ((Prelude.succ) (unsafeCoerce x)) n)
        (unsafeCoerce (ordinal_subType n))))

ordinal_eqType :: Prelude.Int -> Eqtype.Equality__Coq_type
ordinal_eqType n =
  unsafeCoerce (ordinal_eqMixin n)

ordinal_choiceMixin :: Prelude.Int -> Choice.Choice__Coq_mixin_of Prelude.Int
ordinal_choiceMixin n =
  unsafeCoerce
    (Choice.sub_choiceMixin Choice.nat_choiceType (\x ->
      (Prelude.<=) ((Prelude.succ) (unsafeCoerce x)) n)
      (unsafeCoerce (ordinal_subType n)))

ordinal_choiceType :: Prelude.Int -> Choice.Choice__Coq_type
ordinal_choiceType n =
  Choice.Choice__Class (Eqtype._Equality__coq_class (ordinal_eqType n))
    (unsafeCoerce (ordinal_choiceMixin n))

ordinal_countMixin :: Prelude.Int -> Choice.Countable__Coq_mixin_of
                      Prelude.Int
ordinal_countMixin n =
  unsafeCoerce
    (Choice.sub_countMixin Choice.nat_countType (\x ->
      (Prelude.<=) ((Prelude.succ) (unsafeCoerce x)) n)
      (unsafeCoerce (ordinal_subType n)))

ord_enum :: Prelude.Int -> [] Prelude.Int
ord_enum n =
  Seq.pmap
    (unsafeCoerce
      (Eqtype.insub (\x -> (Prelude.<=) ((Prelude.succ) x) n)
        (ordinal_subType n))) (Seq.iota 0 n)

ordinal_finMixin :: Prelude.Int -> Finite__Coq_mixin_of
ordinal_finMixin n =
  Finite__Mixin (unsafeCoerce (ordinal_countMixin n))
    (unsafeCoerce (ord_enum n))

ordinal_finType :: Prelude.Int -> Finite__Coq_type
ordinal_finType n =
  Finite__Class (Choice._Choice__coq_class (ordinal_choiceType n))
    (ordinal_finMixin n)

ord0 :: Prelude.Int -> Prelude.Int
ord0 n' =
   0

inord :: Prelude.Int -> Prelude.Int -> Prelude.Int
inord n' m =
  unsafeCoerce
    (Eqtype.insubd (\x ->
      (Prelude.<=) ((Prelude.succ) x) ((Prelude.succ) n'))
      (ordinal_subType ((Prelude.succ) n')) (unsafeCoerce (ord0 n')) m)