@@ -423,27 +423,23 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
423423 )
424424 }
425425
426- /**
427- * Holds if `app` is a possible instantiation of `tm` at `path`. That is
428- * the type at `path` in `tm` is either a type parameter or equal to the
429- * type at the same path in `app`.
430- */
431- bindingset [ app, abs, tm, path]
432- private predicate satisfiesConcreteTypeAt (
433- App app , TypeAbstraction abs , TypeMention tm , TypePath path
426+ pragma [ nomagic]
427+ private Type resolveNthTypeAt (
428+ App app , TypeAbstraction abs , TypeMention tm , int i , TypePath path
434429 ) {
435- exists ( Type t |
436- tm .resolveTypeAt ( path ) = t and
437- if t = abs .getATypeParameter ( ) then any ( ) else app .getTypeAt ( path ) = t
438- )
430+ potentialInstantiationOf ( app , abs , tm ) and
431+ path = getNthPath ( tm , i ) and
432+ result = tm .resolveTypeAt ( path )
439433 }
440434
441435 pragma [ nomagic]
442436 private predicate satisfiesConcreteTypesFromIndex (
443437 App app , TypeAbstraction abs , TypeMention tm , int i
444438 ) {
445- potentialInstantiationOf ( app , abs , tm ) and
446- satisfiesConcreteTypeAt ( app , abs , tm , getNthPath ( tm , i ) ) and
439+ exists ( Type t , TypePath path |
440+ t = resolveNthTypeAt ( app , abs , tm , i , path ) and
441+ if t = abs .getATypeParameter ( ) then any ( ) else app .getTypeAt ( path ) = t
442+ ) and
447443 // Recurse unless we are at the first path
448444 if i = 0 then any ( ) else satisfiesConcreteTypesFromIndex ( app , abs , tm , i - 1 )
449445 }
@@ -467,24 +463,34 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
467463 * Gets the path to the `i`th occurrence of `tp` within `tm` per some
468464 * arbitrary order, if any.
469465 */
466+ pragma [ nomagic]
470467 private TypePath getNthTypeParameterPath ( TypeMention tm , TypeParameter tp , int i ) {
471468 result =
472469 rank [ i + 1 ] ( TypePath path | tp = tm .resolveTypeAt ( path ) and relevantTypeMention ( tm ) | path )
473470 }
474471
472+ pragma [ nomagic]
473+ private predicate typeParametersEqualFromIndexBase (
474+ App app , TypeAbstraction abs , TypeMention tm , TypeParameter tp , TypePath path
475+ ) {
476+ path = getNthTypeParameterPath ( tm , tp , 0 ) and
477+ satisfiesConcreteTypes ( app , abs , tm ) and
478+ // no need to compute this predicate if there is only one path
479+ exists ( getNthTypeParameterPath ( tm , tp , 1 ) )
480+ }
481+
475482 pragma [ nomagic]
476483 private predicate typeParametersEqualFromIndex (
477484 App app , TypeAbstraction abs , TypeMention tm , TypeParameter tp , Type t , int i
478485 ) {
479- satisfiesConcreteTypes ( app , abs , tm ) and
480486 exists ( TypePath path |
481- path = getNthTypeParameterPath ( tm , tp , i ) and
482487 t = app .getTypeAt ( path ) and
483488 if i = 0
484- then
485- // no need to compute this predicate if there is only one path
486- exists ( getNthTypeParameterPath ( tm , tp , 1 ) )
487- else typeParametersEqualFromIndex ( app , abs , tm , tp , t , i - 1 )
489+ then typeParametersEqualFromIndexBase ( app , abs , tm , tp , path )
490+ else (
491+ typeParametersEqualFromIndex ( app , abs , tm , tp , t , i - 1 ) and
492+ path = getNthTypeParameterPath ( tm , tp , i )
493+ )
488494 )
489495 }
490496
@@ -1040,6 +1046,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10401046 /**
10411047 * Holds if `at` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
10421048 */
1049+ pragma [ nomagic]
10431050 private predicate hasConstraintMention (
10441051 RelevantAccess at , TypeAbstraction abs , TypeMention sub , Type constraint ,
10451052 TypeMention constraintMention
@@ -1063,6 +1070,30 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10631070 )
10641071 }
10651072
1073+ pragma [ nomagic]
1074+ predicate satisfiesConstraintTypeMention0 (
1075+ RelevantAccess at , Access a , AccessPosition apos , TypePath prefix , Type constraint ,
1076+ TypeAbstraction abs , TypeMention sub , TypePath path , Type t
1077+ ) {
1078+ exists ( TypeMention constraintMention |
1079+ at = MkRelevantAccess ( a , apos , prefix ) and
1080+ hasConstraintMention ( at , abs , sub , constraint , constraintMention ) and
1081+ conditionSatisfiesConstraintTypeAt ( abs , sub , constraintMention , path , t )
1082+ )
1083+ }
1084+
1085+ pragma [ nomagic]
1086+ predicate satisfiesConstraintTypeMention1 (
1087+ RelevantAccess at , Access a , AccessPosition apos , TypePath prefix , Type constraint ,
1088+ TypePath path , TypePath pathToTypeParamInSub
1089+ ) {
1090+ exists ( TypeAbstraction abs , TypeMention sub , TypeParameter tp |
1091+ satisfiesConstraintTypeMention0 ( at , a , apos , prefix , constraint , abs , sub , path , tp ) and
1092+ tp = abs .getATypeParameter ( ) and
1093+ sub .resolveTypeAt ( pathToTypeParamInSub ) = tp
1094+ )
1095+ }
1096+
10661097 /**
10671098 * Holds if the type at `a`, `apos`, and `path` satisfies the constraint
10681099 * `constraint` with the type `t` at `path`.
@@ -1071,22 +1102,18 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10711102 predicate satisfiesConstraintTypeMention (
10721103 Access a , AccessPosition apos , TypePath prefix , Type constraint , TypePath path , Type t
10731104 ) {
1105+ exists ( TypeAbstraction abs |
1106+ satisfiesConstraintTypeMention0 ( _, a , apos , prefix , constraint , abs , _, path , t ) and
1107+ not t = abs .getATypeParameter ( )
1108+ )
1109+ or
10741110 exists (
1075- RelevantAccess at , TypeAbstraction abs , TypeMention sub , Type t0 , TypePath prefix0 ,
1076- TypeMention constraintMention
1111+ RelevantAccess at , TypePath prefix0 , TypePath pathToTypeParamInSub , TypePath suffix
10771112 |
1078- at = MkRelevantAccess ( a , apos , prefix ) and
1079- hasConstraintMention ( at , abs , sub , constraint , constraintMention ) and
1080- conditionSatisfiesConstraintTypeAt ( abs , sub , constraintMention , prefix0 , t0 )
1081- |
1082- not t0 = abs .getATypeParameter ( ) and t = t0 and path = prefix0
1083- or
1084- t0 = abs .getATypeParameter ( ) and
1085- exists ( TypePath path3 , TypePath suffix |
1086- sub .resolveTypeAt ( path3 ) = t0 and
1087- at .getTypeAt ( path3 .appendInverse ( suffix ) ) = t and
1088- path = prefix0 .append ( suffix )
1089- )
1113+ satisfiesConstraintTypeMention1 ( at , a , apos , prefix , constraint , prefix0 ,
1114+ pathToTypeParamInSub ) and
1115+ at .getTypeAt ( pathToTypeParamInSub .appendInverse ( suffix ) ) = t and
1116+ path = prefix0 .append ( suffix )
10901117 )
10911118 }
10921119 }
@@ -1289,14 +1316,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
12891316 exists ( DeclarationPosition dpos | accessDeclarationPositionMatch ( apos , dpos ) |
12901317 // A suffix of `path` leads to a type parameter in the target
12911318 exists ( Declaration target , TypePath prefix , TypeParameter tp , TypePath suffix |
1292- tp = target .getDeclaredType ( pragma [ only_bind_into ] ( dpos ) , prefix ) and
1319+ tp = target .getDeclaredType ( dpos , prefix ) and
12931320 path = prefix .append ( suffix ) and
12941321 typeMatch ( a , target , suffix , result , tp )
12951322 )
12961323 or
12971324 // `path` corresponds directly to a concrete type in the declaration
12981325 exists ( Declaration target |
1299- result = target .getDeclaredType ( pragma [ only_bind_into ] ( dpos ) , path ) and
1326+ result = target .getDeclaredType ( dpos , path ) and
13001327 target = a .getTarget ( ) and
13011328 not result instanceof TypeParameter
13021329 )
0 commit comments