1 import Base 2 import ../libs/JSON.bend as J 3 import ./JSON_StringProof.bend as S 4 5 def after_mode(action: J.LexAction, mode: J.LexMode) -> J.LexMode: 6 match action: 7 case J.LexBackslash{}: J.Escaped{} 8 case J.LexEscapedChar{}: J.Quoted{} 9 case J.LexStringEnd{}: J.Outside{} 10 case J.LexStringChar{}: J.Quoted{} 11 case J.LexQuote{}: J.Quoted{} 12 case J.LexWhitespace{}: J.Outside{} 13 case J.LexPunctuation{_}: J.Outside{} 14 case J.LexRaw{}: J.Outside{} 15 case J.LexStop{}: mode 16 17 def after_reversed(action: J.LexAction, head: Char, reversed: String) -> String: 18 match action: 19 case J.LexBackslash{}: SCon{'\\', reversed} 20 case J.LexEscapedChar{}: SCon{head, reversed} 21 case J.LexStringEnd{}: SNil{} 22 case J.LexStringChar{}: SCon{head, reversed} 23 case J.LexQuote{}: SCon{'"', SNil{}} 24 case J.LexWhitespace{}: SNil{} 25 case J.LexPunctuation{_}: SNil{} 26 case J.LexRaw{}: SCon{head, reversed} 27 case J.LexStop{}: SCon{head, reversed} 28 29 def after_acc(action: J.LexAction, 30 head: Char, 31 reversed: String, 32 acc: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>: 33 match action: 34 case J.LexBackslash{}: acc 35 case J.LexEscapedChar{}: acc 36 case J.LexStringEnd{}: J.Payload{String.reverse(SCon{'"', reversed})} <> acc 37 case J.LexStringChar{}: acc 38 case J.LexQuote{}: J.flush_lexeme(reversed, acc) 39 case J.LexWhitespace{}: J.flush_lexeme(reversed, acc) 40 case J.LexPunctuation{character}: J.Punctuation{character} <> J.flush_lexeme(reversed, acc) 41 case J.LexRaw{}: acc 42 case J.LexStop{}: acc 43 44 def lexemes_step(+head: Char, 45 +tail: String, 46 +mode: J.LexMode, 47 +reversed: String, 48 +acc: List<&2, J.Lexeme>, 49 action: J.LexAction) -> {J.lexemes(SCon{head, tail}, mode, reversed, acc, action) == J.lex_scan(tail, after_mode(action, mode), after_reversed(action, head, reversed), after_acc(action, head, reversed, acc)) : List<&2, J.Lexeme>}: 50 match action: 51 case J.LexStop{}: {==} 52 case J.LexEscapedChar{}: {==} 53 case J.LexBackslash{}: {==} 54 case J.LexStringEnd{}: {==} 55 case J.LexStringChar{}: {==} 56 case J.LexQuote{}: {==} 57 case J.LexWhitespace{}: {==} 58 case J.LexPunctuation{character}: {==} 59 case J.LexRaw{}: {==} 60 61 def lex_scan_step(+head: Char, 62 +tail: String, 63 +mode: J.LexMode, 64 +reversed: String, 65 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(SCon{head, tail}, mode, reversed, acc) == J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)) : List<&2, J.Lexeme>}: 66 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail}, mode, reversed, acc), 67 J.lexemes(SCon{head, tail}, mode, reversed, acc, J.lex_seed_action(SCon{head, tail}, mode)), 68 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 69 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 70 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 71 {==}, lexemes_step(head, tail, mode, reversed, acc, J.lex_seed_action(SCon{head, tail}, mode))) 72 73 def prefix_mode(text: String, +mode: J.LexMode) -> J.LexMode: 74 match text: 75 case SNil{}: mode 76 case SCon{+head, +tail}: 77 prefix_mode(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode)) 78 79 def prefix_reversed(text: String, +mode: J.LexMode, +reversed: String) -> String: 80 match text: 81 case SNil{}: reversed 82 case SCon{+head, +tail}: 83 prefix_reversed(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 84 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed)) 85 86 def prefix_acc(text: String, 87 +mode: J.LexMode, 88 +reversed: String, 89 +acc: List<&2, J.Lexeme>) -> List<&2, J.Lexeme>: 90 match text: 91 case SNil{}: acc 92 case SCon{+head, +tail}: 93 prefix_acc(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 94 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 95 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)) 96 97 def prefix_mode_append(+text: String, 98 +suffix: String, 99 +mode: J.LexMode) -> {prefix_mode(text ++ suffix, mode) == prefix_mode(suffix, prefix_mode(text, mode)) : J.LexMode}: 100 match text: 101 case SNil{}: {==} 102 case SCon{head, tail}: 103 prefix_mode_append(tail, suffix, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode)) 104 105 def prefix_reversed_append(+text: String, 106 +suffix: String, 107 +mode: J.LexMode, 108 +reversed: String) -> {prefix_reversed(text ++ suffix, mode, reversed) == prefix_reversed(suffix, prefix_mode(text, mode), prefix_reversed(text, mode, reversed)) : String}: 109 match text: 110 case SNil{}: {==} 111 case SCon{head, tail}: 112 prefix_reversed_append(tail, suffix, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 113 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed)) 114 115 def prefix_acc_append(+text: String, 116 +suffix: String, 117 +mode: J.LexMode, 118 +reversed: String, 119 +acc: List<&2, J.Lexeme>) -> {prefix_acc(text ++ suffix, mode, reversed, acc) == prefix_acc(suffix, prefix_mode(text, mode), prefix_reversed(text, mode, reversed), prefix_acc(text, mode, reversed, acc)) : List<&2, J.Lexeme>}: 120 match text: 121 case SNil{}: {==} 122 case SCon{head, tail}: 123 prefix_acc_append(tail, suffix, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 124 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 125 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)) 126 127 def lex_scan_append(+text: String, 128 +suffix: String, 129 +mode: J.LexMode, 130 +reversed: String, 131 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(text ++ suffix, mode, reversed, acc) == J.lex_scan(suffix, prefix_mode(text, mode), prefix_reversed(text, mode, reversed), prefix_acc(text, mode, reversed, acc)) : List<&2, J.Lexeme>}: 132 match text: 133 case SNil{}: {==} 134 case SCon{head, tail}: 135 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ suffix, mode, reversed, acc), 136 J.lex_scan(tail ++ suffix, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 137 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 138 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 139 J.lex_scan(suffix, prefix_mode(SCon{head, tail}, mode), prefix_reversed(SCon{head, tail}, mode, reversed), 140 prefix_acc(SCon{head, tail}, mode, reversed, acc)), 141 lex_scan_step(head, tail ++ suffix, mode, reversed, acc), 142 lex_scan_append(tail, suffix, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 143 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 144 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc))) 145 146 def lex_scan_context(+text: String, 147 +mode1: J.LexMode, 148 +reversed1: String, 149 +acc1: List<&2, J.Lexeme>, 150 +mode2: J.LexMode, 151 +reversed2: String, 152 +acc2: List<&2, J.Lexeme>, 153 mode_eq: {mode1 == mode2 : J.LexMode}, 154 reversed_eq: {reversed1 == reversed2 : String}, 155 acc_eq: {acc1 == acc2 : List<&2, J.Lexeme>}) -> {J.lex_scan(text, mode1, reversed1, acc1) == J.lex_scan(text, mode2, reversed2, acc2) : List<&2, J.Lexeme>}: 156 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, mode1, reversed1, acc1), 157 J.lex_scan(text, mode2, reversed1, acc1), J.lex_scan(text, mode2, reversed2, acc2), 158 Equal.cong(J.LexMode, List<&2, J.Lexeme>, mode => J.lex_scan(text, mode, reversed1, acc1), mode1, mode2, mode_eq), 159 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(text, mode2, reversed1, acc1), 160 J.lex_scan(text, mode2, reversed2, acc1), J.lex_scan(text, mode2, reversed2, acc2), 161 Equal.cong(String, List<&2, J.Lexeme>, reversed => J.lex_scan(text, mode2, reversed, acc1), 162 reversed1, reversed2, reversed_eq), 163 Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, acc => J.lex_scan(text, mode2, reversed2, acc), 164 acc1, acc2, acc_eq))) 165 166 def scan_punctuation_char(+character: Char, 167 +tail: String, 168 +reversed: String, 169 +acc: List<&2, J.Lexeme>, 170 action: {J.lex_seed_action(SCon{character, tail}, J.Outside{}) == J.LexPunctuation{character} : J.LexAction}) -> {J.lex_scan(SCon{character, tail}, J.Outside{}, reversed, acc) == J.lex_scan(tail, J.Outside{}, SNil{}, J.Punctuation{character} <> J.flush_lexeme(reversed, acc)) : List<&2, J.Lexeme>}: 171 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{character, tail}, J.Outside{}, reversed, acc), 172 J.lex_scan(tail, after_mode(J.LexPunctuation{character}, J.Outside{}), 173 after_reversed(J.LexPunctuation{character}, character, reversed), 174 after_acc(J.LexPunctuation{character}, character, reversed, acc)), 175 J.lex_scan(tail, J.Outside{}, SNil{}, J.Punctuation{character} <> J.flush_lexeme(reversed, acc)), 176 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{character, tail}, J.Outside{}, reversed, acc), 177 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{character, tail}, J.Outside{}), J.Outside{}), 178 after_reversed(J.lex_seed_action(SCon{character, tail}, J.Outside{}), character, reversed), 179 after_acc(J.lex_seed_action(SCon{character, tail}, J.Outside{}), character, reversed, acc)), 180 J.lex_scan(tail, after_mode(J.LexPunctuation{character}, J.Outside{}), 181 after_reversed(J.LexPunctuation{character}, character, reversed), 182 after_acc(J.LexPunctuation{character}, character, reversed, acc)), 183 lex_scan_step(character, tail, J.Outside{}, reversed, acc), 184 Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lex_scan(tail, after_mode(action, J.Outside{}), 185 after_reversed(action, character, reversed), after_acc(action, character, reversed, acc)), 186 J.lex_seed_action(SCon{character, tail}, J.Outside{}), J.LexPunctuation{character}, action)), 187 {==}) 188 189 def raw_string_seed(+character: Char, 190 +tail: String, 191 classifier: {J.Raw{} == J.escape_class(character) : J.EscapeClass}) -> {J.lex_seed_action(SCon{character, tail}, J.Quoted{}) == J.LexStringChar{} : J.LexAction}: 192 Equal.trans(J.LexAction, J.lex_seed_action(SCon{character, tail}, J.Quoted{}), 193 J.quote_lex_action(J.quote_action_from_class(J.escape_class(character))), J.LexStringChar{}, 194 {==}, 195 Equal.cong(J.EscapeClass, J.LexAction, class => J.quote_lex_action(J.quote_action_from_class(class)), 196 J.escape_class(character), J.Raw{}, Equal.sym(J.EscapeClass, J.Raw{}, J.escape_class(character), classifier))) 197 198 def scan_raw_string_char(+character: Char, 199 +tail: String, 200 +reversed: String, 201 +acc: List<&2, J.Lexeme>, 202 classifier: {J.Raw{} == J.escape_class(character) : J.EscapeClass}) -> {J.lex_scan(SCon{character, tail}, J.Quoted{}, reversed, acc) == J.lex_scan(tail, J.Quoted{}, SCon{character, reversed}, acc) : List<&2, J.Lexeme>}: 203 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{character, tail}, J.Quoted{}, reversed, acc), 204 J.lex_scan(tail, after_mode(J.LexStringChar{}, J.Quoted{}), after_reversed(J.LexStringChar{}, character, reversed), after_acc(J.LexStringChar{}, character, reversed, acc)), 205 J.lex_scan(tail, J.Quoted{}, SCon{character, reversed}, acc), 206 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{character, tail}, J.Quoted{}, reversed, acc), 207 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{character, tail}, J.Quoted{}), J.Quoted{}), 208 after_reversed(J.lex_seed_action(SCon{character, tail}, J.Quoted{}), character, reversed), 209 after_acc(J.lex_seed_action(SCon{character, tail}, J.Quoted{}), character, reversed, acc)), 210 J.lex_scan(tail, after_mode(J.LexStringChar{}, J.Quoted{}), after_reversed(J.LexStringChar{}, character, reversed), after_acc(J.LexStringChar{}, character, reversed, acc)), 211 lex_scan_step(character, tail, J.Quoted{}, reversed, acc), 212 Equal.cong(J.LexAction, List<&2, J.Lexeme>, action => J.lex_scan(tail, after_mode(action, J.Quoted{}), after_reversed(action, character, reversed), after_acc(action, character, reversed, acc)), 213 J.lex_seed_action(SCon{character, tail}, J.Quoted{}), J.LexStringChar{}, raw_string_seed(character, tail, classifier))), 214 {==}) 215 216 def scan_escape_char(+character: Char, 217 +tail: String, 218 +reversed: String, 219 +acc: List<&2, J.Lexeme>, 220 +class: J.EscapeClass, 221 classifier: {class == J.escape_class(character) : J.EscapeClass}) -> {J.lex_scan(J.escape_char_from_class(character, class) ++ tail, J.Quoted{}, reversed, acc) == J.lex_scan(tail, J.Quoted{}, String.reverse(J.escape_char_from_class(character, class)) ++ reversed, acc) : List<&2, J.Lexeme>}: 222 match class: 223 case J.Raw{}: 224 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(J.escape_char_from_class(character, J.Raw{}) ++ tail, J.Quoted{}, reversed, acc), 225 J.lex_scan(SCon{character, tail}, J.Quoted{}, reversed, acc), 226 J.lex_scan(tail, J.Quoted{}, SCon{character, reversed}, acc), 227 Equal.cong(String, List<&2, J.Lexeme>, text => J.lex_scan(text, J.Quoted{}, reversed, acc), 228 J.escape_char_from_class(character, J.Raw{}) ++ tail, SCon{character, tail}, {==}), 229 scan_raw_string_char(character, tail, reversed, acc, classifier)) 230 case J.Backslash{}: {==} 231 case J.Quote{}: {==} 232 case J.Control0{}: {==} 233 case J.Control1{}: {==} 234 case J.Control2{}: {==} 235 case J.Control3{}: {==} 236 case J.Control4{}: {==} 237 case J.Control5{}: {==} 238 case J.Control6{}: {==} 239 case J.Control7{}: {==} 240 case J.Control8{}: {==} 241 case J.Control9{}: {==} 242 case J.Control10{}: {==} 243 case J.Control11{}: {==} 244 case J.Control12{}: {==} 245 case J.Control13{}: {==} 246 case J.Control14{}: {==} 247 case J.Control15{}: {==} 248 case J.Control16{}: {==} 249 case J.Control17{}: {==} 250 case J.Control18{}: {==} 251 case J.Control19{}: {==} 252 case J.Control20{}: {==} 253 case J.Control21{}: {==} 254 case J.Control22{}: {==} 255 case J.Control23{}: {==} 256 case J.Control24{}: {==} 257 case J.Control25{}: {==} 258 case J.Control26{}: {==} 259 case J.Control27{}: {==} 260 case J.Control28{}: {==} 261 case J.Control29{}: {==} 262 case J.Control30{}: {==} 263 case J.Control31{}: {==} 264 265 def escape_reverse(text: String, reversed: String) -> String: 266 match text: 267 case SNil{}: reversed 268 case SCon{head, tail}: 269 escape_reverse(tail, String.reverse(J.escape_char(head)) ++ reversed) 270 271 def escape_reverse_shape(+text: String, 272 +reversed: String) -> {String.reverse(escape_reverse(text, reversed)) == String.reverse(reversed) ++ J.escape_string(text) : String}: 273 match text: 274 case SNil{}: Equal.sym(String, String.reverse(reversed) ++ J.escape_string(SNil{}), String.reverse(reversed), S.append_nil(String.reverse(reversed))) 275 case SCon{head, tail}: 276 Equal.trans(String, 277 String.reverse(escape_reverse(tail, String.reverse(J.escape_char(head)) ++ reversed)), 278 String.reverse(String.reverse(J.escape_char(head)) ++ reversed) ++ J.escape_string(tail), 279 String.reverse(reversed) ++ J.escape_string(SCon{head, tail}), 280 escape_reverse_shape(tail, String.reverse(J.escape_char(head)) ++ reversed), 281 Equal.trans(String, 282 String.reverse(String.reverse(J.escape_char(head)) ++ reversed) ++ J.escape_string(tail), 283 (String.reverse(reversed) ++ String.reverse(String.reverse(J.escape_char(head)))) ++ J.escape_string(tail), 284 String.reverse(reversed) ++ (J.escape_char(head) ++ J.escape_string(tail)), 285 Equal.cong(String, String, value => value ++ J.escape_string(tail), 286 String.reverse(String.reverse(J.escape_char(head)) ++ reversed), 287 String.reverse(reversed) ++ String.reverse(String.reverse(J.escape_char(head))), 288 S.reverse_append(String.reverse(J.escape_char(head)), reversed)), 289 Equal.trans(String, 290 (String.reverse(reversed) ++ String.reverse(String.reverse(J.escape_char(head)))) ++ J.escape_string(tail), 291 String.reverse(reversed) ++ (String.reverse(String.reverse(J.escape_char(head))) ++ J.escape_string(tail)), 292 String.reverse(reversed) ++ (J.escape_char(head) ++ J.escape_string(tail)), 293 S.append_assoc(String.reverse(reversed), String.reverse(String.reverse(J.escape_char(head))), J.escape_string(tail)), 294 Equal.cong(String, String, value => String.reverse(reversed) ++ (value ++ J.escape_string(tail)), 295 String.reverse(String.reverse(J.escape_char(head))), J.escape_char(head), S.reverse_twice(J.escape_char(head)))))) 296 297 def scan_escape_string(+text: String, 298 +suffix: String, 299 +reversed: String, 300 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(J.escape_string(text) ++ suffix, J.Quoted{}, reversed, acc) == J.lex_scan(suffix, J.Quoted{}, escape_reverse(text, reversed), acc) : List<&2, J.Lexeme>}: 301 match text: 302 case SNil{}: {==} 303 case SCon{+head, +tail}: 304 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(J.escape_string(text) ++ suffix, J.Quoted{}, reversed, acc), 305 J.lex_scan(J.escape_char(head) ++ (J.escape_string(tail) ++ suffix), J.Quoted{}, reversed, acc), 306 J.lex_scan(suffix, J.Quoted{}, escape_reverse(text, reversed), acc), 307 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Quoted{}, reversed, acc), 308 J.escape_string(text) ++ suffix, J.escape_char(head) ++ (J.escape_string(tail) ++ suffix), 309 S.append_assoc(J.escape_char(head), J.escape_string(tail), suffix)), 310 Equal.trans(List<&2, J.Lexeme>, 311 J.lex_scan(J.escape_char(head) ++ (J.escape_string(tail) ++ suffix), J.Quoted{}, reversed, acc), 312 J.lex_scan(J.escape_string(tail) ++ suffix, J.Quoted{}, String.reverse(J.escape_char(head)) ++ reversed, acc), 313 J.lex_scan(suffix, J.Quoted{}, escape_reverse(text, reversed), acc), 314 scan_escape_char(head, J.escape_string(tail) ++ suffix, reversed, acc, J.escape_class(head), {==}), 315 scan_escape_string(tail, suffix, String.reverse(J.escape_char(head)) ++ reversed, acc))) 316 317 def quoted_buffer_payload(+text: String) -> {String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})}) == SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}} : String}: 318 Equal.trans(String, 319 String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})}), 320 String.reverse(escape_reverse(text, SCon{'"', SNil{}})) ++ SCon{'"', SNil{}}, 321 SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, 322 S.reverse_cons('"', escape_reverse(text, SCon{'"', SNil{}})), 323 Equal.trans(String, 324 String.reverse(escape_reverse(text, SCon{'"', SNil{}})) ++ SCon{'"', SNil{}}, 325 (SCon{'"', SNil{}} ++ J.escape_string(text)) ++ SCon{'"', SNil{}}, 326 SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, 327 Equal.cong(String, String, value => value ++ SCon{'"', SNil{}}, 328 String.reverse(escape_reverse(text, SCon{'"', SNil{}})), 329 SCon{'"', SNil{}} ++ J.escape_string(text), 330 escape_reverse_shape(text, SCon{'"', SNil{}})), 331 S.append_assoc(SCon{'"', SNil{}}, J.escape_string(text), SCon{'"', SNil{}}))) 332 333 def lex_rendered_string(+text: String) -> {J.lex_scan(SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, J.Outside{}, SNil{}, Nil{}) == J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> Nil{} : List<&2, J.Lexeme>}: 334 Equal.trans(List<&2, J.Lexeme>, 335 J.lex_scan(SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, J.Outside{}, SNil{}, Nil{}), 336 J.lex_scan(J.escape_string(text) ++ SCon{'"', SNil{}}, J.Quoted{}, SCon{'"', SNil{}}, Nil{}), 337 J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> Nil{}, 338 lex_scan_step('"', J.escape_string(text) ++ SCon{'"', SNil{}}, J.Outside{}, SNil{}, Nil{}), 339 Equal.trans(List<&2, J.Lexeme>, 340 J.lex_scan(J.escape_string(text) ++ SCon{'"', SNil{}}, J.Quoted{}, SCon{'"', SNil{}}, Nil{}), 341 J.lex_scan(SCon{'"', SNil{}}, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), Nil{}), 342 J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> Nil{}, 343 scan_escape_string(text, SCon{'"', SNil{}}, SCon{'"', SNil{}}, Nil{}), 344 Equal.trans(List<&2, J.Lexeme>, 345 J.lex_scan(SCon{'"', SNil{}}, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), Nil{}), 346 J.Payload{String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})})} <> Nil{}, 347 J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> Nil{}, 348 lex_scan_step('"', SNil{}, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), Nil{}), 349 Equal.cong(String, List<&2, J.Lexeme>, payload => J.Payload{payload} <> Nil{}, 350 String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})}), 351 SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, quoted_buffer_payload(text))))) 352 353 def lex_rendered_string_suffix(+text: String, 354 +suffix: String, 355 +acc: List<&2, J.Lexeme>) -> {J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ suffix, J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc) : List<&2, J.Lexeme>}: 356 Equal.trans(List<&2, J.Lexeme>, 357 J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ suffix, J.Outside{}, SNil{}, acc), 358 J.lex_scan(SCon{'"', (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix}, J.Outside{}, SNil{}, acc), 359 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc), 360 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Outside{}, SNil{}, acc), 361 (SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ suffix, 362 SCon{'"', (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix}, {==}), 363 Equal.trans(List<&2, J.Lexeme>, 364 J.lex_scan(SCon{'"', (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix}, J.Outside{}, SNil{}, acc), 365 J.lex_scan((J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix, J.Quoted{}, SCon{'"', SNil{}}, acc), 366 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc), 367 lex_scan_step('"', (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix, J.Outside{}, SNil{}, acc), 368 Equal.trans(List<&2, J.Lexeme>, 369 J.lex_scan((J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix, J.Quoted{}, SCon{'"', SNil{}}, acc), 370 J.lex_scan(J.escape_string(text) ++ (SCon{'"', SNil{}} ++ suffix), J.Quoted{}, SCon{'"', SNil{}}, acc), 371 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc), 372 Equal.cong(String, List<&2, J.Lexeme>, source => J.lex_scan(source, J.Quoted{}, SCon{'"', SNil{}}, acc), 373 (J.escape_string(text) ++ SCon{'"', SNil{}}) ++ suffix, 374 J.escape_string(text) ++ (SCon{'"', SNil{}} ++ suffix), 375 S.append_assoc(J.escape_string(text), SCon{'"', SNil{}}, suffix)), 376 Equal.trans(List<&2, J.Lexeme>, 377 J.lex_scan(J.escape_string(text) ++ (SCon{'"', SNil{}} ++ suffix), J.Quoted{}, SCon{'"', SNil{}}, acc), 378 J.lex_scan(SCon{'"', SNil{}} ++ suffix, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), acc), 379 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc), 380 scan_escape_string(text, SCon{'"', SNil{}} ++ suffix, SCon{'"', SNil{}}, acc), 381 Equal.trans(List<&2, J.Lexeme>, 382 J.lex_scan(SCon{'"', SNil{}} ++ suffix, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), acc), 383 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})})} <> acc), 384 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc), 385 lex_scan_step('"', suffix, J.Quoted{}, escape_reverse(text, SCon{'"', SNil{}}), acc), 386 Equal.cong(String, List<&2, J.Lexeme>, payload => J.lex_scan(suffix, J.Outside{}, SNil{}, J.Payload{payload} <> acc), 387 String.reverse(SCon{'"', escape_reverse(text, SCon{'"', SNil{}})}), 388 SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}, quoted_buffer_payload(text))))))) 389 390 def lex_string_before_punctuation(+text: String, 391 +punctuation: Char, 392 +suffix: String, 393 +acc: List<&2, J.Lexeme>, 394 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, (J.Punctuation{punctuation} <> J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc)) : List<&2, J.Lexeme>}: 395 Equal.trans(List<&2, J.Lexeme>, 396 J.lex_scan((SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}) ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 397 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc), 398 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc), 399 lex_rendered_string_suffix(text, SCon{punctuation, SNil{}} ++ suffix, acc), 400 scan_punctuation_char(punctuation, suffix, SNil{}, J.Payload{SCon{'"', J.escape_string(text) ++ SCon{'"', SNil{}}}} <> acc, action)) 401 402 def lex_null_before_punctuation(+punctuation: Char, 403 +suffix: String, 404 +acc: List<&2, J.Lexeme>, 405 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan("null" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{"null"} <> acc) : List<&2, J.Lexeme>}: 406 Equal.trans(List<&2, J.Lexeme>, 407 J.lex_scan("null" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 408 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, "llun", acc), 409 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{"null"} <> acc), 410 {==}, 411 scan_punctuation_char(punctuation, suffix, "llun", acc, action)) 412 413 def lex_true_before_punctuation(+punctuation: Char, 414 +suffix: String, 415 +acc: List<&2, J.Lexeme>, 416 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan("true" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{"true"} <> acc) : List<&2, J.Lexeme>}: 417 Equal.trans(List<&2, J.Lexeme>, 418 J.lex_scan("true" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 419 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, "eurt", acc), 420 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{"true"} <> acc), 421 {==}, 422 scan_punctuation_char(punctuation, suffix, "eurt", acc, action)) 423 424 def lex_false_before_punctuation(+punctuation: Char, 425 +suffix: String, 426 +acc: List<&2, J.Lexeme>, 427 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan("false" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc) == J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{"false"} <> acc) : List<&2, J.Lexeme>}: 428 Equal.trans(List<&2, J.Lexeme>, 429 J.lex_scan("false" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 430 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, "eslaf", acc), 431 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Payload{"false"} <> acc), 432 {==}, 433 scan_punctuation_char(punctuation, suffix, "eslaf", acc, action)) 434 435 def lex_empty_array_before_punctuation(+punctuation: Char, 436 +suffix: String, 437 +acc: List<&2, J.Lexeme>, 438 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan("[]" ++ (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>}: 439 Equal.trans(List<&2, J.Lexeme>, J.lex_scan("[]" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 440 J.lex_scan(SCon{']', SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}, SNil{}, J.Punctuation{'['} <> acc), 441 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> J.Punctuation{'['} <> acc), 442 scan_punctuation_char('[', SCon{']', SCon{punctuation, SNil{}} ++ suffix}, SNil{}, acc, {==}), 443 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{']', SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}, SNil{}, J.Punctuation{'['} <> acc), 444 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{']'} <> J.Punctuation{'['} <> acc), 445 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{']'} <> J.Punctuation{'['} <> acc), 446 scan_punctuation_char(']', SCon{punctuation, SNil{}} ++ suffix, SNil{}, J.Punctuation{'['} <> acc, {==}), 447 scan_punctuation_char(punctuation, suffix, SNil{}, J.Punctuation{']'} <> J.Punctuation{'['} <> acc, action))) 448 449 def lex_empty_object_before_punctuation(+punctuation: Char, 450 +suffix: String, 451 +acc: List<&2, J.Lexeme>, 452 action: {J.lex_seed_action(SCon{punctuation, suffix}, J.Outside{}) == J.LexPunctuation{punctuation} : J.LexAction}) -> {J.lex_scan("{}" ++ (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>}: 453 Equal.trans(List<&2, J.Lexeme>, J.lex_scan("{}" ++ (SCon{punctuation, SNil{}} ++ suffix), J.Outside{}, SNil{}, acc), 454 J.lex_scan(SCon{'}', SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}, SNil{}, J.Punctuation{'{'} <> acc), 455 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{'}'} <> J.Punctuation{'{'} <> acc), 456 scan_punctuation_char('{', SCon{'}', SCon{punctuation, SNil{}} ++ suffix}, SNil{}, acc, {==}), 457 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{'}', SCon{punctuation, SNil{}} ++ suffix}, J.Outside{}, SNil{}, J.Punctuation{'{'} <> acc), 458 J.lex_scan(SCon{punctuation, SNil{}} ++ suffix, J.Outside{}, SNil{}, J.Punctuation{'}'} <> J.Punctuation{'{'} <> acc), 459 J.lex_scan(suffix, J.Outside{}, SNil{}, J.Punctuation{punctuation} <> J.Punctuation{'}'} <> J.Punctuation{'{'} <> acc), 460 scan_punctuation_char('}', SCon{punctuation, SNil{}} ++ suffix, SNil{}, J.Punctuation{'{'} <> acc, {==}), 461 scan_punctuation_char(punctuation, suffix, SNil{}, J.Punctuation{'}'} <> J.Punctuation{'{'} <> acc, action))) 462 463 def trailing_space(+text: String, 464 +mode: J.LexMode, 465 +reversed: String, 466 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(text ++ " ", mode, reversed, acc) == J.lex_scan(text, mode, reversed, acc) : List<&2, J.Lexeme>}: 467 match text: 468 case SNil{}: 469 match mode: 470 case J.Outside{}: {==} 471 case J.Quoted{}: {==} 472 case J.Escaped{}: {==} 473 case SCon{head, tail}: 474 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ " ", mode, reversed, acc), 475 J.lex_scan(tail ++ " ", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 476 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 477 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 478 J.lex_scan(SCon{head, tail}, mode, reversed, acc), 479 lex_scan_step(head, tail ++ " ", mode, reversed, acc), 480 Equal.trans(List<&2, J.Lexeme>, 481 J.lex_scan(tail ++ " ", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 482 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 483 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 484 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 485 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 486 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 487 J.lex_scan(SCon{head, tail}, mode, reversed, acc), 488 trailing_space(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 489 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 490 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 491 Equal.sym(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail}, mode, reversed, acc), 492 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 493 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 494 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 495 lex_scan_step(head, tail, mode, reversed, acc)))) 496 497 def trailing_tab(+text: String, 498 +mode: J.LexMode, 499 +reversed: String, 500 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(text ++ "\t", mode, reversed, acc) == J.lex_scan(text, mode, reversed, acc) : List<&2, J.Lexeme>}: 501 match text: 502 case SNil{}: 503 match mode: 504 case J.Outside{}: {==} 505 case J.Quoted{}: {==} 506 case J.Escaped{}: {==} 507 case SCon{head, tail}: 508 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ "\t", mode, reversed, acc), 509 J.lex_scan(tail ++ "\t", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 510 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 511 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 512 J.lex_scan(SCon{head, tail}, mode, reversed, acc), 513 lex_scan_step(head, tail ++ "\t", mode, reversed, acc), 514 Equal.trans(List<&2, J.Lexeme>, 515 J.lex_scan(tail ++ "\t", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 516 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 517 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 518 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 519 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 520 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 521 J.lex_scan(SCon{head, tail}, mode, reversed, acc), 522 trailing_tab(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 523 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 524 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 525 Equal.sym(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail}, mode, reversed, acc), 526 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 527 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 528 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 529 lex_scan_step(head, tail, mode, reversed, acc)))) 530 531 def trailing_return(+text: String, 532 +mode: J.LexMode, 533 +reversed: String, 534 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(text ++ "\r", mode, reversed, acc) == J.lex_scan(text, mode, reversed, acc) : List<&2, J.Lexeme>}: 535 match text: 536 case SNil{}: 537 match mode: 538 case J.Outside{}: {==} 539 case J.Quoted{}: {==} 540 case J.Escaped{}: {==} 541 case SCon{head, tail}: 542 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ "\r", mode, reversed, acc), 543 J.lex_scan(tail ++ "\r", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 544 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 545 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 546 J.lex_scan(SCon{head, tail}, mode, reversed, acc), 547 lex_scan_step(head, tail ++ "\r", mode, reversed, acc), 548 Equal.trans(List<&2, J.Lexeme>, 549 J.lex_scan(tail ++ "\r", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 550 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 551 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 552 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 553 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 554 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 555 J.lex_scan(SCon{head, tail}, mode, reversed, acc), 556 trailing_return(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 557 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 558 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 559 Equal.sym(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail}, mode, reversed, acc), 560 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 561 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 562 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 563 lex_scan_step(head, tail, mode, reversed, acc)))) 564 565 def trailing_newline(+text: String, 566 +mode: J.LexMode, 567 +reversed: String, 568 +acc: List<&2, J.Lexeme>) -> {J.lex_scan(text ++ "\n", mode, reversed, acc) == J.lex_scan(text, mode, reversed, acc) : List<&2, J.Lexeme>}: 569 match text: 570 case SNil{}: 571 match mode: 572 case J.Outside{}: {==} 573 case J.Quoted{}: {==} 574 case J.Escaped{}: {==} 575 case SCon{head, tail}: 576 Equal.trans(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail} ++ "\n", mode, reversed, acc), 577 J.lex_scan(tail ++ "\n", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 578 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 579 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 580 J.lex_scan(SCon{head, tail}, mode, reversed, acc), 581 lex_scan_step(head, tail ++ "\n", mode, reversed, acc), 582 Equal.trans(List<&2, J.Lexeme>, 583 J.lex_scan(tail ++ "\n", after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 584 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 585 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 586 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 587 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 588 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 589 J.lex_scan(SCon{head, tail}, mode, reversed, acc), 590 trailing_newline(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 591 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 592 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 593 Equal.sym(List<&2, J.Lexeme>, J.lex_scan(SCon{head, tail}, mode, reversed, acc), 594 J.lex_scan(tail, after_mode(J.lex_seed_action(SCon{head, tail}, mode), mode), 595 after_reversed(J.lex_seed_action(SCon{head, tail}, mode), head, reversed), 596 after_acc(J.lex_seed_action(SCon{head, tail}, mode), head, reversed, acc)), 597 lex_scan_step(head, tail, mode, reversed, acc))))