{-# 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.Show 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.Float
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.Data.List.Base
import qualified MAlonzo.Code.Data.Nat.Show
import qualified MAlonzo.Code.Data.String
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Reflection.AST.Argument
import qualified MAlonzo.Code.Reflection.AST.Argument.Information

-- Reflection.AST.Show.showRelevance
d_showRelevance_6 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Relevance_56 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showRelevance_6 :: T_Relevance_56 -> Text
d_showRelevance_6 T_Relevance_56
v0
  = case T_Relevance_56 -> T_Relevance_56
forall a b. a -> b
coe T_Relevance_56
v0 of
      T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58
        -> Text -> Text
forall a b. a -> b
coe (Text
"relevant" :: Data.Text.Text)
      T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_irrelevant_60
        -> Text -> Text
forall a b. a -> b
coe (Text
"irrelevant" :: Data.Text.Text)
      T_Relevance_56
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showRel
d_showRel_8 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Relevance_56 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showRel_8 :: T_Relevance_56 -> Text
d_showRel_8 T_Relevance_56
v0
  = case T_Relevance_56 -> T_Relevance_56
forall a b. a -> b
coe T_Relevance_56
v0 of
      T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58
        -> Text -> Text
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
      T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_irrelevant_60
        -> Text -> Text
forall a b. a -> b
coe (Text
"." :: Data.Text.Text)
      T_Relevance_56
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showVisibility
d_showVisibility_10 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showVisibility_10 :: T_Visibility_48 -> Text
d_showVisibility_10 T_Visibility_48
v0
  = case T_Visibility_48 -> T_Visibility_48
forall a b. a -> b
coe T_Visibility_48
v0 of
      T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50
        -> Text -> Text
forall a b. a -> b
coe (Text
"visible" :: Data.Text.Text)
      T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_hidden_52
        -> Text -> Text
forall a b. a -> b
coe (Text
"hidden" :: Data.Text.Text)
      T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_instance'8242'_54
        -> Text -> Text
forall a b. a -> b
coe (Text
"instance" :: Data.Text.Text)
      T_Visibility_48
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showQuantity
d_showQuantity_12 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Quantity_62 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showQuantity_12 :: T_Quantity_62 -> Text
d_showQuantity_12 T_Quantity_62
v0
  = case T_Quantity_62 -> T_Quantity_62
forall a b. a -> b
coe T_Quantity_62
v0 of
      T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'0_64
        -> Text -> Text
forall a b. a -> b
coe (Text
"quantity-0" :: Data.Text.Text)
      T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66
        -> Text -> Text
forall a b. a -> b
coe (Text
"quantity-\969" :: Data.Text.Text)
      T_Quantity_62
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showLiteral
d_showLiteral_14 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Literal_124 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showLiteral_14 :: T_Literal_124 -> Text
d_showLiteral_14 T_Literal_124
v0
  = case T_Literal_124 -> T_Literal_124
forall a b. a -> b
coe T_Literal_124
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_nat_128 Integer
v1
        -> (Integer -> Text) -> Integer -> Text
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v1
      MAlonzo.Code.Agda.Builtin.Reflection.C_word64_132 Word64
v1
        -> (Integer -> Text) -> Integer -> Text
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 (Word64 -> Integer
word64ToNat (Word64 -> Word64
forall a b. a -> b
coe Word64
v1))
      MAlonzo.Code.Agda.Builtin.Reflection.C_float_136 T_Float_6
v1
        -> (T_Float_6 -> Text) -> T_Float_6 -> Text
forall a b. a -> b
coe T_Float_6 -> Text
MAlonzo.Code.Agda.Builtin.Float.d_primShowFloat_46 T_Float_6
v1
      MAlonzo.Code.Agda.Builtin.Reflection.C_char_140 T_Char_6
v1
        -> (T_Char_6 -> Text) -> T_Char_6 -> Text
forall a b. a -> b
coe T_Char_6 -> Text
MAlonzo.Code.Agda.Builtin.String.d_primShowChar_20 T_Char_6
v1
      MAlonzo.Code.Agda.Builtin.Reflection.C_string_144 Text
v1
        -> (Text -> Text) -> Text -> Text
forall a b. a -> b
coe Text -> Text
MAlonzo.Code.Agda.Builtin.String.d_primShowString_22 Text
v1
      MAlonzo.Code.Agda.Builtin.Reflection.C_name_148 AgdaAny
v1
        -> (QName -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe QName -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowQName_12 AgdaAny
v1
      MAlonzo.Code.Agda.Builtin.Reflection.C_meta_152 AgdaAny
v1
        -> ((Integer, Integer) -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe (Integer, Integer) -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowMeta_44 AgdaAny
v1
      T_Literal_124
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.visibilityParen
d_visibilityParen_30 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_visibilityParen_30 :: T_Visibility_48 -> Text -> Text
d_visibilityParen_30 T_Visibility_48
v0 Text
v1
  = case T_Visibility_48 -> T_Visibility_48
forall a b. a -> b
coe T_Visibility_48
v0 of
      T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50
        -> (Text -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe Text -> Text
MAlonzo.Code.Data.String.d_parensIfSpace_130 (Text -> AgdaAny
forall a b. a -> b
coe Text
v1)
      T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_hidden_52
        -> (Text -> Text) -> Text -> Text
forall a b. a -> b
coe Text -> Text
MAlonzo.Code.Data.String.Base.d_braces_48 Text
v1
      T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_instance'8242'_54
        -> (Text -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text
MAlonzo.Code.Data.String.Base.d_braces_48
             ((Text -> Text) -> Text -> AgdaAny
forall a b. a -> b
coe Text -> Text
MAlonzo.Code.Data.String.Base.d_braces_48 Text
v1)
      T_Visibility_48
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showTerms
d_showTerms_38 ::
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showTerms_38 :: [T_Arg_88] -> Text
d_showTerms_38 [T_Arg_88]
v0
  = case [T_Arg_88] -> [AgdaAny]
forall a b. a -> b
coe [T_Arg_88]
v0 of
      [] -> Text -> Text
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
      (:) AgdaAny
v1 [AgdaAny]
v2
        -> case AgdaAny -> T_Arg_88
forall a b. a -> b
coe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 T_ArgInfo_76
v3 AgdaAny
v4
               -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
                    Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                    ((T_Visibility_48 -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Visibility_48 -> Text -> Text
d_visibilityParen_30
                       ((T_ArgInfo_76 -> T_Visibility_48) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_ArgInfo_76 -> T_Visibility_48
MAlonzo.Code.Reflection.AST.Argument.Information.d_visibility_16
                          (T_ArgInfo_76 -> AgdaAny
forall a b. a -> b
coe T_ArgInfo_76
v3))
                       ((T_Term_154 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> Text
d_showTerm_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)))
                    (([T_Arg_88] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> Text
d_showTerms_38 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2))
             T_Arg_88
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showTerm
d_showTerm_40 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showTerm_40 :: T_Term_154 -> Text
d_showTerm_40 T_Term_154
v0
  = case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_var_172 Integer
v1 [T_Arg_88]
v2
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             (Text -> AgdaAny
forall a b. a -> b
coe (Text
"var" :: Data.Text.Text))
             ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                ((Integer -> Text) -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v1)
                (([T_Arg_88] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> Text
d_showTerms_38 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v2)))
      MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v1 [T_Arg_88]
v2
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             ((QName -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe QName -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowQName_12 AgdaAny
v1)
             (([T_Arg_88] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> Text
d_showTerms_38 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v2))
      MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v1 [T_Arg_88]
v2
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             ((QName -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe QName -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowQName_12 AgdaAny
v1)
             (([T_Arg_88] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> Text
d_showTerms_38 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v2))
      MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 T_Visibility_48
v1 T_Abs_112
v2
        -> case T_Abs_112 -> T_Abs_112
forall a b. a -> b
coe T_Abs_112
v2 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 Text
v3 AgdaAny
v4
               -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
                    Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                    (Text -> AgdaAny
forall a b. a -> b
coe (Text
"\955" :: Data.Text.Text))
                    ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                       ((T_Visibility_48 -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Visibility_48 -> Text -> Text
d_visibilityParen_30 (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
v1) (Text -> AgdaAny
forall a b. a -> b
coe Text
v3))
                       ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                          (Text -> AgdaAny
forall a b. a -> b
coe (Text
"\8594" :: Data.Text.Text)) ((T_Term_154 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> Text
d_showTerm_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))))
             T_Abs_112
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196 [T_Clause_160]
v1 [T_Arg_88]
v2
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             (Text -> AgdaAny
forall a b. a -> b
coe (Text
"\955 {" :: Data.Text.Text))
             ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                (([T_Clause_160] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Clause_160] -> Text
d_showClauses_50 ([T_Clause_160] -> AgdaAny
forall a b. a -> b
coe [T_Clause_160]
v1))
                ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                   (Text -> AgdaAny
forall a b. a -> b
coe (Text
"}" :: Data.Text.Text)) (([T_Arg_88] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> Text
d_showTerms_38 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v2))))
      MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v1 T_Abs_112
v2
        -> 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
v3 AgdaAny
v4
               -> case T_Abs_112 -> T_Abs_112
forall a b. a -> b
coe T_Abs_112
v2 of
                    MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 Text
v5 AgdaAny
v6
                      -> (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           (Text
"\928 (" :: Data.Text.Text)
                           (Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                              ((T_Visibility_48 -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
                                 T_Visibility_48 -> Text -> Text
d_visibilityParen_30
                                 ((T_ArgInfo_76 -> T_Visibility_48) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_ArgInfo_76 -> T_Visibility_48
MAlonzo.Code.Reflection.AST.Argument.Information.d_visibility_16
                                    (T_ArgInfo_76 -> AgdaAny
forall a b. a -> b
coe T_ArgInfo_76
v3))
                                 (Text -> AgdaAny
forall a b. a -> b
coe Text
v5))
                              ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
                                 Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                                 (Text -> AgdaAny
forall a b. a -> b
coe (Text
":" :: Data.Text.Text))
                                 ((Text -> Text -> Text) -> Text -> Text -> AgdaAny
forall a b. a -> b
coe
                                    Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                                    (Text -> Text
MAlonzo.Code.Data.String.d_parensIfSpace_130
                                       ((T_Term_154 -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe T_Term_154 -> Text
d_showTerm_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)))
                                    (Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                                       (Text -> Text
forall a b. a -> b
coe (Text
")" :: Data.Text.Text))
                                       ((Text -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe
                                          Text -> Text
MAlonzo.Code.Data.String.d_parensIfSpace_130
                                          ((T_Term_154 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> Text
d_showTerm_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)))))))
                    T_Abs_112
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Arg_88
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_agda'45'sort_206 T_Sort_156
v1
        -> (T_Sort_156 -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe T_Sort_156 -> Text
d_showSort_42 (T_Sort_156 -> AgdaAny
forall a b. a -> b
coe T_Sort_156
v1)
      MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210 T_Literal_124
v1
        -> (T_Literal_124 -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe T_Literal_124 -> Text
d_showLiteral_14 (T_Literal_124 -> AgdaAny
forall a b. a -> b
coe T_Literal_124
v1)
      MAlonzo.Code.Agda.Builtin.Reflection.C_meta_214 AgdaAny
v1 [T_Arg_88]
v2
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             (((Integer, Integer) -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (Integer, Integer) -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowMeta_44 AgdaAny
v1)
             (([T_Arg_88] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> Text
d_showTerms_38 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v2))
      T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216
        -> Text -> Text
forall a b. a -> b
coe (Text
"unknown" :: Data.Text.Text)
      T_Term_154
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showSort
d_showSort_42 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Sort_156 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showSort_42 :: T_Sort_156 -> Text
d_showSort_42 T_Sort_156
v0
  = case T_Sort_156 -> T_Sort_156
forall a b. a -> b
coe T_Sort_156
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_set_220 T_Term_154
v1
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             (Text -> AgdaAny
forall a b. a -> b
coe (Text
"Set" :: Data.Text.Text))
             ((Text -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text
MAlonzo.Code.Data.String.d_parensIfSpace_130
                ((T_Term_154 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> Text
d_showTerm_40 (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v1)))
      MAlonzo.Code.Agda.Builtin.Reflection.C_lit_224 Integer
v1
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"Set" :: Data.Text.Text)
             ((Integer -> Text) -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v1)
      MAlonzo.Code.Agda.Builtin.Reflection.C_prop_228 T_Term_154
v1
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             (Text -> AgdaAny
forall a b. a -> b
coe (Text
"Prop" :: Data.Text.Text))
             ((Text -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text
MAlonzo.Code.Data.String.d_parensIfSpace_130
                ((T_Term_154 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> Text
d_showTerm_40 (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v1)))
      MAlonzo.Code.Agda.Builtin.Reflection.C_propLit_232 Integer
v1
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"Prop" :: Data.Text.Text)
             ((Integer -> Text) -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v1)
      MAlonzo.Code.Agda.Builtin.Reflection.C_inf_236 Integer
v1
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"Set\969" :: Data.Text.Text)
             ((Integer -> Text) -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v1)
      T_Sort_156
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_238
        -> Text -> Text
forall a b. a -> b
coe (Text
"unknown" :: Data.Text.Text)
      T_Sort_156
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showPatterns
d_showPatterns_44 ::
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showPatterns_44 :: [T_Arg_88] -> Text
d_showPatterns_44 [T_Arg_88]
v0
  = case [T_Arg_88] -> [AgdaAny]
forall a b. a -> b
coe [T_Arg_88]
v0 of
      [] -> Text -> Text
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
      (:) AgdaAny
v1 [AgdaAny]
v2
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             ((T_Arg_88 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Arg_88 -> Text
du_showArg_116 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)) (([T_Arg_88] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> Text
d_showPatterns_44 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2))
      [AgdaAny]
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showPattern
d_showPattern_46 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Pattern_158 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showPattern_46 :: T_Pattern_158 -> Text
d_showPattern_46 T_Pattern_158
v0
  = case T_Pattern_158 -> T_Pattern_158
forall a b. a -> b
coe T_Pattern_158
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 AgdaAny
v1 [T_Arg_88]
v2
        -> let v3 :: t
v3
                 = (Text -> Text) -> Text -> t
forall a b. a -> b
coe
                     Text -> Text
MAlonzo.Code.Data.String.Base.d_parens_46
                     (Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                        ((QName -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe QName -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowQName_12 AgdaAny
v1)
                        (([T_Arg_88] -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe [T_Arg_88] -> Text
d_showPatterns_44 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v2))) in
           AgdaAny -> Text
forall a b. a -> b
coe
             (case [T_Arg_88] -> [AgdaAny]
forall a b. a -> b
coe [T_Arg_88]
v2 of
                []
                  -> (QName -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe QName -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowQName_12 AgdaAny
v1
                [AgdaAny]
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3)
      MAlonzo.Code.Agda.Builtin.Reflection.C_dot_248 T_Term_154
v1
        -> (Text -> Text -> Text) -> Text -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
             (Text
"." :: Data.Text.Text)
             ((Text -> Text) -> Text -> AgdaAny
forall a b. a -> b
coe
                Text -> Text
MAlonzo.Code.Data.String.Base.d_parens_46 (T_Term_154 -> Text
d_showTerm_40 (T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v1)))
      MAlonzo.Code.Agda.Builtin.Reflection.C_var_252 Integer
v1
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             (Text -> AgdaAny
forall a b. a -> b
coe (Text
"pat-var" :: Data.Text.Text))
             ((Integer -> Text) -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v1)
      MAlonzo.Code.Agda.Builtin.Reflection.C_lit_256 T_Literal_124
v1
        -> (T_Literal_124 -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe T_Literal_124 -> Text
d_showLiteral_14 (T_Literal_124 -> AgdaAny
forall a b. a -> b
coe T_Literal_124
v1)
      MAlonzo.Code.Agda.Builtin.Reflection.C_proj_260 AgdaAny
v1
        -> (QName -> Text) -> AgdaAny -> Text
forall a b. a -> b
coe QName -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowQName_12 AgdaAny
v1
      MAlonzo.Code.Agda.Builtin.Reflection.C_absurd_264 Integer
v1
        -> Text -> Text
forall a b. a -> b
coe (Text
"()" :: Data.Text.Text)
      T_Pattern_158
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showClause
d_showClause_48 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showClause_48 :: T_Clause_160 -> Text
d_showClause_48 T_Clause_160
v0
  = case T_Clause_160 -> T_Clause_160
forall a b. a -> b
coe T_Clause_160
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_clause_272 [T_Σ_14]
v1 [T_Arg_88]
v2 T_Term_154
v3
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             (Text -> AgdaAny
forall a b. a -> b
coe (Text
"[" :: Data.Text.Text))
             ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                (([T_Σ_14] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Σ_14] -> Text
d_showTel_52 ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v1))
                ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                   (Text -> AgdaAny
forall a b. a -> b
coe (Text
"]" :: Data.Text.Text))
                   ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                      (([T_Arg_88] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> Text
d_showPatterns_44 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v2))
                      ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                         (Text -> AgdaAny
forall a b. a -> b
coe (Text
"\8594" :: Data.Text.Text)) ((T_Term_154 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> Text
d_showTerm_40 (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v3))))))
      MAlonzo.Code.Agda.Builtin.Reflection.C_absurd'45'clause_278 [T_Σ_14]
v1 [T_Arg_88]
v2
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             (Text -> AgdaAny
forall a b. a -> b
coe (Text
"[" :: Data.Text.Text))
             ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                (([T_Σ_14] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Σ_14] -> Text
d_showTel_52 ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v1))
                ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                   (Text -> AgdaAny
forall a b. a -> b
coe (Text
"]" :: Data.Text.Text)) (([T_Arg_88] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> Text
d_showPatterns_44 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v2))))
      T_Clause_160
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showClauses
d_showClauses_50 ::
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160] ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showClauses_50 :: [T_Clause_160] -> Text
d_showClauses_50 [T_Clause_160]
v0
  = case [T_Clause_160] -> [AgdaAny]
forall a b. a -> b
coe [T_Clause_160]
v0 of
      [] -> Text -> Text
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
      (:) AgdaAny
v1 [AgdaAny]
v2
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             ((T_Clause_160 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Clause_160 -> Text
d_showClause_48 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
             ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                (Text -> AgdaAny
forall a b. a -> b
coe (Text
";" :: Data.Text.Text)) (([T_Clause_160] -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Clause_160] -> Text
d_showClauses_50 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)))
      [AgdaAny]
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showTel
d_showTel_52 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showTel_52 :: [T_Σ_14] -> Text
d_showTel_52 [T_Σ_14]
v0
  = case [T_Σ_14] -> [AgdaAny]
forall a b. a -> b
coe [T_Σ_14]
v0 of
      [] -> Text -> Text
forall a b. a -> b
coe (Text
"" :: Data.Text.Text)
      (:) AgdaAny
v1 [AgdaAny]
v2
        -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v3 AgdaAny
v4
               -> case AgdaAny -> T_Arg_88
forall a b. a -> b
coe AgdaAny
v4 of
                    MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 T_ArgInfo_76
v5 AgdaAny
v6
                      -> (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. a -> b
coe
                           Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                           (T_Visibility_48 -> Text -> Text
d_visibilityParen_30
                              ((T_ArgInfo_76 -> T_Visibility_48) -> AgdaAny -> T_Visibility_48
forall a b. a -> b
coe
                                 T_ArgInfo_76 -> T_Visibility_48
MAlonzo.Code.Reflection.AST.Argument.Information.d_visibility_16
                                 (T_ArgInfo_76 -> AgdaAny
forall a b. a -> b
coe T_ArgInfo_76
v5))
                              ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
                                 Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
                                 ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                                    (Text -> AgdaAny
forall a b. a -> b
coe (Text
":" :: Data.Text.Text)) ((T_Term_154 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> Text
d_showTerm_40 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)))))
                           ([T_Σ_14] -> Text
d_showTel_52 ([AgdaAny] -> [T_Σ_14]
forall a b. a -> b
coe [AgdaAny]
v2))
                    T_Arg_88
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Σ_14
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show._.showArg
d_showArg_116 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showArg_116 :: T_Arg_88 -> [T_Arg_88] -> T_Arg_88 -> Text
d_showArg_116 ~T_Arg_88
v0 ~[T_Arg_88]
v1 T_Arg_88
v2 = T_Arg_88 -> Text
du_showArg_116 T_Arg_88
v2
du_showArg_116 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_showArg_116 :: T_Arg_88 -> Text
du_showArg_116 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
        -> 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
v3 T_Modality_68
v4
               -> case T_Modality_68 -> T_Modality_68
forall a b. a -> b
coe T_Modality_68
v4 of
                    MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74 T_Relevance_56
v5 T_Quantity_62
v6
                      -> (T_Visibility_48 -> Text -> Text)
-> T_Visibility_48 -> AgdaAny -> Text
forall a b. a -> b
coe
                           T_Visibility_48 -> Text -> Text
du_braces'63'_128 T_Visibility_48
v3
                           ((Text -> Text -> Text) -> Text -> Text -> AgdaAny
forall a b. a -> b
coe
                              Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'43''43'__20
                              (T_Relevance_56 -> Text
d_showRel_8 (T_Relevance_56 -> T_Relevance_56
forall a b. a -> b
coe T_Relevance_56
v5)) (T_Pattern_158 -> Text
d_showPattern_46 (AgdaAny -> T_Pattern_158
forall a b. a -> b
coe AgdaAny
v2)))
                    T_Modality_68
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_ArgInfo_76
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Arg_88
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show._._.braces?
d_braces'63'_128 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Relevance_56 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Quantity_62 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Pattern_158 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_braces'63'_128 :: T_Arg_88
-> [T_Arg_88]
-> T_Visibility_48
-> T_Relevance_56
-> T_Quantity_62
-> T_Pattern_158
-> Text
-> Text
d_braces'63'_128 ~T_Arg_88
v0 ~[T_Arg_88]
v1 T_Visibility_48
v2 ~T_Relevance_56
v3 ~T_Quantity_62
v4 ~T_Pattern_158
v5 = T_Visibility_48 -> Text -> Text
du_braces'63'_128 T_Visibility_48
v2
du_braces'63'_128 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_braces'63'_128 :: T_Visibility_48 -> Text -> Text
du_braces'63'_128 T_Visibility_48
v0
  = case T_Visibility_48 -> T_Visibility_48
forall a b. a -> b
coe T_Visibility_48
v0 of
      T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50
        -> (AgdaAny -> AgdaAny) -> Text -> Text
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)
      T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_hidden_52
        -> (Text -> Text) -> Text -> Text
forall a b. a -> b
coe Text -> Text
MAlonzo.Code.Data.String.Base.d_braces_48
      T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_instance'8242'_54
        -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> Text -> Text
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
             ((Text -> Text) -> AgdaAny
forall a b. a -> b
coe Text -> Text
MAlonzo.Code.Data.String.Base.d_braces_48)
             ((Text -> Text) -> AgdaAny
forall a b. a -> b
coe Text -> Text
MAlonzo.Code.Data.String.Base.d_braces_48)
      T_Visibility_48
_ -> Text -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Show.showDefinition
d_showDefinition_168 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Definition_280 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_showDefinition_168 :: T_Definition_280 -> Text
d_showDefinition_168 T_Definition_280
v0
  = case T_Definition_280 -> T_Definition_280
forall a b. a -> b
coe T_Definition_280
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_function_284 [T_Clause_160]
v1
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             (Text -> AgdaAny
forall a b. a -> b
coe (Text
"function" :: Data.Text.Text))
             ((Text -> Text) -> Text -> AgdaAny
forall a b. a -> b
coe
                Text -> Text
MAlonzo.Code.Data.String.Base.d_braces_48
                ([T_Clause_160] -> Text
d_showClauses_50 ([T_Clause_160] -> [T_Clause_160]
forall a b. a -> b
coe [T_Clause_160]
v1)))
      MAlonzo.Code.Agda.Builtin.Reflection.C_data'45'type_290 Integer
v1 [AgdaAny]
v2
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             (Text -> AgdaAny
forall a b. a -> b
coe (Text
"datatype" :: Data.Text.Text))
             ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                ((Integer -> Text) -> Integer -> AgdaAny
forall a b. a -> b
coe Integer -> Text
MAlonzo.Code.Data.Nat.Show.d_show_56 Integer
v1)
                ((Text -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Text -> Text
MAlonzo.Code.Data.String.Base.d_braces_48
                   ((Text -> [Text] -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      Text -> [Text] -> Text
MAlonzo.Code.Data.String.Base.d_intersperse_30
                      (Text
", " :: Data.Text.Text)
                      (((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
                         ((QName -> Text) -> AgdaAny
forall a b. a -> b
coe QName -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowQName_12)
                         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)))))
      MAlonzo.Code.Agda.Builtin.Reflection.C_record'45'type_296 AgdaAny
v1 [T_Arg_88]
v2
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             (Text -> AgdaAny
forall a b. a -> b
coe (Text
"record" :: Data.Text.Text))
             ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                ((QName -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe QName -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowQName_12 AgdaAny
v1)
                ((Text -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   Text -> Text
MAlonzo.Code.Data.String.Base.d_braces_48
                   ((Text -> [Text] -> Text) -> Text -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      Text -> [Text] -> Text
MAlonzo.Code.Data.String.Base.d_intersperse_30
                      (Text
", " :: Data.Text.Text)
                      (((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
                         (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
                            ((QName -> Text) -> AgdaAny
forall a b. a -> b
coe QName -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowQName_12)
                            ((T_Arg_88 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Arg_88 -> AgdaAny
MAlonzo.Code.Reflection.AST.Argument.du_unArg_74))
                         ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v2)))))
      MAlonzo.Code.Agda.Builtin.Reflection.C_data'45'cons_302 AgdaAny
v1 T_Quantity_62
v2
        -> (Text -> Text -> Text) -> AgdaAny -> AgdaAny -> Text
forall a b. a -> b
coe
             Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
             (Text -> AgdaAny
forall a b. a -> b
coe (Text
"constructor" :: Data.Text.Text))
             ((Text -> Text -> Text) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Text -> Text -> Text
MAlonzo.Code.Data.String.Base.d__'60''43''62'__50
                ((QName -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe QName -> Text
MAlonzo.Code.Agda.Builtin.Reflection.d_primShowQName_12 AgdaAny
v1)
                ((T_Quantity_62 -> Text) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Quantity_62 -> Text
d_showQuantity_12 (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
v2)))
      T_Definition_280
MAlonzo.Code.Agda.Builtin.Reflection.C_axiom_304
        -> Text -> Text
forall a b. a -> b
coe (Text
"axiom" :: Data.Text.Text)
      T_Definition_280
MAlonzo.Code.Agda.Builtin.Reflection.C_prim'45'fun_306
        -> Text -> Text
forall a b. a -> b
coe (Text
"primitive" :: Data.Text.Text)
      T_Definition_280
_ -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError