@@ -1425,24 +1425,56 @@ signature predicate relevantTraitVisibleSig(Element element, Trait trait);
14251425 * at a given element.
14261426 */
14271427module 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+ )
14331441 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 )
14391466 )
14401467 }
14411468
14421469 /** Holds if the trait `trait` is visible at `element`. */
14431470 pragma [ nomagic]
14441471 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+ )
14461478 }
14471479}
14481480
0 commit comments