{-# 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.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
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)
d_ArgChunk_14 :: T_FormatSpec_6 -> ()
d_ArgChunk_14 :: T_FormatSpec_6 -> ()
d_ArgChunk_14 = T_FormatSpec_6 -> ()
forall a. a
erased
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
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
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'__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)))
d_ArgChunk_54 :: T_FormatSpec_6 -> ()
d_ArgChunk_54 :: T_FormatSpec_6 -> ()
d_ArgChunk_54 = T_FormatSpec_6 -> ()
forall a. a
erased
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
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)
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
d_Format_66 :: T_FormatSpec_6 -> ()
d_Format_66 :: T_FormatSpec_6 -> ()
d_Format_66 = T_FormatSpec_6 -> ()
forall a. a
erased
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'__216
(([Integer] -> Integer) -> AgdaAny
forall a b. a -> b
coe [Integer] -> Integer
MAlonzo.Code.Data.List.Base.d_sum_280)
(((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))))
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
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
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_144 (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)
d_RevWord_130 ::
T_FormatSpec_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -> ()
d_RevWord_130 :: T_FormatSpec_6 -> T_String_6 -> ()
d_RevWord_130 = T_FormatSpec_6 -> T_String_6 -> ()
forall a. a
erased
d_Prefix_132 ::
T_FormatSpec_6 -> MAlonzo.Code.Agda.Builtin.String.T_String_6 -> ()
d_Prefix_132 :: T_FormatSpec_6 -> T_String_6 -> ()
d_Prefix_132 = T_FormatSpec_6 -> T_String_6 -> ()
forall a. a
erased
d_toRevString_134 ::
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_134 :: T_FormatSpec_6 -> T_String_6 -> [T_Char_6] -> T_String_6
d_toRevString_134 ~T_FormatSpec_6
v0 ~T_String_6
v1 = [T_Char_6] -> T_String_6
du_toRevString_134
du_toRevString_134 ::
[MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
du_toRevString_134 :: [T_Char_6] -> T_String_6
du_toRevString_134
= ((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_460)
d_push_136 ::
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_136 :: T_FormatSpec_6
-> T_String_6 -> [T_Char_6] -> [T_Chunk_60] -> [T_Chunk_60]
d_push_136 ~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_136 [T_Char_6]
v2 [T_Chunk_60]
v3
du_push_136 ::
[MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
[T_Chunk_60] -> [T_Chunk_60]
du_push_136 :: [T_Char_6] -> [T_Chunk_60] -> [T_Chunk_60]
du_push_136 [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_134 [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)
d_loop_144 ::
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_144 :: T_FormatSpec_6
-> T_String_6
-> [T_Char_6]
-> [T_Char_6]
-> [T_Char_6]
-> T__'8846'__30
d_loop_144 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_60] -> [T_Chunk_60])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Char_6] -> [T_Chunk_60] -> [T_Chunk_60]
du_push_136 ([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_144
(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 :: t
v8
= ((AgdaAny -> AgdaAny) -> T__'8846'__30 -> T__'8846'__30)
-> AgdaAny -> T__'8846'__30 -> t
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_60] -> [T_Chunk_60]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Char_6] -> [T_Chunk_60] -> [T_Chunk_60]
du_push_136 ([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_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 (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_144 (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
d_type_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.Data.Sum.Base.T__'8846'__30
d_type_146 :: T_FormatSpec_6
-> T_String_6 -> [T_Char_6] -> [T_Char_6] -> T__'8846'__30
d_type_146 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_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_184 (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_144
(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
d_chunk_184 ::
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_184 :: T_FormatSpec_6
-> T_String_6
-> [T_Char_6]
-> T_Char_6
-> [T_Char_6]
-> T_Char_6
-> T__'8846'__30
d_chunk_184 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_184 T_FormatSpec_6
v0 [T_Char_6]
v2 [T_Char_6]
v4 T_Char_6
v5
du_chunk_184 ::
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_184 :: T_FormatSpec_6
-> [T_Char_6] -> [T_Char_6] -> T_Char_6 -> T__'8846'__30
du_chunk_184 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
-> (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_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.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_134 [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_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)