{-# 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.Printf.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.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Product.Nary.NonDependent
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Function.Nary.NonDependent.Base
import qualified MAlonzo.Code.Text.Format.Generic
d_PrintfSpec_18 :: p -> p -> p -> ()
d_PrintfSpec_18 p
a0 p
a1 p
a2 = ()
data T_PrintfSpec_18
= C_PrintfSpec'46'constructor_113 (AgdaAny -> AgdaAny -> AgdaAny)
(MAlonzo.Code.Agda.Builtin.String.T_String_6 -> AgdaAny)
d_ArgType_30 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
() -> AgdaAny -> ()
d_ArgType_30 :: () -> T_FormatSpec_6 -> () -> AgdaAny -> ()
d_ArgType_30 = () -> T_FormatSpec_6 -> () -> AgdaAny -> ()
forall a. a
erased
d_ArgChunk_42 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
() -> T_PrintfSpec_18 -> ()
d_ArgChunk_42 :: () -> T_FormatSpec_6 -> () -> T_PrintfSpec_18 -> ()
d_ArgChunk_42 = () -> T_FormatSpec_6 -> () -> T_PrintfSpec_18 -> ()
forall a. a
erased
d_ArgType_44 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
() -> T_PrintfSpec_18 -> AgdaAny -> ()
d_ArgType_44 :: () -> T_FormatSpec_6 -> () -> T_PrintfSpec_18 -> AgdaAny -> ()
d_ArgType_44 = () -> T_FormatSpec_6 -> () -> T_PrintfSpec_18 -> AgdaAny -> ()
forall a. a
erased
d_lexArg_46 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
() ->
T_PrintfSpec_18 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> Maybe AgdaAny
d_lexArg_46 :: ()
-> T_FormatSpec_6
-> ()
-> T_PrintfSpec_18
-> T_Char_6
-> Maybe AgdaAny
d_lexArg_46 ~()
v0 T_FormatSpec_6
v1 ~()
v2 ~T_PrintfSpec_18
v3 = T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny
du_lexArg_46 T_FormatSpec_6
v1
du_lexArg_46 ::
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> Maybe AgdaAny
du_lexArg_46 :: T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny
du_lexArg_46 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
MAlonzo.Code.Text.Format.Generic.d_lexArg_18 (T_FormatSpec_6 -> AgdaAny
forall a b. a -> b
coe T_FormatSpec_6
v0)
d_renderArg_50 :: T_PrintfSpec_18 -> AgdaAny -> AgdaAny -> AgdaAny
d_renderArg_50 :: T_PrintfSpec_18 -> AgdaAny -> AgdaAny -> AgdaAny
d_renderArg_50 T_PrintfSpec_18
v0
= case T_PrintfSpec_18 -> T_PrintfSpec_18
forall a b. a -> b
coe T_PrintfSpec_18
v0 of
C_PrintfSpec'46'constructor_113 AgdaAny -> AgdaAny -> AgdaAny
v1 T_String_6 -> AgdaAny
v2 -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1
T_PrintfSpec_18
_ -> AgdaAny -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_renderStr_52 ::
T_PrintfSpec_18 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> AgdaAny
d_renderStr_52 :: T_PrintfSpec_18 -> T_String_6 -> AgdaAny
d_renderStr_52 T_PrintfSpec_18
v0
= case T_PrintfSpec_18 -> T_PrintfSpec_18
forall a b. a -> b
coe T_PrintfSpec_18
v0 of
C_PrintfSpec'46'constructor_113 AgdaAny -> AgdaAny -> AgdaAny
v1 T_String_6 -> AgdaAny
v2 -> (T_String_6 -> AgdaAny) -> T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6 -> AgdaAny
v2
T_PrintfSpec_18
_ -> T_String_6 -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_Format_64 ::
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 -> ()
d_Format_64 :: T_FormatSpec_6 -> ()
d_Format_64 = T_FormatSpec_6 -> ()
forall a. a
erased
d_Error_66 :: p -> ()
d_Error_66 p
a0 = ()
d_Error_96 :: p -> p -> p -> ()
d_Error_96 p
a0 p
a1 p
a2 = ()
data T_Error_96 = C_Error'46'constructor_421
d_Size_100 ::
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> Integer
d_Size_100 :: T_FormatSpec_6 -> T__'8846'__30 -> Integer
d_Size_100 ~T_FormatSpec_6
v0 T__'8846'__30
v1 = T__'8846'__30 -> Integer
du_Size_100 T__'8846'__30
v1
du_Size_100 :: MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> Integer
du_Size_100 :: T__'8846'__30 -> Integer
du_Size_100 T__'8846'__30
v0
= case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v0 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v1 -> Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v1
-> ([T_Chunk_60] -> Integer) -> AgdaAny -> Integer
forall a b. a -> b
coe [T_Chunk_60] -> Integer
MAlonzo.Code.Text.Format.Generic.du_size_68 AgdaAny
v1
T__'8846'__30
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
d_Printf_108 ::
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> () -> ()
d_Printf_108 :: T_FormatSpec_6 -> () -> T__'8846'__30 -> () -> ()
d_Printf_108 = T_FormatSpec_6 -> () -> T__'8846'__30 -> () -> ()
forall a. a
erased
d_map_118 ::
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_map_118 :: T_FormatSpec_6
-> ()
-> ()
-> ()
-> ()
-> T__'8846'__30
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_map_118 ~T_FormatSpec_6
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 T__'8846'__30
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7 = T__'8846'__30 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_map_118 T__'8846'__30
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_map_118 ::
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_map_118 :: T__'8846'__30 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_map_118 T__'8846'__30
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
= case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v0 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v3 -> AgdaAny
forall a. a
erased
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v3
-> (Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Nary.NonDependent.Base.du_map'8345'_140
(((AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_216 ((Integer -> Integer -> Integer) -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt)
(Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer))
(((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
forall a b. a -> b
coe
(\ AgdaAny
v4 ->
let v5 :: Integer
v5 = Integer
1 :: Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Chunk_60
forall a b. a -> b
coe AgdaAny
v4 of
MAlonzo.Code.Text.Format.Generic.C_Raw_64 T_String_6
v6 -> Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer)
T_Chunk_60
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5)))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)))
((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_ArgChunk_142 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
T_PrintfSpec_18 -> ()
d_ArgChunk_142 :: () -> () -> T_FormatSpec_6 -> T_PrintfSpec_18 -> ()
d_ArgChunk_142 = () -> () -> T_FormatSpec_6 -> T_PrintfSpec_18 -> ()
forall a. a
erased
d_ArgType_144 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
T_PrintfSpec_18 -> AgdaAny -> ()
d_ArgType_144 :: () -> () -> T_FormatSpec_6 -> T_PrintfSpec_18 -> AgdaAny -> ()
d_ArgType_144 = () -> () -> T_FormatSpec_6 -> T_PrintfSpec_18 -> AgdaAny -> ()
forall a. a
erased
d_lexArg_146 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
T_PrintfSpec_18 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> Maybe AgdaAny
d_lexArg_146 :: ()
-> ()
-> T_FormatSpec_6
-> T_PrintfSpec_18
-> T_Char_6
-> Maybe AgdaAny
d_lexArg_146 ~()
v0 ~()
v1 T_FormatSpec_6
v2 ~T_PrintfSpec_18
v3 = T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny
du_lexArg_146 T_FormatSpec_6
v2
du_lexArg_146 ::
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> Maybe AgdaAny
du_lexArg_146 :: T_FormatSpec_6 -> T_Char_6 -> Maybe AgdaAny
du_lexArg_146 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
MAlonzo.Code.Text.Format.Generic.d_lexArg_18 (T_FormatSpec_6 -> AgdaAny
forall a b. a -> b
coe T_FormatSpec_6
v0)
d_renderArg_148 :: T_PrintfSpec_18 -> AgdaAny -> AgdaAny -> AgdaAny
d_renderArg_148 :: T_PrintfSpec_18 -> AgdaAny -> AgdaAny -> AgdaAny
d_renderArg_148 T_PrintfSpec_18
v0 = (T_PrintfSpec_18 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18 -> AgdaAny -> AgdaAny -> AgdaAny
d_renderArg_50 (T_PrintfSpec_18 -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18
v0)
d_renderStr_150 ::
T_PrintfSpec_18 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> AgdaAny
d_renderStr_150 :: T_PrintfSpec_18 -> T_String_6 -> AgdaAny
d_renderStr_150 T_PrintfSpec_18
v0 = (T_PrintfSpec_18 -> T_String_6 -> AgdaAny)
-> AgdaAny -> T_String_6 -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18 -> T_String_6 -> AgdaAny
d_renderStr_52 (T_PrintfSpec_18 -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18
v0)
d_Error_154 :: p -> p -> p -> p -> p -> p -> ()
d_Error_154 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
d_Printf_156 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
T_PrintfSpec_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> () -> ()
d_Printf_156 :: ()
-> ()
-> T_FormatSpec_6
-> T_PrintfSpec_18
-> ()
-> T__'8846'__30
-> ()
-> ()
d_Printf_156 = ()
-> ()
-> T_FormatSpec_6
-> T_PrintfSpec_18
-> ()
-> T__'8846'__30
-> ()
-> ()
forall a. a
erased
d_map_158 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
T_PrintfSpec_18 ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
d_map_158 :: ()
-> ()
-> T_FormatSpec_6
-> T_PrintfSpec_18
-> ()
-> ()
-> ()
-> ()
-> T__'8846'__30
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
d_map_158 ~()
v0 ~()
v1 ~T_FormatSpec_6
v2 ~T_PrintfSpec_18
v3 = ()
-> ()
-> ()
-> ()
-> T__'8846'__30
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_map_158
du_map_158 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
(AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_map_158 :: ()
-> ()
-> ()
-> ()
-> T__'8846'__30
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
du_map_158 ()
v0 ()
v1 ()
v2 ()
v3 T__'8846'__30
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6 = (T__'8846'__30 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> T__'8846'__30 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
du_map_118 T__'8846'__30
v4 AgdaAny -> AgdaAny
v5 AgdaAny
v6
d_lexer_178 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
T_PrintfSpec_18 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_lexer_178 :: ()
-> ()
-> T_FormatSpec_6
-> T_PrintfSpec_18
-> T_String_6
-> T__'8846'__30
d_lexer_178 ~()
v0 ~()
v1 T_FormatSpec_6
v2 ~T_PrintfSpec_18
v3 = T_FormatSpec_6 -> T_String_6 -> T__'8846'__30
du_lexer_178 T_FormatSpec_6
v2
du_lexer_178 ::
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_lexer_178 :: T_FormatSpec_6 -> T_String_6 -> T__'8846'__30
du_lexer_178 T_FormatSpec_6
v0
= (T_FormatSpec_6 -> T_String_6 -> T__'8846'__30)
-> AgdaAny -> T_String_6 -> T__'8846'__30
forall a b. a -> b
coe T_FormatSpec_6 -> T_String_6 -> T__'8846'__30
MAlonzo.Code.Text.Format.Generic.d_lexer_88 (T_FormatSpec_6 -> AgdaAny
forall a b. a -> b
coe T_FormatSpec_6
v0)
d_'10214'_'10215'_182 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
T_PrintfSpec_18 ->
[MAlonzo.Code.Text.Format.Generic.T_Chunk_60] -> AgdaAny
d_'10214'_'10215'_182 :: ()
-> ()
-> T_FormatSpec_6
-> T_PrintfSpec_18
-> [T_Chunk_60]
-> AgdaAny
d_'10214'_'10215'_182 ~()
v0 ~()
v1 ~T_FormatSpec_6
v2 ~T_PrintfSpec_18
v3 = [T_Chunk_60] -> AgdaAny
du_'10214'_'10215'_182
du_'10214'_'10215'_182 ::
[MAlonzo.Code.Text.Format.Generic.T_Chunk_60] -> AgdaAny
du_'10214'_'10215'_182 :: [T_Chunk_60] -> AgdaAny
du_'10214'_'10215'_182
= ([T_Chunk_60] -> AgdaAny) -> [T_Chunk_60] -> AgdaAny
forall a b. a -> b
coe [T_Chunk_60] -> AgdaAny
MAlonzo.Code.Text.Format.Generic.du_'10214'_'10215'_74
d_assemble_198 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
T_PrintfSpec_18 ->
[MAlonzo.Code.Text.Format.Generic.T_Chunk_60] ->
AgdaAny -> [AgdaAny]
d_assemble_198 :: ()
-> ()
-> T_FormatSpec_6
-> T_PrintfSpec_18
-> [T_Chunk_60]
-> AgdaAny
-> [AgdaAny]
d_assemble_198 ~()
v0 ~()
v1 ~T_FormatSpec_6
v2 T_PrintfSpec_18
v3 [T_Chunk_60]
v4 AgdaAny
v5 = T_PrintfSpec_18 -> [T_Chunk_60] -> AgdaAny -> [AgdaAny]
du_assemble_198 T_PrintfSpec_18
v3 [T_Chunk_60]
v4 AgdaAny
v5
du_assemble_198 ::
T_PrintfSpec_18 ->
[MAlonzo.Code.Text.Format.Generic.T_Chunk_60] ->
AgdaAny -> [AgdaAny]
du_assemble_198 :: T_PrintfSpec_18 -> [T_Chunk_60] -> AgdaAny -> [AgdaAny]
du_assemble_198 T_PrintfSpec_18
v0 [T_Chunk_60]
v1 AgdaAny
v2
= case [T_Chunk_60] -> [AgdaAny]
forall a b. a -> b
coe [T_Chunk_60]
v1 of
[] -> [T_Chunk_60] -> [AgdaAny]
forall a b. a -> b
coe [T_Chunk_60]
v1
(:) AgdaAny
v3 [AgdaAny]
v4
-> case AgdaAny -> T_Chunk_60
forall a b. a -> b
coe AgdaAny
v3 of
MAlonzo.Code.Text.Format.Generic.C_Arg_62 AgdaAny
v5
-> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2 of
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
-> (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_PrintfSpec_18 -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_PrintfSpec_18 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18 -> AgdaAny -> AgdaAny -> AgdaAny
d_renderArg_50 T_PrintfSpec_18
v0 AgdaAny
v5 AgdaAny
v6)
((T_PrintfSpec_18 -> [T_Chunk_60] -> AgdaAny -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18 -> [T_Chunk_60] -> AgdaAny -> [AgdaAny]
du_assemble_198 (T_PrintfSpec_18 -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))
T_Σ_14
_ -> [AgdaAny]
forall a. a
MAlonzo.RTE.mazUnreachableError
MAlonzo.Code.Text.Format.Generic.C_Raw_64 T_String_6
v5
-> (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_PrintfSpec_18 -> T_String_6 -> AgdaAny)
-> T_PrintfSpec_18 -> T_String_6 -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18 -> T_String_6 -> AgdaAny
d_renderStr_52 T_PrintfSpec_18
v0 T_String_6
v5)
((T_PrintfSpec_18 -> [T_Chunk_60] -> AgdaAny -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18 -> [T_Chunk_60] -> AgdaAny -> [AgdaAny]
du_assemble_198 (T_PrintfSpec_18 -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18
v0) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) (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_printf'8242'_218 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
T_PrintfSpec_18 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_printf'8242'_218 :: ()
-> ()
-> T_FormatSpec_6
-> T_PrintfSpec_18
-> T__'8846'__30
-> AgdaAny
d_printf'8242'_218 ~()
v0 ~()
v1 ~T_FormatSpec_6
v2 T_PrintfSpec_18
v3 T__'8846'__30
v4 = T_PrintfSpec_18 -> T__'8846'__30 -> AgdaAny
du_printf'8242'_218 T_PrintfSpec_18
v3 T__'8846'__30
v4
du_printf'8242'_218 ::
T_PrintfSpec_18 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_printf'8242'_218 :: T_PrintfSpec_18 -> T__'8846'__30 -> AgdaAny
du_printf'8242'_218 T_PrintfSpec_18
v0 T__'8846'__30
v1
= case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v1 of
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v2 -> AgdaAny
forall a. a
erased
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v2
-> (Integer -> (AgdaAny -> AgdaAny) -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
Integer -> (AgdaAny -> AgdaAny) -> AgdaAny
MAlonzo.Code.Data.Product.Nary.NonDependent.du_curry'8868''8345'_170
(((AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
(AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_216 ((Integer -> Integer -> Integer) -> AgdaAny
forall a b. a -> b
coe Integer -> Integer -> Integer
addInt)
(Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer))
(((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
forall a b. a -> b
coe
(\ AgdaAny
v3 ->
let v4 :: Integer
v4 = Integer
1 :: Integer in
AgdaAny -> AgdaAny
forall a b. a -> b
coe
(case AgdaAny -> T_Chunk_60
forall a b. a -> b
coe AgdaAny
v3 of
MAlonzo.Code.Text.Format.Generic.C_Raw_64 T_String_6
v5 -> Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer)
T_Chunk_60
_ -> Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4)))
(AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)))
((T_PrintfSpec_18 -> [T_Chunk_60] -> AgdaAny -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18 -> [T_Chunk_60] -> AgdaAny -> [AgdaAny]
du_assemble_198 (T_PrintfSpec_18 -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
d_printf_226 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
() ->
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
T_PrintfSpec_18 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> AgdaAny
d_printf_226 :: ()
-> () -> T_FormatSpec_6 -> T_PrintfSpec_18 -> T_String_6 -> AgdaAny
d_printf_226 ~()
v0 ~()
v1 T_FormatSpec_6
v2 T_PrintfSpec_18
v3 T_String_6
v4 = T_FormatSpec_6 -> T_PrintfSpec_18 -> T_String_6 -> AgdaAny
du_printf_226 T_FormatSpec_6
v2 T_PrintfSpec_18
v3 T_String_6
v4
du_printf_226 ::
MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6 ->
T_PrintfSpec_18 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> AgdaAny
du_printf_226 :: T_FormatSpec_6 -> T_PrintfSpec_18 -> T_String_6 -> AgdaAny
du_printf_226 T_FormatSpec_6
v0 T_PrintfSpec_18
v1 T_String_6
v2
= (T_PrintfSpec_18 -> T__'8846'__30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
T_PrintfSpec_18 -> T__'8846'__30 -> AgdaAny
du_printf'8242'_218 (T_PrintfSpec_18 -> AgdaAny
forall a b. a -> b
coe T_PrintfSpec_18
v1)
((T_FormatSpec_6 -> T_String_6 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_FormatSpec_6 -> T_String_6 -> T__'8846'__30
MAlonzo.Code.Text.Format.Generic.d_lexer_88 (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
v2))