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

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



#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"

type Equality__Coq_axiom t = t -> t -> Ssrbool.Coq_reflect

data Equality__Coq_mixin_of t =
   Equality__Mixin (Ssrbool.Coq_rel t) (Equality__Coq_axiom t)

_Equality__op :: (Equality__Coq_mixin_of a1) -> Ssrbool.Coq_rel a1
_Equality__op m =
  case m of {
   Equality__Mixin op0 x -> op0}

type Equality__Coq_type =
  Equality__Coq_mixin_of Any
  -- singleton inductive, whose constructor was Pack
  
type Equality__Coq_sort = Any

_Equality__coq_class :: Equality__Coq_type -> Equality__Coq_mixin_of
                        Equality__Coq_sort
_Equality__coq_class cT =
  cT

eq_op :: Equality__Coq_type -> Ssrbool.Coq_rel Equality__Coq_sort
eq_op t =
  _Equality__op (_Equality__coq_class t)

eqP :: Equality__Coq_type -> Equality__Coq_axiom Equality__Coq_sort
eqP t =
  let {_evar_0_ = \op0 a -> a} in
  case t of {
   Equality__Mixin x x0 -> _evar_0_ x x0}

eqbP :: Equality__Coq_axiom Prelude.Bool
eqbP _top_assumption_ =
  let {
   _evar_0_ = \_top_assumption_0 ->
    let {_evar_0_ = Ssrbool.ReflectT} in
    let {_evar_0_0 = Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     Prelude.True -> _evar_0_;
     Prelude.False -> _evar_0_0}}
  in
  let {
   _evar_0_0 = \_top_assumption_0 ->
    let {_evar_0_0 = Ssrbool.ReflectF} in
    let {_evar_0_1 = Ssrbool.ReflectT} in
    case _top_assumption_0 of {
     Prelude.True -> _evar_0_0;
     Prelude.False -> _evar_0_1}}
  in
  case _top_assumption_ of {
   Prelude.True -> _evar_0_;
   Prelude.False -> _evar_0_0}

bool_eqMixin :: Equality__Coq_mixin_of Prelude.Bool
bool_eqMixin =
  Equality__Mixin (Prelude.==) eqbP

bool_eqType :: Equality__Coq_type
bool_eqType =
  unsafeCoerce bool_eqMixin

data Coq_subType t =
   SubType (Any -> t) (t -> () -> Any) (() -> (t -> () -> Any) -> Any -> Any)

type Coq_sub_sort t = Any

val :: (Ssrbool.Coq_pred a1) -> (Coq_subType a1) -> (Coq_sub_sort a1) -> a1
val p s =
  case s of {
   SubType val0 sub x -> val0}

coq_Sub :: (Ssrbool.Coq_pred a1) -> (Coq_subType a1) -> a1 -> Coq_sub_sort a1
coq_Sub p s x =
  case s of {
   SubType val0 sub x0 -> sub x __}

insub :: (Ssrbool.Coq_pred a1) -> (Coq_subType a1) -> a1 -> Prelude.Maybe
         (Coq_sub_sort a1)
insub p sT x =
  case Ssrbool.idP (p x) of {
   Ssrbool.ReflectT -> Prelude.Just (coq_Sub p sT x);
   Ssrbool.ReflectF -> Prelude.Nothing}

insubd :: (Ssrbool.Coq_pred a1) -> (Coq_subType a1) -> (Coq_sub_sort 
          a1) -> a1 -> Coq_sub_sort a1
insubd p sT u0 x =
  Ssrfun._Option__coq_default u0 (insub p sT x)

sig_subType :: (Ssrbool.Coq_pred a1) -> Coq_subType a1
sig_subType p =
  SubType (unsafeCoerce ) (unsafeCoerce (\x _ -> x)) (\_ k_S u ->
    k_S (unsafeCoerce u) __)

inj_eqAxiom :: Equality__Coq_type -> (a1 -> Equality__Coq_sort) ->
               Equality__Coq_axiom a1
inj_eqAxiom eT f x y =
  Ssrbool.iffP (eq_op eT (f x) (f y)) (eqP eT (f x) (f y))

val_eqP :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->
           (Coq_subType Equality__Coq_sort) -> Equality__Coq_axiom
           (Coq_sub_sort Equality__Coq_sort)
val_eqP t p sT =
  inj_eqAxiom t (val p sT)

sig_eqMixin :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->
               Equality__Coq_mixin_of Equality__Coq_sort
sig_eqMixin t p =
  Equality__Mixin (\x y -> eq_op t ( x) ( y))
    (unsafeCoerce (val_eqP t (\x -> p x) (sig_subType p)))

sig_eqType :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) ->
              Equality__Coq_type
sig_eqType t p =
  unsafeCoerce (sig_eqMixin t p)

pair_eq :: Equality__Coq_type -> Equality__Coq_type -> Ssrbool.Coq_simpl_rel
           ((,) Equality__Coq_sort Equality__Coq_sort)
pair_eq t1 t2 =
   (\u v ->
    (Prelude.&&) (eq_op t1 (Prelude.fst u) (Prelude.fst v))
      (eq_op t2 (Prelude.snd u) (Prelude.snd v)))

pair_eqP :: Equality__Coq_type -> Equality__Coq_type -> Equality__Coq_axiom
            ((,) Equality__Coq_sort Equality__Coq_sort)
pair_eqP t1 t2 _top_assumption_ =
  let {
   _evar_0_ = \x1 x2 _top_assumption_0 ->
    let {
     _evar_0_ = \y1 y2 ->
      Ssrbool.iffP ((Prelude.&&) (eq_op t1 x1 y1) (eq_op t2 x2 y2))
        (Ssrbool.andP (eq_op t1 x1 y1) (eq_op t2 x2 y2))}
    in
    case _top_assumption_0 of {
     (,) x x0 -> _evar_0_ x x0}}
  in
  case _top_assumption_ of {
   (,) x x0 -> _evar_0_ x x0}

prod_eqMixin :: Equality__Coq_type -> Equality__Coq_type ->
                Equality__Coq_mixin_of
                ((,) Equality__Coq_sort Equality__Coq_sort)
prod_eqMixin t1 t2 =
  Equality__Mixin (Ssrbool.rel_of_simpl_rel (pair_eq t1 t2)) (pair_eqP t1 t2)

prod_eqType :: Equality__Coq_type -> Equality__Coq_type -> Equality__Coq_type
prod_eqType t1 t2 =
  unsafeCoerce (prod_eqMixin t1 t2)

opt_eq :: Equality__Coq_type -> (Prelude.Maybe Equality__Coq_sort) ->
          (Prelude.Maybe Equality__Coq_sort) -> Prelude.Bool
opt_eq t u v =
  Ssrfun._Option__apply (\x ->
    Ssrfun._Option__apply (eq_op t x) Prelude.False v)
    (Prelude.not (Ssrbool.isSome v)) u

opt_eqP :: Equality__Coq_type -> Equality__Coq_axiom
           (Prelude.Maybe Equality__Coq_sort)
opt_eqP t _top_assumption_ =
  let {
   _evar_0_ = \x _top_assumption_0 ->
    let {_evar_0_ = \y -> Ssrbool.iffP (eq_op t x y) (eqP t x y)} in
    let {_evar_0_0 = Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     Prelude.Just x0 -> _evar_0_ x0;
     Prelude.Nothing -> _evar_0_0}}
  in
  let {
   _evar_0_0 = \_top_assumption_0 ->
    let {_evar_0_0 = \y -> Ssrbool.ReflectF} in
    let {_evar_0_1 = Ssrbool.ReflectT} in
    case _top_assumption_0 of {
     Prelude.Just x -> _evar_0_0 x;
     Prelude.Nothing -> _evar_0_1}}
  in
  case _top_assumption_ of {
   Prelude.Just x -> _evar_0_ x;
   Prelude.Nothing -> _evar_0_0}

option_eqMixin :: Equality__Coq_type -> Equality__Coq_mixin_of
                  (Prelude.Maybe Equality__Coq_sort)
option_eqMixin t =
  Equality__Mixin (opt_eq t) (opt_eqP t)

option_eqType :: Equality__Coq_type -> Equality__Coq_type
option_eqType t =
  unsafeCoerce (option_eqMixin t)

sum_eq :: Equality__Coq_type -> Equality__Coq_type -> (Prelude.Either
          Equality__Coq_sort Equality__Coq_sort) -> (Prelude.Either
          Equality__Coq_sort Equality__Coq_sort) -> Prelude.Bool
sum_eq t1 t2 u v =
  case u of {
   Prelude.Left x ->
    case v of {
     Prelude.Left y -> eq_op t1 x y;
     Prelude.Right s -> Prelude.False};
   Prelude.Right x ->
    case v of {
     Prelude.Left s -> Prelude.False;
     Prelude.Right y -> eq_op t2 x y}}

sum_eqP :: Equality__Coq_type -> Equality__Coq_type -> Equality__Coq_axiom
           (Prelude.Either Equality__Coq_sort Equality__Coq_sort)
sum_eqP t1 t2 _top_assumption_ =
  let {
   _evar_0_ = \x _top_assumption_0 ->
    let {_evar_0_ = \y -> Ssrbool.iffP (eq_op t1 x y) (eqP t1 x y)} in
    let {_evar_0_0 = \y -> Ssrbool.ReflectF} in
    case _top_assumption_0 of {
     Prelude.Left x0 -> _evar_0_ x0;
     Prelude.Right x0 -> _evar_0_0 x0}}
  in
  let {
   _evar_0_0 = \x _top_assumption_0 ->
    let {_evar_0_0 = \y -> Ssrbool.ReflectF} in
    let {_evar_0_1 = \y -> Ssrbool.iffP (eq_op t2 x y) (eqP t2 x y)} in
    case _top_assumption_0 of {
     Prelude.Left x0 -> _evar_0_0 x0;
     Prelude.Right x0 -> _evar_0_1 x0}}
  in
  case _top_assumption_ of {
   Prelude.Left x -> _evar_0_ x;
   Prelude.Right x -> _evar_0_0 x}

sum_eqMixin :: Equality__Coq_type -> Equality__Coq_type ->
               Equality__Coq_mixin_of
               (Prelude.Either Equality__Coq_sort Equality__Coq_sort)
sum_eqMixin t1 t2 =
  Equality__Mixin (sum_eq t1 t2) (sum_eqP t1 t2)

sum_eqType :: Equality__Coq_type -> Equality__Coq_type -> Equality__Coq_type
sum_eqType t1 t2 =
  unsafeCoerce (sum_eqMixin t1 t2)