@@ -423,27 +423,23 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
423
423
)
424
424
}
425
425
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
434
429
) {
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 )
439
433
}
440
434
441
435
pragma [ nomagic]
442
436
private predicate satisfiesConcreteTypesFromIndex (
443
437
App app , TypeAbstraction abs , TypeMention tm , int i
444
438
) {
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
447
443
// Recurse unless we are at the first path
448
444
if i = 0 then any ( ) else satisfiesConcreteTypesFromIndex ( app , abs , tm , i - 1 )
449
445
}
@@ -467,24 +463,34 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
467
463
* Gets the path to the `i`th occurrence of `tp` within `tm` per some
468
464
* arbitrary order, if any.
469
465
*/
466
+ pragma [ nomagic]
470
467
private TypePath getNthTypeParameterPath ( TypeMention tm , TypeParameter tp , int i ) {
471
468
result =
472
469
rank [ i + 1 ] ( TypePath path | tp = tm .resolveTypeAt ( path ) and relevantTypeMention ( tm ) | path )
473
470
}
474
471
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
+
475
482
pragma [ nomagic]
476
483
private predicate typeParametersEqualFromIndex (
477
484
App app , TypeAbstraction abs , TypeMention tm , TypeParameter tp , Type t , int i
478
485
) {
479
- satisfiesConcreteTypes ( app , abs , tm ) and
480
486
exists ( TypePath path |
481
- path = getNthTypeParameterPath ( tm , tp , i ) and
482
487
t = app .getTypeAt ( path ) and
483
488
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
+ )
488
494
)
489
495
}
490
496
@@ -1040,6 +1046,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
1040
1046
/**
1041
1047
* Holds if `at` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
1042
1048
*/
1049
+ pragma [ nomagic]
1043
1050
private predicate hasConstraintMention (
1044
1051
RelevantAccess at , TypeAbstraction abs , TypeMention sub , Type constraint ,
1045
1052
TypeMention constraintMention
@@ -1063,6 +1070,30 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
1063
1070
)
1064
1071
}
1065
1072
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
+
1066
1097
/**
1067
1098
* Holds if the type at `a`, `apos`, and `path` satisfies the constraint
1068
1099
* `constraint` with the type `t` at `path`.
@@ -1071,22 +1102,18 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
1071
1102
predicate satisfiesConstraintTypeMention (
1072
1103
Access a , AccessPosition apos , TypePath prefix , Type constraint , TypePath path , Type t
1073
1104
) {
1105
+ exists ( TypeAbstraction abs |
1106
+ satisfiesConstraintTypeMention0 ( _, a , apos , prefix , constraint , abs , _, path , t ) and
1107
+ not t = abs .getATypeParameter ( )
1108
+ )
1109
+ or
1074
1110
exists (
1075
- RelevantAccess at , TypeAbstraction abs , TypeMention sub , Type t0 , TypePath prefix0 ,
1076
- TypeMention constraintMention
1111
+ RelevantAccess at , TypePath prefix0 , TypePath pathToTypeParamInSub , TypePath suffix
1077
1112
|
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 )
1090
1117
)
1091
1118
}
1092
1119
}
@@ -1289,14 +1316,14 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
1289
1316
exists ( DeclarationPosition dpos | accessDeclarationPositionMatch ( apos , dpos ) |
1290
1317
// A suffix of `path` leads to a type parameter in the target
1291
1318
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
1293
1320
path = prefix .append ( suffix ) and
1294
1321
typeMatch ( a , target , suffix , result , tp )
1295
1322
)
1296
1323
or
1297
1324
// `path` corresponds directly to a concrete type in the declaration
1298
1325
exists ( Declaration target |
1299
- result = target .getDeclaredType ( pragma [ only_bind_into ] ( dpos ) , path ) and
1326
+ result = target .getDeclaredType ( dpos , path ) and
1300
1327
target = a .getTarget ( ) and
1301
1328
not result instanceof TypeParameter
1302
1329
)
0 commit comments