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

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



#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 Functor f =
  () -> () -> (Any -> Any) -> f -> f
  -- singleton inductive, whose constructor was Build_Functor
  
fmap :: (Functor a1) -> (a2 -> a3) -> a1 -> a1
fmap functor x x0 =
  unsafeCoerce functor __ __ x x0

apply :: (a1 -> a2) -> a1 -> a2
apply f x =
  f x

first :: (a1 -> a2) -> ((,) a1 a3) -> (,) a2 a3
first f x =
  case x of {
   (,) a z -> (,) (f a) z}

curry :: (a1 -> a2 -> a3) -> ((,) a1 a2) -> a3
curry f x =
  case x of {
   (,) a b -> f a b}

data Applicative f =
   Build_Applicative (Functor f) (() -> Any -> f) (() -> () -> f -> f -> f)

is_functor :: (Applicative a1) -> Functor a1
is_functor applicative =
  case applicative of {
   Build_Applicative is_functor0 pure0 ap0 -> is_functor0}

pure :: (Applicative a1) -> a2 -> a1
pure applicative x =
  case applicative of {
   Build_Applicative is_functor0 pure0 ap0 -> unsafeCoerce pure0 __ x}

ap :: (Applicative a1) -> a1 -> a1 -> a1
ap applicative x x0 =
  case applicative of {
   Build_Applicative is_functor0 pure0 ap0 -> ap0 __ __ x x0}

data Monad m =
   Build_Monad (Applicative m) (() -> m -> m)

is_applicative :: (Monad a1) -> Applicative a1
is_applicative monad =
  case monad of {
   Build_Monad is_applicative0 join0 -> is_applicative0}

join :: (Monad a1) -> a1 -> a1
join monad x =
  case monad of {
   Build_Monad is_applicative0 join0 -> join0 __ x}

liftA2 :: (Applicative a1) -> (a2 -> a3 -> a4) -> a1 -> a1 -> a1
liftA2 h f x y =
  ap h (fmap (is_functor h) f x) y

bind :: (Monad a1) -> (a2 -> a1) -> a1 -> a1
bind h f =
  (Prelude..) (join h) (fmap (is_functor (is_applicative h)) f)

mapM :: (Applicative a1) -> (a2 -> a1) -> ([] a2) -> a1
mapM h f l =
  case l of {
   [] -> pure h [];
   (:) x xs -> liftA2 h (\x0 x1 -> (:) x0 x1) (f x) (mapM h f xs)}

mapM_ :: (Monad a1) -> (a2 -> a1) -> ([] a2) -> a1
mapM_ h f l =
  case l of {
   [] -> pure (is_applicative h) ();
   (:) x xs -> bind h (\x0 -> mapM_ h f xs) (f x)}

forM_ :: (Monad a1) -> ([] a2) -> (a2 -> a1) -> a1
forM_ h l f =
  mapM_ h f l

foldM :: (Monad a1) -> (a2 -> a3 -> a1) -> a2 -> ([] a3) -> a1
foldM h f s l =
  case l of {
   [] -> pure (is_applicative h) s;
   (:) y ys -> bind h (\x -> foldM h f x ys) (f s y)}

forFoldM :: (Monad a1) -> a2 -> ([] a3) -> (a2 -> a3 -> a1) -> a1
forFoldM h s l f =
  foldM h f s l

foldrM :: (Monad a1) -> (a3 -> a2 -> a1) -> a2 -> ([] a3) -> a1
foldrM h f s l =
  case l of {
   [] -> pure (is_applicative h) s;
   (:) y ys -> bind h (f y) (foldrM h f s ys)}

forFoldrM :: (Monad a1) -> a2 -> ([] a3) -> (a3 -> a2 -> a1) -> a1
forFoldrM h s l f =
  foldrM h f s l

concat :: ([] ([] a1)) -> [] a1
concat l =
  case l of {
   [] -> [];
   (:) x xs -> (Prelude.++) x (concat xs)}

concatMapM :: (Applicative a1) -> (a2 -> a1) -> ([] a2) -> a1
concatMapM h f l =
  fmap (is_functor h) concat (mapM h f l)

insertM :: (Monad a1) -> (a2 -> a2 -> a1) -> a2 -> ([] a2) -> a1
insertM h p z l =
  case l of {
   [] -> pure (is_applicative h) ((:) z []);
   (:) x xs ->
    bind h (\b ->
      case b of {
       Prelude.True ->
        fmap (is_functor (is_applicative h)) (\x0 -> (:) x x0)
          (insertM h p z xs);
       Prelude.False -> pure (is_applicative h) ((:) z ((:) x xs))}) 
      (p x z)}

type State s a = s -> (,) a s

modify :: (a1 -> a1) -> State a1 ()
modify f i =
  (,) () (f i)

coq_State_Functor :: Functor (State a1 Any)
coq_State_Functor _ _ f x st =
  let {filtered_var = x st} in
  case filtered_var of {
   (,) a st' -> (,) (f a) st'}

coq_State_Applicative :: Applicative (State a1 Any)
coq_State_Applicative =
  Build_Applicative coq_State_Functor (\_ x st -> (,) x st) (\_ _ f x st ->
    let {filtered_var = f st} in
    case filtered_var of {
     (,) f' st' ->
      unsafeCoerce (\f'0 st'0 _ ->
        let {filtered_var0 = x st'0} in
        case filtered_var0 of {
         (,) x' st'' -> (,) (f'0 x') st''}) f' st' __})

coq_State_Monad :: Monad (State a1 Any)
coq_State_Monad =
  Build_Monad coq_State_Applicative (\_ x st ->
    let {filtered_var = x st} in
    case filtered_var of {
     (,) y st' ->
      unsafeCoerce (\y0 st'0 _ ->
        let {filtered_var0 = y0 st'0} in
        case filtered_var0 of {
         (,) a st'' -> (,) a st''}) y st' __})

type StateT s m a = s -> m

getT :: (Applicative a1) -> StateT a2 a1 a2
getT h i =
  pure h ((,) i i)

getsT :: (Applicative a1) -> (a2 -> a3) -> StateT a2 a1 a3
getsT h f s =
  pure h ((,) (f s) s)

putT :: (Applicative a1) -> a2 -> StateT a2 a1 ()
putT h x x0 =
  pure h ((,) () x)

modifyT :: (Applicative a1) -> (a2 -> a2) -> StateT a2 a1 ()
modifyT h f i =
  pure h ((,) () (f i))

coq_StateT_Functor :: (Functor a2) -> Functor (StateT a1 a2 Any)
coq_StateT_Functor h _ _ f x st =
  fmap h (first f) (x st)

coq_StateT_ap :: (Monad a1) -> (StateT a2 a1 (a3 -> a4)) -> (StateT a2 
                 a1 a3) -> StateT a2 a1 a4
coq_StateT_ap h f x st =
  join h
    (fmap (is_functor (is_applicative h)) (\z ->
      case z of {
       (,) f' st' -> fmap (is_functor (is_applicative h)) (first f') (x st')})
      (f st))

coq_StateT_Applicative :: (Monad a1) -> Applicative (StateT a2 a1 Any)
coq_StateT_Applicative h =
  Build_Applicative (coq_StateT_Functor (is_functor (is_applicative h)))
    (\_ x st -> pure (is_applicative h) ((,) x st)) (\_ _ -> coq_StateT_ap h)

coq_StateT_join :: (Monad a1) -> (StateT a2 a1 (StateT a2 a1 a3)) -> StateT
                   a2 a1 a3
coq_StateT_join h x =
  (Prelude..)
    ((Prelude..) (join h)
      (fmap (is_functor (is_applicative h)) (curry apply))) x

coq_StateT_Monad :: (Monad a1) -> Monad (StateT a2 a1 Any)
coq_StateT_Monad h =
  Build_Monad (coq_StateT_Applicative h) (\_ -> coq_StateT_join h)

lift :: (Monad a1) -> a1 -> StateT a2 a1 a3
lift h x st =
  fmap (is_functor (is_applicative h)) (\z -> (,) z st) x