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

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



--unsafeCoerce :: a -> b
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base as GHC.Base
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
import qualified LinearScan.IOExts as IOExts
unsafeCoerce = IOExts.unsafeCoerce
#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_of_rect :: Eqtype.Equality__Coq_type ->
                          ((Choice.Countable__Coq_mixin_of
                          Eqtype.Equality__Coq_sort) -> ([]
                          Eqtype.Equality__Coq_sort) -> () -> a1) ->
                          Finite__Coq_mixin_of -> a1
_Finite__mixin_of_rect t f m =
  case m of {
   Finite__Mixin x x0 -> f x x0 __}

_Finite__mixin_of_rec :: Eqtype.Equality__Coq_type ->
                         ((Choice.Countable__Coq_mixin_of
                         Eqtype.Equality__Coq_sort) -> ([]
                         Eqtype.Equality__Coq_sort) -> () -> a1) ->
                         Finite__Coq_mixin_of -> a1
_Finite__mixin_of_rec t =
  _Finite__mixin_of_rect t

_Finite__mixin_base :: Eqtype.Equality__Coq_type -> Finite__Coq_mixin_of ->
                       Choice.Countable__Coq_mixin_of
                       Eqtype.Equality__Coq_sort
_Finite__mixin_base t m =
  case m of {
   Finite__Mixin mixin_base0 mixin_enum0 -> mixin_base0}

_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_base0 mixin_enum0 -> mixin_enum0}

_Finite__coq_EnumMixin :: Choice.Countable__Coq_type -> ([]
                          Choice.Countable__Coq_sort) -> Finite__Coq_mixin_of
_Finite__coq_EnumMixin t e =
  case t of {
   Choice.Countable__Class base0 m -> Finite__Mixin m e}

_Finite__coq_UniqMixin :: Choice.Countable__Coq_type -> ([]
                          Choice.Countable__Coq_sort) -> Finite__Coq_mixin_of
_Finite__coq_UniqMixin t e =
  _Finite__coq_EnumMixin t e

_Finite__count_enum :: Choice.Countable__Coq_type -> Prelude.Int -> []
                       Choice.Countable__Coq_sort
_Finite__count_enum t n =
  Seq.pmap (unsafeCoerce (Choice.pickle_inv t)) (Seq.iota 0 n)

_Finite__coq_CountMixin :: Choice.Countable__Coq_type -> Prelude.Int ->
                           Finite__Coq_mixin_of
_Finite__coq_CountMixin t n =
  _Finite__coq_EnumMixin t (_Finite__count_enum t n)

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

_Finite__class_of_rect :: ((Choice.Choice__Coq_class_of a1) ->
                          Finite__Coq_mixin_of -> a2) ->
                          (Finite__Coq_class_of a1) -> a2
_Finite__class_of_rect f c =
  case c of {
   Finite__Class x x0 -> f x x0}

_Finite__class_of_rec :: ((Choice.Choice__Coq_class_of a1) ->
                         Finite__Coq_mixin_of -> a2) -> (Finite__Coq_class_of
                         a1) -> a2
_Finite__class_of_rec =
  _Finite__class_of_rect

_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}

_Finite__base2 :: (Finite__Coq_class_of a1) -> Choice.Countable__Coq_class_of
                  a1
_Finite__base2 c =
  Choice.Countable__Class (_Finite__base c)
    (unsafeCoerce
      (_Finite__mixin_base
        (Choice._Choice__base (_Finite__base (unsafeCoerce c)))
        (_Finite__mixin c)))

type Finite__Coq_type =
  Finite__Coq_class_of ()
  -- singleton inductive, whose constructor was Pack
  
_Finite__type_rect :: (() -> (Finite__Coq_class_of ()) -> () -> a1) ->
                      Finite__Coq_type -> a1
_Finite__type_rect f t =
  f __ t __

_Finite__type_rec :: (() -> (Finite__Coq_class_of ()) -> () -> a1) ->
                     Finite__Coq_type -> a1
_Finite__type_rec =
  _Finite__type_rect

type Finite__Coq_sort = ()

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

_Finite__clone :: Finite__Coq_type -> (Finite__Coq_class_of a1) ->
                  Finite__Coq_type
_Finite__clone cT c =
  unsafeCoerce c

_Finite__pack :: (Eqtype.Equality__Coq_mixin_of a1) -> Finite__Coq_mixin_of
                 -> Choice.Choice__Coq_type -> (Choice.Choice__Coq_class_of
                 a1) -> Finite__Coq_mixin_of -> Finite__Coq_type
_Finite__pack b0 m0 bT b m =
  Finite__Class (unsafeCoerce b) m

_Finite__eqType :: Finite__Coq_type -> Eqtype.Equality__Coq_type
_Finite__eqType cT =
  Choice._Choice__base (_Finite__base (_Finite__coq_class cT))

_Finite__choiceType :: Finite__Coq_type -> Choice.Choice__Coq_type
_Finite__choiceType cT =
  _Finite__base (_Finite__coq_class cT)

_Finite__countType :: Finite__Coq_type -> Choice.Countable__Coq_type
_Finite__countType cT =
  _Finite__base2 (_Finite__coq_class 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))

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 ) (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 ( x)) (unsafeCoerce ( 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)