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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
Require Import Coq.ZArith.BinInt Coq.NArith.BinNat Coq.QArith.QArith_base.
Require Import Coq.Lists.List.
Require Import Coq.Strings.String Coq.Strings.Ascii.
Require Crypto.Util.Strings.String.
Require Import Crypto.Util.Strings.HexString.
Require Import Crypto.Util.Strings.Decimal.
Import ListNotations. Local Open Scope list_scope. Local Open Scope string_scope.
Class Show T := show : bool (* parens *) -> T -> string.
Class ShowLines T := show_lines : bool -> T -> list string.
Definition maybe_wrap_parens (parens : bool) (s : string)
:= if parens then "(" ++ s ++ ")" else s.
Definition maybe_wrap_parens_lines (parens : bool) (s : list string)
:= match s, parens with
| s, false => s
| nil, _ => nil
| [s], _ => [maybe_wrap_parens parens s]
| s, true => "(" :: List.map (String " ") s ++ [")"]
end%list.
Global Instance show_lines_of_show {T} `{Show T} : ShowLines T | 1000
:= fun parens v => [show parens v].
Global Instance show_unit : Show unit := fun _ _ => "tt".
Global Instance show_True : Show True := fun _ _ => "I".
Global Instance show_False : Show False := fun _ pf => match pf with end.
Global Instance show_Empty_set : Show Empty_set := fun _ pf => match pf with end.
Global Instance show_bool : Show bool := fun _ b => if b then "true" else "false".
Global Instance show_option {T} `{Show T} : Show (option T)
:= fun p v
=> match v with
| Some v
=> maybe_wrap_parens
p
("Some " ++ show true v)
| None => "None"
end.
Global Instance show_list {T} `{Show T} : Show (list T)
:= fun _ ls => "[" ++ String.concat ", " (List.map (show false) ls) ++ "]".
Global Instance show_prod {A B} `{Show A, Show B} : Show (A * B)
:= fun _ '(a, b) => "(" ++ show false a ++ ", " ++ show true b ++ ")".
Global Instance show_string : Show string := fun _ s => """" ++ s ++ """".
Global Instance show_ascii : Show ascii := fun _ ch => String "'" (String ch "'").
Global Instance show_lines_option {T} `{ShowLines T} : ShowLines (option T)
:= fun p v
=> match v with
| Some v
=> maybe_wrap_parens_lines
p
match show_lines true v with
| [s] => ["Show " ++ s]
| s => "Show"::List.map (String " ") s
end
| None => ["None"]
end.
Global Instance show_lines_list {T} `{ShowLines T} : ShowLines (list T)
:= fun _ ls
=> let ls := List.map (show_lines false) ls in
(if List.forallb
(fun lines => Nat.eqb (List.length lines) 1)
ls
then ["[" ++ String.concat ", " (List.map (String.concat String.NewLine) ls) ++ "]"]%string
else ["["] ++ match ls with
| nil => ["]"]
| x :: xs
=> (List.map (String " ") x)
++ (List.flat_map
(fun x' => "," :: List.map (String " ") x')
xs)
++ ["]"]
end)%list.
Global Instance show_lines_prod {A B} `{ShowLines A, ShowLines B} : ShowLines (A * B)
:= fun _ '(a, b)
=> match show_lines false a, show_lines true b with
| [a], [b] => ["(" ++ a ++ ", " ++ b ++ ")"]%string
| a, b => ["("] ++ a ++ [", "] ++ b ++ [")"]
end%list.
Module Export Decimal.
Global Instance show_positive : Show positive
:= fun _ p
=> decimal_string_of_pos p.
Global Instance show_N : Show N
:= fun _ n
=> match n with
| N0 => "0"
| Npos p => show false p
end.
Global Instance show_nat : Show nat
:= fun _ n => show false (N.of_nat n).
Global Instance show_Z : Show Z
:= fun _ z
=> match z with
| Zneg p => "-" ++ show false p
| Z0 => "0"
| Zpos p => show false p
end.
Global Instance show_Q : Show Q
:= fun parens q
=> if (Qden q =? 1)%positive
then show parens (Qnum q)
else maybe_wrap_parens
parens
(show true (Qnum q) ++ " / " ++ show true (Qden q)).
End Decimal.
Module Hex.
Definition show_positive : Show positive
:= fun _ p => HexString.of_pos p.
Definition show_Z : Show Z
:= fun _ z => HexString.of_Z z.
Definition show_N : Show N
:= fun _ n
=> match n with
| N0 => "0"
| Npos p => show_positive false p
end.
Definition show_nat : Show nat
:= fun _ n => show_N false (N.of_nat n).
Definition show_Q : Show Q
:= fun parens q
=> if (Qden q =? 1)%positive
then show_Z parens (Qnum q)
else maybe_wrap_parens
parens
(show_Z true (Qnum q) ++ " / " ++ show_positive true (Qden q)).
End Hex.
|
