{-# 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 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.String
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Bool.Properties
import qualified MAlonzo.Code.Data.Char.Properties
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.Extrema
import qualified MAlonzo.Code.Data.List.Relation.Unary.Any
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.String.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Relation.Nullary
d_max_46 :: Integer -> [Integer] -> Integer
d_max_46 :: Integer -> [Integer] -> Integer
d_max_46
= (T_TotalOrder_652 -> Any -> [Any] -> Any)
-> Any -> Integer -> [Integer] -> Integer
forall a b. a -> b
coe
T_TotalOrder_652 -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Extrema.du_max_128
(T_TotalOrder_652 -> Any
forall a b. a -> b
coe T_TotalOrder_652
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_1700)
d_toVec_124 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24
d_toVec_124 :: T_String_6 -> T_Vec_24
d_toVec_124 T_String_6
v0
= ([Any] -> T_Vec_24) -> Any -> T_Vec_24
forall a b. a -> b
coe
[Any] -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_fromList_660
((T_String_6 -> String) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v0)
d_fromVec_130 ::
Integer ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_fromVec_130 :: Integer -> T_Vec_24 -> T_String_6
d_fromVec_130 ~Integer
v0 T_Vec_24
v1 = T_Vec_24 -> T_String_6
du_fromVec_130 T_Vec_24
v1
du_fromVec_130 ::
MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
du_fromVec_130 :: T_Vec_24 -> T_String_6
du_fromVec_130 T_Vec_24
v0
= (String -> T_String_6) -> Any -> T_String_6
forall a b. a -> b
coe
String -> T_String_6
MAlonzo.Code.Agda.Builtin.String.d_primStringFromList_14
((T_Vec_24 -> [Any]) -> Any -> Any
forall a b. a -> b
coe T_Vec_24 -> [Any]
MAlonzo.Code.Data.Vec.Base.du_toList_652 (T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v0))
d_parensIfSpace_132 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
MAlonzo.Code.Agda.Builtin.String.T_String_6
d_parensIfSpace_132 :: T_String_6 -> T_String_6
d_parensIfSpace_132 T_String_6
v0
= let v1 :: Bool
v1
= T_Dec_32 -> Bool
MAlonzo.Code.Relation.Nullary.d_does_42
(((Any -> T_Dec_32) -> [Any] -> T_Dec_32) -> Any -> Any -> T_Dec_32
forall a b. a -> b
coe
(Any -> T_Dec_32) -> [Any] -> T_Dec_32
MAlonzo.Code.Data.List.Relation.Unary.Any.du_any'63'_138
((T_Char_6 -> T_Char_6 -> T_Dec_32) -> Any -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_32
MAlonzo.Code.Data.Char.Properties.d__'8799'__14 (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
' '))
((T_String_6 -> String) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v0)) in
Any -> T_String_6
forall a b. a -> b
coe
(if Bool -> Bool
forall a b. a -> b
coe Bool
v1
then (T_String_6 -> T_String_6) -> Any -> Any
forall a b. a -> b
coe T_String_6 -> T_String_6
MAlonzo.Code.Data.String.Base.d_parens_38 (T_String_6 -> Any
forall a b. a -> b
coe T_String_6
v0)
else T_String_6 -> Any
forall a b. a -> b
coe T_String_6
v0)
d_wordsBy_148 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> ()) ->
(MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
[MAlonzo.Code.Agda.Builtin.String.T_String_6]
d_wordsBy_148 :: T_Level_18
-> (T_Char_6 -> T_Level_18)
-> (T_Char_6 -> T_Dec_32)
-> T_String_6
-> [T_String_6]
d_wordsBy_148 ~T_Level_18
v0 ~T_Char_6 -> T_Level_18
v1 T_Char_6 -> T_Dec_32
v2 T_String_6
v3 = (T_Char_6 -> T_Dec_32) -> T_String_6 -> [T_String_6]
du_wordsBy_148 T_Char_6 -> T_Dec_32
v2 T_String_6
v3
du_wordsBy_148 ::
(MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
[MAlonzo.Code.Agda.Builtin.String.T_String_6]
du_wordsBy_148 :: (T_Char_6 -> T_Dec_32) -> T_String_6 -> [T_String_6]
du_wordsBy_148 T_Char_6 -> T_Dec_32
v0 T_String_6
v1
= ((Any -> Any) -> [Any] -> [Any]) -> Any -> Any -> [T_String_6]
forall a b. a -> b
coe
(Any -> Any) -> [Any] -> [Any]
MAlonzo.Code.Data.List.Base.du_map_22
((String -> T_String_6) -> Any
forall a b. a -> b
coe String -> T_String_6
MAlonzo.Code.Agda.Builtin.String.d_primStringFromList_14)
(((Any -> T_Dec_32) -> [Any] -> [[Any]])
-> (T_Char_6 -> T_Dec_32) -> Any -> Any
forall a b. a -> b
coe
(Any -> T_Dec_32) -> [Any] -> [[Any]]
MAlonzo.Code.Data.List.Base.du_wordsBy_920 T_Char_6 -> T_Dec_32
v0
((T_String_6 -> String) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v1))
d_words_152 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
[MAlonzo.Code.Agda.Builtin.String.T_String_6]
d_words_152 :: T_String_6 -> [T_String_6]
d_words_152
= ((T_Char_6 -> T_Dec_32) -> T_String_6 -> [T_String_6])
-> Any -> T_String_6 -> [T_String_6]
forall a b. a -> b
coe
(T_Char_6 -> T_Dec_32) -> T_String_6 -> [T_String_6]
du_wordsBy_148
((Any -> T_Dec_32) -> Any
forall a b. a -> b
coe
(\ Any
v0 ->
Bool -> T_Dec_32
MAlonzo.Code.Data.Bool.Properties.d_T'63'_2210
((T_Char_6 -> Bool) -> Any -> Bool
forall a b. a -> b
coe T_Char_6 -> Bool
MAlonzo.Code.Agda.Builtin.Char.d_primIsSpace_14 Any
v0)))
d_linesBy_160 ::
MAlonzo.Code.Agda.Primitive.T_Level_18 ->
(MAlonzo.Code.Agda.Builtin.Char.T_Char_6 -> ()) ->
(MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
[MAlonzo.Code.Agda.Builtin.String.T_String_6]
d_linesBy_160 :: T_Level_18
-> (T_Char_6 -> T_Level_18)
-> (T_Char_6 -> T_Dec_32)
-> T_String_6
-> [T_String_6]
d_linesBy_160 ~T_Level_18
v0 ~T_Char_6 -> T_Level_18
v1 T_Char_6 -> T_Dec_32
v2 T_String_6
v3 = (T_Char_6 -> T_Dec_32) -> T_String_6 -> [T_String_6]
du_linesBy_160 T_Char_6 -> T_Dec_32
v2 T_String_6
v3
du_linesBy_160 ::
(MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
[MAlonzo.Code.Agda.Builtin.String.T_String_6]
du_linesBy_160 :: (T_Char_6 -> T_Dec_32) -> T_String_6 -> [T_String_6]
du_linesBy_160 T_Char_6 -> T_Dec_32
v0 T_String_6
v1
= ((Any -> Any) -> [Any] -> [Any]) -> Any -> Any -> [T_String_6]
forall a b. a -> b
coe
(Any -> Any) -> [Any] -> [Any]
MAlonzo.Code.Data.List.Base.du_map_22
((String -> T_String_6) -> Any
forall a b. a -> b
coe String -> T_String_6
MAlonzo.Code.Agda.Builtin.String.d_primStringFromList_14)
(((Any -> T_Dec_32) -> [Any] -> [[Any]])
-> (T_Char_6 -> T_Dec_32) -> Any -> Any
forall a b. a -> b
coe
(Any -> T_Dec_32) -> [Any] -> [[Any]]
MAlonzo.Code.Data.List.Base.du_linesBy_882 T_Char_6 -> T_Dec_32
v0
((T_String_6 -> String) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> String
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v1))
d_lines_164 ::
MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
[MAlonzo.Code.Agda.Builtin.String.T_String_6]
d_lines_164 :: T_String_6 -> [T_String_6]
d_lines_164
= ((T_Char_6 -> T_Dec_32) -> T_String_6 -> [T_String_6])
-> Any -> T_String_6 -> [T_String_6]
forall a b. a -> b
coe
(T_Char_6 -> T_Dec_32) -> T_String_6 -> [T_String_6]
du_linesBy_160
((T_Char_6 -> T_Char_6 -> T_Dec_32) -> Any -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_32
MAlonzo.Code.Data.Char.Properties.d__'8799'__14 (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
'\n'))
d_rectangle_172 ::
Integer ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24
d_rectangle_172 :: Integer -> T_Vec_24 -> T_Vec_24 -> T_Vec_24
d_rectangle_172 ~Integer
v0 T_Vec_24
v1 T_Vec_24
v2 = T_Vec_24 -> T_Vec_24 -> T_Vec_24
du_rectangle_172 T_Vec_24
v1 T_Vec_24
v2
du_rectangle_172 ::
MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24
du_rectangle_172 :: T_Vec_24 -> T_Vec_24 -> T_Vec_24
du_rectangle_172 T_Vec_24
v0 T_Vec_24
v1
= ((Any -> Any -> Any) -> T_Vec_24 -> T_Vec_24 -> T_Vec_24)
-> Any -> Any -> Any -> T_Vec_24
forall a b. a -> b
coe
(Any -> Any -> Any) -> T_Vec_24 -> T_Vec_24 -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_zipWith_258
((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 -> Any -> Any -> Any
forall a b. a -> b
coe Any
v2 ((T_Vec_24 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Vec_24 -> Integer
du_width_184 (T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v1)))) (T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v0)
(T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v1)
d_sizes_182 ::
Integer ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24 -> [Integer]
d_sizes_182 :: Integer -> T_Vec_24 -> T_Vec_24 -> [Integer]
d_sizes_182 ~Integer
v0 ~T_Vec_24
v1 T_Vec_24
v2 = T_Vec_24 -> [Integer]
du_sizes_182 T_Vec_24
v2
du_sizes_182 :: MAlonzo.Code.Data.Vec.Base.T_Vec_24 -> [Integer]
du_sizes_182 :: T_Vec_24 -> [Integer]
du_sizes_182 T_Vec_24
v0
= ((Any -> Any) -> [Any] -> [Any]) -> Any -> Any -> [Integer]
forall a b. a -> b
coe
(Any -> Any) -> [Any] -> [Any]
MAlonzo.Code.Data.List.Base.du_map_22
((T_String_6 -> Integer) -> Any
forall a b. a -> b
coe T_String_6 -> Integer
MAlonzo.Code.Data.String.Base.d_length_22)
((T_Vec_24 -> [Any]) -> Any -> Any
forall a b. a -> b
coe T_Vec_24 -> [Any]
MAlonzo.Code.Data.Vec.Base.du_toList_652 (T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v0))
d_width_184 ::
Integer ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24 -> Integer
d_width_184 :: Integer -> T_Vec_24 -> T_Vec_24 -> Integer
d_width_184 ~Integer
v0 ~T_Vec_24
v1 T_Vec_24
v2 = T_Vec_24 -> Integer
du_width_184 T_Vec_24
v2
du_width_184 :: MAlonzo.Code.Data.Vec.Base.T_Vec_24 -> Integer
du_width_184 :: T_Vec_24 -> Integer
du_width_184 T_Vec_24
v0
= (T_TotalOrder_652 -> Any -> [Any] -> Any)
-> T_TotalOrder_652 -> Integer -> Any -> Integer
forall a b. a -> b
coe
T_TotalOrder_652 -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Extrema.du_max_128
T_TotalOrder_652
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_1700
(Integer
0 :: Integer) ((T_Vec_24 -> [Integer]) -> Any -> Any
forall a b. a -> b
coe T_Vec_24 -> [Integer]
du_sizes_182 (T_Vec_24 -> Any
forall a b. a -> b
coe T_Vec_24
v0))
d_rectangle'737'_192 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24
d_rectangle'737'_192 :: Integer -> T_Char_6 -> T_Vec_24 -> T_Vec_24
d_rectangle'737'_192 Integer
v0 T_Char_6
v1
= (T_Vec_24 -> T_Vec_24 -> T_Vec_24) -> Any -> T_Vec_24 -> T_Vec_24
forall a b. a -> b
coe
T_Vec_24 -> T_Vec_24 -> T_Vec_24
du_rectangle_172
((Integer -> Any -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Any -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_replicate_490 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
((T_Char_6 -> Integer -> T_String_6 -> T_String_6) -> Any -> Any
forall a b. a -> b
coe T_Char_6 -> Integer -> T_String_6 -> T_String_6
MAlonzo.Code.Data.String.Base.d_padLeft_56 (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v1)))
d_rectangle'691'_198 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24
d_rectangle'691'_198 :: Integer -> T_Char_6 -> T_Vec_24 -> T_Vec_24
d_rectangle'691'_198 Integer
v0 T_Char_6
v1
= (T_Vec_24 -> T_Vec_24 -> T_Vec_24) -> Any -> T_Vec_24 -> T_Vec_24
forall a b. a -> b
coe
T_Vec_24 -> T_Vec_24 -> T_Vec_24
du_rectangle_172
((Integer -> Any -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Any -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_replicate_490 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
((T_Char_6 -> Integer -> T_String_6 -> T_String_6) -> Any -> Any
forall a b. a -> b
coe T_Char_6 -> Integer -> T_String_6 -> T_String_6
MAlonzo.Code.Data.String.Base.d_padRight_82 (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v1)))
d_rectangle'7580'_204 ::
Integer ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24 ->
MAlonzo.Code.Data.Vec.Base.T_Vec_24
d_rectangle'7580'_204 :: Integer -> T_Char_6 -> T_Char_6 -> T_Vec_24 -> T_Vec_24
d_rectangle'7580'_204 Integer
v0 T_Char_6
v1 T_Char_6
v2
= (T_Vec_24 -> T_Vec_24 -> T_Vec_24) -> Any -> T_Vec_24 -> T_Vec_24
forall a b. a -> b
coe
T_Vec_24 -> T_Vec_24 -> T_Vec_24
du_rectangle_172
((Integer -> Any -> T_Vec_24) -> Any -> Any -> Any
forall a b. a -> b
coe
Integer -> Any -> T_Vec_24
MAlonzo.Code.Data.Vec.Base.du_replicate_490 (Integer -> Any
forall a b. a -> b
coe Integer
v0)
((T_Char_6 -> T_Char_6 -> Integer -> T_String_6 -> T_String_6)
-> Any -> Any -> Any
forall a b. a -> b
coe
T_Char_6 -> T_Char_6 -> Integer -> T_String_6 -> T_String_6
MAlonzo.Code.Data.String.Base.d_padBoth_108 (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v1) (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v2)))