@@ -731,20 +731,24 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
731
731
IsInstantiationOfInputSig< TypeMentionTypeTree >
732
732
{
733
733
pragma [ nomagic]
734
- private predicate typeCondition ( Type type , TypeAbstraction abs , TypeMentionTypeTree lhs ) {
735
- conditionSatisfiesConstraint ( abs , lhs , _) and type = resolveTypeMentionRoot ( lhs )
734
+ private predicate typeCondition (
735
+ Type type , TypeAbstraction abs , TypeMentionTypeTree condition
736
+ ) {
737
+ conditionSatisfiesConstraint ( abs , condition , _) and
738
+ type = resolveTypeMentionRoot ( condition )
736
739
}
737
740
738
741
pragma [ nomagic]
739
- private predicate typeConstraint ( Type type , TypeMentionTypeTree rhs ) {
740
- conditionSatisfiesConstraint ( _, _, rhs ) and type = resolveTypeMentionRoot ( rhs )
742
+ private predicate typeConstraint ( Type type , TypeMentionTypeTree constraint ) {
743
+ conditionSatisfiesConstraint ( _, _, constraint ) and
744
+ type = resolveTypeMentionRoot ( constraint )
741
745
}
742
746
743
747
predicate potentialInstantiationOf (
744
- TypeMentionTypeTree condition , TypeAbstraction abs , TypeMention constraint
748
+ TypeMentionTypeTree constraint , TypeAbstraction abs , TypeMention condition
745
749
) {
746
750
exists ( Type type |
747
- typeConstraint ( type , condition ) and typeCondition ( type , abs , constraint )
751
+ typeConstraint ( type , constraint ) and typeCondition ( type , abs , condition )
748
752
)
749
753
}
750
754
}
@@ -761,20 +765,20 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
761
765
constraint .resolveTypeAt ( path ) = t
762
766
or
763
767
// recursive case
764
- exists ( TypeAbstraction midAbs , TypeMention midSup , TypeMention midSub |
765
- conditionSatisfiesConstraint ( abs , condition , midSup ) and
766
- // NOTE: `midAbs` describe the free type variables in `midSub `, hence
768
+ exists ( TypeAbstraction midAbs , TypeMention midConstraint , TypeMention midCondition |
769
+ conditionSatisfiesConstraint ( abs , condition , midConstraint ) and
770
+ // NOTE: `midAbs` describe the free type variables in `midCondition `, hence
767
771
// we use that for instantiation check.
768
- IsInstantiationOf< TypeMentionTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( midSup ,
769
- midAbs , midSub )
772
+ IsInstantiationOf< TypeMentionTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( midConstraint ,
773
+ midAbs , midCondition )
770
774
|
771
- conditionSatisfiesConstraintTypeAt ( midAbs , midSub , constraint , path , t ) and
775
+ conditionSatisfiesConstraintTypeAt ( midAbs , midCondition , constraint , path , t ) and
772
776
not t = midAbs .getATypeParameter ( )
773
777
or
774
778
exists ( TypePath prefix , TypePath suffix , TypeParameter tp |
775
779
tp = midAbs .getATypeParameter ( ) and
776
- conditionSatisfiesConstraintTypeAt ( midAbs , midSub , constraint , prefix , tp ) and
777
- instantiatesWith ( midSup , midSub , tp , suffix , t ) and
780
+ conditionSatisfiesConstraintTypeAt ( midAbs , midCondition , constraint , prefix , tp ) and
781
+ instantiatesWith ( midConstraint , midCondition , tp , suffix , t ) and
778
782
path = prefix .append ( suffix )
779
783
)
780
784
)
@@ -949,23 +953,24 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
949
953
*/
950
954
pragma [ nomagic]
951
955
private predicate hasConstraintMention (
952
- HasTypeTree tt , TypeAbstraction abs , TypeMention sub , Type constraint ,
956
+ HasTypeTree tt , TypeAbstraction abs , TypeMention condition , Type constraint ,
953
957
TypeMention constraintMention
954
958
) {
955
959
exists ( Type type | hasTypeConstraint ( tt , type , constraint ) |
956
960
not exists ( countConstraintImplementations ( type , constraint ) ) and
957
- conditionSatisfiesConstraintTypeAt ( abs , sub , constraintMention , _, _) and
958
- resolveTypeMentionRoot ( sub ) = abs .getATypeParameter ( ) and
961
+ conditionSatisfiesConstraintTypeAt ( abs , condition , constraintMention , _, _) and
962
+ resolveTypeMentionRoot ( condition ) = abs .getATypeParameter ( ) and
959
963
constraint = resolveTypeMentionRoot ( constraintMention )
960
964
or
961
965
countConstraintImplementations ( type , constraint ) > 0 and
962
- rootTypesSatisfaction ( type , constraint , abs , sub , constraintMention ) and
966
+ rootTypesSatisfaction ( type , constraint , abs , condition , constraintMention ) and
963
967
// When there are multiple ways the type could implement the
964
968
// constraint we need to find the right implementation, which is the
965
969
// one where the type instantiates the precondition.
966
970
if multipleConstraintImplementations ( type , constraint )
967
971
then
968
- IsInstantiationOf< HasTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( tt , abs , sub )
972
+ IsInstantiationOf< HasTypeTree , IsInstantiationOfInput > :: isInstantiationOf ( tt , abs ,
973
+ condition )
969
974
else any ( )
970
975
)
971
976
}
0 commit comments