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