/
Common.v
260 lines (213 loc) · 9.89 KB
/
Common.v
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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List.
Require Import Crypto.Util.Option.
Require Import Crypto.Util.OptionList.
Require Import Crypto.Util.Strings.String.
Require Import Crypto.Util.Strings.Ascii.
Require Import Crypto.Util.Notations.
Import ListNotations.
Local Open Scope list_scope.
Local Open Scope option_scope.
Local Open Scope char_scope.
Local Open Scope string_scope.
Definition ParserAction T := string -> list (T * string).
Delimit Scope parse_scope with parse.
Bind Scope parse_scope with ParserAction.
Definition parse_impossible {T} : ParserAction T
:= fun s => [].
Definition parse_empty : ParserAction unit
:= fun s
=> if s =? ""
then [(tt, "")]
else [].
Definition parse_seq_gen {A B C} (f : A -> B -> C) (p1 : ParserAction A) (p2 : ParserAction B) : ParserAction C
:= fun s
=> flat_map
(fun '(a, s) => List.map (fun '(b, s) => (f a b, s)) (p2 s))
(p1 s).
Definition parse_alt_gen {A B C} (f : A + B -> C) (p1 : ParserAction A) (p2 : ParserAction B) : ParserAction C
:= fun s
=> ((List.map (fun '(v, s) => (f (inl v), s)) (p1 s))
++ List.map (fun '(v, s) => (f (inr v), s)) (p2 s))%list.
Definition parse_alt {A} (p1 p2 : ParserAction A) : ParserAction A
:= parse_alt_gen (fun aa => match aa with inl a => a | inr a => a end) p1 p2.
Notation ε := parse_empty.
Infix "||" := parse_alt : parse_scope.
Infix "||->{ f }" := (parse_alt_gen f) : parse_scope.
Infix ";;->{ f }" := (parse_seq_gen f) : parse_scope.
Infix ";;" := (parse_seq_gen (@pair _ _)) : parse_scope.
Infix ";;L" := (parse_seq_gen (fun l r => l)) : parse_scope.
Infix ";;R" := (parse_seq_gen (fun l r => r)) : parse_scope.
Definition parse_alpha_char (lower : bool) (upper : bool) : ParserAction ascii
:= fun s
=> match s with
| EmptyString => []
| String ch s'
=> if ((lower && ("a" <=? ch) && (ch <=? "z")) || (upper && ("A" <=? ch) && (ch <=? "Z")))%char%bool
then [(ch, s')]
else []
end.
Notation "[A-Z]" := (parse_alpha_char false true) : parse_scope.
Notation "[a-z]" := (parse_alpha_char true false) : parse_scope.
Notation "[a-zA-Z]" := (parse_alpha_char true true) : parse_scope.
Definition parse_ascii (prefix : ascii) : ParserAction ascii
:= fun s
=> match s with
| EmptyString => []
| String ch s' => if (ch =? prefix)%char
then [(ch, s')]
else []
end.
Coercion parse_ascii : ascii >-> ParserAction.
Definition parse_ascii_case_insensitive (prefix : ascii) : ParserAction ascii
:= fun s
=> match s with
| EmptyString => []
| String ch s' => if (Ascii.to_lower ch =? Ascii.to_lower prefix)%char
then [(ch, s')]
else []
end.
Definition parse_str (prefix : string) : ParserAction string
:= fun s
=> if startswith prefix s
then [(prefix, substring (String.length prefix) (String.length s) s)]
else [].
Coercion parse_str : string >-> ParserAction.
Definition parse_str_case_insensitive (prefix : string) : ParserAction string
:= fun s
=> let '(s1, s2) := (substring 0 (String.length prefix) s,
substring (String.length prefix) (String.length s) s) in
if (String.to_lower prefix =? String.to_lower s1)%string
then [(s1, s2)]
else [].
Notation casefold := parse_str_case_insensitive (only parsing).
Definition parse_map {A B} (f : A -> B) : ParserAction A -> ParserAction B
:= fun p s
=> List.map (fun '(v, s) => (f v, s)) (p s).
Definition parse_filter {A} (f : A -> bool) : ParserAction A -> ParserAction A
:= fun p s
=> List.filter (fun '(v, s) => f v) (p s).
Definition parse_flat_map {A B} (f : A -> list B) : ParserAction A -> ParserAction B
:= fun p s
=> List.flat_map (fun '(v, s) => List.map (fun fv => (fv, s)) (f v)) (p s).
Definition parse_option_list_map {A B} (f : A -> option B) : ParserAction A -> ParserAction B
:= parse_flat_map (fun a => match f a with Some v => [v] | None => [] end).
Definition parse_maybe {A} (p : ParserAction A) : ParserAction (option A)
:= (p ||->{ fun v => match v with inl v => Some v | inr _ => None end } "")%parse.
Notation "f ?" := (parse_maybe f) : parse_scope.
Definition option_to_list {A} (v : option A) : list A
:= match v with
| Some v => [v]
| None => []
end.
Definition option_list_to_list {A} (v : option (list A)) : list A
:= match v with
| Some v => v
| None => []
end.
Definition fuel {A} (p : nat -> ParserAction A) : ParserAction A
:= fun s => p (S (String.length s)) s.
Fixpoint parse_plus_fueled {A} (p : ParserAction A) (fuel : nat) : ParserAction (list A)
:= (p ;;->{ @cons _ } (match fuel with
| O => fun s => []
| S fuel => parse_map option_list_to_list ((parse_plus_fueled p fuel)?)
end)).
Definition parse_plus {A} (p : ParserAction A) : ParserAction (list A)
:= fuel (parse_plus_fueled p).
Definition parse_star {A} (p : ParserAction A) : ParserAction (list A)
:= parse_map option_list_to_list ((parse_plus p)?).
Definition parse_lookahead {A} (p : ParserAction A) : ParserAction A
:= fun s => List.map (fun '(a, _) => (a, s)) (p s).
Definition parse_lookahead_not {A} (p : ParserAction A) : ParserAction unit
:= fun s => match p s with
| [] => [(tt, s)]
| _ => []
end.
Notation "p +" := (parse_plus p) : parse_scope.
Notation "p *" := (parse_star p) : parse_scope.
Definition whitespace : list ascii
:= [" "; "009" (* \t *); "010" (* \n *); "013" (* \r *); "012" (* \f *); "011" (* \v *)]%char.
Definition whitespace_strs : list string
:= Eval compute in List.map (fun ch => String ch "") whitespace.
Definition parse_alt_list {T} (ls : list (ParserAction T)) : ParserAction T
:= List.fold_left ((fun p2 p1 => p1 ||->{ fun v => match v with inl v => v | inr v => v end } p2)%parse)
ls
parse_impossible.
Definition parse_strs {T} (ls : list (string * T)) : ParserAction T
:= parse_alt_list (List.map (fun '(s, v) => parse_map (fun _ => v) (s:string)) ls).
Definition parse_one_whitespace : ParserAction string
:= Eval cbv [List.fold_right List.fold_left whitespace whitespace_strs List.tl List.hd parse_strs List.combine] in
(List.fold_left (B:=string) parse_alt (tl whitespace_strs) (hd " " whitespace_strs)).
Notation "[\s]" := parse_one_whitespace : parse_scope.
Definition parse_any_whitespace : ParserAction (list string)
:= Eval cbv [parse_one_whitespace] in
(parse_one_whitespace)*.
Definition strip_whitespace_around {A} (p : ParserAction A) : ParserAction A
:= parse_any_whitespace ;;->{ fun _ v => v }
p ;;->{ fun v _ => v }
parse_any_whitespace.
Definition strip_whitespace_before {A} (p : ParserAction A) : ParserAction A
:= parse_any_whitespace ;;->{ fun _ v => v }
p.
Definition strip_whitespace_after {A} (p : ParserAction A) : ParserAction A
:= p ;;->{ fun v _ => v }
parse_any_whitespace.
Definition parse_list_gen {A} (leftbr sep rightbr : string) (parse : ParserAction A) : ParserAction (list A)
:= (strip_whitespace_around leftbr)
;;->{ fun _ v => v }
((parse ;;->{ @cons _ }
(strip_whitespace_around sep ;;->{ fun _ tl => tl } parse)* ))?
;;->{ fun v _ => match v with None => [] | Some ls => ls end }
strip_whitespace_around rightbr.
Definition parse_list_gen_no_leading_trailing_space {A} (leftbr sep rightbr : string) (parse : ParserAction A) : ParserAction (list A)
:= (strip_whitespace_after leftbr)
;;->{ fun _ v => v }
((parse ;;->{ @cons _ }
(strip_whitespace_around sep ;;->{ fun _ tl => tl } parse)* ))?
;;->{ fun v _ => match v with None => [] | Some ls => ls end }
strip_whitespace_before rightbr.
Definition parse_list {A} (parse : ParserAction A) : ParserAction (list A)
:= parse_list_gen "[" ";" "]" parse.
Definition parse_list_Python_style {A} (parse : ParserAction A) : ParserAction (list A)
:= parse_list_gen "[" "," "]" parse.
Definition parse_list_Mathematica_style {A} (parse : ParserAction A) : ParserAction (list A)
:= parse_list_gen "{" "," "}" parse.
Definition parse_comma_list {A} (parse : ParserAction A) : ParserAction (list A)
:= parse_list_gen "" "," "" parse.
Definition parse_semicolon_list {A} (parse : ParserAction A) : ParserAction (list A)
:= parse_list_gen "" ";" "" parse.
Definition parse_any_list {A} (parse : ParserAction A) : ParserAction (list A)
:= parse_list parse || parse_list_Python_style parse || parse_list_Mathematica_style parse || parse_comma_list parse || parse_semicolon_list parse.
Fixpoint split_before_first (f : ascii -> bool) (s : string) : string * string
:= match s with
| EmptyString => (EmptyString, EmptyString)
| String ch rest
=> if f ch
then (EmptyString, s)
else let '(s1, s2) := split_before_first f rest in
(String ch s1, s2)
end.
Fixpoint split_before_first_skip (f : ascii -> bool) (s : string) (skip : nat) : string * string
:= match skip, s with
| 0, _ => split_before_first f s
| _, EmptyString => (EmptyString, EmptyString)
| S skip', String ch rest
=> let '(s1, s2) := split_before_first_skip f rest skip' in
(String ch s1, s2)
end.
Definition finalize {A} (p : ParserAction A) : string -> option A
:= fun s => match (p ;;->{fun v _ => v} ε)%parse s with
| [(v, _)] => Some v
| _ => None
end.
(*
Definition parse_ch {T} (ls : list (ascii * T)) (s : string) : option (T * string)
:= match s with
| EmptyString => None
| String ch s
=> List.fold_right
(fun '(ch', t) default
=> if ascii_beq ch ch' then Some (t, s) else default)
None
ls
end.
*)