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