{-# 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.Text.Format.Generic 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.Char
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Category.Applicative.Indexed
import qualified MAlonzo.Code.Category.Functor
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Data.Sum.Categorical.Left
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Level
import qualified MAlonzo.Code.Strict

-- Text.Format.Generic.FormatSpec
d_FormatSpec_6 :: ()
d_FormatSpec_6 = ()
newtype T_FormatSpec_6
  = C_FormatSpec'46'constructor_27 (MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
                                    Maybe AgdaAny)
-- Text.Format.Generic.FormatSpec.ArgChunk
d_ArgChunk_14 :: T_FormatSpec_6 -> ()
d_ArgChunk_14 :: T_FormatSpec_6 -> ()
d_ArgChunk_14 = T_FormatSpec_6 -> ()
forall a. a
erased
-- Text.Format.Generic.FormatSpec.ArgType
d_ArgType_16 :: T_FormatSpec_6 -> AgdaAny -> ()
d_ArgType_16 :: T_FormatSpec_6 -> AgdaAny -> ()
d_ArgType_16 = T_FormatSpec_6 -> AgdaAny -> ()
forall a. a
erased
-- Text.Format.Generic.FormatSpec.lexArg
d_lexArg_18 ::
  T_FormatSpec_6 ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> Maybe AgdaAny
d_lexArg_18 :: T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny
d_lexArg_18 T_FormatSpec_6
v0
  = case T_FormatSpec_6 -> T_FormatSpec_6
forall a b. a -> b
coe T_FormatSpec_6
v0 of
      C_FormatSpec'46'constructor_27 T_Char_6 -> Maybe AgdaAny
v3 -> (T_Char_6 -> Maybe AgdaAny) -> T_Char_6 -> Maybe AgdaAny
forall a b. a -> b
coe T_Char_6 -> Maybe AgdaAny
v3
      T_FormatSpec_6
_ -> T_Char_6 -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Text.Format.Generic._.unionSpec
d_unionSpec_24 ::
  T_FormatSpec_6 -> T_FormatSpec_6 -> T_FormatSpec_6
d_unionSpec_24 :: T_FormatSpec_6 -> T_FormatSpec_6 -> T_FormatSpec_6
d_unionSpec_24 T_FormatSpec_6
v0 T_FormatSpec_6
v1
  = ((T_Char_6 -> Maybe AgdaAny) -> T_FormatSpec_6)
-> (AgdaAny -> AgdaAny) -> T_FormatSpec_6
forall a b. a -> b
coe
      (T_Char_6 -> Maybe AgdaAny) -> T_FormatSpec_6
C_FormatSpec'46'constructor_27
      (\ AgdaAny
v2 ->
         (Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           Maybe AgdaAny -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du__'60''8739''62'__84
           (((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_map_68
              ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38)
              ((T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny)
-> T_FormatSpec_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny
d_lexArg_18 T_FormatSpec_6
v0 AgdaAny
v2))
           (((AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              (AgdaAny -> AgdaAny) -> Maybe AgdaAny -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_map_68
              ((AgdaAny -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42)
              ((T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny)
-> T_FormatSpec_6 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny
d_lexArg_18 T_FormatSpec_6
v1 AgdaAny
v2)))
-- Text.Format.Generic.Format._.ArgChunk
d_ArgChunk_54 :: T_FormatSpec_6 -> ()
d_ArgChunk_54 :: T_FormatSpec_6 -> ()
d_ArgChunk_54 = T_FormatSpec_6 -> ()
forall a. a
erased
-- Text.Format.Generic.Format._.ArgType
d_ArgType_56 :: T_FormatSpec_6 -> AgdaAny -> ()
d_ArgType_56 :: T_FormatSpec_6 -> AgdaAny -> ()
d_ArgType_56 = T_FormatSpec_6 -> AgdaAny -> ()
forall a. a
erased
-- Text.Format.Generic.Format._.lexArg
d_lexArg_58 ::
  T_FormatSpec_6 ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> Maybe AgdaAny
d_lexArg_58 :: T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny
d_lexArg_58 T_FormatSpec_6
v0 = (T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny)
-> AgdaAny -> T_Char_6 -> Maybe AgdaAny
forall a b. a -> b
coe T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny
d_lexArg_18 (T_FormatSpec_6 -> AgdaAny
forall a b. a -> b
coe T_FormatSpec_6
v0)
-- Text.Format.Generic.Format.Chunk
d_Chunk_60 :: p -> ()
d_Chunk_60 p
a0 = ()
data T_Chunk_60
  = C_Arg_62 AgdaAny |
    C_Raw_64 MAlonzo.Code.Agda.Builtin.String.T_String_6
-- Text.Format.Generic.Format.Format
d_Format_66 :: T_FormatSpec_6 -> ()
d_Format_66 :: T_FormatSpec_6 -> ()
d_Format_66 = T_FormatSpec_6 -> ()
forall a. a
erased
-- Text.Format.Generic.Format.size
d_size_68 :: T_FormatSpec_6 -> [T_Chunk_60] -> Integer
d_size_68 :: T_FormatSpec_6 -> [T_Chunk_60] -> Integer
d_size_68 ~T_FormatSpec_6
v0 = [T_Chunk_60] -> Integer
du_size_68
du_size_68 :: [T_Chunk_60] -> Integer
du_size_68 :: [T_Chunk_60] -> Integer
du_size_68
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> [T_Chunk_60] -> Integer
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
      (([Integer] -> Integer) -> AgdaAny
forall a b. a -> b
coe [Integer] -> Integer
MAlonzo.Code.Data.List.Base.d_sum_292)
      (((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
forall a b. a -> b
coe
            (\ AgdaAny
v0 ->
               let v1 :: Integer
v1 = Integer
1 :: Integer in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (case AgdaAny -> T_Chunk_60
forall a b. a -> b
coe AgdaAny
v0 of
                    C_Raw_64 T_String_6
v2 -> Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer)
                    T_Chunk_60
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1))))
-- Text.Format.Generic.Format.⟦_⟧
d_'10214'_'10215'_74 :: T_FormatSpec_6 -> [T_Chunk_60] -> AgdaAny
d_'10214'_'10215'_74 :: T_FormatSpec_6 -> [T_Chunk_60] -> AgdaAny
d_'10214'_'10215'_74 ~T_FormatSpec_6
v0 [T_Chunk_60]
v1 = [T_Chunk_60] -> AgdaAny
du_'10214'_'10215'_74 [T_Chunk_60]
v1
du_'10214'_'10215'_74 :: [T_Chunk_60] -> AgdaAny
du_'10214'_'10215'_74 :: [T_Chunk_60] -> AgdaAny
du_'10214'_'10215'_74 [T_Chunk_60]
v0
  = case [T_Chunk_60] -> [AgdaAny]
forall a b. a -> b
coe [T_Chunk_60]
v0 of
      []
        -> (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)
      (:) AgdaAny
v1 [AgdaAny]
v2
        -> case AgdaAny -> T_Chunk_60
forall a b. a -> b
coe AgdaAny
v1 of
             C_Arg_62 AgdaAny
v3
               -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
forall a. a
erased
                    (([T_Chunk_60] -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Chunk_60] -> AgdaAny
du_'10214'_'10215'_74 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2))
             C_Raw_64 T_String_6
v3 -> ([T_Chunk_60] -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Chunk_60] -> AgdaAny
du_'10214'_'10215'_74 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
             T_Chunk_60
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Text.Format.Generic.Format.Error
d_Error_82 :: p -> ()
d_Error_82 p
a0 = ()
data T_Error_82
  = C_UnexpectedEndOfString_84 MAlonzo.Code.Agda.Builtin.String.T_String_6 |
    C_InvalidType_86 MAlonzo.Code.Agda.Builtin.String.T_String_6
                     MAlonzo.Code.Agda.Builtin.Char.T_Char_6
                     MAlonzo.Code.Agda.Builtin.String.T_String_6
-- Text.Format.Generic.Format.lexer
d_lexer_88 ::
  T_FormatSpec_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_lexer_88 :: T_FormatSpec_6 -> T_String_6 -> T__'8846'__30
d_lexer_88 T_FormatSpec_6
v0 T_String_6
v1
  = (T_FormatSpec_6
 -> T_String_6
 -> [T_Char_6]
 -> [T_Char_6]
 -> [T_Char_6]
 -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
forall a b. a -> b
coe
      T_FormatSpec_6
-> T_String_6
-> [T_Char_6]
-> [T_Char_6]
-> [T_Char_6]
-> T__'8846'__30
d_loop_134 (T_FormatSpec_6 -> AgdaAny
forall a b. a -> b
coe T_FormatSpec_6
v0) (T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6
v1)
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
      ((T_String_6 -> [T_Char_6]) -> T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6 -> [T_Char_6]
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v1)
-- Text.Format.Generic.Format._.RevWord
d_RevWord_120 ::
  T_FormatSpec_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -> ()
d_RevWord_120 :: T_FormatSpec_6 -> T_String_6 -> ()
d_RevWord_120 = T_FormatSpec_6 -> T_String_6 -> ()
forall a. a
erased
-- Text.Format.Generic.Format._.Prefix
d_Prefix_122 ::
  T_FormatSpec_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -> ()
d_Prefix_122 :: T_FormatSpec_6 -> T_String_6 -> ()
d_Prefix_122 = T_FormatSpec_6 -> T_String_6 -> ()
forall a. a
erased
-- Text.Format.Generic.Format._.toRevString
d_toRevString_124 ::
  T_FormatSpec_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_toRevString_124 :: T_FormatSpec_6 -> T_String_6 -> [T_Char_6] -> T_String_6
d_toRevString_124 ~T_FormatSpec_6
v0 ~T_String_6
v1 = [T_Char_6] -> T_String_6
du_toRevString_124
du_toRevString_124 ::
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_toRevString_124 :: [T_Char_6] -> T_String_6
du_toRevString_124
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> [T_Char_6] -> T_String_6
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
      (([T_Char_6] -> T_String_6) -> AgdaAny
forall a b. a -> b
coe [T_Char_6] -> T_String_6
MAlonzo.Code.Agda.Builtin.String.d_primStringFromList_14)
      (([AgdaAny] -> [AgdaAny]) -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_reverse_804)
-- Text.Format.Generic.Format._.push
d_push_126 ::
  T_FormatSpec_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  [T_Chunk_60] -> [T_Chunk_60]
d_push_126 :: T_FormatSpec_6
-> T_String_6 -> [T_Char_6] -> [T_Chunk_60] -> [T_Chunk_60]
d_push_126 ~T_FormatSpec_6
v0 ~T_String_6
v1 [T_Char_6]
v2 [T_Chunk_60]
v3 = [T_Char_6] -> [T_Chunk_60] -> [T_Chunk_60]
du_push_126 [T_Char_6]
v2 [T_Chunk_60]
v3
du_push_126 ::
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  [T_Chunk_60] -> [T_Chunk_60]
du_push_126 :: [T_Char_6] -> [T_Chunk_60] -> [T_Chunk_60]
du_push_126 [T_Char_6]
v0 [T_Chunk_60]
v1
  = let v2 :: t
v2
          = (AgdaAny -> [AgdaAny] -> [AgdaAny]) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
              AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
              ((T_String_6 -> T_Chunk_60) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_String_6 -> T_Chunk_60
C_Raw_64 (([T_Char_6] -> T_String_6) -> [T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6] -> T_String_6
du_toRevString_124 [T_Char_6]
v0)) ([T_Chunk_60] -> AgdaAny
forall a b. a -> b
coe [T_Chunk_60]
v1) in
    AgdaAny -> [T_Chunk_60]
forall a b. a -> b
coe
      (case [T_Char_6] -> [AgdaAny]
forall a b. a -> b
coe [T_Char_6]
v0 of
         [] -> [T_Chunk_60] -> AgdaAny
forall a b. a -> b
coe [T_Chunk_60]
v1
         [AgdaAny]
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2)
-- Text.Format.Generic.Format._.loop
d_loop_134 ::
  T_FormatSpec_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_loop_134 :: T_FormatSpec_6
-> T_String_6
-> [T_Char_6]
-> [T_Char_6]
-> [T_Char_6]
-> T__'8846'__30
d_loop_134 T_FormatSpec_6
v0 T_String_6
v1 [T_Char_6]
v2 [T_Char_6]
v3 [T_Char_6]
v4
  = case [T_Char_6] -> [AgdaAny]
forall a b. a -> b
coe [T_Char_6]
v4 of
      []
        -> (T_RawIApplicative_38 -> () -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
             T_RawIApplicative_38 -> () -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Category.Applicative.Indexed.d_pure_58
             (T_RawIApplicative_38 -> AgdaAny
forall a b. a -> b
coe T_RawIApplicative_38
MAlonzo.Code.Data.Sum.Categorical.Left.du_applicative_20)
             AgdaAny
forall a. a
erased (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
             (([T_Char_6] -> [T_Chunk_60] -> [T_Chunk_60])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Char_6] -> [T_Chunk_60] -> [T_Chunk_60]
du_push_126 ([T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6]
v2) ([T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6]
v4))
      (:) AgdaAny
v5 [AgdaAny]
v6
        -> let v7 :: T__'8846'__30
v7
                 = T_FormatSpec_6
-> T_String_6
-> [T_Char_6]
-> [T_Char_6]
-> [T_Char_6]
-> T__'8846'__30
d_loop_134
                     (T_FormatSpec_6 -> T_FormatSpec_6
forall a b. a -> b
coe T_FormatSpec_6
v0) (T_String_6 -> T_String_6
forall a b. a -> b
coe T_String_6
v1)
                     ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T_Char_6]
forall a b. a -> b
coe
                        AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) ([T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6]
v2))
                     ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T_Char_6]
forall a b. a -> b
coe
                        AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) ([T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6]
v3))
                     ([AgdaAny] -> [T_Char_6]
forall a b. a -> b
coe [AgdaAny]
v6) in
           AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
             (case AgdaAny -> T_Char_6
forall a b. a -> b
coe AgdaAny
v5 of
                T_Char_6
'%'
                  -> let v8 :: b
v8
                           = let v8 :: b
v8
                                   = T_RawIApplicative_38 -> b
forall a b. a -> b
coe T_RawIApplicative_38
MAlonzo.Code.Data.Sum.Categorical.Left.du_applicative_20 in
                             AgdaAny -> b
forall a b. a -> b
coe
                               (let v9 :: b
v9 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                                AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                  (let v10 :: b
v10 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                                   AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     ((T_RawFunctor_24
 -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
                                        T_RawFunctor_24
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Category.Functor.d__'60''36''62'__30
                                        ((T_RawIApplicative_38 -> AgdaAny -> AgdaAny -> T_RawFunctor_24)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T_RawIApplicative_38 -> AgdaAny -> AgdaAny -> T_RawFunctor_24
MAlonzo.Code.Category.Applicative.Indexed.du_rawFunctor_72
                                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v10))
                                        AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased (([T_Char_6] -> [T_Chunk_60] -> [T_Chunk_60]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Char_6] -> [T_Chunk_60] -> [T_Chunk_60]
du_push_126 ([T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6]
v2))
                                        (T_FormatSpec_6
-> T_String_6 -> [T_Char_6] -> [T_Char_6] -> T__'8846'__30
d_type_136
                                           (T_FormatSpec_6 -> T_FormatSpec_6
forall a b. a -> b
coe T_FormatSpec_6
v0) (T_String_6 -> T_String_6
forall a b. a -> b
coe T_String_6
v1)
                                           ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T_Char_6]
forall a b. a -> b
coe
                                              AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_Char_6 -> AgdaAny
forall a b. a -> b
coe T_Char_6
'%')
                                              ([T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6]
v3))
                                           ([AgdaAny] -> [T_Char_6]
forall a b. a -> b
coe [AgdaAny]
v6))))) in
                     AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v6 of
                          (:) AgdaAny
v9 [AgdaAny]
v10
                            -> case AgdaAny -> T_Char_6
forall a b. a -> b
coe AgdaAny
v9 of
                                 T_Char_6
'%'
                                   -> (T_FormatSpec_6
 -> T_String_6
 -> [T_Char_6]
 -> [T_Char_6]
 -> [T_Char_6]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_FormatSpec_6
-> T_String_6
-> [T_Char_6]
-> [T_Char_6]
-> [T_Char_6]
-> T__'8846'__30
d_loop_134 (T_FormatSpec_6 -> AgdaAny
forall a b. a -> b
coe T_FormatSpec_6
v0) (T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6
v1)
                                        ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_Char_6 -> AgdaAny
forall a b. a -> b
coe T_Char_6
'%')
                                           ([T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6]
v2))
                                        ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_Char_6 -> AgdaAny
forall a b. a -> b
coe T_Char_6
'%')
                                           ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (T_Char_6 -> AgdaAny
forall a b. a -> b
coe T_Char_6
'%')
                                              ([T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6]
v3)))
                                        ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v10)
                                 T_Char_6
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8
                          [AgdaAny]
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8)
                T_Char_6
_ -> T__'8846'__30 -> AgdaAny
forall a b. a -> b
coe T__'8846'__30
v7)
      [AgdaAny]
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Text.Format.Generic.Format._.type
d_type_136 ::
  T_FormatSpec_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_type_136 :: T_FormatSpec_6
-> T_String_6 -> [T_Char_6] -> [T_Char_6] -> T__'8846'__30
d_type_136 T_FormatSpec_6
v0 T_String_6
v1 [T_Char_6]
v2 [T_Char_6]
v3
  = case [T_Char_6] -> [AgdaAny]
forall a b. a -> b
coe [T_Char_6]
v3 of
      []
        -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
             AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
             ((T_String_6 -> T_Error_82) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_String_6 -> T_Error_82
C_UnexpectedEndOfString_84 (T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6
v1))
      (:) AgdaAny
v4 [AgdaAny]
v5
        -> (T_RawIApplicative_38
 -> ()
 -> ()
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T__'8846'__30
forall a b. a -> b
coe
             T_RawIApplicative_38
-> ()
-> ()
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Category.Applicative.Indexed.d__'8859'__66
             (T_RawIApplicative_38 -> AgdaAny
forall a b. a -> b
coe T_RawIApplicative_38
MAlonzo.Code.Data.Sum.Categorical.Left.du_applicative_20)
             AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
             (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
             (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
             (let v6 :: b
v6
                    = T_RawIApplicative_38 -> b
forall a b. a -> b
coe T_RawIApplicative_38
MAlonzo.Code.Data.Sum.Categorical.Left.du_applicative_20 in
              AgdaAny -> AgdaAny
forall a b. a -> b
coe
                (let v7 :: b
v7 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                 AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   (let v8 :: b
v8 = () -> b
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8 in
                    AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      ((T_RawFunctor_24
 -> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_RawFunctor_24
-> () -> () -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Category.Functor.d__'60''36''62'__30
                         ((T_RawIApplicative_38 -> AgdaAny -> AgdaAny -> T_RawFunctor_24)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                            T_RawIApplicative_38 -> AgdaAny -> AgdaAny -> T_RawFunctor_24
MAlonzo.Code.Category.Applicative.Indexed.du_rawFunctor_72 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v6)
                            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v8))
                         AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased ((AgdaAny -> [AgdaAny] -> [AgdaAny]) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22)
                         ((T_FormatSpec_6
 -> [T_Char_6] -> [T_Char_6] -> T_Char_6 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_FormatSpec_6
-> [T_Char_6] -> [T_Char_6] -> T_Char_6 -> T__'8846'__30
du_chunk_174 (T_FormatSpec_6 -> AgdaAny
forall a b. a -> b
coe T_FormatSpec_6
v0) ([T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6]
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))))))
             (T_FormatSpec_6
-> T_String_6
-> [T_Char_6]
-> [T_Char_6]
-> [T_Char_6]
-> T__'8846'__30
d_loop_134
                (T_FormatSpec_6 -> T_FormatSpec_6
forall a b. a -> b
coe T_FormatSpec_6
v0) (T_String_6 -> T_String_6
forall a b. a -> b
coe T_String_6
v1)
                ([AgdaAny] -> [T_Char_6]
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
                ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T_Char_6]
forall a b. a -> b
coe
                   AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) ([T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6]
v2))
                ([AgdaAny] -> [T_Char_6]
forall a b. a -> b
coe [AgdaAny]
v5))
      [AgdaAny]
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Text.Format.Generic.Format._._.chunk
d_chunk_174 ::
  T_FormatSpec_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_chunk_174 :: T_FormatSpec_6
-> T_String_6
-> [T_Char_6]
-> T_Char_6
-> [T_Char_6]
-> T_Char_6
-> T__'8846'__30
d_chunk_174 T_FormatSpec_6
v0 ~T_String_6
v1 [T_Char_6]
v2 ~T_Char_6
v3 [T_Char_6]
v4 T_Char_6
v5 = T_FormatSpec_6
-> [T_Char_6] -> [T_Char_6] -> T_Char_6 -> T__'8846'__30
du_chunk_174 T_FormatSpec_6
v0 [T_Char_6]
v2 [T_Char_6]
v4 T_Char_6
v5
du_chunk_174 ::
  T_FormatSpec_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_chunk_174 :: T_FormatSpec_6
-> [T_Char_6] -> [T_Char_6] -> T_Char_6 -> T__'8846'__30
du_chunk_174 T_FormatSpec_6
v0 [T_Char_6]
v1 [T_Char_6]
v2 T_Char_6
v3
  = let v4 :: t
v4 = (T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny)
-> T_FormatSpec_6 -> T_Char_6 -> t
forall a b. a -> b
coe T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny
d_lexArg_18 T_FormatSpec_6
v0 T_Char_6
v3 in
    AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
      (case AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4 of
         MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v5
           -> (T_RawIApplicative_38 -> () -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_RawIApplicative_38 -> () -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Category.Applicative.Indexed.d_pure_58
                (T_RawIApplicative_38 -> AgdaAny
forall a b. a -> b
coe T_RawIApplicative_38
MAlonzo.Code.Data.Sum.Categorical.Left.du_applicative_20)
                AgdaAny
forall a. a
erased (() -> AgdaAny
forall a b. a -> b
coe ()
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
                ((AgdaAny -> T_Chunk_60) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Chunk_60
C_Arg_62 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
         Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
           -> (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
MAlonzo.Code.Strict.du_force'8242'_14 () ()
MAlonzo.Code.Level.d_0ℓ_22
                (([T_Char_6] -> T_String_6) -> [T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6] -> T_String_6
du_toRevString_124 [T_Char_6]
v1)
                (\ AgdaAny
v5 ->
                   (() -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                     () -> () -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny
MAlonzo.Code.Strict.du_force'8242'_14 () ()
MAlonzo.Code.Level.d_0ℓ_22
                     (([T_Char_6] -> T_String_6) -> [T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6] -> T_String_6
MAlonzo.Code.Agda.Builtin.String.d_primStringFromList_14 [T_Char_6]
v2)
                     (\ AgdaAny
v6 ->
                        (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                          ((T_String_6 -> T_Char_6 -> T_String_6 -> T_Error_82)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_String_6 -> T_Char_6 -> T_String_6 -> T_Error_82
C_InvalidType_86 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) (T_Char_6 -> AgdaAny
forall a b. a -> b
coe T_Char_6
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))))
         Maybe AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)