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