{-# 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 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.Maybe
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Text.Format.Generic
d_ArgChunk_4 :: ()
d_ArgChunk_4 = ()
data T_ArgChunk_4
= C_ℕArg_6 | C_ℤArg_8 | C_FloatArg_10 | C_CharArg_12 |
C_StringArg_14
d_ArgType_18 :: T_ArgChunk_4 -> ()
d_ArgType_18 :: T_ArgChunk_4 -> ()
d_ArgType_18 = T_ArgChunk_4 -> ()
forall a. a
erased
d_lexArg_20 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> Maybe T_ArgChunk_4
d_lexArg_20 :: T_Char_6 -> Maybe T_ArgChunk_4
d_lexArg_20 T_Char_6
v0
= let v1 :: b
v1 = Maybe Any -> b
forall a b. a -> b
coe Maybe Any
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 in
Any -> Maybe T_ArgChunk_4
forall a b. a -> b
coe
(case T_Char_6 -> T_Char_6
forall a b. a -> b
coe T_Char_6
v0 of
T_Char_6
'c'
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (T_ArgChunk_4 -> Any
forall a b. a -> b
coe T_ArgChunk_4
C_CharArg_12)
T_Char_6
'd' -> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (T_ArgChunk_4 -> Any
forall a b. a -> b
coe T_ArgChunk_4
C_ℤArg_8)
T_Char_6
'f'
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (T_ArgChunk_4 -> Any
forall a b. a -> b
coe T_ArgChunk_4
C_FloatArg_10)
T_Char_6
'i' -> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (T_ArgChunk_4 -> Any
forall a b. a -> b
coe T_ArgChunk_4
C_ℤArg_8)
T_Char_6
's'
-> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (T_ArgChunk_4 -> Any
forall a b. a -> b
coe T_ArgChunk_4
C_StringArg_14)
T_Char_6
'u' -> (Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe Any -> Maybe Any
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (T_ArgChunk_4 -> Any
forall a b. a -> b
coe T_ArgChunk_4
C_ℕArg_6)
T_Char_6
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v1)
d_formatSpec_22 :: MAlonzo.Code.Text.Format.Generic.T_FormatSpec_6
d_formatSpec_22 :: T_FormatSpec_6
d_formatSpec_22
= ((T_Char_6 -> Maybe Any) -> T_FormatSpec_6)
-> (T_Char_6 -> Maybe T_ArgChunk_4) -> T_FormatSpec_6
forall a b. a -> b
coe
(T_Char_6 -> Maybe Any) -> T_FormatSpec_6
MAlonzo.Code.Text.Format.Generic.C_FormatSpec'46'constructor_27
T_Char_6 -> Maybe T_ArgChunk_4
d_lexArg_20
d_Chunk_28 :: ()
d_Chunk_28 = ()
d_Error_30 :: ()
d_Error_30 = ()
d_Format_32 :: ()
d_Format_32 :: ()
d_Format_32 = ()
forall a. a
erased
d_lexer_40 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_lexer_40 :: T_String_6 -> T__'8846'__30
d_lexer_40
= (T_FormatSpec_6 -> T_String_6 -> T__'8846'__30)
-> Any -> 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 -> Any
forall a b. a -> b
coe T_FormatSpec_6
d_formatSpec_22)
d_size_42 ::
[MAlonzo.Code.Text.Format.Generic.T_Chunk_60] -> Integer
d_size_42 :: [T_Chunk_60] -> Integer
d_size_42 = ([T_Chunk_60] -> Integer) -> [T_Chunk_60] -> Integer
forall a b. a -> b
coe [T_Chunk_60] -> Integer
MAlonzo.Code.Text.Format.Generic.du_size_68
d_'10214'_'10215'_44 ::
[MAlonzo.Code.Text.Format.Generic.T_Chunk_60] -> AgdaAny
d_'10214'_'10215'_44 :: [T_Chunk_60] -> Any
d_'10214'_'10215'_44
= ([T_Chunk_60] -> Any) -> [T_Chunk_60] -> Any
forall a b. a -> b
coe [T_Chunk_60] -> Any
MAlonzo.Code.Text.Format.Generic.du_'10214'_'10215'_74