@@ -1427,34 +1427,57 @@ signature predicate relevantTraitVisibleSig(Element element, Trait trait);
14271427 * at a given element.
14281428 */
14291429module TraitIsVisible< relevantTraitVisibleSig / 2 relevantTraitVisible> {
1430- /** Holds if the trait might be looked up in `encl`. */
1431- private predicate traitLookup ( ItemNode encl , Element element , Trait trait ) {
1432- // lookup in immediately enclosing item
1433- relevantTraitVisible ( element , trait ) and
1434- encl .getADescendant ( ) = element
1430+ private newtype TNode =
1431+ TTrait ( Trait t ) or
1432+ TItemNode ( ItemNode i ) or
1433+ TElement ( Element e ) { relevantTraitVisible ( e , _) }
1434+
1435+ private predicate isTrait ( TNode n ) { n instanceof TTrait }
1436+
1437+ private predicate step ( TNode n1 , TNode n2 ) {
1438+ exists ( Trait t1 , ItemNode i2 |
1439+ n1 = TTrait ( t1 ) and
1440+ n2 = TItemNode ( i2 ) and
1441+ t1 = i2 .getASuccessor ( _, _)
1442+ )
14351443 or
1436- // lookup in an outer scope, but only if the trait is not declared in inner scope
1437- exists ( ItemNode mid |
1438- traitLookup ( mid , element , trait ) and
1439- not trait = mid .getASuccessor ( _, _) and
1440- encl = getOuterScope ( mid )
1444+ exists ( ItemNode i1 , ItemNode i2 |
1445+ n1 = TItemNode ( i1 ) and
1446+ n2 = TItemNode ( i2 ) and
1447+ i1 = getOuterScope ( i2 )
1448+ )
1449+ or
1450+ exists ( ItemNode i1 , Element e2 |
1451+ n1 = TItemNode ( i1 ) and
1452+ n2 = TElement ( e2 ) and
1453+ i1 .getADescendant ( ) = e2
14411454 )
14421455 }
14431456
1457+ private predicate isElement ( TNode n ) { n instanceof TElement }
1458+
1459+ private predicate traitIsVisibleTC ( TNode trait , TNode element ) =
1460+ doublyBoundedFastTC( step / 2 , isTrait / 1 , isElement / 1 ) ( trait , element )
1461+
1462+ // /** Holds if the trait might be looked up in `encl`. */
1463+ // private predicate traitLookup(ItemNode encl, Element element, Trait trait) {
1464+ // // lookup in immediately enclosing item
1465+ // relevantTraitVisible(element, trait) and
1466+ // encl.getADescendant() = element
1467+ // or
1468+ // // lookup in an outer scope, but only if the trait is not declared in inner scope
1469+ // exists(ItemNode mid |
1470+ // traitLookup(mid, element, trait) and
1471+ // not trait = mid.getASuccessor(_, _) and
1472+ // encl = getOuterScope(mid)
1473+ // )
1474+ // }
14441475 /** Holds if the trait `trait` is visible at `element`. */
14451476 pragma [ nomagic]
14461477 predicate traitIsVisible ( Element element , Trait trait ) {
1447- exists ( ItemNode encl | traitLookup ( encl , element , trait ) and trait = encl .getASuccessor ( _, _) )
1448- }
1449-
1450- /** Holds if the trait `trait` is _not_ visible at `element`. */
1451- pragma [ nomagic]
1452- predicate traitIsNotVisible ( Element element , Trait trait ) {
1453- exists ( ItemNode top |
1454- traitLookup ( top , element , trait ) and
1455- not exists ( getOuterScope ( top ) ) and
1456- not trait = top .getASuccessor ( _, _)
1457- )
1478+ // exists(ItemNode encl | traitLookup(encl, element, trait) and trait = encl.getASuccessor(_, _))
1479+ traitIsVisibleTC ( TTrait ( trait ) , TElement ( element ) ) and
1480+ relevantTraitVisible ( element , trait )
14581481 }
14591482}
14601483
0 commit comments