/
Show.lagda.md
79 lines (61 loc) · 1.88 KB
/
Show.lagda.md
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
<!--
```agda
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
```
-->
```agda
module Data.String.Show where
```
# The Show class
```agda
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
```