{-# 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.Data.String.Base 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.Nat
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.NonEmpty.Base
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Nat.Base
import qualified MAlonzo.Code.Function.Base
d__'8776'__6 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> ()
d__'8776'__6 :: Text -> Text -> ()
d__'8776'__6 = Text -> Text -> ()
forall a. a
erased
d__'60'__8 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> ()
d__'60'__8 :: Text -> Text -> ()
d__'60'__8 = Text -> Text -> ()
forall a. a
erased
d__'8804'__10 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> ()
d__'8804'__10 :: Text -> Text -> ()
d__'8804'__10 = Text -> Text -> ()
forall a. a
erased
d_head_12 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
Maybe MAlonzo.Code.Agda.Builtin.Char.T_Char_6
d_head_12 :: Text -> Maybe T_Char_6
d_head_12
= ((Any -> Any) -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Text -> Maybe T_Char_6
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Function.Base.du__'8728''8242'__226
(((Any -> Any) -> Maybe Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du_map_68
((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v0))))
((Text -> Maybe (T_Char_6, Text)) -> Any
forall a b. a -> b
coe Text -> Maybe (T_Char_6, Text)
MAlonzo.Code.Agda.Builtin.String.d_primStringUncons_10)
d_tail_14 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
Maybe MAlonzo.Code.Agda.Builtin.String.T_String_6
d_tail_14 :: Text -> Maybe Text
d_tail_14
= ((Any -> Any) -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> Text -> Maybe Text
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Function.Base.du__'8728''8242'__226
(((Any -> Any) -> Maybe Any -> Maybe Any) -> Any -> Any
forall a b. a -> b
coe
(Any -> Any) -> Maybe Any -> Maybe Any
MAlonzo.Code.Data.Maybe.Base.du_map_68
((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v0 -> T_Σ_14 -> Any
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 (Any -> T_Σ_14
forall a b. a -> b
coe Any
v0))))
((Text -> Maybe (T_Char_6, Text)) -> Any
forall a b. a -> b
coe Text -> Maybe (T_Char_6, Text)
MAlonzo.Code.Agda.Builtin.String.d_primStringUncons_10)
d_fromChar_16 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_fromChar_16 :: T_Char_6 -> Text
d_fromChar_16
= ((Any -> Any) -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> T_Char_6 -> Text
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Function.Base.du__'8728''8242'__226
((String -> Text) -> Any
forall a b. a -> b
coe String -> Text
MAlonzo.Code.Agda.Builtin.String.d_primStringFromList_14)
((Any -> [Any]) -> Any
forall a b. a -> b
coe Any -> [Any]
MAlonzo.Code.Data.List.Base.du_'91'_'93'_298)
d_fromList'8314'_18 ::
MAlonzo.Code.Data.List.NonEmpty.Base.T_List'8314'_24 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_fromList'8314'_18 :: T_List'8314'_24 -> Text
d_fromList'8314'_18
= ((Any -> Any) -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> T_List'8314'_24 -> Text
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Function.Base.du__'8728''8242'__226
((String -> Text) -> Any
forall a b. a -> b
coe String -> Text
MAlonzo.Code.Agda.Builtin.String.d_primStringFromList_14)
((T_List'8314'_24 -> [Any]) -> Any
forall a b. a -> b
coe T_List'8314'_24 -> [Any]
MAlonzo.Code.Data.List.NonEmpty.Base.du_toList_62)
d__'43''43'__20 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d__'43''43'__20 :: Text -> Text -> Text
d__'43''43'__20
= (Text -> Text -> Text) -> Text -> Text -> Text
forall a b. a -> b
coe Text -> Text -> Text
MAlonzo.Code.Agda.Builtin.String.d_primStringAppend_16
d_length_22 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 -> Integer
d_length_22 :: Text -> Integer
d_length_22 Text
v0
= ([Any] -> Integer) -> Any -> Integer
forall a b. a -> b
coe
[Any] -> Integer
MAlonzo.Code.Data.List.Base.du_length_296
((Text -> String) -> Text -> Any
forall a b. a -> b
coe Text -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 Text
v0)
d_replicate_24 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_replicate_24 :: Integer -> T_Char_6 -> Text
d_replicate_24 Integer
v0 T_Char_6
v1
= (String -> Text) -> Any -> Text
forall a b. a -> b
coe
String -> Text
MAlonzo.Code.Agda.Builtin.String.d_primStringFromList_14
((Integer -> Any -> [Any]) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Any -> [Any]
MAlonzo.Code.Data.List.Base.du_replicate_306 (Integer -> Any
forall a b. a -> b
coe Integer
v0) (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v1))
d_concat_28 ::
[MAlonzo.Code.Agda.Builtin.String.T_String_6] ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_concat_28 :: [Text] -> Text
d_concat_28
= ((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> [Text] -> Text
forall a b. a -> b
coe
(Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_240 ((Text -> Text -> Text) -> Any
forall a b. a -> b
coe Text -> Text -> Text
d__'43''43'__20)
(Text -> Any
forall a b. a -> b
coe (Text
"" :: Data.Text.Text))
d_intersperse_30 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
[MAlonzo.Code.Agda.Builtin.String.T_String_6] ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_intersperse_30 :: Text -> [Text] -> Text
d_intersperse_30 Text
v0
= ((Any -> Any) -> (Any -> Any) -> Any -> Any)
-> Any -> Any -> [Text] -> Text
forall a b. a -> b
coe
(Any -> Any) -> (Any -> Any) -> Any -> Any
MAlonzo.Code.Function.Base.du__'8728''8242'__226 (([Text] -> Text) -> Any
forall a b. a -> b
coe [Text] -> Text
d_concat_28)
((Any -> [Any] -> [Any]) -> Any -> Any
forall a b. a -> b
coe Any -> [Any] -> [Any]
MAlonzo.Code.Data.List.Base.du_intersperse_70 (Text -> Any
forall a b. a -> b
coe Text
v0))
d_unwords_34 ::
[MAlonzo.Code.Agda.Builtin.String.T_String_6] ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_unwords_34 :: [Text] -> Text
d_unwords_34 = (Text -> [Text] -> Text) -> Any -> [Text] -> Text
forall a b. a -> b
coe Text -> [Text] -> Text
d_intersperse_30 (Text -> Any
forall a b. a -> b
coe (Text
" " :: Data.Text.Text))
d_unlines_36 ::
[MAlonzo.Code.Agda.Builtin.String.T_String_6] ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_unlines_36 :: [Text] -> Text
d_unlines_36 = (Text -> [Text] -> Text) -> Any -> [Text] -> Text
forall a b. a -> b
coe Text -> [Text] -> Text
d_intersperse_30 (Text -> Any
forall a b. a -> b
coe (Text
"\n" :: Data.Text.Text))
d_parens_38 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_parens_38 :: Text -> Text
d_parens_38 Text
v0
= (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
d__'43''43'__20 (Text
"(" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe Text -> Text -> Text
d__'43''43'__20 Text
v0 (Text
")" :: Data.Text.Text))
d_braces_42 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_braces_42 :: Text -> Text
d_braces_42 Text
v0
= (Text -> Text -> Text) -> Text -> Any -> Text
forall a b. a -> b
coe
Text -> Text -> Text
d__'43''43'__20 (Text
"{" :: Data.Text.Text)
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe Text -> Text -> Text
d__'43''43'__20 Text
v0 (Text
"}" :: Data.Text.Text))
d__'60''43''62'__46 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d__'60''43''62'__46 :: Text -> Text -> Text
d__'60''43''62'__46 Text
v0 Text
v1
= let v2 :: b
v2
= let v2 :: t
v2
= (Text -> Text -> Text) -> Text -> Any -> t
forall a b. a -> b
coe
Text -> Text -> Text
d__'43''43'__20 Text
v0
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe Text -> Text -> Text
d__'43''43'__20 (Text
" " :: Data.Text.Text) Text
v1) in
Any -> b
forall a b. a -> b
coe
(case Text -> Text
forall a b. a -> b
coe Text
v1 of
Text
l | Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
(==) Text
l (Text
"" :: Data.Text.Text) -> Text -> Any
forall a b. a -> b
coe Text
v0
Text
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2) in
Any -> Text
forall a b. a -> b
coe
(case Text -> Text
forall a b. a -> b
coe Text
v0 of
Text
l | Text -> Text -> Bool
forall a. Eq a => a -> a -> Bool
(==) Text
l (Text
"" :: Data.Text.Text) -> Text -> Any
forall a b. a -> b
coe Text
v1
Text
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v2)
d_padLeft_56 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
Integer ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_padLeft_56 :: T_Char_6 -> Integer -> Text -> Text
d_padLeft_56 T_Char_6
v0 Integer
v1 Text
v2
= let v3 :: t
v3
= (Integer -> Integer -> Integer) -> Integer -> Any -> t
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v1
(((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_240
(let v3 :: a -> Integer
v3 = \ a
v3 -> Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (a -> Integer
forall a b. a -> b
coe a
v3) in
Any -> Any
forall a b. a -> b
coe ((Any -> Any -> Integer) -> Any
forall a b. a -> b
coe (\ Any
v4 -> Any -> Integer
forall {a}. a -> Integer
v3)))
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
((Text -> String) -> Text -> Any
forall a b. a -> b
coe Text -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 Text
v2)) in
Any -> Text
forall a b. a -> b
coe
(let v4 :: t
v4
= (Text -> Text -> Text) -> Text -> Text -> t
forall a b. a -> b
coe Text -> Text -> Text
d__'43''43'__20 (Integer -> T_Char_6 -> Text
d_replicate_24 (Any -> Integer
forall a b. a -> b
coe Any
forall a. a
v3) (T_Char_6 -> T_Char_6
forall a b. a -> b
coe T_Char_6
v0)) Text
v2 in
Any -> Any
forall a b. a -> b
coe
(case Any -> Integer
forall a b. a -> b
coe Any
forall a. a
v3 of
Integer
0 -> Text -> Any
forall a b. a -> b
coe Text
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4))
d_padRight_82 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
Integer ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_padRight_82 :: T_Char_6 -> Integer -> Text -> Text
d_padRight_82 T_Char_6
v0 Integer
v1 Text
v2
= let v3 :: t
v3
= (Integer -> Integer -> Integer) -> Integer -> Any -> t
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v1
(((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_240
(let v3 :: a -> Integer
v3 = \ a
v3 -> Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (a -> Integer
forall a b. a -> b
coe a
v3) in
Any -> Any
forall a b. a -> b
coe ((Any -> Any -> Integer) -> Any
forall a b. a -> b
coe (\ Any
v4 -> Any -> Integer
forall {a}. a -> Integer
v3)))
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
((Text -> String) -> Text -> Any
forall a b. a -> b
coe Text -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 Text
v2)) in
Any -> Text
forall a b. a -> b
coe
(let v4 :: t
v4
= (Text -> Text -> Text) -> Text -> Text -> t
forall a b. a -> b
coe Text -> Text -> Text
d__'43''43'__20 Text
v2 (Integer -> T_Char_6 -> Text
d_replicate_24 (Any -> Integer
forall a b. a -> b
coe Any
forall a. a
v3) (T_Char_6 -> T_Char_6
forall a b. a -> b
coe T_Char_6
v0)) in
Any -> Any
forall a b. a -> b
coe
(case Any -> Integer
forall a b. a -> b
coe Any
forall a. a
v3 of
Integer
0 -> Text -> Any
forall a b. a -> b
coe Text
v2
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4))
d_padBoth_108 ::
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
Integer ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_padBoth_108 :: T_Char_6 -> T_Char_6 -> Integer -> Text -> Text
d_padBoth_108 T_Char_6
v0 T_Char_6
v1 Integer
v2 Text
v3
= let v4 :: t
v4
= (Integer -> Integer -> Integer) -> Integer -> Any -> t
forall a b. a -> b
coe
Integer -> Integer -> Integer
MAlonzo.Code.Agda.Builtin.Nat.d__'45'__22 Integer
v2
(((Any -> Any -> Any) -> Any -> [Any] -> Any)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
(Any -> Any -> Any) -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Base.du_foldr_240
(let v4 :: a -> Integer
v4 = \ a
v4 -> Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (a -> Integer
forall a b. a -> b
coe a
v4) in
Any -> Any
forall a b. a -> b
coe ((Any -> Any -> Integer) -> Any
forall a b. a -> b
coe (\ Any
v5 -> Any -> Integer
forall {a}. a -> Integer
v4)))
(Integer -> Any
forall a b. a -> b
coe (Integer
0 :: Integer))
((Text -> String) -> Text -> Any
forall a b. a -> b
coe Text -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 Text
v3)) in
Any -> Text
forall a b. a -> b
coe
(let v5 :: t
v5
= (Text -> Text -> Text) -> Text -> Any -> t
forall a b. a -> b
coe
Text -> Text -> Text
d__'43''43'__20
(Integer -> T_Char_6 -> Text
d_replicate_24
((Integer -> Integer) -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_'8970'_'47'2'8971'_126 (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4))
(T_Char_6 -> T_Char_6
forall a b. a -> b
coe T_Char_6
v0))
((Text -> Text -> Text) -> Text -> Text -> Any
forall a b. a -> b
coe
Text -> Text -> Text
d__'43''43'__20 Text
v3
(Integer -> T_Char_6 -> Text
d_replicate_24
((Integer -> Integer) -> Any -> Integer
forall a b. a -> b
coe Integer -> Integer
MAlonzo.Code.Data.Nat.Base.d_'8968'_'47'2'8969'_130 (Any -> Any
forall a b. a -> b
coe Any
forall a. a
v4))
(T_Char_6 -> T_Char_6
forall a b. a -> b
coe T_Char_6
v1))) in
Any -> Any
forall a b. a -> b
coe
(case Any -> Integer
forall a b. a -> b
coe Any
forall a. a
v4 of
Integer
0 -> Text -> Any
forall a b. a -> b
coe Text
v3
Integer
_ -> Any -> Any
forall a b. a -> b
coe Any
forall a. a
v5))
d_Alignment_140 :: ()
d_Alignment_140 = ()
data T_Alignment_140 = C_Left_142 | C_Center_144 | C_Right_146
d_fromAlignment_148 ::
T_Alignment_140 ->
Integer ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_fromAlignment_148 :: T_Alignment_140 -> Integer -> Text -> Text
d_fromAlignment_148 T_Alignment_140
v0
= case T_Alignment_140 -> T_Alignment_140
forall a b. a -> b
coe T_Alignment_140
v0 of
T_Alignment_140
C_Left_142 -> (T_Char_6 -> Integer -> Text -> Text)
-> Any -> Integer -> Text -> Text
forall a b. a -> b
coe T_Char_6 -> Integer -> Text -> Text
d_padRight_82 (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
' ')
T_Alignment_140
C_Center_144 -> (T_Char_6 -> T_Char_6 -> Integer -> Text -> Text)
-> Any -> Any -> Integer -> Text -> Text
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> Integer -> Text -> Text
d_padBoth_108 (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
' ') (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
' ')
T_Alignment_140
C_Right_146 -> (T_Char_6 -> Integer -> Text -> Text)
-> Any -> Integer -> Text -> Text
forall a b. a -> b
coe T_Char_6 -> Integer -> Text -> Text
d_padLeft_56 (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
' ')
T_Alignment_140
_ -> Integer -> Text -> Text
forall a. a
MAlonzo.RTE.mazUnreachableError