@@ -1036,6 +1036,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10361036 /**
10371037 * Holds if `at` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
10381038 */
1039+ pragma [ nomagic]
10391040 private predicate hasConstraintMention (
10401041 RelevantAccess at , TypeAbstraction abs , TypeMention sub , Type constraint ,
10411042 TypeMention constraintMention
@@ -1059,6 +1060,30 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10591060 )
10601061 }
10611062
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+
10621087 /**
10631088 * Holds if the type at `a`, `apos`, and `path` satisfies the constraint
10641089 * `constraint` with the type `t` at `path`.
@@ -1067,22 +1092,18 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
10671092 predicate satisfiesConstraintTypeMention (
10681093 Access a , AccessPosition apos , TypePath prefix , Type constraint , TypePath path , Type t
10691094 ) {
1095+ exists ( TypeAbstraction abs |
1096+ satisfiesConstraintTypeMention0 ( _, a , apos , prefix , constraint , abs , _, path , t ) and
1097+ not t = abs .getATypeParameter ( )
1098+ )
1099+ or
10701100 exists (
1071- RelevantAccess at , TypeAbstraction abs , TypeMention sub , Type t0 , TypePath prefix0 ,
1072- TypeMention constraintMention
1101+ RelevantAccess at , TypePath prefix0 , TypePath pathToTypeParamInSub , TypePath suffix
10731102 |
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 )
10861107 )
10871108 }
10881109 }
0 commit comments