{-# 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.Membership.DecSetoid
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.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Nullary

-- Data.String._.max
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)
-- Data.String._._∈?_
d__'8712''63'__102 ::
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  [MAlonzo.Code.Agda.Builtin.Char.T_Char_6] ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8712''63'__102 :: T_Char_6 -> [T_Char_6] -> T_Dec_32
d__'8712''63'__102
  = let v0 :: T_Char_6 -> T_Char_6 -> T_Dec_32
v0 = T_Char_6 -> T_Char_6 -> T_Dec_32
MAlonzo.Code.Data.Char.Properties.d__'8799'__14 in
    Any -> T_Char_6 -> [T_Char_6] -> T_Dec_32
forall a b. a -> b
coe
      ((T_DecSetoid_84 -> Any -> [Any] -> T_Dec_32) -> Any -> Any
forall a b. a -> b
coe
         T_DecSetoid_84 -> Any -> [Any] -> T_Dec_32
MAlonzo.Code.Data.List.Membership.DecSetoid.du__'8712''63'__62
         (((Any -> Any -> T_Dec_32) -> T_DecSetoid_84) -> Any -> Any
forall a b. a -> b
coe
            (Any -> Any -> T_Dec_32) -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_254
            ((T_Char_6 -> T_Char_6 -> T_Dec_32) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_32
v0)))
-- Data.String.toVec
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 -> [T_Char_6]) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> [T_Char_6]
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v0)
-- Data.String.fromVec
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
  = ([T_Char_6] -> T_String_6) -> Any -> T_String_6
forall a b. a -> b
coe
      [T_Char_6] -> 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))
-- Data.String.parensIfSpace
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
              ((T_DecSetoid_84 -> Any -> [Any] -> T_Dec_32)
-> Any -> Any -> Any -> T_Dec_32
forall a b. a -> b
coe
                 T_DecSetoid_84 -> Any -> [Any] -> T_Dec_32
MAlonzo.Code.Data.List.Membership.DecSetoid.du__'8712''63'__62
                 (((Any -> Any -> T_Dec_32) -> T_DecSetoid_84) -> Any -> Any
forall a b. a -> b
coe
                    (Any -> Any -> T_Dec_32) -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_254
                    ((T_Char_6 -> T_Char_6 -> T_Dec_32) -> 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 -> [T_Char_6]) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> [T_Char_6]
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)
-- Data.String.wordsBy
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
      (([T_Char_6] -> T_String_6) -> Any
forall a b. a -> b
coe [T_Char_6] -> 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 -> [T_Char_6]) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> [T_Char_6]
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v1))
-- Data.String.words
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)))
-- Data.String.linesBy
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
      (([T_Char_6] -> T_String_6) -> Any
forall a b. a -> b
coe [T_Char_6] -> 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 -> [T_Char_6]) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> [T_Char_6]
MAlonzo.Code.Agda.Builtin.String.d_primStringToList_12 T_String_6
v1))
-- Data.String.lines
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'))
-- Data.String.rectangle
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)
-- Data.String._.sizes
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))
-- Data.String._.width
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))
-- Data.String.rectangleˡ
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)))
-- Data.String.rectangleʳ
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)))
-- Data.String.rectangleᶜ
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)))