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