@@ -1036,6 +1036,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
1036
1036
/**
1037
1037
* Holds if `at` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
1038
1038
*/
1039
+ pragma [ nomagic]
1039
1040
private predicate hasConstraintMention (
1040
1041
RelevantAccess at , TypeAbstraction abs , TypeMention sub , Type constraint ,
1041
1042
TypeMention constraintMention
@@ -1059,6 +1060,30 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
1059
1060
)
1060
1061
}
1061
1062
1063
+ pragma [ nomagic]
1064
+ predicate satisfiesConstraintTypeMention0 (
1065
+ RelevantAccess at , Access a , AccessPosition apos , TypePath prefix , Type constraint ,
1066
+ TypeAbstraction abs , TypeMention sub , TypePath path , Type t
1067
+ ) {
1068
+ exists ( TypeMention constraintMention |
1069
+ at = MkRelevantAccess ( a , apos , prefix ) and
1070
+ hasConstraintMention ( at , abs , sub , constraint , constraintMention ) and
1071
+ conditionSatisfiesConstraintTypeAt ( abs , sub , constraintMention , path , t )
1072
+ )
1073
+ }
1074
+
1075
+ pragma [ nomagic]
1076
+ predicate satisfiesConstraintTypeMention1 (
1077
+ RelevantAccess at , Access a , AccessPosition apos , TypePath prefix , Type constraint ,
1078
+ TypePath path , TypePath pathToTypeParamInSub
1079
+ ) {
1080
+ exists ( TypeAbstraction abs , TypeMention sub , TypeParameter tp |
1081
+ satisfiesConstraintTypeMention0 ( at , a , apos , prefix , constraint , abs , sub , path , tp ) and
1082
+ tp = abs .getATypeParameter ( ) and
1083
+ sub .resolveTypeAt ( pathToTypeParamInSub ) = tp
1084
+ )
1085
+ }
1086
+
1062
1087
/**
1063
1088
* Holds if the type at `a`, `apos`, and `path` satisfies the constraint
1064
1089
* `constraint` with the type `t` at `path`.
@@ -1067,22 +1092,18 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
1067
1092
predicate satisfiesConstraintTypeMention (
1068
1093
Access a , AccessPosition apos , TypePath prefix , Type constraint , TypePath path , Type t
1069
1094
) {
1095
+ exists ( TypeAbstraction abs |
1096
+ satisfiesConstraintTypeMention0 ( _, a , apos , prefix , constraint , abs , _, path , t ) and
1097
+ not t = abs .getATypeParameter ( )
1098
+ )
1099
+ or
1070
1100
exists (
1071
- RelevantAccess at , TypeAbstraction abs , TypeMention sub , Type t0 , TypePath prefix0 ,
1072
- TypeMention constraintMention
1101
+ RelevantAccess at , TypePath prefix0 , TypePath pathToTypeParamInSub , TypePath suffix
1073
1102
|
1074
- at = MkRelevantAccess ( a , apos , prefix ) and
1075
- hasConstraintMention ( at , abs , sub , constraint , constraintMention ) and
1076
- conditionSatisfiesConstraintTypeAt ( abs , sub , constraintMention , prefix0 , t0 )
1077
- |
1078
- not t0 = abs .getATypeParameter ( ) and t = t0 and path = prefix0
1079
- or
1080
- t0 = abs .getATypeParameter ( ) and
1081
- exists ( TypePath path3 , TypePath suffix |
1082
- sub .resolveTypeAt ( path3 ) = t0 and
1083
- at .getTypeAt ( path3 .appendInverse ( suffix ) ) = t and
1084
- path = prefix0 .append ( suffix )
1085
- )
1103
+ satisfiesConstraintTypeMention1 ( at , a , apos , prefix , constraint , prefix0 ,
1104
+ pathToTypeParamInSub ) and
1105
+ at .getTypeAt ( pathToTypeParamInSub .appendInverse ( suffix ) ) = t and
1106
+ path = prefix0 .append ( suffix )
1086
1107
)
1087
1108
}
1088
1109
}
0 commit comments