@@ -1425,24 +1425,56 @@ signature predicate relevantTraitVisibleSig(Element element, Trait trait);
1425
1425
* at a given element.
1426
1426
*/
1427
1427
module TraitIsVisible< relevantTraitVisibleSig / 2 relevantTraitVisible> {
1428
- /** Holds if the trait might be looked up in `encl`. */
1429
- private predicate traitLookup ( ItemNode encl , Element element , Trait trait ) {
1430
- // lookup in immediately enclosing item
1431
- relevantTraitVisible ( element , trait ) and
1432
- encl .getADescendant ( ) = element
1428
+ private newtype TNode =
1429
+ TTrait ( Trait t ) { relevantTraitVisible ( _, t ) } or
1430
+ TItemNode ( ItemNode i ) or
1431
+ TElement ( Element e ) { relevantTraitVisible ( e , _) }
1432
+
1433
+ private predicate isTrait ( TNode n ) { n instanceof TTrait }
1434
+
1435
+ private predicate step ( TNode n1 , TNode n2 ) {
1436
+ exists ( Trait t1 , ItemNode i2 |
1437
+ n1 = TTrait ( t1 ) and
1438
+ n2 = TItemNode ( i2 ) and
1439
+ t1 = i2 .getASuccessor ( _, _)
1440
+ )
1433
1441
or
1434
- // lookup in an outer scope, but only if the trait is not declared in inner scope
1435
- exists ( ItemNode mid |
1436
- traitLookup ( mid , element , trait ) and
1437
- not trait = mid .getASuccessor ( _, _) and
1438
- encl = getOuterScope ( mid )
1442
+ exists ( ItemNode i1 , ItemNode i2 |
1443
+ n1 = TItemNode ( i1 ) and
1444
+ n2 = TItemNode ( i2 ) and
1445
+ i1 = getOuterScope ( i2 )
1446
+ )
1447
+ or
1448
+ exists ( ItemNode i1 , Element e2 |
1449
+ n1 = TItemNode ( i1 ) and
1450
+ n2 = TElement ( e2 ) and
1451
+ i1 .getADescendant ( ) = e2
1452
+ )
1453
+ }
1454
+
1455
+ private predicate isElement ( TNode n ) { n instanceof TElement }
1456
+
1457
+ private predicate traitIsVisibleTC ( TNode trait , TNode element ) =
1458
+ doublyBoundedFastTC( step / 2 , isTrait / 1 , isElement / 1 ) ( trait , element )
1459
+
1460
+ pragma [ nomagic]
1461
+ private predicate relevantTraitVisibleLift ( TNode trait , TElement element ) {
1462
+ exists ( Trait t , Element e |
1463
+ trait = TTrait ( t ) and
1464
+ element = TElement ( e ) and
1465
+ relevantTraitVisible ( e , t )
1439
1466
)
1440
1467
}
1441
1468
1442
1469
/** Holds if the trait `trait` is visible at `element`. */
1443
1470
pragma [ nomagic]
1444
1471
predicate traitIsVisible ( Element element , Trait trait ) {
1445
- exists ( ItemNode encl | traitLookup ( encl , element , trait ) and trait = encl .getASuccessor ( _, _) )
1472
+ exists ( TNode t , TNode e |
1473
+ traitIsVisibleTC ( t , e ) and
1474
+ relevantTraitVisibleLift ( t , e ) and
1475
+ t = TTrait ( trait ) and
1476
+ e = TElement ( element )
1477
+ )
1446
1478
}
1447
1479
}
1448
1480
0 commit comments