{-# 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.Reflection.Abstraction 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.Reflection
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Data.String.Properties
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Product

-- Reflection.Abstraction.map
d_map_12 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112
d_map_12 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> T_Abs_112
-> T_Abs_112
d_map_12 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 T_Abs_112
v5 = (AgdaAny -> AgdaAny) -> T_Abs_112 -> T_Abs_112
du_map_12 AgdaAny -> AgdaAny
v4 T_Abs_112
v5
du_map_12 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112
du_map_12 :: (AgdaAny -> AgdaAny) -> T_Abs_112 -> T_Abs_112
du_map_12 AgdaAny -> AgdaAny
v0 T_Abs_112
v1
  = case T_Abs_112 -> T_Abs_112
forall a b. a -> b
coe T_Abs_112
v1 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 T_String_6
v2 AgdaAny
v3
        -> (T_String_6 -> AgdaAny -> T_Abs_112)
-> AgdaAny -> AgdaAny -> T_Abs_112
forall a b. a -> b
coe
             T_String_6 -> AgdaAny -> T_Abs_112
MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 (T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3)
      T_Abs_112
_ -> T_Abs_112
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.Abstraction.abs-injective₁
d_abs'45'injective'8321'_28 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_abs'45'injective'8321'_28 :: T_Level_18
-> T_Level_18
-> T_String_6
-> T_String_6
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_abs'45'injective'8321'_28 = T_Level_18
-> T_Level_18
-> T_String_6
-> T_String_6
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.Abstraction.abs-injective₂
d_abs'45'injective'8322'_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_abs'45'injective'8322'_38 :: T_Level_18
-> T_Level_18
-> T_String_6
-> T_String_6
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_abs'45'injective'8322'_38 = T_Level_18
-> T_Level_18
-> T_String_6
-> T_String_6
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.Abstraction.abs-injective
d_abs'45'injective_48 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_abs'45'injective_48 :: T_Level_18
-> T_Level_18
-> T_String_6
-> T_String_6
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T_Σ_14
d_abs'45'injective_48 ~T_Level_18
v0 ~T_Level_18
v1 ~T_String_6
v2 ~T_String_6
v3 ~AgdaAny
v4 ~AgdaAny
v5
  = T__'8801'__12 -> T_Σ_14
du_abs'45'injective_48
du_abs'45'injective_48 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_abs'45'injective_48 :: T__'8801'__12 -> T_Σ_14
du_abs'45'injective_48
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.du_'60'_'44'_'62'_132 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Reflection.Abstraction.unAbs
d_unAbs_50 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 -> AgdaAny
d_unAbs_50 :: T_Level_18 -> T_Level_18 -> T_Abs_112 -> AgdaAny
d_unAbs_50 ~T_Level_18
v0 ~T_Level_18
v1 T_Abs_112
v2 = T_Abs_112 -> AgdaAny
du_unAbs_50 T_Abs_112
v2
du_unAbs_50 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 -> AgdaAny
du_unAbs_50 :: T_Abs_112 -> AgdaAny
du_unAbs_50 T_Abs_112
v0
  = case T_Abs_112 -> T_Abs_112
forall a b. a -> b
coe T_Abs_112
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 T_String_6
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T_Abs_112
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.Abstraction.unAbs-dec
d_unAbs'45'dec_60 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d_unAbs'45'dec_60 :: T_Level_18
-> T_Level_18 -> T_Abs_112 -> T_Abs_112 -> T_Dec_32 -> T_Dec_32
d_unAbs'45'dec_60 ~T_Level_18
v0 ~T_Level_18
v1 T_Abs_112
v2 T_Abs_112
v3 T_Dec_32
v4 = T_Abs_112 -> T_Abs_112 -> T_Dec_32 -> T_Dec_32
du_unAbs'45'dec_60 T_Abs_112
v2 T_Abs_112
v3 T_Dec_32
v4
du_unAbs'45'dec_60 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du_unAbs'45'dec_60 :: T_Abs_112 -> T_Abs_112 -> T_Dec_32 -> T_Dec_32
du_unAbs'45'dec_60 T_Abs_112
v0 T_Abs_112
v1 T_Dec_32
v2
  = case T_Abs_112 -> T_Abs_112
forall a b. a -> b
coe T_Abs_112
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 T_String_6
v3 AgdaAny
v4
        -> case T_Abs_112 -> T_Abs_112
forall a b. a -> b
coe T_Abs_112
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 T_String_6
v5 AgdaAny
v6
               -> ((AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.du_uncurry_264 AgdaAny
forall a. a
erased)
                    ((T_Dec_32 -> T_Dec_32 -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_32 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Product.du__'215''45'dec__30
                       ((T_String_6 -> T_String_6 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_String_6 -> T_String_6 -> T_Dec_32
MAlonzo.Code.Data.String.Properties.d__'8799'__54 (T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6
v3)
                          (T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6
v5))
                       (T_Dec_32 -> AgdaAny
forall a b. a -> b
coe T_Dec_32
v2))
             T_Abs_112
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Abs_112
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.Abstraction.≡-dec
d_'8801''45'dec_72 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'8801''45'dec_72 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_Abs_112
-> T_Abs_112
-> T_Dec_32
d_'8801''45'dec_72 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 T_Abs_112
v3 T_Abs_112
v4 = (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_Abs_112 -> T_Abs_112 -> T_Dec_32
du_'8801''45'dec_72 AgdaAny -> AgdaAny -> T_Dec_32
v2 T_Abs_112
v3 T_Abs_112
v4
du_'8801''45'dec_72 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'8801''45'dec_72 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_Abs_112 -> T_Abs_112 -> T_Dec_32
du_'8801''45'dec_72 AgdaAny -> AgdaAny -> T_Dec_32
v0 T_Abs_112
v1 T_Abs_112
v2
  = (T_Abs_112 -> T_Abs_112 -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
      T_Abs_112 -> T_Abs_112 -> T_Dec_32 -> T_Dec_32
du_unAbs'45'dec_60 (T_Abs_112 -> AgdaAny
forall a b. a -> b
coe T_Abs_112
v1) (T_Abs_112 -> AgdaAny
forall a b. a -> b
coe T_Abs_112
v2)
      ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0 ((T_Abs_112 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Abs_112 -> AgdaAny
du_unAbs_50 (T_Abs_112 -> AgdaAny
forall a b. a -> b
coe T_Abs_112
v1)) ((T_Abs_112 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Abs_112 -> AgdaAny
du_unAbs_50 (T_Abs_112 -> AgdaAny
forall a b. a -> b
coe T_Abs_112
v2)))