open import 1Lab.Type

open import Data.Reflection.Fixity
open import Data.String.Base
open import Data.Float.Base
open import Data.Char.Base
open import Data.List.Base
open import Data.Word.Base

open import Meta.Append

module Data.String.Show where

The Show classπŸ”—

record ShowS : Type where
  constructor showS
  field
    unshowS : String β†’ String

instance
  From-string-ShowS : From-string ShowS
  From-string-ShowS .From-string.Constraint _ = ⊀
  From-string-ShowS .from-string s = showS (s <>_)

  Append-ShowS : Append ShowS
  Append-ShowS .Append.mempty                     = showS id
  Append-ShowS .Append._<>_ (showS k1) (showS k2) = showS (k1 ∘ k2)

record Show {β„“} (A : Type β„“) : Type β„“ where
  field
    -- Convert a value into a difference-string, using the given
    -- precedence to determine whether or not parentheses are necessary.
    shows-prec : Precedence β†’ A β†’ ShowS

    -- Convert a value into a string suitable for printing.
    show      : A β†’ String

open Show ⦃ ... ⦄ public

default-show : βˆ€ {β„“} {A : Type β„“} β†’ (A β†’ String) β†’ Show A
default-show s = record
  { shows-prec = Ξ» _ x β†’ from-string (s x)
  ; show       = s
  }

show-parens : Bool β†’ ShowS β†’ ShowS
show-parens true  x = "(" <> x <> ")"
show-parens false x = x

private module P where primitive
  primShowChar       : Char   β†’ String
  primShowString     : String β†’ String
  primShowNat        : Nat    β†’ String
  primShowFloat      : Float  β†’ String

instance
  Show-Word64 : Show Word64
  Show-Word64 = default-show Ξ» x β†’ P.primShowNat (word64β†’nat x)

  Show-Nat : Show Nat
  Show-Nat = default-show P.primShowNat

  Show-String : Show String
  Show-String = default-show P.primShowString

  Show-Char : Show Char
  Show-Char = default-show P.primShowChar

  Show-Float : Show Float
  Show-Float = default-show P.primShowFloat