@@ -1540,25 +1540,55 @@ signature predicate relevantTraitVisibleSig(Element element, Trait trait);
15401540 * at a given element.
15411541 */
15421542module TraitIsVisible< relevantTraitVisibleSig / 2 relevantTraitVisible> {
1543- /** Holds if the trait might be looked up in `encl`. */
1544- private predicate traitLookup ( ItemNode encl , Element element , Trait trait ) {
1545- // lookup in immediately enclosing item
1546- relevantTraitVisible ( element , trait ) and
1547- encl .getADescendant ( ) = element
1543+ private newtype TNode =
1544+ TTrait ( Trait t ) { relevantTraitVisible ( _, t ) } or
1545+ TItemNode ( ItemNode i ) or
1546+ TElement ( Element e ) { relevantTraitVisible ( e , _) }
1547+
1548+ private predicate isTrait ( TNode n ) { n instanceof TTrait }
1549+
1550+ private predicate step ( TNode n1 , TNode n2 ) {
1551+ exists ( Trait t1 , ItemNode i2 |
1552+ n1 = TTrait ( t1 ) and
1553+ n2 = TItemNode ( i2 ) and
1554+ t1 = i2 .getASuccessor ( _, _, _)
1555+ )
15481556 or
1549- // lookup in an outer scope, but only if the trait is not declared in inner scope
1550- exists ( ItemNode mid |
1551- traitLookup ( mid , element , trait ) and
1552- not trait = mid .getASuccessor ( _, _, _) and
1553- encl = getOuterScope ( mid )
1557+ exists ( ItemNode i1 , ItemNode i2 |
1558+ n1 = TItemNode ( i1 ) and
1559+ n2 = TItemNode ( i2 ) and
1560+ i1 = getOuterScope ( i2 )
1561+ )
1562+ or
1563+ exists ( ItemNode i1 , Element e2 |
1564+ n1 = TItemNode ( i1 ) and
1565+ n2 = TElement ( e2 ) and
1566+ i1 .getADescendant ( ) = e2
1567+ )
1568+ }
1569+
1570+ private predicate isElement ( TNode n ) { n instanceof TElement }
1571+
1572+ private predicate traitIsVisibleTC ( TNode trait , TNode element ) =
1573+ doublyBoundedFastTC( step / 2 , isTrait / 1 , isElement / 1 ) ( trait , element )
1574+
1575+ pragma [ nomagic]
1576+ private predicate relevantTraitVisibleLift ( TNode trait , TElement element ) {
1577+ exists ( Trait t , Element e |
1578+ trait = TTrait ( t ) and
1579+ element = TElement ( e ) and
1580+ relevantTraitVisible ( e , t )
15541581 )
15551582 }
15561583
15571584 /** Holds if the trait `trait` is visible at `element`. */
15581585 pragma [ nomagic]
15591586 predicate traitIsVisible ( Element element , Trait trait ) {
1560- exists ( ItemNode encl |
1561- traitLookup ( encl , element , trait ) and trait = encl .getASuccessor ( _, _, _)
1587+ exists ( TNode t , TNode e |
1588+ traitIsVisibleTC ( t , e ) and
1589+ relevantTraitVisibleLift ( t , e ) and
1590+ t = TTrait ( trait ) and
1591+ e = TElement ( element )
15621592 )
15631593 }
15641594}
0 commit comments