@@ -463,24 +463,34 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
463
463
* Gets the path to the `i`th occurrence of `tp` within `tm` per some
464
464
* arbitrary order, if any.
465
465
*/
466
+ pragma [ nomagic]
466
467
private TypePath getNthTypeParameterPath ( TypeMention tm , TypeParameter tp , int i ) {
467
468
result =
468
469
rank [ i + 1 ] ( TypePath path | tp = tm .resolveTypeAt ( path ) and relevantTypeMention ( tm ) | path )
469
470
}
470
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
+
471
482
pragma [ nomagic]
472
483
private predicate typeParametersEqualFromIndex (
473
484
App app , TypeAbstraction abs , TypeMention tm , TypeParameter tp , Type t , int i
474
485
) {
475
- satisfiesConcreteTypes ( app , abs , tm ) and
476
486
exists ( TypePath path |
477
- path = getNthTypeParameterPath ( tm , tp , i ) and
478
487
t = app .getTypeAt ( path ) and
479
488
if i = 0
480
- then
481
- // no need to compute this predicate if there is only one path
482
- exists ( getNthTypeParameterPath ( tm , tp , 1 ) )
483
- 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
+ )
484
494
)
485
495
}
486
496
0 commit comments