PROOF.bend
qasim-bend-kit@0.1.0.1 · 310 lines · 0 definitions
1import Base
2import qasim-bend-kit@0.1.0.1/LAWS.bend as L
3import qasim-bend-kit@0.1.0.1/libs/JSON.bend as Json
4import qasim-bend-kit@0.1.0.1/libs/URL.bend as URL
5import qasim-bend-kit@0.1.0.1/proof/JSON_StringProof.bend as StringProof
6import qasim-bend-kit@0.1.0.1/proof/JSON_PrimitiveProof.bend as PrimitiveProof
7import qasim-bend-kit@0.1.0.1/proof/JSON_NumberLexProof.bend as NumberLexProof
8import qasim-bend-kit@0.1.0.1/proof/JSON_ParallelProof.bend as ParallelProof
9import qasim-bend-kit@0.1.0.1/proof/JSON_LexWhitespaceProof.bend as LexWhitespaceProof
10import qasim-bend-kit@0.1.0.1/proof/JSON_AssemblyProof.bend as AssemblyProof
11import qasim-bend-kit@0.1.0.1/proof/JSON_SourceProof.bend as SourceProof
12import qasim-bend-kit@0.1.0.1/proof/JSON_RenderLexProof.bend as RenderLexProof
13
14def ResultValue() -> Type:
15 Result<&1, &1, Json.Error, Json.Value>
16
17def parse_for_equality(text: String) -> ResultValue():
18 Json.parse(text)
19
20def assemble_atom(result: ResultValue()) -> {Json.assemble(Json.Atom{result} <> Nil{}, Json.NeedValue{Json.Top{}}) == result : ResultValue()}:
21 match result:
22 case Done{value}: {==}
23 case Fail{Json.Error{}}: {==}
24
25def parallel_single(+text: String) -> {Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}) == Json.decode_lexeme(Json.Payload{text}) <> Nil{} : List<Json.Token>}:
26 Equal.trans(List<Json.Token>, Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}),
27 ParallelProof.flat(Json.Payload{text} <> Nil{}, Nil{}), Json.decode_lexeme(Json.Payload{text}) <> Nil{},
28 ParallelProof.decode(Json.Payload{text} <> Nil{}, Nil{}), {==})
29
30def assemble_source(+value: Json.Value) -> {Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}), Json.NeedValue{Json.Top{}}) == Done{value} : ResultValue()}:
31 Equal.trans(ResultValue(),
32 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}), Json.NeedValue{Json.Top{}}),
33 Json.assemble(AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}), AssemblyProof.start(value, AssemblyProof.Whole{}, Nil{}, Nil{}, Json.Top{})),
34 Done{value},
35 Equal.cong(List<Json.Token>, ResultValue(), tokens => Json.assemble(tokens, Json.NeedValue{Json.Top{}}),
36 Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}),
37 AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}),
38 Equal.trans(List<Json.Token>,
39 Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}),
40 SourceProof.token_source(Json.source(value, False{}, Nil{}), Nil{}),
41 AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}),
42 Equal.trans(List<Json.Token>,
43 Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(value, False{}, Nil{}))), Nil{}),
44 ParallelProof.flat(Json.source(value, False{}, Nil{}), Nil{}),
45 SourceProof.token_source(Json.source(value, False{}, Nil{}), Nil{}),
46 ParallelProof.decode(Json.source(value, False{}, Nil{}), Nil{}),
47 Equal.sym(List<Json.Token>, SourceProof.token_source(Json.source(value, False{}, Nil{}), Nil{}),
48 ParallelProof.flat(Json.source(value, False{}, Nil{}), Nil{}),
49 SourceProof.token_source_flat(Json.source(value, False{}, Nil{}), Nil{}))),
50 SourceProof.source_tokens(value, AssemblyProof.Whole{}, Nil{}, Nil{}))),
51 Equal.trans(ResultValue(),
52 Json.assemble(AssemblyProof.tokens(value, AssemblyProof.Whole{}, Nil{}), AssemblyProof.start(value, AssemblyProof.Whole{}, Nil{}, Nil{}, Json.Top{})),
53 Json.assemble(Nil{}, Json.assembly_resume(Json.Top{}, value)),
54 Done{value},
55 AssemblyProof.roundtrip(value, AssemblyProof.Whole{}, Nil{}, Nil{}, Nil{}, Json.Top{}), {==}))
56
57def parse_number_payload(+text: String,
58 +certificate: Json.NumberCert<text>) -> {Json.parse_normalized(text) == Done{Json.Number{text, certificate}} : ResultValue()}:
59 Equal.trans(ResultValue(), Json.parse_normalized(text),
60 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
61 Done{Json.Number{text, certificate}},
62 Equal.cong(List<&2, Json.Lexeme>, ResultValue(), items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
63 Json.lex_scan(text, Json.Outside{}, SNil{}, Nil{}), Json.Payload{text} <> Nil{},
64 NumberLexProof.lex_number_payload(text, PrimitiveProof.cert_valid(text, certificate))),
65 Equal.trans(ResultValue(),
66 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
67 Json.decode_payload(text), Done{Json.Number{text, certificate}},
68 Equal.trans(ResultValue(),
69 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
70 Json.assemble(Json.decode_lexeme(Json.Payload{text}) <> Nil{}, Json.NeedValue{Json.Top{}}),
71 Json.decode_payload(text),
72 Equal.cong(List<Json.Token>, ResultValue(), tokens => Json.assemble(tokens, Json.NeedValue{Json.Top{}}),
73 Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{text} <> Nil{})), Nil{}),
74 Json.decode_lexeme(Json.Payload{text}) <> Nil{},
75 parallel_single(text)),
76 Equal.trans(ResultValue(),
77 Json.assemble(Json.decode_lexeme(Json.Payload{text}) <> Nil{}, Json.NeedValue{Json.Top{}}),
78 Json.decode_payload(text), Json.decode_payload(text),
79 assemble_atom(Json.decode_payload(text)), {==})),
80 PrimitiveProof.number_roundtrip(text, certificate)))
81
82def assembled_string_payload(+text: String) -> {Json.assemble(Json.Atom{Json.decode_payload("\"" ++ Json.escape_string(text) ++ "\"")} <> Nil{}, Json.NeedValue{Json.Top{}}) == Done{Json.Str{text}} : ResultValue()}:
83 Equal.cong(ResultValue(), ResultValue(), result => Json.assemble(Json.Atom{result} <> Nil{}, Json.NeedValue{Json.Top{}}),
84 Json.decode_payload("\"" ++ Json.escape_string(text) ++ "\""), Done{Json.Str{text}}, StringProof.string_payload(text))
85
86def parse_string_payload(+text: String) -> {Json.parse_normalized("\"" ++ Json.escape_string(text) ++ "\"") == Done{Json.Str{text}} : ResultValue()}:
87 Equal.trans(ResultValue(), Json.parse_normalized("\"" ++ Json.escape_string(text) ++ "\""),
88 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
89 Done{Json.Str{text}},
90 Equal.cong(List<&2, Json.Lexeme>, ResultValue(), items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
91 Json.lex_scan("\"" ++ Json.escape_string(text) ++ "\"", Json.Outside{}, SNil{}, Nil{}),
92 Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""} <> Nil{},
93 LexWhitespaceProof.lex_rendered_string(text)),
94 Equal.trans(ResultValue(),
95 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""} <> Nil{})), Nil{}), Json.NeedValue{Json.Top{}}),
96 Json.assemble(Json.decode_lexeme(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""}) <> Nil{}, Json.NeedValue{Json.Top{}}),
97 Done{Json.Str{text}},
98 Equal.cong(List<Json.Token>, ResultValue(), tokens => Json.assemble(tokens, Json.NeedValue{Json.Top{}}),
99 Json.token_list(Json.decode_tree(Json.lex_tree(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""} <> Nil{})), Nil{}),
100 Json.decode_lexeme(Json.Payload{"\"" ++ Json.escape_string(text) ++ "\""}) <> Nil{},
101 parallel_single("\"" ++ Json.escape_string(text) ++ "\"")),
102 assembled_string_payload(text)))
103
104def parse_leading_space(+text: String) -> {Json.parse(" " ++ text) == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
105 {==}
106
107def parse_trailing_space(+text: String) -> {Json.parse(text ++ " ") == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
108 Equal.cong(List<&2, Json.Lexeme>, ResultValue(),
109 items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
110 Json.lex_scan(text ++ " ", Json.Outside{}, SNil{}, Nil{}),
111 Json.lex_scan(text, Json.Outside{}, SNil{}, Nil{}),
112 LexWhitespaceProof.trailing_space(text, Json.Outside{}, SNil{}, Nil{}))
113
114def parse_trailing_tab(+text: String) -> {Json.parse(text ++ "\t") == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
115 Equal.cong(List<&2, Json.Lexeme>, ResultValue(),
116 items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
117 Json.lex_scan(text ++ "\t", Json.Outside{}, SNil{}, Nil{}),
118 Json.lex_scan(text, Json.Outside{}, SNil{}, Nil{}),
119 LexWhitespaceProof.trailing_tab(text, Json.Outside{}, SNil{}, Nil{}))
120
121def parse_trailing_return(+text: String) -> {Json.parse(text ++ "\r") == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
122 Equal.cong(List<&2, Json.Lexeme>, ResultValue(),
123 items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
124 Json.lex_scan(text ++ "\r", Json.Outside{}, SNil{}, Nil{}),
125 Json.lex_scan(text, Json.Outside{}, SNil{}, Nil{}),
126 LexWhitespaceProof.trailing_return(text, Json.Outside{}, SNil{}, Nil{}))
127
128def parse_trailing_newline(+text: String) -> {Json.parse(text ++ "\n") == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
129 Equal.cong(List<&2, Json.Lexeme>, ResultValue(),
130 items => Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
131 Json.lex_scan(text ++ "\n", Json.Outside{}, SNil{}, Nil{}),
132 Json.lex_scan(text, Json.Outside{}, SNil{}, Nil{}),
133 LexWhitespaceProof.trailing_newline(text, Json.Outside{}, SNil{}, Nil{}))
134
135def parse_suffix_space(+text: String,
136 +suffix: String) -> {Json.parse(text ++ (suffix ++ " ")) == Json.parse(text ++ suffix) : Result<&1, &1, Json.Error, Json.Value>}:
137 Equal.trans(ResultValue(), Json.parse(text ++ (suffix ++ " ")), Json.parse((text ++ suffix) ++ " "), Json.parse(text ++ suffix),
138 Equal.sym(ResultValue(), Json.parse((text ++ suffix) ++ " "), Json.parse(text ++ (suffix ++ " ")),
139 Equal.cong(String, ResultValue(), parse_for_equality, (text ++ suffix) ++ " ", text ++ (suffix ++ " "), StringProof.append_assoc(text, suffix, " "))),
140 parse_trailing_space(text ++ suffix))
141
142def parse_suffix_tab(+text: String,
143 +suffix: String) -> {Json.parse(text ++ (suffix ++ "\t")) == Json.parse(text ++ suffix) : Result<&1, &1, Json.Error, Json.Value>}:
144 Equal.trans(ResultValue(), Json.parse(text ++ (suffix ++ "\t")), Json.parse((text ++ suffix) ++ "\t"), Json.parse(text ++ suffix),
145 Equal.sym(ResultValue(), Json.parse((text ++ suffix) ++ "\t"), Json.parse(text ++ (suffix ++ "\t")),
146 Equal.cong(String, ResultValue(), parse_for_equality, (text ++ suffix) ++ "\t", text ++ (suffix ++ "\t"), StringProof.append_assoc(text, suffix, "\t"))),
147 parse_trailing_tab(text ++ suffix))
148
149def parse_suffix_return(+text: String,
150 +suffix: String) -> {Json.parse(text ++ (suffix ++ "\r")) == Json.parse(text ++ suffix) : Result<&1, &1, Json.Error, Json.Value>}:
151 Equal.trans(ResultValue(), Json.parse(text ++ (suffix ++ "\r")), Json.parse((text ++ suffix) ++ "\r"), Json.parse(text ++ suffix),
152 Equal.sym(ResultValue(), Json.parse((text ++ suffix) ++ "\r"), Json.parse(text ++ (suffix ++ "\r")),
153 Equal.cong(String, ResultValue(), parse_for_equality, (text ++ suffix) ++ "\r", text ++ (suffix ++ "\r"), StringProof.append_assoc(text, suffix, "\r"))),
154 parse_trailing_return(text ++ suffix))
155
156def parse_suffix_newline(+text: String,
157 +suffix: String) -> {Json.parse(text ++ (suffix ++ "\n")) == Json.parse(text ++ suffix) : Result<&1, &1, Json.Error, Json.Value>}:
158 Equal.trans(ResultValue(), Json.parse(text ++ (suffix ++ "\n")), Json.parse((text ++ suffix) ++ "\n"), Json.parse(text ++ suffix),
159 Equal.sym(ResultValue(), Json.parse((text ++ suffix) ++ "\n"), Json.parse(text ++ (suffix ++ "\n")),
160 Equal.cong(String, ResultValue(), parse_for_equality, (text ++ suffix) ++ "\n", text ++ (suffix ++ "\n"), StringProof.append_assoc(text, suffix, "\n"))),
161 parse_trailing_newline(text ++ suffix))
162
163def parse_leading_surround(+text: String) -> {Json.parse(" \n\t\r" ++ text) == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
164 {==}
165
166def parse_surrounding_space(+text: String) -> {Json.parse(" \n\t\r" ++ text ++ "\r\t\n ") == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}:
167 Equal.trans(ResultValue(), Json.parse(" \n\t\r" ++ text ++ "\r\t\n "), Json.parse(text ++ "\r\t\n "), Json.parse(text),
168 parse_leading_surround(text ++ "\r\t\n "),
169 Equal.trans(ResultValue(), Json.parse(text ++ "\r\t\n "), Json.parse(text ++ "\r\t\n"), Json.parse(text),
170 parse_suffix_space(text, "\r\t\n"),
171 Equal.trans(ResultValue(), Json.parse(text ++ "\r\t\n"), Json.parse(text ++ "\r\t"), Json.parse(text),
172 parse_suffix_newline(text, "\r\t"),
173 Equal.trans(ResultValue(), Json.parse(text ++ "\r\t"), Json.parse(text ++ "\r"), Json.parse(text),
174 parse_suffix_tab(text, "\r"), parse_trailing_return(text)))))
175
176def L.parses_null():
177 {==}
178
179def L.parses_true():
180 {==}
181
182def L.parses_false():
183 {==}
184
185def L.rejects_trailing_garbage():
186 {==}
187
188def L.rejects_second_value():
189 {==}
190
191def L.rejects_invalid_null():
192 {==}
193
194def L.rejects_invalid_true():
195 {==}
196
197def L.rejects_invalid_false():
198 {==}
199
200def L.rejects_empty_input():
201 {==}
202
203def L.rejects_whitespace_only():
204 {==}
205
206def L.parses_empty_string():
207 {==}
208
209def L.parses_simple_string():
210 {==}
211
212def L.parses_newline_escape():
213 {==}
214
215def L.parses_quote_escape():
216 {==}
217
218def L.parses_backslash_escape():
219 {==}
220
221def L.rejects_unterminated_string():
222 {==}
223
224def L.parses_empty_array():
225 {==}
226
227def L.parses_literal_array():
228 {==}
229
230def L.rejects_array_trailing_comma():
231 {==}
232
233def L.parses_empty_object():
234 {==}
235
236def L.rejects_unquoted_object_key():
237 {==}
238
239def L.rejects_object_trailing_comma():
240 {==}
241
242def L.parses_nested_containers():
243 {==}
244
245def L.rejects_non_json_whitespace():
246 {==}
247
248def L.rejects_raw_string_control():
249 {==}
250
251def L.parses_unicode_escape():
252 {==}
253
254def L.parses_unicode_surrogate_pair():
255 {==}
256
257def L.parses_fraction_and_exponent():
258 {==}
259
260def L.rejects_malformed_number_forms():
261 {==}
262
263def L.preserves_array_order():
264 {==}
265
266def L.preserves_object_order_and_duplicates():
267 {==}
268
269def L.gpu_single_matches_cpu(text):
270 {==}
271
272def L.preserves_number_lexeme():
273 {==}
274
275def L.gpu_batch_matches_cpu(batch):
276 {==}
277
278
279def L.stringify_parse_roundtrip(value):
280 +v = value
281 Equal.trans(ResultValue(), Json.parse(Json.stringify(v)),
282 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(Json.source(v, False{}, Nil{}))), Nil{}), Json.NeedValue{Json.Top{}}),
283 Done{v},
284 Equal.cong(List<&2, Json.Lexeme>, ResultValue(), items =>
285 Json.assemble(Json.token_list(Json.decode_tree(Json.lex_tree(items)), Nil{}), Json.NeedValue{Json.Top{}}),
286 Json.lex_scan(Json.stringify(v), Json.Outside{}, SNil{}, Nil{}),
287 Json.source(v, False{}, Nil{}), RenderLexProof.lex_source(v)),
288 assemble_source(v))
289
290def L.accepts_leading_space(value):
291 +v = value
292 Equal.trans(Result<&1, &1, Json.Error, Json.Value>, Json.parse(" " ++ Json.stringify(v)), Json.parse(Json.stringify(v)), Done{v}, parse_leading_space(Json.stringify(v)), L.stringify_parse_roundtrip(v))
293
294def L.accepts_trailing_space(value):
295 +v = value
296 Equal.trans(Result<&1, &1, Json.Error, Json.Value>, Json.parse(Json.stringify(v) ++ " "), Json.parse(Json.stringify(v)), Done{v}, parse_trailing_space(Json.stringify(v)), L.stringify_parse_roundtrip(v))
297
298def L.accepts_surrounding_space(value):
299 +v = value
300 Equal.trans(Result<&1, &1, Json.Error, Json.Value>, Json.parse(" \n\t\r" ++ Json.stringify(v) ++ "\r\t\n "), Json.parse(Json.stringify(v)), Done{v}, parse_surrounding_space(Json.stringify(v)), L.stringify_parse_roundtrip(v))
301
302
303def L.url_component_ascii():
304 {==}
305
306def L.url_component_reserved():
307 {==}
308
309def L.url_component_utf8():
310 {==}