{-# 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.Information where

import Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Equality qualified
import MAlonzo.Code.Agda.Builtin.Reflection qualified
import MAlonzo.Code.Agda.Builtin.Sigma qualified
import MAlonzo.Code.Data.Product.Base qualified
import MAlonzo.Code.Reflection.AST.Argument.Modality qualified
import MAlonzo.Code.Reflection.AST.Argument.Visibility qualified
import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                    mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                    word64ToNat)
import MAlonzo.RTE qualified

-- Reflection.AST.Argument.Information.visibility
d_visibility_16 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48
d_visibility_16 :: T_ArgInfo_76 -> T_Visibility_48
d_visibility_16 T_ArgInfo_76
v0
  = case T_ArgInfo_76 -> T_ArgInfo_76
forall a b. a -> b
coe T_ArgInfo_76
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82 T_Visibility_48
v1 T_Modality_68
v2
        -> T_Visibility_48 -> T_Visibility_48
forall a b. a -> b
coe T_Visibility_48
v1
      T_ArgInfo_76
_ -> T_Visibility_48
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Argument.Information.modality
d_modality_20 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Modality_68
d_modality_20 :: T_ArgInfo_76 -> T_Modality_68
d_modality_20 T_ArgInfo_76
v0
  = case T_ArgInfo_76 -> T_ArgInfo_76
forall a b. a -> b
coe T_ArgInfo_76
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82 T_Visibility_48
v1 T_Modality_68
v2
        -> T_Modality_68 -> T_Modality_68
forall a b. a -> b
coe T_Modality_68
v2
      T_ArgInfo_76
_ -> T_Modality_68
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Argument.Information.arg-info-injective₁
d_arg'45'info'45'injective'8321'_24 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Modality_68 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Modality_68 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_arg'45'info'45'injective'8321'_24 :: T_Visibility_48
-> T_Modality_68
-> T_Visibility_48
-> T_Modality_68
-> T__'8801'__12
-> T__'8801'__12
d_arg'45'info'45'injective'8321'_24 = T_Visibility_48
-> T_Modality_68
-> T_Visibility_48
-> T_Modality_68
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Argument.Information.arg-info-injective₂
d_arg'45'info'45'injective'8322'_26 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Modality_68 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Modality_68 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_arg'45'info'45'injective'8322'_26 :: T_Visibility_48
-> T_Modality_68
-> T_Visibility_48
-> T_Modality_68
-> T__'8801'__12
-> T__'8801'__12
d_arg'45'info'45'injective'8322'_26 = T_Visibility_48
-> T_Modality_68
-> T_Visibility_48
-> T_Modality_68
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Argument.Information.arg-info-injective
d_arg'45'info'45'injective_28 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Modality_68 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Modality_68 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_arg'45'info'45'injective_28 :: T_Visibility_48
-> T_Modality_68
-> T_Visibility_48
-> T_Modality_68
-> T__'8801'__12
-> T_Σ_14
d_arg'45'info'45'injective_28 ~T_Visibility_48
v0 ~T_Modality_68
v1 ~T_Visibility_48
v2 ~T_Modality_68
v3
  = T__'8801'__12 -> T_Σ_14
du_arg'45'info'45'injective_28
du_arg'45'info'45'injective_28 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_arg'45'info'45'injective_28 :: T__'8801'__12 -> T_Σ_14
du_arg'45'info'45'injective_28
  = ((Any -> Any) -> (Any -> Any) -> Any -> T_Σ_14)
-> Any -> Any -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> Any -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 Any
forall a. a
erased Any
forall a. a
erased
-- Reflection.AST.Argument.Information._≟_
d__'8799'__30 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_ArgInfo_76 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799'__30 :: T_ArgInfo_76 -> T_ArgInfo_76 -> T_Dec_20
d__'8799'__30 T_ArgInfo_76
v0 T_ArgInfo_76
v1
  = case T_ArgInfo_76 -> T_ArgInfo_76
forall a b. a -> b
coe T_ArgInfo_76
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82 T_Visibility_48
v2 T_Modality_68
v3
        -> case T_ArgInfo_76 -> T_ArgInfo_76
forall a b. a -> b
coe T_ArgInfo_76
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82 T_Visibility_48
v4 T_Modality_68
v5
               -> ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> Any -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
                    (Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((Any -> Any -> Any) -> T_Σ_14 -> Any) -> Any -> Any
forall a b. a -> b
coe (Any -> Any -> Any) -> T_Σ_14 -> Any
MAlonzo.Code.Data.Product.Base.du_uncurry_244 Any
forall a. a
erased)
                    ((T__'8801'__12 -> T_Σ_14) -> Any
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_arg'45'info'45'injective_28)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
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_Visibility_48 -> T_Visibility_48 -> T_Dec_20)
-> Any -> Any -> Any
forall a b. a -> b
coe
                          T_Visibility_48 -> T_Visibility_48 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Argument.Visibility.d__'8799'__8
                          (T_Visibility_48 -> Any
forall a b. a -> b
coe T_Visibility_48
v2) (T_Visibility_48 -> Any
forall a b. a -> b
coe T_Visibility_48
v4))
                       ((T_Modality_68 -> T_Modality_68 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                          T_Modality_68 -> T_Modality_68 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Argument.Modality.d__'8799'__30
                          (T_Modality_68 -> Any
forall a b. a -> b
coe T_Modality_68
v3) (T_Modality_68 -> Any
forall a b. a -> b
coe T_Modality_68
v5)))
             T_ArgInfo_76
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_ArgInfo_76
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError