@@ -238,7 +238,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
238
238
}
239
239
240
240
/** A class that represents a type tree. */
241
- signature class TypeTreeSig {
241
+ private signature class TypeTreeSig {
242
242
Type resolveTypeAt ( TypePath path ) ;
243
243
244
244
/** Gets a textual representation of this type abstraction. */
@@ -357,21 +357,38 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
357
357
result = tm .resolveTypeAt ( TypePath:: nil ( ) )
358
358
}
359
359
360
- signature module IsInstantiationOfSig < TypeTreeSig App> {
360
+ signature module IsInstantiationOfInputSig < TypeTreeSig App> {
361
361
/**
362
362
* Holds if `abs` is a type abstraction under which `tm` occurs and if
363
363
* `app` is potentially the result of applying the abstraction to type
364
364
* some type argument.
365
365
*/
366
366
predicate potentialInstantiationOf ( App app , TypeAbstraction abs , TypeMention tm ) ;
367
+
368
+ /**
369
+ * Holds if `constraint` might occur as the third argument of
370
+ * `potentialInstantiationOf`. Defaults to simply projecting the third
371
+ * argument of `potentialInstantiationOf`.
372
+ */
373
+ default predicate relevantTypeMention ( TypeMention tm ) { potentialInstantiationOf ( _, _, tm ) }
367
374
}
368
375
369
- module IsInstantiationOf< TypeTreeSig App, IsInstantiationOfSig< App > Input> {
376
+ /**
377
+ * Provides functionality for determining if a type is a possible
378
+ * instantiation of a type mention containing type parameters.
379
+ */
380
+ module IsInstantiationOf< TypeTreeSig App, IsInstantiationOfInputSig< App > Input> {
370
381
private import Input
371
382
372
383
/** Gets the `i`th path in `tm` per some arbitrary order. */
384
+ pragma [ nomagic]
373
385
private TypePath getNthPath ( TypeMention tm , int i ) {
374
- result = rank [ i + 1 ] ( TypePath path | exists ( tm .resolveTypeAt ( path ) ) | path )
386
+ result =
387
+ rank [ i + 1 ] ( TypePath path |
388
+ exists ( tm .resolveTypeAt ( path ) ) and relevantTypeMention ( tm )
389
+ |
390
+ path
391
+ )
375
392
}
376
393
377
394
/**
@@ -389,6 +406,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
389
406
)
390
407
}
391
408
409
+ pragma [ nomagic]
392
410
private predicate satisfiesConcreteTypesFromIndex (
393
411
App app , TypeAbstraction abs , TypeMention tm , int i
394
412
) {
@@ -398,7 +416,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
398
416
if i = 0 then any ( ) else satisfiesConcreteTypesFromIndex ( app , abs , tm , i - 1 )
399
417
}
400
418
401
- pragma [ inline ]
419
+ pragma [ nomagic ]
402
420
private predicate satisfiesConcreteTypes ( App app , TypeAbstraction abs , TypeMention tm ) {
403
421
satisfiesConcreteTypesFromIndex ( app , abs , tm , max ( int i | exists ( getNthPath ( tm , i ) ) ) )
404
422
}
@@ -417,18 +435,19 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
417
435
* arbitrary order, if any.
418
436
*/
419
437
private TypePath getNthTypeParameterPath ( TypeMention tm , TypeParameter tp , int i ) {
420
- result = rank [ i + 1 ] ( TypePath path | tp = tm .resolveTypeAt ( path ) | path )
438
+ result =
439
+ rank [ i + 1 ] ( TypePath path | tp = tm .resolveTypeAt ( path ) and relevantTypeMention ( tm ) | path )
421
440
}
422
441
442
+ pragma [ nomagic]
423
443
private predicate typeParametersEqualFromIndex (
424
- App app , TypeAbstraction abs , TypeMention tm , TypeParameter tp , int i
444
+ App app , TypeAbstraction abs , TypeMention tm , TypeParameter tp , Type t , int i
425
445
) {
426
446
potentialInstantiationOf ( app , abs , tm ) and
427
- exists ( TypePath path , TypePath nextPath |
447
+ exists ( TypePath path |
428
448
path = getNthTypeParameterPath ( tm , tp , i ) and
429
- nextPath = getNthTypeParameterPath ( tm , tp , i - 1 ) and
430
- app .resolveTypeAt ( path ) = app .resolveTypeAt ( nextPath ) and
431
- if i = 1 then any ( ) else typeParametersEqualFromIndex ( app , abs , tm , tp , i - 1 )
449
+ t = app .resolveTypeAt ( path ) and
450
+ if i = 0 then any ( ) else typeParametersEqualFromIndex ( app , abs , tm , tp , t , i - 1 )
432
451
)
433
452
}
434
453
@@ -443,7 +462,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
443
462
exists ( int n | n = max ( int i | exists ( getNthTypeParameterPath ( tm , tp , i ) ) ) |
444
463
// If the largest index is 0, then there are no equalities to check as
445
464
// the type parameter only occurs once.
446
- if n = 0 then any ( ) else typeParametersEqualFromIndex ( app , abs , tm , tp , n )
465
+ if n = 0 then any ( ) else typeParametersEqualFromIndex ( app , abs , tm , tp , _ , n )
447
466
)
448
467
)
449
468
}
@@ -488,7 +507,6 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
488
507
* - `Pair<int, string>` is _not_ an instantiation of `Pair<string, string>`
489
508
*/
490
509
predicate isInstantiationOf ( App app , TypeAbstraction abs , TypeMention tm ) {
491
- potentialInstantiationOf ( app , abs , tm ) and
492
510
satisfiesConcreteTypes ( app , abs , tm ) and
493
511
typeParametersHaveEqualInstantiation ( app , abs , tm )
494
512
}
@@ -513,7 +531,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
513
531
)
514
532
}
515
533
516
- module IsInstantiationOfInput implements IsInstantiationOfSig < TypeMention > {
534
+ module IsInstantiationOfInput implements IsInstantiationOfInputSig < TypeMention > {
517
535
pragma [ nomagic]
518
536
private predicate typeCondition ( Type type , TypeAbstraction abs , TypeMention lhs ) {
519
537
conditionSatisfiesConstraint ( abs , lhs , _) and type = resolveTypeMentionRoot ( lhs )
@@ -954,7 +972,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
954
972
Location getLocation ( ) { result = a .getLocation ( ) }
955
973
}
956
974
957
- private module IsInstantiationOfInput implements IsInstantiationOfSig < RelevantAccess > {
975
+ private module IsInstantiationOfInput implements IsInstantiationOfInputSig < RelevantAccess > {
958
976
predicate potentialInstantiationOf (
959
977
RelevantAccess at , TypeAbstraction abs , TypeMention cond
960
978
) {
@@ -965,6 +983,10 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
965
983
countConstraintImplementations ( type , constraint ) > 1
966
984
)
967
985
}
986
+
987
+ predicate relevantTypeMention ( TypeMention constraint ) {
988
+ rootTypesSatisfaction ( _, _, _, constraint , _)
989
+ }
968
990
}
969
991
970
992
/**
0 commit comments