@@ -1641,25 +1641,55 @@ signature predicate relevantTraitVisibleSig(Element element, Trait trait);
16411641 * at a given element.
16421642 */
16431643module TraitIsVisible< relevantTraitVisibleSig / 2 relevantTraitVisible> {
1644- /** Holds if the trait might be looked up in `encl`. */
1645- private predicate traitLookup ( ItemNode encl , Element element , Trait trait ) {
1646- // lookup in immediately enclosing item
1647- relevantTraitVisible ( element , trait ) and
1648- encl .getADescendant ( ) = element
1644+ private newtype TNode =
1645+ TTrait ( Trait t ) { relevantTraitVisible ( _, t ) } or
1646+ TItemNode ( ItemNode i ) or
1647+ TElement ( Element e ) { relevantTraitVisible ( e , _) }
1648+
1649+ private predicate isTrait ( TNode n ) { n instanceof TTrait }
1650+
1651+ private predicate step ( TNode n1 , TNode n2 ) {
1652+ exists ( Trait t1 , ItemNode i2 |
1653+ n1 = TTrait ( t1 ) and
1654+ n2 = TItemNode ( i2 ) and
1655+ t1 = i2 .getASuccessor ( _, _, _)
1656+ )
16491657 or
1650- // lookup in an outer scope, but only if the trait is not declared in inner scope
1651- exists ( ItemNode mid |
1652- traitLookup ( mid , element , trait ) and
1653- not trait = mid .getASuccessor ( _, _, _) and
1654- encl = getOuterScope ( mid )
1658+ exists ( ItemNode i1 , ItemNode i2 |
1659+ n1 = TItemNode ( i1 ) and
1660+ n2 = TItemNode ( i2 ) and
1661+ i1 = getOuterScope ( i2 )
1662+ )
1663+ or
1664+ exists ( ItemNode i1 , Element e2 |
1665+ n1 = TItemNode ( i1 ) and
1666+ n2 = TElement ( e2 ) and
1667+ i1 .getADescendant ( ) = e2
1668+ )
1669+ }
1670+
1671+ private predicate isElement ( TNode n ) { n instanceof TElement }
1672+
1673+ private predicate traitIsVisibleTC ( TNode trait , TNode element ) =
1674+ doublyBoundedFastTC( step / 2 , isTrait / 1 , isElement / 1 ) ( trait , element )
1675+
1676+ pragma [ nomagic]
1677+ private predicate relevantTraitVisibleLift ( TNode trait , TElement element ) {
1678+ exists ( Trait t , Element e |
1679+ trait = TTrait ( t ) and
1680+ element = TElement ( e ) and
1681+ relevantTraitVisible ( e , t )
16551682 )
16561683 }
16571684
16581685 /** Holds if the trait `trait` is visible at `element`. */
16591686 pragma [ nomagic]
16601687 predicate traitIsVisible ( Element element , Trait trait ) {
1661- exists ( ItemNode encl |
1662- traitLookup ( encl , element , trait ) and trait = encl .getASuccessor ( _, _, _)
1688+ exists ( TNode t , TNode e |
1689+ traitIsVisibleTC ( t , e ) and
1690+ relevantTraitVisibleLift ( t , e ) and
1691+ t = TTrait ( trait ) and
1692+ e = TElement ( element )
16631693 )
16641694 }
16651695}
0 commit comments