@@ -372,26 +372,85 @@ module BindingStringParser<BindingStringReaderSig BindingStringReader> {
372
372
this = MkDoubleQuoteToken ( _, _, _, result )
373
373
}
374
374
375
- Token getNext ( ) {
376
- result .getBegin ( ) = this .getEnd ( ) + 1 and
377
- result .getReader ( ) = this .getReader ( )
375
+ /**
376
+ * Gets the next contiguous token after the end of this token.
377
+ */
378
+ Token getNextAfterEnd ( ) {
379
+ // Find the last contained token, then get the next token after that
380
+ result = getNextAfterContained ( ) and
381
+ // Ensure contiguous tokens
382
+ consecutiveToken ( this , result )
378
383
}
379
384
380
- predicate isFirst ( ) {
381
- not exists ( Token other |
382
- other .getBegin ( ) < this .getBegin ( ) and other .getReader ( ) = this .getReader ( )
385
+ bindingset [ t1, t2]
386
+ pragma [ inline_late]
387
+ private predicate consecutiveToken ( Token t1 , Token t2 ) { t1 .getEnd ( ) + 1 = t2 .getBegin ( ) }
388
+
389
+ /**
390
+ * Gets the next token that occurs after the start of this token.
391
+ */
392
+ private Token getNext ( ) {
393
+ exists ( int pos |
394
+ tokenOrdering ( this .getReader ( ) , this , pos ) and
395
+ tokenOrdering ( this .getReader ( ) , result , pos + uniqueTokensAtPosition ( this .getReader ( ) , pos ) )
383
396
)
384
397
}
385
398
399
+ /**
400
+ * Get the last token contained by this token.
401
+ */
402
+ pragma [ noinline]
403
+ private Token getNextAfterContained ( ) {
404
+ exists ( Token lastToken |
405
+ contains ( lastToken ) and
406
+ result = lastToken .getNext ( ) and
407
+ not contains ( result )
408
+ )
409
+ }
410
+
411
+ predicate isFirst ( ) { tokenOrdering ( this .getReader ( ) , this , 1 ) }
412
+
386
413
predicate contains ( Token t ) {
387
- this .getReader ( ) = t .getReader ( ) and
388
- this .getBegin ( ) < t .getBegin ( ) and
389
- this .getEnd ( ) > t .getEnd ( )
414
+ // base case, every token contains itself
415
+ t = this
416
+ or
417
+ // Recursive case, find an existing token contained by this token, and determine whether the next token is
418
+ // contained
419
+ exists ( Token prev |
420
+ this .contains ( prev ) and
421
+ prev .getNext ( ) = t and
422
+ // In the case of overlapping ranges, report tokens that begin inside this token as "contained"
423
+ this .getEnd ( ) >= t .getBegin ( )
424
+ )
390
425
}
391
426
392
427
stdlib:: Location getLocation ( ) { result = getReader ( ) .getLocation ( ) }
393
428
}
394
429
430
+ /**
431
+ * Holds if `t` is ordered at `position` according to the location of the beginning of the token.
432
+ *
433
+ * Note: `position` is not contiguous as certain strings may be matched by multiple tokens. In this
434
+ * case those tokens will all have the same `position`, and the subsequent token will have
435
+ * `position + count(tokens_with_current_position)`.
436
+ */
437
+ private predicate tokenOrdering ( BindingStringReader reader , Token t , int position ) {
438
+ t =
439
+ rank [ position ] ( Token token |
440
+ token .getReader ( ) = reader
441
+ |
442
+ token order by token .getBegin ( ) , token .getEnd ( )
443
+ )
444
+ }
445
+
446
+ /**
447
+ * Identify how many tokens are at a given position in the ordering, i.e. have the same beginning and end.
448
+ */
449
+ private int uniqueTokensAtPosition ( BindingStringReader reader , int position ) {
450
+ tokenOrdering ( reader , _, position ) and
451
+ result = count ( Token t | tokenOrdering ( reader , t , position ) )
452
+ }
453
+
395
454
private class WhiteSpaceToken extends Token , MkWhiteSpaceToken { }
396
455
397
456
private class CommaToken extends Token , MkCommaToken { }
@@ -431,10 +490,10 @@ module BindingStringParser<BindingStringReaderSig BindingStringReader> {
431
490
private class DotToken extends Token , MkDot { }
432
491
433
492
private Token getNextSkippingWhitespace ( Token t ) {
434
- result = t .getNext ( ) and
493
+ result = t .getNextAfterEnd ( ) and
435
494
not result instanceof WhiteSpaceToken
436
495
or
437
- exists ( WhiteSpaceToken ws | ws = t .getNext ( ) | result = getNextSkippingWhitespace ( ws ) )
496
+ exists ( WhiteSpaceToken ws | ws = t .getNextAfterEnd ( ) | result = getNextSkippingWhitespace ( ws ) )
438
497
}
439
498
440
499
private newtype TMemberList =
0 commit comments