{-# 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.AST.Argument 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.Primitive
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Reflection.AST.Argument.Information
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Reflection.AST.Argument.Args
d_Args_38 :: MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> ()
d_Args_38 :: T_Level_18 -> T_Level_18 -> T_Level_18
d_Args_38 = T_Level_18 -> T_Level_18 -> T_Level_18
forall a. a
erased
-- Reflection.AST.Argument.map
d_map_54 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88
d_map_54 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> T_Arg_88
-> T_Arg_88
d_map_54 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 T_Arg_88
v5 = (AgdaAny -> AgdaAny) -> T_Arg_88 -> T_Arg_88
du_map_54 AgdaAny -> AgdaAny
v4 T_Arg_88
v5
du_map_54 ::
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88
du_map_54 :: (AgdaAny -> AgdaAny) -> T_Arg_88 -> T_Arg_88
du_map_54 AgdaAny -> AgdaAny
v0 T_Arg_88
v1
  = case T_Arg_88 -> T_Arg_88
forall a b. a -> b
coe T_Arg_88
v1 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 T_ArgInfo_76
v2 AgdaAny
v3
        -> (T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> T_Arg_88
forall a b. a -> b
coe
             T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 (T_ArgInfo_76 -> AgdaAny
forall a b. a -> b
coe T_ArgInfo_76
v2) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v3)
      T_Arg_88
_ -> T_Arg_88
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Argument.map-Args
d_map'45'Args_62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88]
d_map'45'Args_62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> [T_Arg_88]
-> [T_Arg_88]
d_map'45'Args_62 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 AgdaAny -> AgdaAny
v4 [T_Arg_88]
v5 = (AgdaAny -> AgdaAny) -> [T_Arg_88] -> [T_Arg_88]
du_map'45'Args_62 AgdaAny -> AgdaAny
v4 [T_Arg_88]
v5
du_map'45'Args_62 ::
  (AgdaAny -> AgdaAny) ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88]
du_map'45'Args_62 :: (AgdaAny -> AgdaAny) -> [T_Arg_88] -> [T_Arg_88]
du_map'45'Args_62 AgdaAny -> AgdaAny
v0 [T_Arg_88]
v1
  = ((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T_Arg_88]
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22 (((AgdaAny -> AgdaAny) -> T_Arg_88 -> T_Arg_88)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny) -> T_Arg_88 -> T_Arg_88
du_map_54 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0))
      ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v1)
-- Reflection.AST.Argument.arg-injective₁
d_arg'45'injective'8321'_68 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_arg'45'injective'8321'_68 :: T_ArgInfo_76
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> T_ArgInfo_76
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_arg'45'injective'8321'_68 = T_ArgInfo_76
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> T_ArgInfo_76
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Argument.arg-injective₂
d_arg'45'injective'8322'_70 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_arg'45'injective'8322'_70 :: T_ArgInfo_76
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> T_ArgInfo_76
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_arg'45'injective'8322'_70 = T_ArgInfo_76
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> T_ArgInfo_76
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Argument.arg-injective
d_arg'45'injective_72 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_arg'45'injective_72 :: T_ArgInfo_76
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> T_ArgInfo_76
-> AgdaAny
-> T__'8801'__12
-> T_Σ_14
d_arg'45'injective_72 ~T_ArgInfo_76
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny
v3 ~T_ArgInfo_76
v4 ~AgdaAny
v5
  = T__'8801'__12 -> T_Σ_14
du_arg'45'injective_72
du_arg'45'injective_72 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_arg'45'injective_72 :: T__'8801'__12 -> T_Σ_14
du_arg'45'injective_72
  = ((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.Base.du_'60'_'44'_'62'_112 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Reflection.AST.Argument.unArg
d_unArg_74 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 -> AgdaAny
d_unArg_74 :: T_Level_18 -> T_Level_18 -> T_Arg_88 -> AgdaAny
d_unArg_74 ~T_Level_18
v0 ~T_Level_18
v1 T_Arg_88
v2 = T_Arg_88 -> AgdaAny
du_unArg_74 T_Arg_88
v2
du_unArg_74 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 -> AgdaAny
du_unArg_74 :: T_Arg_88 -> AgdaAny
du_unArg_74 T_Arg_88
v0
  = case T_Arg_88 -> T_Arg_88
forall a b. a -> b
coe T_Arg_88
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 T_ArgInfo_76
v1 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T_Arg_88
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Argument.unArg-dec
d_unArg'45'dec_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_unArg'45'dec_84 :: T_Level_18
-> T_Level_18 -> T_Arg_88 -> T_Arg_88 -> T_Dec_20 -> T_Dec_20
d_unArg'45'dec_84 ~T_Level_18
v0 ~T_Level_18
v1 T_Arg_88
v2 T_Arg_88
v3 T_Dec_20
v4 = T_Arg_88 -> T_Arg_88 -> T_Dec_20 -> T_Dec_20
du_unArg'45'dec_84 T_Arg_88
v2 T_Arg_88
v3 T_Dec_20
v4
du_unArg'45'dec_84 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_unArg'45'dec_84 :: T_Arg_88 -> T_Arg_88 -> T_Dec_20 -> T_Dec_20
du_unArg'45'dec_84 T_Arg_88
v0 T_Arg_88
v1 T_Dec_20
v2
  = case T_Arg_88 -> T_Arg_88
forall a b. a -> b
coe T_Arg_88
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 T_ArgInfo_76
v3 AgdaAny
v4
        -> case T_Arg_88 -> T_Arg_88
forall a b. a -> b
coe T_Arg_88
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 T_ArgInfo_76
v5 AgdaAny
v6
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
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.Base.du_uncurry_244 AgdaAny
forall a. a
erased)
                    ((T__'8801'__12 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_arg'45'injective_72)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       ((T_ArgInfo_76 -> T_ArgInfo_76 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_ArgInfo_76 -> T_ArgInfo_76 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Argument.Information.d__'8799'__30
                          (T_ArgInfo_76 -> AgdaAny
forall a b. a -> b
coe T_ArgInfo_76
v3) (T_ArgInfo_76 -> AgdaAny
forall a b. a -> b
coe T_ArgInfo_76
v5))
                       (T_Dec_20 -> AgdaAny
forall a b. a -> b
coe T_Dec_20
v2))
             T_Arg_88
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Arg_88
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Argument.≡-dec
d_'8801''45'dec_96 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_'8801''45'dec_96 :: T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_Arg_88
-> T_Arg_88
-> T_Dec_20
d_'8801''45'dec_96 ~T_Level_18
v0 ~T_Level_18
v1 AgdaAny -> AgdaAny -> T_Dec_20
v2 T_Arg_88
v3 T_Arg_88
v4 = (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_Arg_88 -> T_Arg_88 -> T_Dec_20
du_'8801''45'dec_96 AgdaAny -> AgdaAny -> T_Dec_20
v2 T_Arg_88
v3 T_Arg_88
v4
du_'8801''45'dec_96 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_'8801''45'dec_96 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_Arg_88 -> T_Arg_88 -> T_Dec_20
du_'8801''45'dec_96 AgdaAny -> AgdaAny -> T_Dec_20
v0 T_Arg_88
v1 T_Arg_88
v2
  = (T_Arg_88 -> T_Arg_88 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      T_Arg_88 -> T_Arg_88 -> T_Dec_20 -> T_Dec_20
du_unArg'45'dec_84 (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
v1) (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
v2)
      ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 ((T_Arg_88 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Arg_88 -> AgdaAny
du_unArg_74 (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
v1)) ((T_Arg_88 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Arg_88 -> AgdaAny
du_unArg_74 (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
v2)))