{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Effect.Functor where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Level

-- Effect.Functor.RawFunctor
d_RawFunctor_24 :: p -> p -> p -> ()
d_RawFunctor_24 p
a0 p
a1 p
a2 = ()
newtype T_RawFunctor_24
  = C_RawFunctor'46'constructor_241 (() ->
                                     () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-- Effect.Functor.RawFunctor._<$>_
d__'60''36''62'__30 ::
  T_RawFunctor_24 ->
  () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d__'60''36''62'__30 :: T_RawFunctor_24
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d__'60''36''62'__30 T_RawFunctor_24
v0
  = case T_RawFunctor_24 -> T_RawFunctor_24
forall a b. a -> b
coe T_RawFunctor_24
v0 of
      C_RawFunctor'46'constructor_241 () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
v1 -> (() -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
v1
      T_RawFunctor_24
_ -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Effect.Functor.RawFunctor._<$_
d__'60''36'__32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() -> ()) ->
  T_RawFunctor_24 -> () -> () -> AgdaAny -> AgdaAny -> AgdaAny
d__'60''36'__32 :: ()
-> ()
-> (() -> ())
-> T_RawFunctor_24
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
d__'60''36'__32 ~()
v0 ~()
v1 ~() -> ()
v2 T_RawFunctor_24
v3 ~()
v4 ~()
v5 AgdaAny
v6 AgdaAny
v7
  = T_RawFunctor_24 -> AgdaAny -> AgdaAny -> AgdaAny
du__'60''36'__32 T_RawFunctor_24
v3 AgdaAny
v6 AgdaAny
v7
du__'60''36'__32 ::
  T_RawFunctor_24 -> AgdaAny -> AgdaAny -> AgdaAny
du__'60''36'__32 :: T_RawFunctor_24 -> AgdaAny -> AgdaAny -> AgdaAny
du__'60''36'__32 T_RawFunctor_24
v0 AgdaAny
v1 AgdaAny
v2
  = (T_RawFunctor_24
 -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> T_RawFunctor_24
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_RawFunctor_24
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d__'60''36''62'__30 T_RawFunctor_24
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased (\ AgdaAny
v3 -> AgdaAny
v1) AgdaAny
v2
-- Effect.Functor.RawFunctor._<&>_
d__'60''38''62'__38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() -> ()) ->
  T_RawFunctor_24 ->
  () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
d__'60''38''62'__38 :: ()
-> ()
-> (() -> ())
-> T_RawFunctor_24
-> ()
-> ()
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
d__'60''38''62'__38 ~()
v0 ~()
v1 ~() -> ()
v2 T_RawFunctor_24
v3 ~()
v4 ~()
v5 AgdaAny
v6 AgdaAny -> AgdaAny
v7
  = T_RawFunctor_24 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
du__'60''38''62'__38 T_RawFunctor_24
v3 AgdaAny
v6 AgdaAny -> AgdaAny
v7
du__'60''38''62'__38 ::
  T_RawFunctor_24 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
du__'60''38''62'__38 :: T_RawFunctor_24 -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
du__'60''38''62'__38 T_RawFunctor_24
v0 AgdaAny
v1 AgdaAny -> AgdaAny
v2
  = (T_RawFunctor_24
 -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> T_RawFunctor_24
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_RawFunctor_24
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d__'60''36''62'__30 T_RawFunctor_24
v0 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased AgdaAny -> AgdaAny
v2 AgdaAny
v1
-- Effect.Functor.RawFunctor.ignore
d_ignore_40 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (() -> ()) -> T_RawFunctor_24 -> () -> AgdaAny -> AgdaAny
d_ignore_40 :: ()
-> () -> (() -> ()) -> T_RawFunctor_24 -> () -> AgdaAny -> AgdaAny
d_ignore_40 ~()
v0 ~()
v1 ~() -> ()
v2 T_RawFunctor_24
v3 ~()
v4 = T_RawFunctor_24 -> AgdaAny -> AgdaAny
du_ignore_40 T_RawFunctor_24
v3
du_ignore_40 :: T_RawFunctor_24 -> AgdaAny -> AgdaAny
du_ignore_40 :: T_RawFunctor_24 -> AgdaAny -> AgdaAny
du_ignore_40 T_RawFunctor_24
v0
  = (T_RawFunctor_24 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_RawFunctor_24 -> AgdaAny -> AgdaAny -> AgdaAny
du__'60''36'__32 (T_RawFunctor_24 -> AgdaAny
forall a b. a -> b
coe T_RawFunctor_24
v0)
      ((AgdaAny -> T_Lift_8) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> T_Lift_8
MAlonzo.Code.Level.C_lift_20
         (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
-- Effect.Functor.Morphism
d_Morphism_58 :: p -> p -> p -> p -> p -> p -> p -> ()
d_Morphism_58 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 = ()
newtype T_Morphism_58
  = C_Morphism'46'constructor_3741 (() -> AgdaAny -> AgdaAny)
-- Effect.Functor.Morphism.op
d_op_76 :: T_Morphism_58 -> () -> AgdaAny -> AgdaAny
d_op_76 :: T_Morphism_58 -> () -> AgdaAny -> AgdaAny
d_op_76 T_Morphism_58
v0
  = case T_Morphism_58 -> T_Morphism_58
forall a b. a -> b
coe T_Morphism_58
v0 of
      C_Morphism'46'constructor_3741 () -> AgdaAny -> AgdaAny
v1 -> (() -> AgdaAny -> AgdaAny) -> () -> AgdaAny -> AgdaAny
forall a b. a -> b
coe () -> AgdaAny -> AgdaAny
v1
      T_Morphism_58
_ -> () -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Effect.Functor.Morphism.op-<$>
d_op'45''60''36''62'_82 ::
  T_Morphism_58 ->
  () ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_op'45''60''36''62'_82 :: T_Morphism_58
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> T__'8801'__12
d_op'45''60''36''62'_82 = T_Morphism_58
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> T__'8801'__12
forall a. a
erased