@@ -866,6 +866,108 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
866866
867867 private import BaseTypes
868868
869+ signature module SatisfiesConstraintInputSig< HasTypeTreeSig HasTypeTree> {
870+ /** Holds if it is relevant to know if `term` satisfies `constraint`. */
871+ predicate relevantConstraint ( HasTypeTree term , Type constraint ) ;
872+ }
873+
874+ module SatisfiesConstraint<
875+ HasTypeTreeSig HasTypeTree, SatisfiesConstraintInputSig< HasTypeTree > Input>
876+ {
877+ private import Input
878+
879+ private module IsInstantiationOfInput implements IsInstantiationOfInputSig< HasTypeTree > {
880+ predicate potentialInstantiationOf ( HasTypeTree tt , TypeAbstraction abs , TypeMention cond ) {
881+ exists ( Type constraint , Type type |
882+ type = tt .getTypeAt ( TypePath:: nil ( ) ) and
883+ relevantConstraint ( tt , constraint ) and
884+ rootTypesSatisfaction ( type , constraint , abs , cond , _) and
885+ // We only need to check instantiations where there are multiple candidates.
886+ countConstraintImplementations ( type , constraint ) > 1
887+ )
888+ }
889+
890+ predicate relevantTypeMention ( TypeMention constraint ) {
891+ rootTypesSatisfaction ( _, _, _, constraint , _)
892+ }
893+ }
894+
895+ /** Holds if the type tree has the type `type` and should satisfy `constraint`. */
896+ pragma [ nomagic]
897+ private predicate hasTypeConstraint ( HasTypeTree term , Type type , Type constraint ) {
898+ type = term .getTypeAt ( TypePath:: nil ( ) ) and
899+ relevantConstraint ( term , constraint )
900+ }
901+
902+ /**
903+ * Holds if `tt` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
904+ */
905+ pragma [ nomagic]
906+ private predicate hasConstraintMention (
907+ HasTypeTree tt , TypeAbstraction abs , TypeMention sub , Type constraint ,
908+ TypeMention constraintMention
909+ ) {
910+ exists ( Type type | hasTypeConstraint ( tt , type , constraint ) |
911+ not exists ( countConstraintImplementations ( type , constraint ) ) and
912+ conditionSatisfiesConstraintTypeAt ( abs , sub , constraintMention , _, _) and
913+ resolveTypeMentionRoot ( sub ) = abs .getATypeParameter ( ) and
914+ constraint = resolveTypeMentionRoot ( constraintMention )
915+ or
916+ countConstraintImplementations ( type , constraint ) > 0 and
917+ rootTypesSatisfaction ( type , constraint , abs , sub , constraintMention ) and
918+ // When there are multiple ways the type could implement the
919+ // constraint we need to find the right implementation, which is the
920+ // one where the type instantiates the precondition.
921+ if countConstraintImplementations ( type , constraint ) > 1
922+ then
923+ IsInstantiationOf< HasTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( tt , abs , sub )
924+ else any ( )
925+ )
926+ }
927+
928+ pragma [ nomagic]
929+ private predicate satisfiesConstraintTypeMention0 (
930+ HasTypeTree tt , Type constraint , TypeAbstraction abs , TypeMention sub , TypePath path , Type t
931+ ) {
932+ exists ( TypeMention constraintMention |
933+ hasConstraintMention ( tt , abs , sub , constraint , constraintMention ) and
934+ conditionSatisfiesConstraintTypeAt ( abs , sub , constraintMention , path , t )
935+ )
936+ }
937+
938+ pragma [ nomagic]
939+ private predicate satisfiesConstraintTypeMention1 (
940+ HasTypeTree tt , Type constraint , TypePath path , TypePath pathToTypeParamInSub
941+ ) {
942+ exists ( TypeAbstraction abs , TypeMention sub , TypeParameter tp |
943+ satisfiesConstraintTypeMention0 ( tt , constraint , abs , sub , path , tp ) and
944+ tp = abs .getATypeParameter ( ) and
945+ sub .resolveTypeAt ( pathToTypeParamInSub ) = tp
946+ )
947+ }
948+
949+ /**
950+ * Holds if the type tree at `tt` satisfies the constraint `constraint`
951+ * with the type `t` at `path`.
952+ */
953+ pragma [ nomagic]
954+ predicate satisfiesConstraintType ( HasTypeTree tt , Type constraint , TypePath path , Type t ) {
955+ exists ( TypeAbstraction abs |
956+ satisfiesConstraintTypeMention0 ( tt , constraint , abs , _, path , t ) and
957+ not t = abs .getATypeParameter ( )
958+ )
959+ or
960+ exists ( TypePath prefix0 , TypePath pathToTypeParamInSub , TypePath suffix |
961+ satisfiesConstraintTypeMention1 ( tt , constraint , prefix0 , pathToTypeParamInSub ) and
962+ tt .getTypeAt ( pathToTypeParamInSub .appendInverse ( suffix ) ) = t and
963+ path = prefix0 .append ( suffix )
964+ )
965+ or
966+ tt .getTypeAt ( TypePath:: nil ( ) ) = constraint and
967+ t = tt .getTypeAt ( path )
968+ }
969+ }
970+
869971 /** Provides the input to `Matching`. */
870972 signature module MatchingInputSig {
871973 /**
@@ -1129,11 +1231,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
11291231 adjustedAccessType ( a , apos , target , path .appendInverse ( suffix ) , result )
11301232 }
11311233
1132- /** Holds if this relevant access has the type `type` and should satisfy `constraint`. */
1133- predicate hasTypeConstraint ( Type type , Type constraint ) {
1134- adjustedAccessType ( a , apos , target , path , type ) and
1135- relevantAccessConstraint ( a , target , apos , path , constraint )
1136- }
1234+ /** Holds if this relevant access should satisfy `constraint`. */
1235+ Type getConstraint ( ) { relevantAccessConstraint ( a , target , apos , path , result ) }
11371236
11381237 string toString ( ) {
11391238 result = a .toString ( ) + ", " + apos .toString ( ) + ", " + path .toString ( )
@@ -1142,94 +1241,20 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
11421241 Location getLocation ( ) { result = a .getLocation ( ) }
11431242 }
11441243
1145- private module IsInstantiationOfInput implements IsInstantiationOfInputSig< RelevantAccess > {
1146- predicate potentialInstantiationOf (
1147- RelevantAccess at , TypeAbstraction abs , TypeMention cond
1148- ) {
1149- exists ( Type constraint , Type type |
1150- at .hasTypeConstraint ( type , constraint ) and
1151- rootTypesSatisfaction ( type , constraint , abs , cond , _) and
1152- // We only need to check instantiations where there are multiple candidates.
1153- countConstraintImplementations ( type , constraint ) > 1
1154- )
1244+ private module SatisfiesConstraintInput implements
1245+ SatisfiesConstraintInputSig< RelevantAccess >
1246+ {
1247+ predicate relevantConstraint ( RelevantAccess at , Type constraint ) {
1248+ constraint = at .getConstraint ( )
11551249 }
1156-
1157- predicate relevantTypeMention ( TypeMention constraint ) {
1158- rootTypesSatisfaction ( _, _, _, constraint , _)
1159- }
1160- }
1161-
1162- /**
1163- * Holds if `at` satisfies `constraint` through `abs`, `sub`, and `constraintMention`.
1164- */
1165- pragma [ nomagic]
1166- private predicate hasConstraintMention (
1167- RelevantAccess at , TypeAbstraction abs , TypeMention sub , Type constraint ,
1168- TypeMention constraintMention
1169- ) {
1170- exists ( Type type | at .hasTypeConstraint ( type , constraint ) |
1171- not exists ( countConstraintImplementations ( type , constraint ) ) and
1172- conditionSatisfiesConstraintTypeAt ( abs , sub , constraintMention , _, _) and
1173- resolveTypeMentionRoot ( sub ) = abs .getATypeParameter ( ) and
1174- constraint = resolveTypeMentionRoot ( constraintMention )
1175- or
1176- countConstraintImplementations ( type , constraint ) > 0 and
1177- rootTypesSatisfaction ( type , constraint , abs , sub , constraintMention ) and
1178- // When there are multiple ways the type could implement the
1179- // constraint we need to find the right implementation, which is the
1180- // one where the type instantiates the precondition.
1181- if countConstraintImplementations ( type , constraint ) > 1
1182- then
1183- IsInstantiationOf< RelevantAccess , IsInstantiationOfInput > :: isInstantiationOf ( at , abs ,
1184- sub )
1185- else any ( )
1186- )
11871250 }
11881251
1189- pragma [ nomagic]
1190- predicate satisfiesConstraintTypeMention0 (
1191- RelevantAccess at , Access a , AccessPosition apos , TypePath prefix , Type constraint ,
1192- TypeAbstraction abs , TypeMention sub , TypePath path , Type t
1193- ) {
1194- exists ( TypeMention constraintMention |
1195- at = MkRelevantAccess ( a , _, apos , prefix ) and
1196- hasConstraintMention ( at , abs , sub , constraint , constraintMention ) and
1197- conditionSatisfiesConstraintTypeAt ( abs , sub , constraintMention , path , t )
1198- )
1199- }
1200-
1201- pragma [ nomagic]
1202- predicate satisfiesConstraintTypeMention1 (
1203- RelevantAccess at , Access a , AccessPosition apos , TypePath prefix , Type constraint ,
1204- TypePath path , TypePath pathToTypeParamInSub
1205- ) {
1206- exists ( TypeAbstraction abs , TypeMention sub , TypeParameter tp |
1207- satisfiesConstraintTypeMention0 ( at , a , apos , prefix , constraint , abs , sub , path , tp ) and
1208- tp = abs .getATypeParameter ( ) and
1209- sub .resolveTypeAt ( pathToTypeParamInSub ) = tp
1210- )
1211- }
1212-
1213- /**
1214- * Holds if the type at `a`, `apos`, and `path` satisfies the constraint
1215- * `constraint` with the type `t` at `path`.
1216- */
1217- pragma [ nomagic]
1218- predicate satisfiesConstraintTypeMention (
1252+ predicate satisfiesConstraintType (
12191253 Access a , AccessPosition apos , TypePath prefix , Type constraint , TypePath path , Type t
12201254 ) {
1221- exists ( TypeAbstraction abs |
1222- satisfiesConstraintTypeMention0 ( _, a , apos , prefix , constraint , abs , _, path , t ) and
1223- not t = abs .getATypeParameter ( )
1224- )
1225- or
1226- exists (
1227- RelevantAccess at , TypePath prefix0 , TypePath pathToTypeParamInSub , TypePath suffix
1228- |
1229- satisfiesConstraintTypeMention1 ( at , a , apos , prefix , constraint , prefix0 ,
1230- pathToTypeParamInSub ) and
1231- at .getTypeAt ( pathToTypeParamInSub .appendInverse ( suffix ) ) = t and
1232- path = prefix0 .append ( suffix )
1255+ exists ( RelevantAccess at | at = MkRelevantAccess ( a , _, apos , prefix ) |
1256+ SatisfiesConstraint< RelevantAccess , SatisfiesConstraintInput > :: satisfiesConstraintType ( at ,
1257+ constraint , path , t )
12331258 )
12341259 }
12351260 }
@@ -1366,7 +1391,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
13661391 accessDeclarationPositionMatch ( apos , dpos ) and
13671392 typeParameterConstraintHasTypeParameter ( target , dpos , pathToTp2 , _, constraint , pathToTp ,
13681393 tp ) and
1369- AccessConstraint:: satisfiesConstraintTypeMention ( a , apos , pathToTp2 , constraint ,
1394+ AccessConstraint:: satisfiesConstraintType ( a , apos , pathToTp2 , constraint ,
13701395 pathToTp .appendInverse ( path ) , t )
13711396 )
13721397 }
0 commit comments