{-# 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.Data.List.Base
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Nat.ListAction
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Data.Sum.Effectful.Left
import qualified MAlonzo.Code.Effect.Applicative
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Function.Strict
import qualified MAlonzo.Code.Level

-- Text.Format.Generic.FormatSpec
d_FormatSpec_6 :: ()
d_FormatSpec_6 = ()
newtype T_FormatSpec_6
  = C_constructor_20 (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_constructor_20 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_26 ::
  T_FormatSpec_6 -> T_FormatSpec_6 -> T_FormatSpec_6
d_unionSpec_26 :: T_FormatSpec_6 -> T_FormatSpec_6 -> T_FormatSpec_6
d_unionSpec_26 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_constructor_20
      (\ 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'__80
           (((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_64
              ((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_64
              ((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_56 :: T_FormatSpec_6 -> ()
d_ArgChunk_56 :: T_FormatSpec_6 -> ()
d_ArgChunk_56 = T_FormatSpec_6 -> ()
forall a. a
erased
-- Text.Format.Generic.Format._.ArgType
d_ArgType_58 :: T_FormatSpec_6 -> AgdaAny -> ()
d_ArgType_58 :: T_FormatSpec_6 -> AgdaAny -> ()
d_ArgType_58 = T_FormatSpec_6 -> AgdaAny -> ()
forall a. a
erased
-- Text.Format.Generic.Format._.lexArg
d_lexArg_60 ::
  T_FormatSpec_6 ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> Maybe AgdaAny
d_lexArg_60 :: T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny
d_lexArg_60 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_62 :: p -> ()
d_Chunk_62 p
a0 = ()
data T_Chunk_62
  = C_Arg_64 AgdaAny |
    C_Raw_66 MAlonzo.Code.Agda.Builtin.String.T_String_6
-- Text.Format.Generic.Format.Format
d_Format_68 :: T_FormatSpec_6 -> ()
d_Format_68 :: T_FormatSpec_6 -> ()
d_Format_68 = T_FormatSpec_6 -> ()
forall a. a
erased
-- Text.Format.Generic.Format.size
d_size_70 :: T_FormatSpec_6 -> [T_Chunk_62] -> Integer
d_size_70 :: T_FormatSpec_6 -> [T_Chunk_62] -> Integer
d_size_70 ~T_FormatSpec_6
v0 = [T_Chunk_62] -> Integer
du_size_70
du_size_70 :: [T_Chunk_62] -> Integer
du_size_70 :: [T_Chunk_62] -> Integer
du_size_70
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> [T_Chunk_62] -> Integer
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
      (([Integer] -> Integer) -> AgdaAny
forall a b. a -> b
coe [Integer] -> Integer
MAlonzo.Code.Data.Nat.ListAction.d_sum_6)
      (((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_62
forall a b. a -> b
coe AgdaAny
v0 of
                    C_Raw_66 T_String_6
v2 -> Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer)
                    T_Chunk_62
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1))))
-- Text.Format.Generic.Format.⟦_⟧
d_'10214'_'10215'_76 :: T_FormatSpec_6 -> [T_Chunk_62] -> AgdaAny
d_'10214'_'10215'_76 :: T_FormatSpec_6 -> [T_Chunk_62] -> AgdaAny
d_'10214'_'10215'_76 ~T_FormatSpec_6
v0 [T_Chunk_62]
v1 = [T_Chunk_62] -> AgdaAny
du_'10214'_'10215'_76 [T_Chunk_62]
v1
du_'10214'_'10215'_76 :: [T_Chunk_62] -> AgdaAny
du_'10214'_'10215'_76 :: [T_Chunk_62] -> AgdaAny
du_'10214'_'10215'_76 [T_Chunk_62]
v0
  = case [T_Chunk_62] -> [AgdaAny]
forall a b. a -> b
coe [T_Chunk_62]
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_62
forall a b. a -> b
coe AgdaAny
v1 of
             C_Arg_64 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_62] -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Chunk_62] -> AgdaAny
du_'10214'_'10215'_76 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2))
             C_Raw_66 T_String_6
v3 -> ([T_Chunk_62] -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Chunk_62] -> AgdaAny
du_'10214'_'10215'_76 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
             T_Chunk_62
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Text.Format.Generic.Format.Error
d_Error_84 :: p -> ()
d_Error_84 p
a0 = ()
data T_Error_84
  = C_UnexpectedEndOfString_86 MAlonzo.Code.Agda.Builtin.String.T_String_6 |
    C_InvalidType_88 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_90 ::
  T_FormatSpec_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_lexer_90 :: T_FormatSpec_6 -> T_String_6 -> T__'8846'__30
d_lexer_90 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_146 (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_132 ::
  T_FormatSpec_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -> ()
d_RevWord_132 :: T_FormatSpec_6 -> T_String_6 -> ()
d_RevWord_132 = T_FormatSpec_6 -> T_String_6 -> ()
forall a. a
erased
-- Text.Format.Generic.Format._.Prefix
d_Prefix_134 ::
  T_FormatSpec_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -> ()
d_Prefix_134 :: T_FormatSpec_6 -> T_String_6 -> ()
d_Prefix_134 = T_FormatSpec_6 -> T_String_6 -> ()
forall a. a
erased
-- Text.Format.Generic.Format._.toRevString
d_toRevString_136 ::
  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_136 :: T_FormatSpec_6 -> T_String_6 -> [T_Char_6] -> T_String_6
d_toRevString_136 ~T_FormatSpec_6
v0 ~T_String_6
v1 = [T_Char_6] -> T_String_6
du_toRevString_136
du_toRevString_136 ::
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_toRevString_136 :: [T_Char_6] -> T_String_6
du_toRevString_136
  = ((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'__216
      (([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_444)
-- Text.Format.Generic.Format._.push
d_push_138 ::
  T_FormatSpec_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  [T_Chunk_62] -> [T_Chunk_62]
d_push_138 :: T_FormatSpec_6
-> T_String_6 -> [T_Char_6] -> [T_Chunk_62] -> [T_Chunk_62]
d_push_138 ~T_FormatSpec_6
v0 ~T_String_6
v1 [T_Char_6]
v2 [T_Chunk_62]
v3 = [T_Char_6] -> [T_Chunk_62] -> [T_Chunk_62]
du_push_138 [T_Char_6]
v2 [T_Chunk_62]
v3
du_push_138 ::
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  [T_Chunk_62] -> [T_Chunk_62]
du_push_138 :: [T_Char_6] -> [T_Chunk_62] -> [T_Chunk_62]
du_push_138 [T_Char_6]
v0 [T_Chunk_62]
v1
  = let v2 :: AgdaAny
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_String_6 -> T_Chunk_62) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_String_6 -> T_Chunk_62
C_Raw_66 (([T_Char_6] -> T_String_6) -> [T_Char_6] -> AgdaAny
forall a b. a -> b
coe [T_Char_6] -> T_String_6
du_toRevString_136 [T_Char_6]
v0)) ([T_Chunk_62] -> AgdaAny
forall a b. a -> b
coe [T_Chunk_62]
v1) in
    AgdaAny -> [T_Chunk_62]
forall a b. a -> b
coe
      (case [T_Char_6] -> [AgdaAny]
forall a b. a -> b
coe [T_Char_6]
v0 of
         [] -> [T_Chunk_62] -> AgdaAny
forall a b. a -> b
coe [T_Chunk_62]
v1
         [AgdaAny]
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
-- Text.Format.Generic.Format._.loop
d_loop_146 ::
  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_146 :: T_FormatSpec_6
-> T_String_6
-> [T_Char_6]
-> [T_Char_6]
-> [T_Char_6]
-> T__'8846'__30
d_loop_146 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
      []
        -> (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'8322'_42
             (([T_Char_6] -> [T_Chunk_62] -> [T_Chunk_62])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Char_6] -> [T_Chunk_62] -> [T_Chunk_62]
du_push_138 ([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_146
                     (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 :: AgdaAny
v8
                           = ((AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30)
-> AgdaAny -> T__'8846'__30 -> AgdaAny
forall a b. a -> b
coe
                               (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map'8322'_94
                               (([T_Char_6] -> [T_Chunk_62] -> [T_Chunk_62]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Char_6] -> [T_Chunk_62] -> [T_Chunk_62]
du_push_138 ([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_148
                                  (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_146 (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
v8
                          [AgdaAny]
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
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_148 ::
  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_148 :: T_FormatSpec_6
-> T_String_6 -> [T_Char_6] -> [T_Char_6] -> T__'8846'__30
d_type_148 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_84) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_String_6 -> T_Error_84
C_UnexpectedEndOfString_86 (T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6
v1))
      (:) AgdaAny
v4 [AgdaAny]
v5
        -> (T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe
             T_RawApplicative_20 -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Effect.Applicative.du__'8859'__70
             (T_RawApplicative_20 -> AgdaAny
forall a b. a -> b
coe T_RawApplicative_20
MAlonzo.Code.Data.Sum.Effectful.Left.du_applicative_20)
             (((AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                (AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_map'8322'_94
                ((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_186 (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_146
                (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_186 ::
  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_186 :: T_FormatSpec_6
-> T_String_6
-> [T_Char_6]
-> T_Char_6
-> [T_Char_6]
-> T_Char_6
-> T__'8846'__30
d_chunk_186 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_186 T_FormatSpec_6
v0 [T_Char_6]
v2 [T_Char_6]
v4 T_Char_6
v5
du_chunk_186 ::
  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_186 :: T_FormatSpec_6
-> [T_Char_6] -> [T_Char_6] -> T_Char_6 -> T__'8846'__30
du_chunk_186 T_FormatSpec_6
v0 [T_Char_6]
v1 [T_Char_6]
v2 T_Char_6
v3
  = let v4 :: AgdaAny
v4 = (T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny)
-> T_FormatSpec_6 -> T_Char_6 -> AgdaAny
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
v4 of
         MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v5
           -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 ((AgdaAny -> T_Chunk_62) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Chunk_62
C_Arg_64 (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.Function.Strict.du_force'8242'_56 ()
                ()
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_136 [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.Function.Strict.du_force'8242'_56 ()
                     ()
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_84)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_String_6 -> T_Char_6 -> T_String_6 -> T_Error_84
C_InvalidType_88 (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)