1 import Base 2 import ./LAWS.bend as L 3 import ./libs/JSON.bend as Json 4 import ./libs/URL.bend as URL 5 import ./proof/JSON_StringProof.bend as StringProof 6 import ./proof/JSON_PrimitiveProof.bend as PrimitiveProof 7 import ./proof/JSON_NumberLexProof.bend as NumberLexProof 8 import ./proof/JSON_ParallelProof.bend as ParallelProof 9 import ./proof/JSON_LexWhitespaceProof.bend as LexWhitespaceProof 10 import ./proof/JSON_AssemblyProof.bend as AssemblyProof 11 import ./proof/JSON_SourceProof.bend as SourceProof 12 import ./proof/JSON_RenderLexProof.bend as RenderLexProof 13 14 def ResultValue() -> Type: 15 Result<&1, &1, Json.Error, Json.Value> 16 17 def parse_for_equality(text: String) -> ResultValue(): 18 Json.parse(text) 19 20 def 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 25 def 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}: 26 Equal.trans(List, 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 30 def 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, 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, 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, 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, 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 57 def parse_number_payload(+text: String, 58 +certificate: Json.NumberCert) -> {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, 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 82 def 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 86 def 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, 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 104 def parse_leading_space(+text: String) -> {Json.parse(" " ++ text) == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}: 105 {==} 106 107 def 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 114 def 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 121 def 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 128 def 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 135 def 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 142 def 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 149 def 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 156 def 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 163 def parse_leading_surround(+text: String) -> {Json.parse(" \n\t\r" ++ text) == Json.parse(text) : Result<&1, &1, Json.Error, Json.Value>}: 164 {==} 165 166 def 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 176 def L.parses_null(): 177 {==} 178 179 def L.parses_true(): 180 {==} 181 182 def L.parses_false(): 183 {==} 184 185 def L.rejects_trailing_garbage(): 186 {==} 187 188 def L.rejects_second_value(): 189 {==} 190 191 def L.rejects_invalid_null(): 192 {==} 193 194 def L.rejects_invalid_true(): 195 {==} 196 197 def L.rejects_invalid_false(): 198 {==} 199 200 def L.rejects_empty_input(): 201 {==} 202 203 def L.rejects_whitespace_only(): 204 {==} 205 206 def L.parses_empty_string(): 207 {==} 208 209 def L.parses_simple_string(): 210 {==} 211 212 def L.parses_newline_escape(): 213 {==} 214 215 def L.parses_quote_escape(): 216 {==} 217 218 def L.parses_backslash_escape(): 219 {==} 220 221 def L.rejects_unterminated_string(): 222 {==} 223 224 def L.parses_empty_array(): 225 {==} 226 227 def L.parses_literal_array(): 228 {==} 229 230 def L.rejects_array_trailing_comma(): 231 {==} 232 233 def L.parses_empty_object(): 234 {==} 235 236 def L.rejects_unquoted_object_key(): 237 {==} 238 239 def L.rejects_object_trailing_comma(): 240 {==} 241 242 def L.parses_nested_containers(): 243 {==} 244 245 def L.rejects_non_json_whitespace(): 246 {==} 247 248 def L.rejects_raw_string_control(): 249 {==} 250 251 def L.parses_unicode_escape(): 252 {==} 253 254 def L.parses_unicode_surrogate_pair(): 255 {==} 256 257 def L.parses_fraction_and_exponent(): 258 {==} 259 260 def L.rejects_malformed_number_forms(): 261 {==} 262 263 def L.preserves_array_order(): 264 {==} 265 266 def L.preserves_object_order_and_duplicates(): 267 {==} 268 269 def L.gpu_single_matches_cpu(text): 270 {==} 271 272 def L.preserves_number_lexeme(): 273 {==} 274 275 def L.gpu_batch_matches_cpu(batch): 276 {==} 277 278 279 def 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 290 def 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 294 def 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 298 def 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 303 def L.url_component_ascii(): 304 {==} 305 306 def L.url_component_reserved(): 307 {==} 308 309 def L.url_component_utf8(): 310 {==}