@@ -1549,25 +1549,55 @@ signature predicate relevantTraitVisibleSig(Element element, Trait trait);
15491549 * at a given element.
15501550 */
15511551module TraitIsVisible< relevantTraitVisibleSig / 2 relevantTraitVisible> {
1552- /** Holds if the trait might be looked up in `encl`. */
1553- private predicate traitLookup ( ItemNode encl , Element element , Trait trait ) {
1554- // lookup in immediately enclosing item
1555- relevantTraitVisible ( element , trait ) and
1556- encl .getADescendant ( ) = element
1552+ private newtype TNode =
1553+ TTrait ( Trait t ) { relevantTraitVisible ( _, t ) } or
1554+ TItemNode ( ItemNode i ) or
1555+ TElement ( Element e ) { relevantTraitVisible ( e , _) }
1556+
1557+ private predicate isTrait ( TNode n ) { n instanceof TTrait }
1558+
1559+ private predicate step ( TNode n1 , TNode n2 ) {
1560+ exists ( Trait t1 , ItemNode i2 |
1561+ n1 = TTrait ( t1 ) and
1562+ n2 = TItemNode ( i2 ) and
1563+ t1 = i2 .getASuccessor ( _, _, _)
1564+ )
15571565 or
1558- // lookup in an outer scope, but only if the trait is not declared in inner scope
1559- exists ( ItemNode mid |
1560- traitLookup ( mid , element , trait ) and
1561- not trait = mid .getASuccessor ( _, _, _) and
1562- encl = getOuterScope ( mid )
1566+ exists ( ItemNode i1 , ItemNode i2 |
1567+ n1 = TItemNode ( i1 ) and
1568+ n2 = TItemNode ( i2 ) and
1569+ i1 = getOuterScope ( i2 )
1570+ )
1571+ or
1572+ exists ( ItemNode i1 , Element e2 |
1573+ n1 = TItemNode ( i1 ) and
1574+ n2 = TElement ( e2 ) and
1575+ i1 .getADescendant ( ) = e2
1576+ )
1577+ }
1578+
1579+ private predicate isElement ( TNode n ) { n instanceof TElement }
1580+
1581+ private predicate traitIsVisibleTC ( TNode trait , TNode element ) =
1582+ doublyBoundedFastTC( step / 2 , isTrait / 1 , isElement / 1 ) ( trait , element )
1583+
1584+ pragma [ nomagic]
1585+ private predicate relevantTraitVisibleLift ( TNode trait , TElement element ) {
1586+ exists ( Trait t , Element e |
1587+ trait = TTrait ( t ) and
1588+ element = TElement ( e ) and
1589+ relevantTraitVisible ( e , t )
15631590 )
15641591 }
15651592
15661593 /** Holds if the trait `trait` is visible at `element`. */
15671594 pragma [ nomagic]
15681595 predicate traitIsVisible ( Element element , Trait trait ) {
1569- exists ( ItemNode encl |
1570- traitLookup ( encl , element , trait ) and trait = encl .getASuccessor ( _, _, _)
1596+ exists ( TNode t , TNode e |
1597+ traitIsVisibleTC ( t , e ) and
1598+ relevantTraitVisibleLift ( t , e ) and
1599+ t = TTrait ( trait ) and
1600+ e = TElement ( element )
15711601 )
15721602 }
15731603}
0 commit comments