@@ -866,16 +866,18 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
866866
867867 private import BaseTypes
868868
869- signature module SatisfiesConstraintSig < HasTypeTreeSig TypeTree > {
869+ signature module SatisfiesConstraintInputSig < HasTypeTreeSig HasTypeTree > {
870870 /** Holds if it is relevant to know if `term` satisfies `constraint`. */
871- predicate relevantConstraint ( TypeTree term , Type constraint ) ;
871+ predicate relevantConstraint ( HasTypeTree term , Type constraint ) ;
872872 }
873873
874- module SatisfiesConstraint< HasTypeTreeSig TypeTree, SatisfiesConstraintSig< TypeTree > Input> {
875- import Input
874+ module SatisfiesConstraint<
875+ HasTypeTreeSig HasTypeTree, SatisfiesConstraintInputSig< HasTypeTree > Input>
876+ {
877+ private import Input
876878
877- private module IsInstantiationOfInput implements IsInstantiationOfInputSig< TypeTree > {
878- predicate potentialInstantiationOf ( TypeTree tt , TypeAbstraction abs , TypeMention cond ) {
879+ private module IsInstantiationOfInput implements IsInstantiationOfInputSig< HasTypeTree > {
880+ predicate potentialInstantiationOf ( HasTypeTree tt , TypeAbstraction abs , TypeMention cond ) {
879881 exists ( Type constraint , Type type |
880882 type = tt .getTypeAt ( TypePath:: nil ( ) ) and
881883 relevantConstraint ( tt , constraint ) and
@@ -891,7 +893,8 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
891893 }
892894
893895 /** Holds if the type tree has the type `type` and should satisfy `constraint`. */
894- private predicate hasTypeConstraint ( TypeTree term , Type type , Type constraint ) {
896+ pragma [ nomagic]
897+ private predicate hasTypeConstraint ( HasTypeTree term , Type type , Type constraint ) {
895898 type = term .getTypeAt ( TypePath:: nil ( ) ) and
896899 relevantConstraint ( term , constraint )
897900 }
@@ -901,7 +904,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
901904 */
902905 pragma [ nomagic]
903906 private predicate hasConstraintMention (
904- TypeTree tt , TypeAbstraction abs , TypeMention sub , Type constraint ,
907+ HasTypeTree tt , TypeAbstraction abs , TypeMention sub , Type constraint ,
905908 TypeMention constraintMention
906909 ) {
907910 exists ( Type type | hasTypeConstraint ( tt , type , constraint ) |
@@ -916,14 +919,15 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
916919 // constraint we need to find the right implementation, which is the
917920 // one where the type instantiates the precondition.
918921 if countConstraintImplementations ( type , constraint ) > 1
919- then IsInstantiationOf< TypeTree , IsInstantiationOfInput > :: isInstantiationOf ( tt , abs , sub )
922+ then
923+ IsInstantiationOf< HasTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( tt , abs , sub )
920924 else any ( )
921925 )
922926 }
923927
924928 pragma [ nomagic]
925929 private predicate satisfiesConstraintTypeMention0 (
926- TypeTree tt , Type constraint , TypeAbstraction abs , TypeMention sub , TypePath path , Type t
930+ HasTypeTree tt , Type constraint , TypeAbstraction abs , TypeMention sub , TypePath path , Type t
927931 ) {
928932 exists ( TypeMention constraintMention |
929933 hasConstraintMention ( tt , abs , sub , constraint , constraintMention ) and
@@ -933,7 +937,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
933937
934938 pragma [ nomagic]
935939 private predicate satisfiesConstraintTypeMention1 (
936- TypeTree tt , Type constraint , TypePath path , TypePath pathToTypeParamInSub
940+ HasTypeTree tt , Type constraint , TypePath path , TypePath pathToTypeParamInSub
937941 ) {
938942 exists ( TypeAbstraction abs , TypeMention sub , TypeParameter tp |
939943 satisfiesConstraintTypeMention0 ( tt , constraint , abs , sub , path , tp ) and
@@ -947,7 +951,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
947951 * with the type `t` at `path`.
948952 */
949953 pragma [ nomagic]
950- predicate satisfiesConstraintTypeMention ( TypeTree tt , Type constraint , TypePath path , Type t ) {
954+ predicate satisfiesConstraintType ( HasTypeTree tt , Type constraint , TypePath path , Type t ) {
951955 exists ( TypeAbstraction abs |
952956 satisfiesConstraintTypeMention0 ( tt , constraint , abs , _, path , t ) and
953957 not t = abs .getATypeParameter ( )
@@ -958,6 +962,9 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
958962 tt .getTypeAt ( pathToTypeParamInSub .appendInverse ( suffix ) ) = t and
959963 path = prefix0 .append ( suffix )
960964 )
965+ or
966+ tt .getTypeAt ( TypePath:: nil ( ) ) = constraint and
967+ t = tt .getTypeAt ( path )
961968 }
962969 }
963970
@@ -1234,17 +1241,19 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
12341241 Location getLocation ( ) { result = a .getLocation ( ) }
12351242 }
12361243
1237- private module SatisfiesConstraintInput implements SatisfiesConstraintSig< RelevantAccess > {
1244+ private module SatisfiesConstraintInput implements
1245+ SatisfiesConstraintInputSig< RelevantAccess >
1246+ {
12381247 predicate relevantConstraint ( RelevantAccess at , Type constraint ) {
12391248 constraint = at .getConstraint ( )
12401249 }
12411250 }
12421251
1243- predicate satisfiesConstraintTypeMention (
1252+ predicate satisfiesConstraintType (
12441253 Access a , AccessPosition apos , TypePath prefix , Type constraint , TypePath path , Type t
12451254 ) {
12461255 exists ( RelevantAccess at | at = MkRelevantAccess ( a , _, apos , prefix ) |
1247- SatisfiesConstraint< RelevantAccess , SatisfiesConstraintInput > :: satisfiesConstraintTypeMention ( at ,
1256+ SatisfiesConstraint< RelevantAccess , SatisfiesConstraintInput > :: satisfiesConstraintType ( at ,
12481257 constraint , path , t )
12491258 )
12501259 }
@@ -1382,7 +1391,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
13821391 accessDeclarationPositionMatch ( apos , dpos ) and
13831392 typeParameterConstraintHasTypeParameter ( target , dpos , pathToTp2 , _, constraint , pathToTp ,
13841393 tp ) and
1385- AccessConstraint:: satisfiesConstraintTypeMention ( a , apos , pathToTp2 , constraint ,
1394+ AccessConstraint:: satisfiesConstraintType ( a , apos , pathToTp2 , constraint ,
13861395 pathToTp .appendInverse ( path ) , t )
13871396 )
13881397 }
0 commit comments