{-# 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 Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Char qualified
import MAlonzo.Code.Agda.Builtin.String qualified
import MAlonzo.Code.Data.Bool.Base qualified
import MAlonzo.Code.Data.Char.Properties qualified
import MAlonzo.Code.Data.List.Base qualified
import MAlonzo.Code.Data.List.Extrema qualified
import MAlonzo.Code.Data.List.Membership.DecSetoid qualified
import MAlonzo.Code.Data.Nat.Properties qualified
import MAlonzo.Code.Data.String.Base qualified
import MAlonzo.Code.Data.Vec.Base qualified
import MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties qualified
import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                    mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                    word64ToNat)
import MAlonzo.RTE qualified

-- Data.String.toVec
d_toVec_122 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_toVec_122 :: T_String_6 -> T_Vec_28
d_toVec_122 T_String_6
v0
  = ([Any] -> T_Vec_28) -> Any -> T_Vec_28
forall a b. a -> b
coe
      [Any] -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_fromList_600
      ((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)
-- Data.String.fromVec
d_fromVec_128 ::
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_fromVec_128 :: Integer -> T_Vec_28 -> T_String_6
d_fromVec_128 ~Integer
v0 T_Vec_28
v1 = T_Vec_28 -> T_String_6
du_fromVec_128 T_Vec_28
v1
du_fromVec_128 ::
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
du_fromVec_128 :: T_Vec_28 -> T_String_6
du_fromVec_128 T_Vec_28
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_28 -> [Any]) -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> [Any]
MAlonzo.Code.Data.Vec.Base.du_toList_592 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v0))
-- Data.String.parensIfSpace
d_parensIfSpace_130 ::
  MAlonzo.Code.Agda.Builtin.String.T_String_6 ->
  MAlonzo.Code.Agda.Builtin.String.T_String_6
d_parensIfSpace_130 :: T_String_6 -> T_String_6
d_parensIfSpace_130 T_String_6
v0
  = (Bool -> Any -> Any -> Any) -> Any -> Any -> Any -> T_String_6
forall a b. a -> b
coe
      Bool -> Any -> Any -> Any
MAlonzo.Code.Data.Bool.Base.du_if_then_else__44
      ((T_Dec_20 -> Bool) -> Any -> Any
forall a b. a -> b
coe
         T_Dec_20 -> Bool
MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
         ((T_DecSetoid_84 -> Any -> [Any] -> T_Dec_20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
            T_DecSetoid_84 -> Any -> [Any] -> T_Dec_20
MAlonzo.Code.Data.List.Membership.DecSetoid.du__'8712''63'__58
            (((Any -> Any -> T_Dec_20) -> T_DecSetoid_84) -> Any -> Any
forall a b. a -> b
coe
               (Any -> Any -> T_Dec_20) -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_decSetoid_406
               ((T_Char_6 -> T_Char_6 -> T_Dec_20) -> Any
forall a b. a -> b
coe T_Char_6 -> T_Char_6 -> T_Dec_20
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)))
      ((T_String_6 -> T_String_6) -> T_String_6 -> Any
forall a b. a -> b
coe T_String_6 -> T_String_6
MAlonzo.Code.Data.String.Base.d_parens_46 T_String_6
v0) (T_String_6 -> Any
forall a b. a -> b
coe T_String_6
v0)
-- Data.String.rectangle
d_rectangle_136 ::
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_rectangle_136 :: Integer -> T_Vec_28 -> T_Vec_28 -> T_Vec_28
d_rectangle_136 ~Integer
v0 T_Vec_28
v1 T_Vec_28
v2 = T_Vec_28 -> T_Vec_28 -> T_Vec_28
du_rectangle_136 T_Vec_28
v1 T_Vec_28
v2
du_rectangle_136 ::
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
du_rectangle_136 :: T_Vec_28 -> T_Vec_28 -> T_Vec_28
du_rectangle_136 T_Vec_28
v0 T_Vec_28
v1
  = ((Any -> Any -> Any) -> T_Vec_28 -> T_Vec_28 -> T_Vec_28)
-> Any -> Any -> Any -> T_Vec_28
forall a b. a -> b
coe
      (Any -> Any -> Any) -> T_Vec_28 -> T_Vec_28 -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_zipWith_242
      ((Any -> Any) -> Any
forall a b. a -> b
coe (\ Any
v2 -> Any -> Any -> Any
forall a b. a -> b
coe Any
v2 ((T_Vec_28 -> Integer) -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> Integer
du_width_148 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v1)))) (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v0)
      (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v1)
-- Data.String._.sizes
d_sizes_146 ::
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> [Integer]
d_sizes_146 :: Integer -> T_Vec_28 -> T_Vec_28 -> [Integer]
d_sizes_146 ~Integer
v0 ~T_Vec_28
v1 T_Vec_28
v2 = T_Vec_28 -> [Integer]
du_sizes_146 T_Vec_28
v2
du_sizes_146 :: MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> [Integer]
du_sizes_146 :: T_Vec_28 -> [Integer]
du_sizes_146 T_Vec_28
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_28 -> [Any]) -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> [Any]
MAlonzo.Code.Data.Vec.Base.du_toList_592 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v0))
-- Data.String._.width
d_width_148 ::
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> Integer
d_width_148 :: Integer -> T_Vec_28 -> T_Vec_28 -> Integer
d_width_148 ~Integer
v0 ~T_Vec_28
v1 T_Vec_28
v2 = T_Vec_28 -> Integer
du_width_148 T_Vec_28
v2
du_width_148 :: MAlonzo.Code.Data.Vec.Base.T_Vec_28 -> Integer
du_width_148 :: T_Vec_28 -> Integer
du_width_148 T_Vec_28
v0
  = (T_TotalOrder_764 -> Any -> [Any] -> Any)
-> T_TotalOrder_764 -> Integer -> Any -> Integer
forall a b. a -> b
coe
      T_TotalOrder_764 -> Any -> [Any] -> Any
MAlonzo.Code.Data.List.Extrema.du_max_142
      T_TotalOrder_764
MAlonzo.Code.Data.Nat.Properties.d_'8804''45'totalOrder_2826
      (Integer
0 :: Integer) ((T_Vec_28 -> [Integer]) -> Any -> Any
forall a b. a -> b
coe T_Vec_28 -> [Integer]
du_sizes_146 (T_Vec_28 -> Any
forall a b. a -> b
coe T_Vec_28
v0))
-- Data.String.rectangleˡ
d_rectangle'737'_156 ::
  Integer ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_rectangle'737'_156 :: Integer -> T_Char_6 -> T_Vec_28 -> T_Vec_28
d_rectangle'737'_156 Integer
v0 T_Char_6
v1
  = (T_Vec_28 -> T_Vec_28 -> T_Vec_28) -> Any -> T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe
      T_Vec_28 -> T_Vec_28 -> T_Vec_28
du_rectangle_136
      ((Integer -> Any -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> Any -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_replicate_444 (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_60 (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v1)))
-- Data.String.rectangleʳ
d_rectangle'691'_162 ::
  Integer ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_rectangle'691'_162 :: Integer -> T_Char_6 -> T_Vec_28 -> T_Vec_28
d_rectangle'691'_162 Integer
v0 T_Char_6
v1
  = (T_Vec_28 -> T_Vec_28 -> T_Vec_28) -> Any -> T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe
      T_Vec_28 -> T_Vec_28 -> T_Vec_28
du_rectangle_136
      ((Integer -> Any -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> Any -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_replicate_444 (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_70 (T_Char_6 -> Any
forall a b. a -> b
coe T_Char_6
v1)))
-- Data.String.rectangleᶜ
d_rectangle'7580'_168 ::
  Integer ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Agda.Builtin.Char.T_Char_6 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28
d_rectangle'7580'_168 :: Integer -> T_Char_6 -> T_Char_6 -> T_Vec_28 -> T_Vec_28
d_rectangle'7580'_168 Integer
v0 T_Char_6
v1 T_Char_6
v2
  = (T_Vec_28 -> T_Vec_28 -> T_Vec_28) -> Any -> T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe
      T_Vec_28 -> T_Vec_28 -> T_Vec_28
du_rectangle_136
      ((Integer -> Any -> T_Vec_28) -> Any -> Any -> Any
forall a b. a -> b
coe
         Integer -> Any -> T_Vec_28
MAlonzo.Code.Data.Vec.Base.du_replicate_444 (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_80 (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)))