1 import Base 2 import ../libs/JSON.bend as J 3 import ./JSON_AssemblyProof.bend as A 4 import ./JSON_PrimitiveProof.bend as P 5 import ./JSON_StringProof.bend as S 6 import ./JSON_ParallelProof.bend as Par 7 import ./JSON_NumberLexProof.bend as Num 8 import ./JSON_LexWhitespaceProof.bend as W 9 import ./JSON_ListProof.bend as LP 10 11 def token_source(xs: List<&2, J.Lexeme>, tail: List) -> List: 12 match xs: 13 case Nil{}: tail 14 case h <> t: J.decode_lexeme(h) <> token_source(t, tail) 15 16 def token_source_flat(+xs: List<&2, J.Lexeme>, 17 -tail: List) -> {token_source(xs, tail) == Par.flat(xs, tail) : List}: 18 match xs: 19 case Nil{}: {==} 20 case head <> rest: 21 Equal.cong(List, List, tokens => J.decode_lexeme(head) <> tokens, 22 token_source(rest, tail), Par.flat(rest, tail), token_source_flat(rest, tail)) 23 24 def is_members(mode: A.Mode) -> Bool: 25 match mode: 26 case A.Whole{}: False{} 27 case A.Members{}: True{} 28 29 def token_string(text: String) -> J.Token: 30 J.Atom{Done{J.Str{text}}} 31 32 def nested_render_append(+outer: J.Value, 33 +inner: J.Value, 34 +inner_members: Bool, 35 +prefix: String, 36 +suffix: String, 37 +outer_append: {J.render(outer, False{}, J.render(inner, inner_members, prefix)) ++ suffix == J.render(outer, False{}, J.render(inner, inner_members, prefix) ++ suffix) : String}, 38 +inner_append: {J.render(inner, inner_members, prefix) ++ suffix == J.render(inner, inner_members, prefix ++ suffix) : String}) -> {J.render(outer, False{}, J.render(inner, inner_members, prefix)) ++ suffix == J.render(outer, False{}, J.render(inner, inner_members, prefix ++ suffix)) : String}: 39 Equal.trans(String, 40 J.render(outer, False{}, J.render(inner, inner_members, prefix)) ++ suffix, 41 J.render(outer, False{}, J.render(inner, inner_members, prefix) ++ suffix), 42 J.render(outer, False{}, J.render(inner, inner_members, prefix ++ suffix)), 43 outer_append, 44 Equal.cong(String, String, text => J.render(outer, False{}, text), 45 J.render(inner, inner_members, prefix) ++ suffix, 46 J.render(inner, inner_members, prefix ++ suffix), 47 inner_append)) 48 49 50 def render_object_field_append(+prefix: String, 51 +key: String, 52 +text: String, 53 +suffix: String) -> {J.render_object_field(prefix, key, text) ++ suffix == J.render_object_field(prefix, key, text ++ suffix) : String}: 54 S.append_assoc(prefix ++ ("\"" ++ J.escape_string(key) ++ "\":"), text, suffix) 55 56 def render_append(+value: J.Value, 57 +members: Bool, 58 +prefix: String, 59 +suffix: String) -> {J.render(value, members, prefix) ++ suffix == J.render(value, members, prefix ++ suffix) : String}: 60 match value: 61 case J.Null{}: S.append_assoc("null", prefix, suffix) 62 case J.Bool{truth}: 63 match truth: 64 case True{}: S.append_assoc("true", prefix, suffix) 65 case False{}: S.append_assoc("false", prefix, suffix) 66 case J.Number{lexeme, certificate}: S.append_assoc(lexeme, prefix, suffix) 67 case J.Str{text}: 68 Equal.cong(String, String, rest => SCon{'"', rest}, 69 (J.escape_string(text) ++ (SCon{'"', SNil{}} ++ prefix)) ++ suffix, 70 J.escape_string(text) ++ (SCon{'"', SNil{}} ++ (prefix ++ suffix)), 71 Equal.trans(String, 72 (J.escape_string(text) ++ (SCon{'"', SNil{}} ++ prefix)) ++ suffix, 73 J.escape_string(text) ++ ((SCon{'"', SNil{}} ++ prefix) ++ suffix), 74 J.escape_string(text) ++ (SCon{'"', SNil{}} ++ (prefix ++ suffix)), 75 S.append_assoc(J.escape_string(text), SCon{'"', SNil{}} ++ prefix, suffix), 76 Equal.cong(String, String, value => J.escape_string(text) ++ value, 77 (SCon{'"', SNil{}} ++ prefix) ++ suffix, 78 SCon{'"', SNil{}} ++ (prefix ++ suffix), 79 S.append_assoc(SCon{'"', SNil{}}, prefix, suffix)))) 80 case J.Arr{Nil{}}: 81 match members: 82 case False{}: S.append_assoc("[]", prefix, suffix) 83 case True{}: S.append_assoc("]", prefix, suffix) 84 case J.Arr{head <> tail}: 85 match members: 86 case False{}: 87 Equal.trans(String, ("[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix))) ++ suffix, 88 "[" ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix), 89 "[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)), 90 S.append_assoc("[", J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)), suffix), 91 Equal.trans(String, "[" ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix), 92 "[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix), 93 "[" ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)), 94 Equal.cong(String, String, text => "[" ++ text, 95 J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix, 96 J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix), 97 render_append(head, False{}, J.render(J.Arr{tail}, True{}, prefix), suffix)), 98 Equal.cong(String, String, text => "[" ++ J.render(head, False{}, text), 99 J.render(J.Arr{tail}, True{}, prefix) ++ suffix, 100 J.render(J.Arr{tail}, True{}, prefix ++ suffix), 101 render_append(J.Arr{tail}, True{}, prefix, suffix)))) 102 case True{}: 103 Equal.trans(String, ("," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix))) ++ suffix, 104 "," ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix), 105 "," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)), 106 S.append_assoc(",", J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)), suffix), 107 Equal.trans(String, "," ++ (J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix), 108 "," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix), 109 "," ++ J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix ++ suffix)), 110 Equal.cong(String, String, text => "," ++ text, 111 J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix)) ++ suffix, 112 J.render(head, False{}, J.render(J.Arr{tail}, True{}, prefix) ++ suffix), 113 render_append(head, False{}, J.render(J.Arr{tail}, True{}, prefix), suffix)), 114 Equal.cong(String, String, text => "," ++ J.render(head, False{}, text), 115 J.render(J.Arr{tail}, True{}, prefix) ++ suffix, 116 J.render(J.Arr{tail}, True{}, prefix ++ suffix), 117 render_append(J.Arr{tail}, True{}, prefix, suffix)))) 118 case J.Obj{Nil{}}: 119 match members: 120 case False{}: S.append_assoc("{}", prefix, suffix) 121 case True{}: S.append_assoc("}", prefix, suffix) 122 case J.Obj{(key, field_value) <> tail}: 123 match members: 124 case False{}: 125 Equal.trans(String, 126 J.render_object_field("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix))) ++ suffix, 127 J.render_object_field("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix), 128 J.render_object_field("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix))), 129 render_object_field_append("{", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)), suffix), 130 Equal.cong(String, String, text => J.render_object_field("{", key, text), 131 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix, 132 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix)), 133 nested_render_append(field_value, J.Obj{tail}, True{}, prefix, suffix, 134 render_append(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix), suffix), 135 render_append(J.Obj{tail}, True{}, prefix, suffix)))) 136 case True{}: 137 Equal.trans(String, 138 J.render_object_field(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix))) ++ suffix, 139 J.render_object_field(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix), 140 J.render_object_field(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix))), 141 render_object_field_append(",", key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)), suffix), 142 Equal.cong(String, String, text => J.render_object_field(",", key, text), 143 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix, 144 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix)), 145 nested_render_append(field_value, J.Obj{tail}, True{}, prefix, suffix, 146 render_append(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix), suffix), 147 render_append(J.Obj{tail}, True{}, prefix, suffix)))) 148 149 def render_array_singleton_suffix(+head: J.Value, 150 +suffix: String) -> {J.render(J.Arr{head <> Nil{}}, False{}, suffix) == "[" ++ (J.render(head, False{}, SNil{}) ++ ("]" ++ suffix)) : String}: 151 Equal.cong(String, String, text => "[" ++ text, 152 J.render(head, False{}, J.render(J.Arr{Nil{}}, True{}, suffix)), 153 J.render(head, False{}, SNil{}) ++ ("]" ++ suffix), 154 Equal.trans(String, 155 J.render(head, False{}, J.render(J.Arr{Nil{}}, True{}, suffix)), 156 J.render(head, False{}, "]") ++ suffix, 157 J.render(head, False{}, SNil{}) ++ ("]" ++ suffix), 158 Equal.sym(String, J.render(head, False{}, "]") ++ suffix, 159 J.render(head, False{}, J.render(J.Arr{Nil{}}, True{}, suffix)), 160 nested_render_append(head, J.Arr{Nil{}}, True{}, SNil{}, suffix, 161 render_append(head, False{}, "]", suffix), 162 render_append(J.Arr{Nil{}}, True{}, SNil{}, suffix))), 163 Equal.trans(String, 164 J.render(head, False{}, "]") ++ suffix, 165 (J.render(head, False{}, SNil{}) ++ "]") ++ suffix, 166 J.render(head, False{}, SNil{}) ++ ("]" ++ suffix), 167 Equal.cong(String, String, text => text ++ suffix, 168 J.render(head, False{}, "]"), J.render(head, False{}, SNil{}) ++ "]", 169 Equal.sym(String, J.render(head, False{}, SNil{}) ++ "]", 170 J.render(head, False{}, "]"), render_append(head, False{}, SNil{}, "]"))), 171 S.append_assoc(J.render(head, False{}, SNil{}), "]", suffix)))) 172 173 def lex_source_number_before_punctuation(+text: String, 174 +certificate: J.NumberCert, 175 +punctuation: Char, 176 +suffix: String, 177 +acc: List<&2, J.Lexeme>, 178 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Number{text, certificate}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{text} <> acc) : List<&2, J.Lexeme>}: 179 Equal.trans(List<&2, J.Lexeme>, 180 J.lex_scan(J.render(J.Number{text, certificate}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 181 J.lex_scan(text ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 182 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{text} <> acc), 183 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 184 J.render(J.Number{text, certificate}, False{}, SNil{}), text, 185 S.append_nil(text)), 186 Num.lex_certified_number_before_punctuation(text, certificate, punctuation, suffix, acc, action)) 187 188 189 type AtomicValue is Data: 190 AtomicNull{} 191 AtomicTrue{} 192 AtomicFalse{} 193 AtomicNumber{text: String, certificate: J.NumberCert} 194 AtomicString{text: String} 195 196 type SimpleValue is Data: 197 SimpleAtom{atom: AtomicValue} 198 SimpleEmptyArray{} 199 SimpleEmptyObject{} 200 201 def atomic_value(atom: AtomicValue) -> J.Value: 202 match atom: 203 case AtomicNull{}: J.Null{} 204 case AtomicTrue{}: J.Bool{True{}} 205 case AtomicFalse{}: J.Bool{False{}} 206 case AtomicNumber{text, certificate}: J.Number{text, certificate} 207 case AtomicString{text}: J.Str{text} 208 209 def simple_value(simple: SimpleValue) -> J.Value: 210 match simple: 211 case SimpleAtom{atom}: atomic_value(atom) 212 case SimpleEmptyArray{}: J.Arr{Nil{}} 213 case SimpleEmptyObject{}: J.Obj{Nil{}} 214 215 type RenderMode is Data: 216 RenderWhole{} 217 RenderMembers{} 218 RenderAfterSeparator{} 219 220 type JsonPunctuation is Data: 221 ArrayEnd{} 222 ObjectEnd{} 223 MemberComma{} 224 KeyColon{} 225 226 def punctuation_char(mark: JsonPunctuation) -> Char: 227 match mark: 228 case ArrayEnd{}: ']' 229 case ObjectEnd{}: '}' 230 case MemberComma{}: ',' 231 case KeyColon{}: ':' 232 233 def punctuation_action(mark: JsonPunctuation, 234 suffix: String) -> {J.lex_seed_action(SCon{punctuation_char(mark), suffix}, J.Outside{}) == J.LexPunctuation{punctuation_char(mark)} : J.LexAction}: 235 match mark: 236 case ArrayEnd{}: {==} 237 case ObjectEnd{}: {==} 238 case MemberComma{}: {==} 239 case KeyColon{}: {==} 240 241 def render_after_separator(value: J.Value, suffix: String) -> String: 242 match value: 243 case J.Arr{Nil{}}: "]" ++ suffix 244 case J.Arr{head <> tail}: J.render(head, False{}, J.render(J.Arr{tail}, True{}, suffix)) 245 case J.Obj{Nil{}}: "}" ++ suffix 246 case J.Obj{(key, field_value) <> tail}: 247 J.render_object_field(SNil{}, key, J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, suffix))) 248 case _: J.render(value, False{}, suffix) 249 250 def render_task(value: J.Value, mode: RenderMode, suffix: String) -> String: 251 match mode: 252 case RenderWhole{}: J.render(value, False{}, suffix) 253 case RenderMembers{}: J.render(value, True{}, suffix) 254 case RenderAfterSeparator{}: render_after_separator(value, suffix) 255 256 def source_after_separator(value: J.Value, suffix: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>: 257 match value: 258 case J.Arr{Nil{}}: J.Punctuation{']'} <> suffix 259 case J.Arr{head <> tail}: J.source(head, False{}, J.source(J.Arr{tail}, True{}, suffix)) 260 case J.Obj{Nil{}}: J.Punctuation{'}'} <> suffix 261 case J.Obj{(key, field_value) <> tail}: 262 J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, suffix))) 263 case _: J.source(value, False{}, suffix) 264 265 def source_task(value: J.Value, mode: RenderMode, suffix: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>: 266 match mode: 267 case RenderWhole{}: J.source(value, False{}, suffix) 268 case RenderMembers{}: J.source(value, True{}, suffix) 269 case RenderAfterSeparator{}: source_after_separator(value, suffix) 270 271 def reverse_source_task(value: J.Value, mode: RenderMode) -> List<&2, J.Lexeme>: 272 List.reverse(&2, J.Lexeme, source_task(value, mode, Nil{})) 273 274 def source_text_append(+text: String, 275 +first: List<&2, J.Lexeme>, 276 +second: List<&2, J.Lexeme>) -> {J.source_text(text, List.append(&2, J.Lexeme, first, second)) == List.append(&2, J.Lexeme, J.source_text(text, first), second) : List<&2, J.Lexeme>}: 277 {==} 278 279 def source_append(+value: J.Value, 280 +members: Bool, 281 +first: List<&2, J.Lexeme>, 282 +second: List<&2, J.Lexeme>) -> {J.source(value, members, List.append(&2, J.Lexeme, first, second)) == List.append(&2, J.Lexeme, J.source(value, members, first), second) : List<&2, J.Lexeme>}: 283 match value: 284 case J.Null{}: source_text_append("null", first, second) 285 case J.Bool{truth}: 286 match truth: 287 case True{}: source_text_append("true", first, second) 288 case False{}: source_text_append("false", first, second) 289 case J.Number{lexeme, certificate}: source_text_append(lexeme, first, second) 290 case J.Str{text}: source_text_append("\"" ++ J.escape_string(text) ++ "\"", first, second) 291 case J.Arr{Nil{}}: 292 match members: 293 case False{}: {==} 294 case True{}: {==} 295 case J.Arr{head <> tail}: 296 match members: 297 case False{}: 298 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{'['} <> xs, 299 J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))), 300 List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second), 301 Equal.trans(List<&2, J.Lexeme>, 302 J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))), 303 J.source(head, False{}, List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second)), 304 List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second), 305 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(head, False{}, xs), 306 J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second)), 307 List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second), 308 source_append(J.Arr{tail}, True{}, first, second)), 309 source_append(head, False{}, J.source(J.Arr{tail}, True{}, first), second))) 310 case True{}: 311 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{','} <> xs, 312 J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))), 313 List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second), 314 Equal.trans(List<&2, J.Lexeme>, 315 J.source(head, False{}, J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second))), 316 J.source(head, False{}, List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second)), 317 List.append(&2, J.Lexeme, J.source(head, False{}, J.source(J.Arr{tail}, True{}, first)), second), 318 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(head, False{}, xs), 319 J.source(J.Arr{tail}, True{}, List.append(&2, J.Lexeme, first, second)), 320 List.append(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, first), second), 321 source_append(J.Arr{tail}, True{}, first, second)), 322 source_append(head, False{}, J.source(J.Arr{tail}, True{}, first), second))) 323 case J.Obj{Nil{}}: 324 match members: 325 case False{}: {==} 326 case True{}: {==} 327 case J.Obj{(key, field_value) <> tail}: 328 match members: 329 case False{}: 330 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{'{'} <> xs, 331 J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)))), 332 List.append(&2, J.Lexeme, J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first))), second), 333 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> xs), 334 J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))), 335 List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second), 336 Equal.trans(List<&2, J.Lexeme>, 337 J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))), 338 J.source(field_value, False{}, List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second)), 339 List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second), 340 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(field_value, False{}, xs), 341 J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)), 342 List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second), 343 source_append(J.Obj{tail}, True{}, first, second)), 344 source_append(field_value, False{}, J.source(J.Obj{tail}, True{}, first), second)))) 345 case True{}: 346 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.Punctuation{','} <> xs, 347 J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)))), 348 List.append(&2, J.Lexeme, J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first))), second), 349 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source_text("\"" ++ J.escape_string(key) ++ "\"", J.Punctuation{':'} <> xs), 350 J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))), 351 List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second), 352 Equal.trans(List<&2, J.Lexeme>, 353 J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second))), 354 J.source(field_value, False{}, List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second)), 355 List.append(&2, J.Lexeme, J.source(field_value, False{}, J.source(J.Obj{tail}, True{}, first)), second), 356 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => J.source(field_value, False{}, xs), 357 J.source(J.Obj{tail}, True{}, List.append(&2, J.Lexeme, first, second)), 358 List.append(&2, J.Lexeme, J.source(J.Obj{tail}, True{}, first), second), 359 source_append(J.Obj{tail}, True{}, first, second)), 360 source_append(field_value, False{}, J.source(J.Obj{tail}, True{}, first), second)))) 361 362 def reverse_source_suffix(+value: J.Value, 363 +members: Bool, 364 +suffix: List<&2, J.Lexeme>) -> {List.reverse(&2, J.Lexeme, J.source(value, members, suffix)) == List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, suffix), List.reverse(&2, J.Lexeme, J.source(value, members, Nil{}))) : List<&2, J.Lexeme>}: 365 Equal.trans(List<&2, J.Lexeme>, 366 List.reverse(&2, J.Lexeme, J.source(value, members, suffix)), 367 List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme, J.source(value, members, Nil{}), suffix)), 368 List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, suffix), 369 List.reverse(&2, J.Lexeme, J.source(value, members, Nil{}))), 370 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items), 371 J.source(value, members, suffix), 372 List.append(&2, J.Lexeme, J.source(value, members, Nil{}), suffix), 373 source_append(value, members, Nil{}, suffix)), 374 LP.reverse_append(J.Lexeme, J.source(value, members, Nil{}), suffix)) 375 376 def reverse_source_text(+text: String, 377 +suffix: List<&2, J.Lexeme>) -> {List.reverse(&2, J.Lexeme, J.source_text(text, suffix)) == List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, suffix), J.Payload{text} <> Nil{}) : List<&2, J.Lexeme>}: 378 LP.reverse_cons(J.Lexeme, J.Payload{text}, suffix) 379 380 def reverse_source_colon_value_tail(+value: J.Value, 381 +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> {List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))) == List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})) : List<&2, J.Lexeme>}: 382 Equal.trans(List<&2, J.Lexeme>, 383 List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))), 384 List.append(&2, J.Lexeme, 385 List.reverse(&2, J.Lexeme, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))), 386 J.Punctuation{':'} <> Nil{}), 387 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), 388 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})), 389 LP.reverse_cons(J.Lexeme, J.Punctuation{':'}, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))), 390 Equal.trans(List<&2, J.Lexeme>, 391 List.append(&2, J.Lexeme, 392 List.reverse(&2, J.Lexeme, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))), 393 J.Punctuation{':'} <> Nil{}), 394 List.append(&2, J.Lexeme, 395 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), reverse_source_task(value, RenderWhole{})), 396 J.Punctuation{':'} <> Nil{}), 397 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), 398 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})), 399 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => 400 List.append(&2, J.Lexeme, xs, J.Punctuation{':'} <> Nil{}), 401 List.reverse(&2, J.Lexeme, J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))), 402 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), reverse_source_task(value, RenderWhole{})), 403 reverse_source_suffix(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))), 404 LP.append_assoc(J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), 405 reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}))) 406 407 def reverse_source_object_after_separator(+key: String, 408 +value: J.Value, 409 +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> {reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})) : List<&2, J.Lexeme>}: 410 Equal.trans(List<&2, J.Lexeme>, 411 reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}), 412 List.append(&2, J.Lexeme, 413 List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))), 414 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}), 415 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), 416 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), 417 J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})), 418 reverse_source_text("\"" ++ J.escape_string(key) ++ "\"", 419 J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))), 420 Equal.trans(List<&2, J.Lexeme>, 421 List.append(&2, J.Lexeme, 422 List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))), 423 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}), 424 List.append(&2, J.Lexeme, 425 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), 426 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})), 427 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}), 428 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), 429 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), 430 J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})), 431 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => 432 List.append(&2, J.Lexeme, xs, J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}), 433 List.reverse(&2, J.Lexeme, J.Punctuation{':'} <> J.source(value, False{}, J.source(J.Obj{tail}, True{}, Nil{}))), 434 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), 435 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})), 436 reverse_source_colon_value_tail(value, tail)), 437 Equal.trans(List<&2, J.Lexeme>, 438 List.append(&2, J.Lexeme, 439 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), 440 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{})), 441 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}), 442 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), 443 List.append(&2, J.Lexeme, 444 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}), 445 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})), 446 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), 447 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), 448 J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})), 449 LP.append_assoc(J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), 450 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}), 451 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}), 452 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => 453 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{tail}, RenderMembers{}), xs), 454 List.append(&2, J.Lexeme, 455 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}), 456 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}), 457 List.append(&2, J.Lexeme, reverse_source_task(value, RenderWhole{}), 458 List.append(&2, J.Lexeme, J.Punctuation{':'} <> Nil{}, J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{})), 459 LP.append_assoc(J.Lexeme, reverse_source_task(value, RenderWhole{}), J.Punctuation{':'} <> Nil{}, 460 J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> Nil{}))))) 461 462 def reverse_source_object_members_after_separator(+key: String, 463 +value: J.Value, 464 +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> {reverse_source_task(J.Obj{(key, value) <> tail}, RenderMembers{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}) : List<&2, J.Lexeme>}: 465 Equal.trans(List<&2, J.Lexeme>, 466 reverse_source_task(J.Obj{(key, value) <> tail}, RenderMembers{}), 467 List.reverse(&2, J.Lexeme, J.Punctuation{','} <> source_after_separator(J.Obj{(key, value) <> tail}, Nil{})), 468 List.append(&2, J.Lexeme, reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}), 469 J.Punctuation{','} <> Nil{}), 470 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items), 471 J.source(J.Obj{(key, value) <> tail}, True{}, Nil{}), 472 J.Punctuation{','} <> source_after_separator(J.Obj{(key, value) <> tail}, Nil{}), 473 {==}), 474 LP.reverse_cons(J.Lexeme, J.Punctuation{','}, source_after_separator(J.Obj{(key, value) <> tail}, Nil{}))) 475 476 def reverse_source_array_whole(+head: J.Value, 477 +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderWhole{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})) : List<&2, J.Lexeme>}: 478 Equal.trans(List<&2, J.Lexeme>, 479 reverse_source_task(J.Arr{head <> tail}, RenderWhole{}), 480 List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme, 481 J.Punctuation{'['} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{}))), 482 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), 483 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})), 484 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items), 485 J.source(J.Arr{head <> tail}, False{}, Nil{}), 486 List.append(&2, J.Lexeme, J.Punctuation{'['} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})), 487 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.Punctuation{'['} <> items, 488 J.source(head, False{}, J.source(J.Arr{tail}, True{}, Nil{})), 489 List.append(&2, J.Lexeme, J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})), 490 source_append(head, False{}, Nil{}, J.source(J.Arr{tail}, True{}, Nil{})))), 491 Equal.trans(List<&2, J.Lexeme>, 492 List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme, 493 J.Punctuation{'['} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{}))), 494 List.append(&2, J.Lexeme, 495 List.reverse(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, Nil{})), 496 List.reverse(&2, J.Lexeme, J.Punctuation{'['} <> J.source(head, False{}, Nil{}))), 497 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), 498 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})), 499 LP.reverse_append(J.Lexeme, J.Punctuation{'['} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})), 500 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), items), 501 List.reverse(&2, J.Lexeme, J.Punctuation{'['} <> J.source(head, False{}, Nil{})), 502 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{}), 503 LP.reverse_cons(J.Lexeme, J.Punctuation{'['}, J.source(head, False{}, Nil{}))))) 504 505 def reverse_source_array_members(+head: J.Value, 506 +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderMembers{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{','} <> Nil{})) : List<&2, J.Lexeme>}: 507 Equal.trans(List<&2, J.Lexeme>, 508 reverse_source_task(J.Arr{head <> tail}, RenderMembers{}), 509 List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme, 510 J.Punctuation{','} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{}))), 511 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), 512 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{','} <> Nil{})), 513 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items), 514 J.source(J.Arr{head <> tail}, True{}, Nil{}), 515 List.append(&2, J.Lexeme, J.Punctuation{','} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})), 516 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.Punctuation{','} <> items, 517 J.source(head, False{}, J.source(J.Arr{tail}, True{}, Nil{})), 518 List.append(&2, J.Lexeme, J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})), 519 source_append(head, False{}, Nil{}, J.source(J.Arr{tail}, True{}, Nil{})))), 520 Equal.trans(List<&2, J.Lexeme>, 521 List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme, 522 J.Punctuation{','} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{}))), 523 List.append(&2, J.Lexeme, 524 List.reverse(&2, J.Lexeme, J.source(J.Arr{tail}, True{}, Nil{})), 525 List.reverse(&2, J.Lexeme, J.Punctuation{','} <> J.source(head, False{}, Nil{}))), 526 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), 527 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{','} <> Nil{})), 528 LP.reverse_append(J.Lexeme, J.Punctuation{','} <> J.source(head, False{}, Nil{}), J.source(J.Arr{tail}, True{}, Nil{})), 529 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), items), 530 List.reverse(&2, J.Lexeme, J.Punctuation{','} <> J.source(head, False{}, Nil{})), 531 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{','} <> Nil{}), 532 LP.reverse_cons(J.Lexeme, J.Punctuation{','}, J.source(head, False{}, Nil{}))))) 533 534 def reverse_source_array_after_separator(+head: J.Value, 535 +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})) : List<&2, J.Lexeme>}: 536 reverse_source_suffix(head, False{}, J.source(J.Arr{tail}, True{}, Nil{})) 537 538 def reverse_source_array_after_separator_whole(+head: J.Value, 539 +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderWhole{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}) : List<&2, J.Lexeme>}: 540 Equal.trans(List<&2, J.Lexeme>, 541 reverse_source_task(J.Arr{head <> tail}, RenderWhole{}), 542 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), 543 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})), 544 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}), 545 reverse_source_array_whole(head, tail), 546 Equal.trans(List<&2, J.Lexeme>, 547 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), 548 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})), 549 List.append(&2, J.Lexeme, 550 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})), 551 J.Punctuation{'['} <> Nil{}), 552 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}), 553 Equal.sym(List<&2, J.Lexeme>, 554 List.append(&2, J.Lexeme, 555 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})), 556 J.Punctuation{'['} <> Nil{}), 557 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), 558 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})), 559 LP.append_assoc(J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), 560 reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> Nil{})), 561 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => 562 List.append(&2, J.Lexeme, items, J.Punctuation{'['} <> Nil{}), 563 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})), 564 reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), 565 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), 566 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})), 567 reverse_source_array_after_separator(head, tail))))) 568 569 def reverse_source_array_members_after_separator(+head: J.Value, 570 +tail: List<&2, J.Value>) -> {reverse_source_task(J.Arr{head <> tail}, RenderMembers{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}) : List<&2, J.Lexeme>}: 571 Equal.trans(List<&2, J.Lexeme>, 572 reverse_source_task(J.Arr{head <> tail}, RenderMembers{}), 573 List.reverse(&2, J.Lexeme, J.Punctuation{','} <> source_after_separator(J.Arr{head <> tail}, Nil{})), 574 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> tail}, RenderAfterSeparator{}), 575 J.Punctuation{','} <> Nil{}), 576 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items), 577 J.source(J.Arr{head <> tail}, True{}, Nil{}), 578 J.Punctuation{','} <> source_after_separator(J.Arr{head <> tail}, Nil{}), 579 {==}), 580 LP.reverse_cons(J.Lexeme, J.Punctuation{','}, source_after_separator(J.Arr{head <> tail}, Nil{}))) 581 582 def source_separator(value: J.Value) -> List<&2, J.Lexeme>: 583 match value: 584 case J.Arr{Nil{}}: Nil{} 585 case J.Arr{_ <> _}: J.Punctuation{','} <> Nil{} 586 case J.Obj{Nil{}}: Nil{} 587 case J.Obj{_ <> _}: J.Punctuation{','} <> Nil{} 588 case _: Nil{} 589 590 def separator_text(value: J.Value) -> String: 591 match value: 592 case J.Arr{Nil{}}: SNil{} 593 case J.Arr{_ <> _}: "," 594 case J.Obj{Nil{}}: SNil{} 595 case J.Obj{_ <> _}: "," 596 case _: SNil{} 597 598 def render_members_decompose(+value: J.Value, 599 +suffix: String) -> {J.render(value, True{}, suffix) == separator_text(value) ++ render_after_separator(value, suffix) : String}: 600 match value: 601 case J.Null{}: {==} 602 case J.Bool{truth}: 603 match truth: 604 case True{}: {==} 605 case False{}: {==} 606 case J.Number{lexeme, certificate}: {==} 607 case J.Str{text}: {==} 608 case J.Arr{Nil{}}: {==} 609 case J.Arr{head <> tail}: {==} 610 case J.Obj{Nil{}}: {==} 611 case J.Obj{(key, field_value) <> tail}: {==} 612 613 def render_after_separator_array_decompose(+head: J.Value, 614 +tail: List<&2, J.Value>, 615 +suffix: String) -> {render_after_separator(J.Arr{head <> tail}, suffix) == J.render(head, False{}, SNil{}) ++ (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix)) : String}: 616 Equal.trans(String, 617 render_after_separator(J.Arr{head <> tail}, suffix), 618 J.render(head, False{}, SNil{}) ++ J.render(J.Arr{tail}, True{}, suffix), 619 J.render(head, False{}, SNil{}) ++ 620 (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix)), 621 Equal.sym(String, 622 J.render(head, False{}, SNil{}) ++ J.render(J.Arr{tail}, True{}, suffix), 623 render_after_separator(J.Arr{head <> tail}, suffix), 624 render_append(head, False{}, SNil{}, J.render(J.Arr{tail}, True{}, suffix))), 625 Equal.cong(String, String, text => J.render(head, False{}, SNil{}) ++ text, 626 J.render(J.Arr{tail}, True{}, suffix), 627 separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix), 628 render_members_decompose(J.Arr{tail}, suffix))) 629 630 def render_after_separator_object_decompose(+key: String, 631 +value: J.Value, 632 +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>, +suffix: String) -> {render_after_separator(J.Obj{(key, value) <> tail}, suffix) == J.render_object_field(SNil{}, key, J.render(value, False{}, SNil{}) ++ (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix))) : String}: 633 Equal.cong(String, String, text => J.render_object_field(SNil{}, key, text), 634 J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)), 635 J.render(value, False{}, SNil{}) ++ 636 (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)), 637 Equal.trans(String, 638 J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)), 639 J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix), 640 J.render(value, False{}, SNil{}) ++ 641 (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)), 642 Equal.sym(String, 643 J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix), 644 J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)), 645 render_append(value, False{}, SNil{}, J.render(J.Obj{tail}, True{}, suffix))), 646 Equal.cong(String, String, text => J.render(value, False{}, SNil{}) ++ text, 647 J.render(J.Obj{tail}, True{}, suffix), 648 separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix), 649 render_members_decompose(J.Obj{tail}, suffix)))) 650 651 def render_object_whole_decompose(+key: String, 652 +value: J.Value, 653 +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>, +suffix: String) -> {J.render(J.Obj{(key, value) <> tail}, False{}, suffix) == J.render_object_field("{", key, J.render(value, False{}, SNil{}) ++ (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix))) : String}: 654 Equal.cong(String, String, text => J.render_object_field("{", key, text), 655 J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)), 656 J.render(value, False{}, SNil{}) ++ 657 (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)), 658 Equal.trans(String, 659 J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)), 660 J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix), 661 J.render(value, False{}, SNil{}) ++ 662 (separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix)), 663 Equal.sym(String, 664 J.render(value, False{}, SNil{}) ++ J.render(J.Obj{tail}, True{}, suffix), 665 J.render(value, False{}, J.render(J.Obj{tail}, True{}, suffix)), 666 render_append(value, False{}, SNil{}, J.render(J.Obj{tail}, True{}, suffix))), 667 Equal.cong(String, String, text => J.render(value, False{}, SNil{}) ++ text, 668 J.render(J.Obj{tail}, True{}, suffix), 669 separator_text(J.Obj{tail}) ++ render_after_separator(J.Obj{tail}, suffix), 670 render_members_decompose(J.Obj{tail}, suffix)))) 671 672 def render_array_whole_decompose(+head: J.Value, 673 +tail: List<&2, J.Value>, 674 +suffix: String) -> {J.render(J.Arr{head <> tail}, False{}, suffix) == "[" ++ (J.render(head, False{}, SNil{}) ++ (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix))) : String}: 675 Equal.cong(String, String, text => "[" ++ text, 676 render_after_separator(J.Arr{head <> tail}, suffix), 677 J.render(head, False{}, SNil{}) ++ 678 (separator_text(J.Arr{tail}) ++ render_after_separator(J.Arr{tail}, suffix)), 679 render_after_separator_array_decompose(head, tail, suffix)) 680 681 def render_after_separator_append(+value: J.Value, 682 +prefix: String, 683 +suffix: String) -> {render_after_separator(value, prefix) ++ suffix == render_after_separator(value, prefix ++ suffix) : String}: 684 match value: 685 case J.Arr{Nil{}}: S.append_assoc("]", prefix, suffix) 686 case J.Arr{head <> tail}: 687 nested_render_append(head, J.Arr{tail}, True{}, prefix, suffix, 688 render_append(head, False{}, J.render(J.Arr{tail}, True{}, prefix), suffix), 689 render_append(J.Arr{tail}, True{}, prefix, suffix)) 690 case J.Obj{Nil{}}: S.append_assoc("}", prefix, suffix) 691 case J.Obj{(key, field_value) <> tail}: 692 Equal.trans(String, 693 render_after_separator(J.Obj{(key, field_value) <> tail}, prefix) ++ suffix, 694 J.render_object_field(SNil{}, key, 695 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix), 696 render_after_separator(J.Obj{(key, field_value) <> tail}, prefix ++ suffix), 697 render_object_field_append(SNil{}, key, 698 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)), suffix), 699 Equal.cong(String, String, text => J.render_object_field(SNil{}, key, text), 700 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix)) ++ suffix, 701 J.render(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix ++ suffix)), 702 nested_render_append(field_value, J.Obj{tail}, True{}, prefix, suffix, 703 render_append(field_value, False{}, J.render(J.Obj{tail}, True{}, prefix), suffix), 704 render_append(J.Obj{tail}, True{}, prefix, suffix)))) 705 case J.Null{}: render_append(J.Null{}, False{}, prefix, suffix) 706 case J.Bool{truth}: 707 match truth: 708 case True{}: render_append(J.Bool{True{}}, False{}, prefix, suffix) 709 case False{}: render_append(J.Bool{False{}}, False{}, prefix, suffix) 710 case J.Number{lexeme, certificate}: 711 render_append(J.Number{lexeme, certificate}, False{}, prefix, suffix) 712 case J.Str{text}: render_append(J.Str{text}, False{}, prefix, suffix) 713 714 def render_task_append(+value: J.Value, 715 +mode: RenderMode, 716 +prefix: String, 717 +suffix: String) -> {render_task(value, mode, prefix) ++ suffix == render_task(value, mode, prefix ++ suffix) : String}: 718 match mode: 719 case RenderWhole{}: render_append(value, False{}, prefix, suffix) 720 case RenderMembers{}: render_append(value, True{}, prefix, suffix) 721 case RenderAfterSeparator{}: render_after_separator_append(value, prefix, suffix) 722 723 def render_after_separator_array_single(+head: J.Value, 724 +suffix: String) -> {render_after_separator(J.Arr{head <> Nil{}}, suffix) == render_task(head, RenderWhole{}, "]" ++ suffix) : String}: 725 Equal.trans(String, 726 render_after_separator(J.Arr{head <> Nil{}}, suffix), 727 J.render(head, False{}, SNil{}) ++ (separator_text(J.Arr{Nil{}}) ++ render_after_separator(J.Arr{Nil{}}, suffix)), 728 render_task(head, RenderWhole{}, "]" ++ suffix), 729 render_after_separator_array_decompose(head, Nil{}, suffix), 730 Equal.trans(String, 731 J.render(head, False{}, SNil{}) ++ (separator_text(J.Arr{Nil{}}) ++ render_after_separator(J.Arr{Nil{}}, suffix)), 732 J.render(head, False{}, SNil{}) ++ ("]" ++ suffix), 733 render_task(head, RenderWhole{}, "]" ++ suffix), 734 Equal.cong(String, String, text => J.render(head, False{}, SNil{}) ++ text, 735 separator_text(J.Arr{Nil{}}) ++ render_after_separator(J.Arr{Nil{}}, suffix), "]" ++ suffix, {==}), 736 render_task_append(head, RenderWhole{}, SNil{}, "]" ++ suffix))) 737 738 def render_after_separator_array_many(+head: J.Value, 739 +next: J.Value, 740 +tail: List<&2, J.Value>, 741 +suffix: String) -> {render_after_separator(J.Arr{head <> next <> tail}, suffix) == render_task(head, RenderWhole{}, "," ++ render_after_separator(J.Arr{next <> tail}, suffix)) : String}: 742 Equal.trans(String, 743 render_after_separator(J.Arr{head <> next <> tail}, suffix), 744 J.render(head, False{}, SNil{}) ++ 745 (separator_text(J.Arr{next <> tail}) ++ render_after_separator(J.Arr{next <> tail}, suffix)), 746 render_task(head, RenderWhole{}, "," ++ render_after_separator(J.Arr{next <> tail}, suffix)), 747 render_after_separator_array_decompose(head, next <> tail, suffix), 748 render_task_append(head, RenderWhole{}, SNil{}, "," ++ render_after_separator(J.Arr{next <> tail}, suffix))) 749 750 751 752 753 def source_members_decompose(+value: J.Value, 754 +suffix: List<&2, J.Lexeme>) -> {J.source(value, True{}, suffix) == List.append(&2, J.Lexeme, source_separator(value), source_after_separator(value, suffix)) : List<&2, J.Lexeme>}: 755 match value: 756 case J.Null{}: {==} 757 case J.Bool{truth}: 758 match truth: 759 case True{}: {==} 760 case False{}: {==} 761 case J.Number{lexeme, certificate}: {==} 762 case J.Str{text}: {==} 763 case J.Arr{Nil{}}: {==} 764 case J.Arr{head <> tail}: {==} 765 case J.Obj{Nil{}}: {==} 766 case J.Obj{(key, field_value) <> tail}: {==} 767 768 def atomic_source(atom: AtomicValue) -> List<&2, J.Lexeme>: 769 match atom: 770 case AtomicNull{}: J.Payload{"null"} <> Nil{} 771 case AtomicTrue{}: J.Payload{"true"} <> Nil{} 772 case AtomicFalse{}: J.Payload{"false"} <> Nil{} 773 case AtomicNumber{text, _}: J.Payload{text} <> Nil{} 774 case AtomicString{text}: J.Payload{"\"" ++ J.escape_string(text) ++ "\""} <> Nil{} 775 776 def atomic_source_reverse(+atom: AtomicValue) -> {atomic_source(atom) == List.reverse(&2, J.Lexeme, J.source(atomic_value(atom), False{}, Nil{})) : List<&2, J.Lexeme>}: 777 match atom: 778 case AtomicNull{}: {==} 779 case AtomicTrue{}: {==} 780 case AtomicFalse{}: {==} 781 case AtomicNumber{text, certificate}: {==} 782 case AtomicString{text}: {==} 783 784 def lex_atomic_source_before_punctuation(+atom: AtomicValue, 785 +punctuation: Char, 786 +suffix: String, 787 +acc: List<&2, J.Lexeme>, 788 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(atomic_value(atom), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(atom), acc)) : List<&2, J.Lexeme>}: 789 match atom: 790 case AtomicNull{}: 791 Equal.trans(List<&2, J.Lexeme>, 792 J.lex_scan(J.render(J.Null{}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 793 J.lex_scan("null" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 794 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(AtomicNull{}), acc)), 795 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 796 J.render(J.Null{}, False{}, SNil{}), "null", S.append_nil("null")), 797 W.lex_null_before_punctuation(punctuation, suffix, acc, action)) 798 case AtomicTrue{}: 799 Equal.trans(List<&2, J.Lexeme>, 800 J.lex_scan(J.render(J.Bool{True{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 801 J.lex_scan("true" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 802 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(AtomicTrue{}), acc)), 803 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 804 J.render(J.Bool{True{}}, False{}, SNil{}), "true", S.append_nil("true")), 805 W.lex_true_before_punctuation(punctuation, suffix, acc, action)) 806 case AtomicFalse{}: 807 Equal.trans(List<&2, J.Lexeme>, 808 J.lex_scan(J.render(J.Bool{False{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 809 J.lex_scan("false" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 810 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(AtomicFalse{}), acc)), 811 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 812 J.render(J.Bool{False{}}, False{}, SNil{}), "false", S.append_nil("false")), 813 W.lex_false_before_punctuation(punctuation, suffix, acc, action)) 814 case AtomicNumber{text, certificate}: 815 lex_source_number_before_punctuation(text, certificate, punctuation, suffix, acc, action) 816 case AtomicString{text}: 817 Equal.trans(List<&2, J.Lexeme>, 818 J.lex_scan(J.render(J.Str{text}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 819 J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 820 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(AtomicString{text}), acc)), 821 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 822 J.render(J.Str{text}, False{}, SNil{}), SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, {==}), 823 W.lex_string_before_punctuation(text, punctuation, suffix, acc, action)) 824 825 def lex_atomic_reverse_before_punctuation(+atom: AtomicValue, 826 +punctuation: Char, 827 +suffix: String, 828 +acc: List<&2, J.Lexeme>, 829 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(atomic_value(atom), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, J.source(atomic_value(atom), False{}, Nil{})), acc)) : List<&2, J.Lexeme>}: 830 Equal.trans(List<&2, J.Lexeme>, 831 J.lex_scan(J.render(atomic_value(atom), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 832 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, atomic_source(atom), acc)), 833 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, J.source(atomic_value(atom), False{}, Nil{})), acc)), 834 lex_atomic_source_before_punctuation(atom, punctuation, suffix, acc, action), 835 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, items, acc)), 836 atomic_source(atom), 837 List.reverse(&2, J.Lexeme, J.source(atomic_value(atom), False{}, Nil{})), 838 atomic_source_reverse(atom))) 839 840 def lex_atomic_value_source(+atom: AtomicValue) -> {J.lex_scan(J.stringify(atomic_value(atom)), J.Outside{}, SNil{}, Nil{}) == J.source(atomic_value(atom), False{}, Nil{}) : List<&2, J.Lexeme>}: 841 match atom: 842 case AtomicNull{}: {==} 843 case AtomicTrue{}: {==} 844 case AtomicFalse{}: {==} 845 case AtomicNumber{text, certificate}: 846 Equal.trans(List<&2, J.Lexeme>, 847 J.lex_scan(J.stringify(J.Number{text, certificate}), J.Outside{}, SNil{}, Nil{}), 848 J.lex_scan(text, J.Outside{}, SNil{}, Nil{}), 849 J.source(J.Number{text, certificate}, False{}, Nil{}), 850 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Outside{}, SNil{}, Nil{}), 851 J.stringify(J.Number{text, certificate}), text, S.append_nil(text)), 852 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, J.Outside{}, SNil{}, Nil{}), 853 J.Payload{text} <> Nil{}, J.source(J.Number{text, certificate}, False{}, Nil{}), 854 Num.lex_number_payload(text, P.cert_valid(text, certificate)), {==})) 855 case AtomicString{text}: 856 W.lex_rendered_string(text) 857 858 859 def lex_source_empty_array_before_punctuation(+punctuation: Char, 860 +suffix: String, 861 +acc: List<&2, J.Lexeme>, 862 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Arr{Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> J.Punctuation{'['} <> acc) : List<&2, J.Lexeme>}: 863 Equal.trans(List<&2, J.Lexeme>, 864 J.lex_scan(J.render(J.Arr{Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 865 J.lex_scan("[]" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 866 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> J.Punctuation{'['} <> acc), 867 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 868 J.render(J.Arr{Nil{}}, False{}, SNil{}), "[]", S.append_nil("[]")), 869 W.lex_empty_array_before_punctuation(punctuation, suffix, acc, action)) 870 871 def lex_source_empty_object_before_punctuation(+punctuation: Char, 872 +suffix: String, 873 +acc: List<&2, J.Lexeme>, 874 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Obj{Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{'}'} <> J.Punctuation{'{'} <> acc) : List<&2, J.Lexeme>}: 875 Equal.trans(List<&2, J.Lexeme>, 876 J.lex_scan(J.render(J.Obj{Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 877 J.lex_scan("{}" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 878 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{'}'} <> J.Punctuation{'{'} <> acc), 879 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 880 J.render(J.Obj{Nil{}}, False{}, SNil{}), "{}", S.append_nil("{}")), 881 W.lex_empty_object_before_punctuation(punctuation, suffix, acc, action)) 882 883 def lex_empty_array_reverse_before_punctuation(+punctuation: Char, 884 +suffix: String, 885 +acc: List<&2, J.Lexeme>, 886 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Arr{Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, J.source(J.Arr{Nil{}}, False{}, Nil{})), acc)) : List<&2, J.Lexeme>}: 887 lex_source_empty_array_before_punctuation(punctuation, suffix, acc, action) 888 889 def lex_empty_object_reverse_before_punctuation(+punctuation: Char, 890 +suffix: String, 891 +acc: List<&2, J.Lexeme>, 892 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Obj{Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, J.source(J.Obj{Nil{}}, False{}, Nil{})), acc)) : List<&2, J.Lexeme>}: 893 lex_source_empty_object_before_punctuation(punctuation, suffix, acc, action) 894 895 def lex_simple_before_punctuation(+simple: SimpleValue, 896 +punctuation: Char, 897 +suffix: String, 898 +acc: List<&2, J.Lexeme>, 899 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(simple_value(simple), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, J.source(simple_value(simple), False{}, Nil{})), acc)) : List<&2, J.Lexeme>}: 900 match simple: 901 case SimpleAtom{atom}: lex_atomic_reverse_before_punctuation(atom, punctuation, suffix, acc, action) 902 case SimpleEmptyArray{}: lex_empty_array_reverse_before_punctuation(punctuation, suffix, acc, action) 903 case SimpleEmptyObject{}: lex_empty_object_reverse_before_punctuation(punctuation, suffix, acc, action) 904 905 def lex_close_before_punctuation(+closing: Char, 906 +punctuation: Char, 907 +suffix: String, 908 +acc: List<&2, J.Lexeme>, 909 close_action: {J.lex_seed_action(SCon{closing, SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}) == J.LexPunctuation{closing} : J.LexAction}, 910 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(SCon{closing, SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{closing} <> acc) : List<&2, J.Lexeme>}: 911 Equal.trans(List<&2, J.Lexeme>, 912 J.lex_scan(SCon{closing, SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}, SNil{}, acc), 913 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{closing} <> acc), 914 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{closing} <> acc), 915 W.scan_punctuation_char(closing, SCon{punctuation, SNil{}} ++ suffix, SNil{}, acc, close_action), 916 W.scan_punctuation_char(punctuation, suffix, SNil{}, J.Punctuation{closing} <> acc, action)) 917 918 def lex_object_key_before_colon(+key: String, 919 +suffix: String, 920 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{':'} <> J.Payload{"\"" ++ J.escape_string(key) ++ "\""} <> acc) : List<&2, J.Lexeme>}: 921 W.lex_string_before_punctuation(key, ':', suffix, acc, {==}) 922 923 def atomic_task_render(atom: AtomicValue, 924 mode: RenderMode) -> {render_task(atomic_value(atom), mode, SNil{}) == J.render(atomic_value(atom), False{}, SNil{}) : String}: 925 match atom mode: 926 case AtomicNull{} RenderWhole{}: {==} 927 case AtomicTrue{} RenderWhole{}: {==} 928 case AtomicFalse{} RenderWhole{}: {==} 929 case AtomicNumber{text, certificate} RenderWhole{}: {==} 930 case AtomicString{text} RenderWhole{}: {==} 931 case AtomicNull{} RenderMembers{}: {==} 932 case AtomicTrue{} RenderMembers{}: {==} 933 case AtomicFalse{} RenderMembers{}: {==} 934 case AtomicNumber{text, certificate} RenderMembers{}: {==} 935 case AtomicString{text} RenderMembers{}: {==} 936 case AtomicNull{} RenderAfterSeparator{}: {==} 937 case AtomicTrue{} RenderAfterSeparator{}: {==} 938 case AtomicFalse{} RenderAfterSeparator{}: {==} 939 case AtomicNumber{text, certificate} RenderAfterSeparator{}: {==} 940 case AtomicString{text} RenderAfterSeparator{}: {==} 941 942 def atomic_task_source(atom: AtomicValue, 943 mode: RenderMode) -> {reverse_source_task(atomic_value(atom), mode) == reverse_source_task(atomic_value(atom), RenderWhole{}) : List<&2, J.Lexeme>}: 944 match atom mode: 945 case AtomicNull{} RenderWhole{}: {==} 946 case AtomicTrue{} RenderWhole{}: {==} 947 case AtomicFalse{} RenderWhole{}: {==} 948 case AtomicNumber{text, certificate} RenderWhole{}: {==} 949 case AtomicString{text} RenderWhole{}: {==} 950 case AtomicNull{} RenderMembers{}: {==} 951 case AtomicTrue{} RenderMembers{}: {==} 952 case AtomicFalse{} RenderMembers{}: {==} 953 case AtomicNumber{text, certificate} RenderMembers{}: {==} 954 case AtomicString{text} RenderMembers{}: {==} 955 case AtomicNull{} RenderAfterSeparator{}: {==} 956 case AtomicTrue{} RenderAfterSeparator{}: {==} 957 case AtomicFalse{} RenderAfterSeparator{}: {==} 958 case AtomicNumber{text, certificate} RenderAfterSeparator{}: {==} 959 case AtomicString{text} RenderAfterSeparator{}: {==} 960 961 def lex_atomic_task_before_punctuation(+atom: AtomicValue, 962 +mode: RenderMode, 963 +punctuation: Char, 964 +suffix: String, 965 +acc: List<&2, J.Lexeme>, 966 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(render_task(atomic_value(atom), mode, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, reverse_source_task(atomic_value(atom), mode), acc)) : List<&2, J.Lexeme>}: 967 Equal.trans(List<&2, J.Lexeme>, 968 J.lex_scan(render_task(atomic_value(atom), mode, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), 969 J.Outside{}, SNil{}, acc), 970 J.lex_scan(J.render(atomic_value(atom), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), 971 J.Outside{}, SNil{}, acc), 972 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> 973 List.append(&2, J.Lexeme, reverse_source_task(atomic_value(atom), mode), acc)), 974 Equal.cong(String, List<&2, J.Lexeme>, text => 975 J.lex_scan(text ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 976 render_task(atomic_value(atom), mode, SNil{}), J.render(atomic_value(atom), False{}, SNil{}), 977 atomic_task_render(atom, mode)), 978 Equal.trans(List<&2, J.Lexeme>, 979 J.lex_scan(J.render(atomic_value(atom), False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), 980 J.Outside{}, SNil{}, acc), 981 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> 982 List.append(&2, J.Lexeme, reverse_source_task(atomic_value(atom), RenderWhole{}), acc)), 983 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> 984 List.append(&2, J.Lexeme, reverse_source_task(atomic_value(atom), mode), acc)), 985 lex_atomic_reverse_before_punctuation(atom, punctuation, suffix, acc, action), 986 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => 987 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> 988 List.append(&2, J.Lexeme, items, acc)), 989 reverse_source_task(atomic_value(atom), RenderWhole{}), 990 reverse_source_task(atomic_value(atom), mode), 991 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(atomic_value(atom), mode), 992 reverse_source_task(atomic_value(atom), RenderWhole{}), atomic_task_source(atom, mode))))) 993 994 def lex_simple_task_before_punctuation(+simple: SimpleValue, 995 +mode: RenderMode, 996 +punctuation: Char, 997 +suffix: String, 998 +acc: List<&2, J.Lexeme>, 999 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(render_task(simple_value(simple), mode, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(simple), mode), acc)) : List<&2, J.Lexeme>}: 1000 match simple mode: 1001 case SimpleAtom{atom} RenderWhole{}: 1002 lex_atomic_task_before_punctuation(atom, RenderWhole{}, punctuation, suffix, acc, action) 1003 case SimpleAtom{atom} RenderMembers{}: 1004 lex_atomic_task_before_punctuation(atom, RenderMembers{}, punctuation, suffix, acc, action) 1005 case SimpleAtom{atom} RenderAfterSeparator{}: 1006 lex_atomic_task_before_punctuation(atom, RenderAfterSeparator{}, punctuation, suffix, acc, action) 1007 case SimpleEmptyArray{} RenderWhole{}: 1008 lex_empty_array_reverse_before_punctuation(punctuation, suffix, acc, action) 1009 case SimpleEmptyArray{} RenderMembers{}: 1010 lex_close_before_punctuation(']', punctuation, suffix, acc, {==}, action) 1011 case SimpleEmptyArray{} RenderAfterSeparator{}: 1012 lex_close_before_punctuation(']', punctuation, suffix, acc, {==}, action) 1013 case SimpleEmptyObject{} RenderWhole{}: 1014 lex_empty_object_reverse_before_punctuation(punctuation, suffix, acc, action) 1015 case SimpleEmptyObject{} RenderMembers{}: 1016 lex_close_before_punctuation('}', punctuation, suffix, acc, {==}, action) 1017 case SimpleEmptyObject{} RenderAfterSeparator{}: 1018 lex_close_before_punctuation('}', punctuation, suffix, acc, {==}, action) 1019 1020 def lex_simple_task_suffix_before_punctuation(+simple: SimpleValue, 1021 +mode: RenderMode, 1022 +punctuation: Char, 1023 +suffix: String, 1024 +acc: List<&2, J.Lexeme>, 1025 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(render_task(simple_value(simple), mode, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(simple), mode), acc)) : List<&2, J.Lexeme>}: 1026 Equal.trans(List<&2, J.Lexeme>, 1027 J.lex_scan(render_task(simple_value(simple), mode, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 1028 J.lex_scan(render_task(simple_value(simple), mode, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 1029 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> 1030 List.append(&2, J.Lexeme, reverse_source_task(simple_value(simple), mode), acc)), 1031 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc), 1032 render_task(simple_value(simple), mode, SCon{punctuation, SNil{}} ++ suffix), 1033 render_task(simple_value(simple), mode, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), 1034 Equal.sym(String, 1035 render_task(simple_value(simple), mode, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), 1036 render_task(simple_value(simple), mode, SCon{punctuation, SNil{}} ++ suffix), 1037 render_task_append(simple_value(simple), mode, SNil{}, SCon{punctuation, SNil{}} ++ suffix))), 1038 lex_simple_task_before_punctuation(simple, mode, punctuation, suffix, acc, action)) 1039 1040 def lex_array_singleton_value_before_punctuation(+head: J.Value, 1041 +punctuation: Char, 1042 +suffix: String, 1043 +acc: List<&2, J.Lexeme>, 1044 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}, 1045 head_lex: {J.lex_scan(J.render(head, False{}, SNil{}) ++ (SCon{']', SCon{punctuation, SNil{}} ++ suffix}), J.Outside{}, SNil{}, J.Punctuation{'['} <> acc) == J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc)) : List<&2, J.Lexeme>}) -> {J.lex_scan(J.render(J.Arr{head <> Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc)) : List<&2, J.Lexeme>}: 1046 Equal.trans(List<&2, J.Lexeme>, 1047 J.lex_scan(J.render(J.Arr{head <> Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 1048 J.lex_scan("[" ++ (J.render(head, False{}, SNil{}) ++ ("]" ++ (SCon{punctuation, SNil{}} ++ suffix))), J.Outside{}, SNil{}, acc), 1049 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> 1050 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc)), 1051 Equal.trans(List<&2, J.Lexeme>, 1052 J.lex_scan(J.render(J.Arr{head <> Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 1053 J.lex_scan(J.render(J.Arr{head <> Nil{}}, False{}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 1054 J.lex_scan("[" ++ (J.render(head, False{}, SNil{}) ++ ("]" ++ (SCon{punctuation, SNil{}} ++ suffix))), J.Outside{}, SNil{}, acc), 1055 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc), 1056 J.render(J.Arr{head <> Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), 1057 J.render(J.Arr{head <> Nil{}}, False{}, SCon{punctuation, SNil{}} ++ suffix), 1058 render_append(J.Arr{head <> Nil{}}, False{}, SNil{}, SCon{punctuation, SNil{}} ++ suffix)), 1059 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc), 1060 J.render(J.Arr{head <> Nil{}}, False{}, SCon{punctuation, SNil{}} ++ suffix), 1061 "[" ++ (J.render(head, False{}, SNil{}) ++ ("]" ++ (SCon{punctuation, SNil{}} ++ suffix))), 1062 render_array_singleton_suffix(head, SCon{punctuation, SNil{}} ++ suffix))), 1063 Equal.trans(List<&2, J.Lexeme>, 1064 J.lex_scan("[" ++ (J.render(head, False{}, SNil{}) ++ ("]" ++ (SCon{punctuation, SNil{}} ++ suffix))), J.Outside{}, SNil{}, acc), 1065 J.lex_scan(J.render(head, False{}, SNil{}) ++ (SCon{']', SCon{punctuation, SNil{}} ++ suffix}), J.Outside{}, SNil{}, J.Punctuation{'['} <> acc), 1066 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> 1067 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc)), 1068 W.scan_punctuation_char('[', J.render(head, False{}, SNil{}) ++ ("]" ++ (SCon{punctuation, SNil{}} ++ suffix)), SNil{}, acc, {==}), 1069 Equal.trans(List<&2, J.Lexeme>, 1070 J.lex_scan(J.render(head, False{}, SNil{}) ++ (SCon{']', SCon{punctuation, SNil{}} ++ suffix}), J.Outside{}, SNil{}, J.Punctuation{'['} <> acc), 1071 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <> 1072 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc)), 1073 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> 1074 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc)), 1075 head_lex, 1076 W.scan_punctuation_char(punctuation, suffix, SNil{}, J.Punctuation{']'} <> 1077 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), J.Punctuation{'['} <> acc), action)))) 1078 1079 def lex_array_singleton_before_punctuation(+head: SimpleValue, 1080 +punctuation: Char, 1081 +suffix: String, 1082 +acc: List<&2, J.Lexeme>, 1083 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan(J.render(J.Arr{simple_value(head) <> Nil{}}, False{}, SNil{}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), J.Punctuation{'['} <> acc)) : List<&2, J.Lexeme>}: 1084 lex_array_singleton_value_before_punctuation(simple_value(head), punctuation, suffix, acc, action, 1085 lex_simple_task_before_punctuation(head, RenderWhole{}, ']', SCon{punctuation, SNil{}} ++ suffix, 1086 J.Punctuation{'['} <> acc, {==})) 1087 1088 def lex_array_after_separator_single(+head: J.Value, 1089 +punctuation: Char, 1090 +suffix: String, 1091 +acc: List<&2, J.Lexeme>, 1092 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}, 1093 head_lex: {J.lex_scan(render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)), J.Outside{}, SNil{}, acc) == J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2, 1094 J.Lexeme>}) -> {J.lex_scan(render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2, J.Lexeme>}: 1095 Equal.trans(List<&2, J.Lexeme>, 1096 J.lex_scan(render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix), 1097 J.Outside{}, SNil{}, acc), 1098 J.lex_scan(render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)), 1099 J.Outside{}, SNil{}, acc), 1100 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> 1101 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1102 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc), 1103 render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix), 1104 render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)), 1105 render_after_separator_array_single(head, SCon{punctuation, SNil{}} ++ suffix)), 1106 Equal.trans(List<&2, J.Lexeme>, 1107 J.lex_scan(render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)), 1108 J.Outside{}, SNil{}, acc), 1109 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <> 1110 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1111 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> 1112 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1113 head_lex, 1114 W.scan_punctuation_char(punctuation, suffix, SNil{}, J.Punctuation{']'} <> 1115 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc), action))) 1116 1117 def lex_array_after_separator_single_source(+head: J.Value, 1118 +punctuation: Char, 1119 +suffix: String, 1120 +acc: List<&2, J.Lexeme>, 1121 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}, 1122 head_lex: {J.lex_scan(render_task(head, RenderWhole{}, "]" ++ (SCon{punctuation, SNil{}} ++ suffix)), J.Outside{}, SNil{}, acc) == J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2, 1123 J.Lexeme>}) -> {J.lex_scan(render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> Nil{}}, RenderAfterSeparator{}), acc)) : List<&2, J.Lexeme>}: 1124 Equal.trans(List<&2, J.Lexeme>, 1125 J.lex_scan(render_after_separator(J.Arr{head <> Nil{}}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 1126 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> 1127 J.Punctuation{']'} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1128 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> 1129 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> Nil{}}, RenderAfterSeparator{}), acc)), 1130 lex_array_after_separator_single(head, punctuation, suffix, acc, action, head_lex), 1131 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.lex_scan(suffix, J.Outside{}, SNil{}, 1132 J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, items, acc)), 1133 J.Punctuation{']'} <> reverse_source_task(head, RenderWhole{}), 1134 reverse_source_task(J.Arr{head <> Nil{}}, RenderAfterSeparator{}), 1135 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{head <> Nil{}}, RenderAfterSeparator{}), 1136 J.Punctuation{']'} <> reverse_source_task(head, RenderWhole{}), 1137 reverse_source_array_after_separator(head, Nil{})))) 1138 1139 def reverse_array_after_separator_acc_many(+head: J.Value, 1140 +next: J.Value, 1141 +tail: List<&2, J.Value>, 1142 +acc: List<&2, J.Lexeme>) -> {List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc) : List<&2, J.Lexeme>}: 1143 Equal.trans(List<&2, J.Lexeme>, 1144 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), 1145 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1146 List.append(&2, J.Lexeme, 1147 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}), 1148 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1149 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc), 1150 Equal.sym(List<&2, J.Lexeme>, 1151 List.append(&2, J.Lexeme, 1152 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}), 1153 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1154 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), 1155 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1156 LP.append_assoc(J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), 1157 J.Punctuation{','} <> Nil{}, List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc))), 1158 Equal.trans(List<&2, J.Lexeme>, 1159 List.append(&2, J.Lexeme, 1160 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}), 1161 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1162 List.append(&2, J.Lexeme, 1163 reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), 1164 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1165 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc), 1166 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => 1167 List.append(&2, J.Lexeme, xs, List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1168 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}), 1169 reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), 1170 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), 1171 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}), 1172 reverse_source_array_members_after_separator(next, tail))), 1173 Equal.trans(List<&2, J.Lexeme>, 1174 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), 1175 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1176 List.append(&2, J.Lexeme, 1177 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})), acc), 1178 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc), 1179 Equal.sym(List<&2, J.Lexeme>, 1180 List.append(&2, J.Lexeme, 1181 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})), acc), 1182 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), 1183 List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1184 LP.append_assoc(J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), 1185 reverse_source_task(head, RenderWhole{}), acc)), 1186 Equal.sym(List<&2, J.Lexeme>, 1187 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc), 1188 List.append(&2, J.Lexeme, 1189 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})), acc), 1190 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, xs => List.append(&2, J.Lexeme, xs, acc), 1191 reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), 1192 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderMembers{}), reverse_source_task(head, RenderWhole{})), 1193 reverse_source_array_after_separator(head, next <> tail)))))) 1194 1195 def lex_array_after_separator_many(+head: J.Value, 1196 +next: J.Value, 1197 +tail: List<&2, J.Value>, 1198 +punctuation: Char, 1199 +suffix: String, 1200 +acc: List<&2, J.Lexeme>, 1201 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}, 1202 head_lex: {J.lex_scan(render_task(head, RenderWhole{}, "," ++ render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix)), J.Outside{}, SNil{}, acc) == J.lex_scan(render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) : List<&2, J.Lexeme>}, 1203 tail_lex: {J.lex_scan(render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc))) : List<&2, J.Lexeme>}) -> {J.lex_scan(render_after_separator(J.Arr{head <> next <> tail}, SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc)) : List<&2, J.Lexeme>}: 1204 Equal.trans(List<&2, J.Lexeme>, 1205 J.lex_scan(render_after_separator(J.Arr{head <> next <> tail}, SCon{punctuation, SNil{}} ++ suffix), 1206 J.Outside{}, SNil{}, acc), 1207 J.lex_scan(render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix), 1208 J.Outside{}, SNil{}, J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1209 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> 1210 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc)), 1211 Equal.trans(List<&2, J.Lexeme>, 1212 J.lex_scan(render_after_separator(J.Arr{head <> next <> tail}, SCon{punctuation, SNil{}} ++ suffix), 1213 J.Outside{}, SNil{}, acc), 1214 J.lex_scan(render_task(head, RenderWhole{}, "," ++ render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix)), 1215 J.Outside{}, SNil{}, acc), 1216 J.lex_scan(render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix), 1217 J.Outside{}, SNil{}, J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1218 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc), 1219 render_after_separator(J.Arr{head <> next <> tail}, SCon{punctuation, SNil{}} ++ suffix), 1220 render_task(head, RenderWhole{}, "," ++ render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix)), 1221 render_after_separator_array_many(head, next, tail, SCon{punctuation, SNil{}} ++ suffix)), 1222 head_lex), 1223 Equal.trans(List<&2, J.Lexeme>, 1224 J.lex_scan(render_after_separator(J.Arr{next <> tail}, SCon{punctuation, SNil{}} ++ suffix), 1225 J.Outside{}, SNil{}, J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1226 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> 1227 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), 1228 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc))), 1229 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> 1230 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc)), 1231 tail_lex, 1232 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> items), 1233 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{next <> tail}, RenderAfterSeparator{}), 1234 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(head, RenderWhole{}), acc)), 1235 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{head <> next <> tail}, RenderAfterSeparator{}), acc), 1236 reverse_array_after_separator_acc_many(head, next, tail, acc)))) 1237 1238 def lex_array_after_separator_two_simple(+first: SimpleValue, 1239 +second: SimpleValue, 1240 +mark: JsonPunctuation, 1241 +suffix: String, 1242 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(render_after_separator(J.Arr{simple_value(first) <> simple_value(second) <> Nil{}}, SCon{punctuation_char(mark), SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation_char(mark)} <> List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_value(first) <> simple_value(second) <> Nil{}}, RenderAfterSeparator{}), acc)) : List<&2, J.Lexeme>}: 1243 lex_array_after_separator_many(simple_value(first), simple_value(second), Nil{}, punctuation_char(mark), suffix, acc, punctuation_action(mark, suffix), 1244 lex_simple_task_suffix_before_punctuation(first, RenderWhole{}, ',', render_after_separator(J.Arr{simple_value(second) <> Nil{}}, SCon{punctuation_char(mark), SNil{}} ++ suffix), acc, {==}), 1245 Equal.trans(List<&2, J.Lexeme>, 1246 J.lex_scan(render_after_separator(J.Arr{simple_value(second) <> Nil{}}, SCon{punctuation_char(mark), SNil{}} ++ suffix), 1247 J.Outside{}, SNil{}, J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(first), RenderWhole{}), acc)), 1248 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation_char(mark)} <> J.Punctuation{']'} <> 1249 List.append(&2, J.Lexeme, reverse_source_task(simple_value(second), RenderWhole{}), 1250 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(first), RenderWhole{}), acc))), 1251 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation_char(mark)} <> 1252 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_value(second) <> Nil{}}, RenderAfterSeparator{}), 1253 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(first), RenderWhole{}), acc))), 1254 lex_array_after_separator_single(simple_value(second), punctuation_char(mark), suffix, 1255 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(first), RenderWhole{}), acc), punctuation_action(mark, suffix), 1256 lex_simple_task_suffix_before_punctuation(second, RenderWhole{}, ']', SCon{punctuation_char(mark), SNil{}} ++ suffix, 1257 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(first), RenderWhole{}), acc), {==})), 1258 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => 1259 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation_char(mark)} <> 1260 List.append(&2, J.Lexeme, items, J.Punctuation{','} <> 1261 List.append(&2, J.Lexeme, reverse_source_task(simple_value(first), RenderWhole{}), acc))), 1262 J.Punctuation{']'} <> reverse_source_task(simple_value(second), RenderWhole{}), 1263 reverse_source_task(J.Arr{simple_value(second) <> Nil{}}, RenderAfterSeparator{}), 1264 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{simple_value(second) <> Nil{}}, RenderAfterSeparator{}), 1265 J.Punctuation{']'} <> reverse_source_task(simple_value(second), RenderWhole{}), 1266 reverse_source_array_after_separator(simple_value(second), Nil{}))))) 1267 1268 def simple_values(values: List<&2, SimpleValue>) -> List<&2, J.Value>: 1269 match values: 1270 case Nil{}: Nil{} 1271 case head <> tail: simple_value(head) <> simple_values(tail) 1272 1273 def lex_simple_array_after_separator_end(+values: List<&2, SimpleValue>, 1274 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, acc) == J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), acc)) : List<&2, J.Lexeme>}: 1275 match values: 1276 case Nil{}: 1277 W.scan_punctuation_char(']', SNil{}, SNil{}, acc, {==}) 1278 case head <> Nil{}: 1279 Equal.trans(List<&2, J.Lexeme>, 1280 J.lex_scan(render_after_separator(J.Arr{simple_value(head) <> Nil{}}, SNil{}), J.Outside{}, SNil{}, acc), 1281 J.lex_scan(render_task(simple_value(head), RenderWhole{}, "]"), J.Outside{}, SNil{}, acc), 1282 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, 1283 reverse_source_task(J.Arr{simple_value(head) <> Nil{}}, RenderAfterSeparator{}), acc)), 1284 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc), 1285 render_after_separator(J.Arr{simple_value(head) <> Nil{}}, SNil{}), 1286 render_task(simple_value(head), RenderWhole{}, "]"), 1287 render_after_separator_array_single(simple_value(head), SNil{})), 1288 Equal.trans(List<&2, J.Lexeme>, 1289 J.lex_scan(render_task(simple_value(head), RenderWhole{}, "]"), J.Outside{}, SNil{}, acc), 1290 J.lex_scan(SNil{}, J.Outside{}, SNil{}, J.Punctuation{']'} <> 1291 List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)), 1292 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, 1293 reverse_source_task(J.Arr{simple_value(head) <> Nil{}}, RenderAfterSeparator{}), acc)), 1294 lex_simple_task_suffix_before_punctuation(head, RenderWhole{}, ']', SNil{}, acc, {==}), 1295 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => 1296 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, items, acc)), 1297 J.Punctuation{']'} <> reverse_source_task(simple_value(head), RenderWhole{}), 1298 reverse_source_task(J.Arr{simple_value(head) <> Nil{}}, RenderAfterSeparator{}), 1299 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{simple_value(head) <> Nil{}}, RenderAfterSeparator{}), 1300 J.Punctuation{']'} <> reverse_source_task(simple_value(head), RenderWhole{}), 1301 reverse_source_array_after_separator(simple_value(head), Nil{}))))) 1302 case head <> next <> tail: 1303 Equal.trans(List<&2, J.Lexeme>, 1304 J.lex_scan(render_after_separator(J.Arr{simple_value(head) <> simple_value(next) <> simple_values(tail)}, SNil{}), J.Outside{}, SNil{}, acc), 1305 J.lex_scan(render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SNil{}), J.Outside{}, SNil{}, 1306 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)), 1307 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, 1308 reverse_source_task(J.Arr{simple_value(head) <> simple_value(next) <> simple_values(tail)}, RenderAfterSeparator{}), acc)), 1309 Equal.trans(List<&2, J.Lexeme>, 1310 J.lex_scan(render_after_separator(J.Arr{simple_value(head) <> simple_value(next) <> simple_values(tail)}, SNil{}), J.Outside{}, SNil{}, acc), 1311 J.lex_scan(render_task(simple_value(head), RenderWhole{}, "," ++ render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SNil{})), 1312 J.Outside{}, SNil{}, acc), 1313 J.lex_scan(render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SNil{}), J.Outside{}, SNil{}, 1314 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)), 1315 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, acc), 1316 render_after_separator(J.Arr{simple_value(head) <> simple_value(next) <> simple_values(tail)}, SNil{}), 1317 render_task(simple_value(head), RenderWhole{}, "," ++ render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SNil{})), 1318 render_after_separator_array_many(simple_value(head), simple_value(next), simple_values(tail), SNil{})), 1319 lex_simple_task_suffix_before_punctuation(head, RenderWhole{}, ',', 1320 render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SNil{}), acc, {==})), 1321 Equal.trans(List<&2, J.Lexeme>, 1322 J.lex_scan(render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SNil{}), J.Outside{}, SNil{}, 1323 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)), 1324 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, 1325 reverse_source_task(J.Arr{simple_value(next) <> simple_values(tail)}, RenderAfterSeparator{}), 1326 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc))), 1327 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, 1328 reverse_source_task(J.Arr{simple_value(head) <> simple_value(next) <> simple_values(tail)}, RenderAfterSeparator{}), acc)), 1329 lex_simple_array_after_separator_end(next <> tail, 1330 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)), 1331 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.lex_scan(SNil{}, J.Outside{}, SNil{}, items), 1332 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_value(next) <> simple_values(tail)}, RenderAfterSeparator{}), 1333 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc)), 1334 List.append(&2, J.Lexeme, 1335 reverse_source_task(J.Arr{simple_value(head) <> simple_value(next) <> simple_values(tail)}, RenderAfterSeparator{}), acc), 1336 reverse_array_after_separator_acc_many(simple_value(head), simple_value(next), simple_values(tail), acc)))) 1337 1338 def reverse_source_array_after_separator_whole_list(+values: List<&2, J.Value>) -> {reverse_source_task(J.Arr{values}, RenderWhole{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Arr{values}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}) : List<&2, J.Lexeme>}: 1339 match values: 1340 case Nil{}: {==} 1341 case head <> tail: reverse_source_array_after_separator_whole(head, tail) 1342 1343 def render_array_whole_after_separator(+values: List<&2, J.Value>, 1344 +suffix: String) -> {J.render(J.Arr{values}, False{}, suffix) == "[" ++ render_after_separator(J.Arr{values}, suffix) : String}: 1345 match values: 1346 case Nil{}: {==} 1347 case head <> tail: {==} 1348 1349 def lex_simple_array_whole(+values: List<&2, SimpleValue>) -> {J.lex_scan(J.render(J.Arr{simple_values(values)}, False{}, SNil{}), J.Outside{}, SNil{}, Nil{}) == J.source(J.Arr{simple_values(values)}, False{}, Nil{}) : List<&2, J.Lexeme>}: 1350 Equal.trans(List<&2, J.Lexeme>, 1351 J.lex_scan(J.render(J.Arr{simple_values(values)}, False{}, SNil{}), J.Outside{}, SNil{}, Nil{}), 1352 J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, J.Punctuation{'['} <> Nil{}), 1353 J.source(J.Arr{simple_values(values)}, False{}, Nil{}), 1354 Equal.trans(List<&2, J.Lexeme>, 1355 J.lex_scan(J.render(J.Arr{simple_values(values)}, False{}, SNil{}), J.Outside{}, SNil{}, Nil{}), 1356 J.lex_scan("[" ++ render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, Nil{}), 1357 J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, J.Punctuation{'['} <> Nil{}), 1358 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Outside{}, SNil{}, Nil{}), 1359 J.render(J.Arr{simple_values(values)}, False{}, SNil{}), 1360 "[" ++ render_after_separator(J.Arr{simple_values(values)}, SNil{}), 1361 render_array_whole_after_separator(simple_values(values), SNil{})), 1362 W.scan_punctuation_char('[', render_after_separator(J.Arr{simple_values(values)}, SNil{}), SNil{}, Nil{}, {==})), 1363 Equal.trans(List<&2, J.Lexeme>, 1364 J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SNil{}), J.Outside{}, SNil{}, J.Punctuation{'['} <> Nil{}), 1365 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, 1366 reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{})), 1367 J.source(J.Arr{simple_values(values)}, False{}, Nil{}), 1368 lex_simple_array_after_separator_end(values, J.Punctuation{'['} <> Nil{}), 1369 Equal.trans(List<&2, J.Lexeme>, 1370 J.lex_scan(SNil{}, J.Outside{}, SNil{}, List.append(&2, J.Lexeme, 1371 reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{})), 1372 J.lex_scan(SNil{}, J.Outside{}, SNil{}, reverse_source_task(J.Arr{simple_values(values)}, RenderWhole{})), 1373 J.source(J.Arr{simple_values(values)}, False{}, Nil{}), 1374 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => J.lex_scan(SNil{}, J.Outside{}, SNil{}, items), 1375 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}), 1376 reverse_source_task(J.Arr{simple_values(values)}, RenderWhole{}), 1377 Equal.sym(List<&2, J.Lexeme>, reverse_source_task(J.Arr{simple_values(values)}, RenderWhole{}), 1378 List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), J.Punctuation{'['} <> Nil{}), 1379 reverse_source_array_after_separator_whole_list(simple_values(values)))), 1380 LP.reverse_twice(J.Lexeme, J.source(J.Arr{simple_values(values)}, False{}, Nil{}))))) 1381 1382 def lex_simple_array_after_separator(+values: List<&2, SimpleValue>, 1383 +mark: JsonPunctuation, 1384 +suffix: String, 1385 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(render_after_separator(J.Arr{simple_values(values)}, SCon{punctuation_char(mark), SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation_char(mark)} <> List.append(&2, J.Lexeme, reverse_source_task(J.Arr{simple_values(values)}, RenderAfterSeparator{}), acc)) : List<&2, J.Lexeme>}: 1386 match values: 1387 case Nil{}: 1388 lex_close_before_punctuation(']', punctuation_char(mark), suffix, acc, {==}, punctuation_action(mark, suffix)) 1389 case head <> Nil{}: 1390 lex_array_after_separator_single_source(simple_value(head), punctuation_char(mark), suffix, acc, 1391 punctuation_action(mark, suffix), 1392 lex_simple_task_suffix_before_punctuation(head, RenderWhole{}, ']', SCon{punctuation_char(mark), SNil{}} ++ suffix, acc, {==})) 1393 case head <> next <> tail: 1394 lex_array_after_separator_many(simple_value(head), simple_value(next), simple_values(tail), 1395 punctuation_char(mark), suffix, acc, punctuation_action(mark, suffix), 1396 lex_simple_task_suffix_before_punctuation(head, RenderWhole{}, ',', 1397 render_after_separator(J.Arr{simple_value(next) <> simple_values(tail)}, SCon{punctuation_char(mark), SNil{}} ++ suffix), 1398 acc, {==}), 1399 lex_simple_array_after_separator(next <> tail, mark, suffix, 1400 J.Punctuation{','} <> List.append(&2, J.Lexeme, reverse_source_task(simple_value(head), RenderWhole{}), acc))) 1401 1402 def source_token_string(+text: String, 1403 +suffix: List<&2, J.Lexeme>, 1404 -tail: List) -> {token_source(J.source_text("\"" ++ J.escape_string(text) ++ "\"", suffix), tail) == token_string(text) <> token_source(suffix, tail) : List}: 1405 Equal.cong(Result<&1, &1, J.Error, J.Value>, List, result => J.Atom{result} <> token_source(suffix, tail), 1406 J.decode_payload("\"" ++ J.escape_string(text) ++ "\""), Done{J.Str{text}}, S.string_payload(text)) 1407 1408 def source_object_key_prefix(+delimiter: Char, 1409 +key: String, 1410 +suffix: List<&2, J.Lexeme>, 1411 -tail: List) -> {token_source(J.Punctuation{delimiter} <> J.source_text("\"" ++ J.escape_string(key) ++ "\"", suffix), tail) == J.Delimiter{delimiter} <> token_string(key) <> token_source(suffix, tail) : List}: 1412 Equal.trans(List, 1413 token_source(J.Punctuation{delimiter} <> J.source_text("\"" ++ J.escape_string(key) ++ "\"", suffix), tail), 1414 J.Delimiter{delimiter} <> token_source(J.source_text("\"" ++ J.escape_string(key) ++ "\"", suffix), tail), 1415 J.Delimiter{delimiter} <> token_string(key) <> token_source(suffix, tail), 1416 {==}, 1417 Equal.cong(List, List, xs => J.Delimiter{delimiter} <> xs, 1418 token_source(J.source_text("\"" ++ J.escape_string(key) ++ "\"", suffix), tail), 1419 token_string(key) <> token_source(suffix, tail), source_token_string(key, suffix, tail))) 1420 1421 def to_bool(mode: A.Mode) -> Bool: 1422 match mode: 1423 case A.Whole{}: False{} 1424 case A.Members{}: True{} 1425 1426 def canonical(value: J.Value, mode: A.Mode, tail: List) -> List: 1427 A.tokens(value, mode, tail) 1428 1429 def canonical_tokens(+value: J.Value, 1430 +mode: A.Mode, 1431 -tail: List) -> {canonical(value, mode, tail) == A.tokens(value, mode, tail) : List}: 1432 {==} 1433 1434 def source_tokens(+value: J.Value, 1435 +mode: A.Mode, 1436 +suffix: List<&2, J.Lexeme>, 1437 -tail: List) -> {token_source(J.source(value, to_bool(mode), suffix), tail) == canonical(value, mode, token_source(suffix, tail)) : List}: 1438 match value: 1439 case J.Null{}: {==} 1440 case J.Bool{truth}: 1441 match truth: 1442 case True{}: {==} 1443 case False{}: {==} 1444 case J.Number{lexeme, certificate}: {==} 1445 case J.Str{text}: {==} 1446 case J.Arr{values}: 1447 match values: 1448 case Nil{}: 1449 match mode: 1450 case A.Whole{}: {==} 1451 case A.Members{}: {==} 1452 case head <> rest: 1453 match mode: 1454 case A.Whole{}: 1455 Equal.trans(List, token_source(J.source(J.Arr{head <> rest}, False{}, suffix), tail), 1456 J.Delimiter{'['} <> canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)), 1457 canonical(J.Arr{head <> rest}, A.Whole{}, token_source(suffix, tail)), 1458 Equal.cong(List, List, xs => J.Delimiter{'['} <> xs, 1459 token_source(J.source(head, False{}, J.source(J.Arr{rest}, True{}, suffix)), tail), 1460 canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)), 1461 source_tokens(head, A.Whole{}, J.source(J.Arr{rest}, True{}, suffix), tail)), 1462 Equal.cong(List, List, xs => J.Delimiter{'['} <> canonical(head, A.Whole{}, xs), 1463 token_source(J.source(J.Arr{rest}, True{}, suffix), tail), canonical(J.Arr{rest}, A.Members{}, token_source(suffix, tail)), 1464 source_tokens(J.Arr{rest}, A.Members{}, suffix, tail))) 1465 case A.Members{}: 1466 Equal.trans(List, token_source(J.source(J.Arr{head <> rest}, True{}, suffix), tail), 1467 J.Delimiter{','} <> canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)), 1468 canonical(J.Arr{head <> rest}, A.Members{}, token_source(suffix, tail)), 1469 Equal.cong(List, List, xs => J.Delimiter{','} <> xs, 1470 token_source(J.source(head, False{}, J.source(J.Arr{rest}, True{}, suffix)), tail), 1471 canonical(head, A.Whole{}, token_source(J.source(J.Arr{rest}, True{}, suffix), tail)), 1472 source_tokens(head, A.Whole{}, J.source(J.Arr{rest}, True{}, suffix), tail)), 1473 Equal.cong(List, List, xs => J.Delimiter{','} <> canonical(head, A.Whole{}, xs), 1474 token_source(J.source(J.Arr{rest}, True{}, suffix), tail), canonical(J.Arr{rest}, A.Members{}, token_source(suffix, tail)), 1475 source_tokens(J.Arr{rest}, A.Members{}, suffix, tail))) 1476 case J.Obj{fields}: 1477 match fields: 1478 case Nil{}: 1479 match mode: 1480 case A.Whole{}: {==} 1481 case A.Members{}: {==} 1482 case (key, field_value) <> rest: 1483 match mode: 1484 case A.Whole{}: 1485 Equal.trans(List, token_source(J.source(J.Obj{(key, field_value) <> rest}, False{}, suffix), tail), 1486 J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), 1487 canonical(J.Obj{(key, field_value) <> rest}, A.Whole{}, token_source(suffix, tail)), 1488 source_object_key_prefix('{', key, J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), 1489 Equal.trans(List, 1490 J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), 1491 J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)), 1492 canonical(J.Obj{(key, field_value) <> rest}, A.Whole{}, token_source(suffix, tail)), 1493 Equal.cong(List, List, xs => J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> xs, 1494 token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), 1495 canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)), 1496 source_tokens(field_value, A.Whole{}, J.source(J.Obj{rest}, True{}, suffix), tail)), 1497 Equal.cong(List, List, xs => J.Delimiter{'{'} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, xs), 1498 token_source(J.source(J.Obj{rest}, True{}, suffix), tail), canonical(J.Obj{rest}, A.Members{}, token_source(suffix, tail)), 1499 source_tokens(J.Obj{rest}, A.Members{}, suffix, tail)))) 1500 case A.Members{}: 1501 Equal.trans(List, token_source(J.source(J.Obj{(key, field_value) <> rest}, True{}, suffix), tail), 1502 J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), 1503 canonical(J.Obj{(key, field_value) <> rest}, A.Members{}, token_source(suffix, tail)), 1504 source_object_key_prefix(',', key, J.Punctuation{':'} <> J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), 1505 Equal.trans(List, 1506 J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), 1507 J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)), 1508 canonical(J.Obj{(key, field_value) <> rest}, A.Members{}, token_source(suffix, tail)), 1509 Equal.cong(List, List, xs => J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> xs, 1510 token_source(J.source(field_value, False{}, J.source(J.Obj{rest}, True{}, suffix)), tail), 1511 canonical(field_value, A.Whole{}, token_source(J.source(J.Obj{rest}, True{}, suffix), tail)), 1512 source_tokens(field_value, A.Whole{}, J.source(J.Obj{rest}, True{}, suffix), tail)), 1513 Equal.cong(List, List, xs => J.Delimiter{','} <> token_string(key) <> J.Delimiter{':'} <> canonical(field_value, A.Whole{}, xs), 1514 token_source(J.source(J.Obj{rest}, True{}, suffix), tail), canonical(J.Obj{rest}, A.Members{}, token_source(suffix, tail)), 1515 source_tokens(J.Obj{rest}, A.Members{}, suffix, tail))))