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

module LinearScan.Yoneda 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.Monad as Monad



#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 Yoneda f a = () -> (a -> Any) -> f

data Isomorphism a b =
   Build_Isomorphism (a -> b) (b -> a)

iso_to :: (Isomorphism a1 a2) -> a1 -> a2
iso_to isomorphism =
  case isomorphism of {
   Build_Isomorphism iso_to0 iso_from -> iso_to0}

coq_Yoneda_lemma :: (Monad.Functor a1) -> Isomorphism (Yoneda a1 a2) a1
coq_Yoneda_lemma h =
  Build_Isomorphism (\x -> unsafeCoerce x __ (\x0 -> x0)) (\x _ k ->
    Monad.fmap h k x)

coq_Yoneda_Functor :: Monad.Functor (Yoneda a1 Any)
coq_Yoneda_Functor _ _ g k _ h =
  k __ ((Prelude..) h g)

coq_Yoneda_Applicative :: (Monad.Applicative a1) -> Monad.Applicative
                          (Yoneda a1 Any)
coq_Yoneda_Applicative h =
  Monad.Build_Applicative coq_Yoneda_Functor (\_ x _ k -> Monad.pure h (k x))
    (\_ _ g x _ k ->
    Monad.ap h (unsafeCoerce g __ ((Prelude..) k))
      (iso_to (coq_Yoneda_lemma (Monad.is_functor h)) x))

coq_Yoneda_join :: (Monad.Monad a1) -> (Yoneda a1 (Yoneda a1 a2)) -> (a2 ->
                   a3) -> a1
coq_Yoneda_join h k h0 =
  Monad.join h (unsafeCoerce k __ (\y -> y __ h0))

coq_Yoneda_Monad :: (Monad.Monad a1) -> Monad.Monad (Yoneda a1 Any)
coq_Yoneda_Monad h =
  Monad.Build_Monad (coq_Yoneda_Applicative (Monad.is_applicative h))
    (unsafeCoerce (\_ x _ -> coq_Yoneda_join h x))