Merge pull request #20848 from hvitved/rust/ranked-forex-rename

Rust: Use `ToIndex` instead of `FromIndex` in ranked `forex` predicates
This commit is contained in:
Tom Hvitved
2025-11-24 13:05:58 +01:00
committed by GitHub
2 changed files with 16 additions and 16 deletions

View File

@@ -352,7 +352,7 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
|
rnk = 0
or
argsAreInstantiationsOfFromIndex(call, abs, f, rnk - 1)
argsAreInstantiationsOfToIndex(call, abs, f, rnk - 1)
)
}
@@ -361,15 +361,15 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
}
}
private module ArgIsInstantiationOfFromIndex =
private module ArgIsInstantiationOfToIndex =
ArgIsInstantiationOf<CallAndPos, ArgIsInstantiationOfInput>;
pragma[nomagic]
private predicate argsAreInstantiationsOfFromIndex(
private predicate argsAreInstantiationsOfToIndex(
Input::Call call, ImplOrTraitItemNode i, Function f, int rnk
) {
exists(FunctionPosition pos |
ArgIsInstantiationOfFromIndex::argIsInstantiationOf(MkCallAndPos(call, pos), i, _) and
ArgIsInstantiationOfToIndex::argIsInstantiationOf(MkCallAndPos(call, pos), i, _) and
call.hasTargetCand(i, f) and
toCheckRanked(i, f, pos, rnk)
)
@@ -382,7 +382,7 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
pragma[nomagic]
predicate argsAreInstantiationsOf(Input::Call call, ImplOrTraitItemNode i, Function f) {
exists(int rnk |
argsAreInstantiationsOfFromIndex(call, i, f, rnk) and
argsAreInstantiationsOfToIndex(call, i, f, rnk) and
rnk = max(int r | toCheckRanked(i, f, _, r))
)
}

View File

@@ -580,7 +580,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
}
pragma[nomagic]
private predicate satisfiesConcreteTypesFromIndex(
private predicate satisfiesConcreteTypesToIndex(
App app, TypeAbstraction abs, Constraint constraint, int i
) {
exists(Type t, TypePath path |
@@ -588,13 +588,13 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
if t = abs.getATypeParameter() then any() else app.getTypeAt(path) = t
) and
// Recurse unless we are at the first path
if i = 0 then any() else satisfiesConcreteTypesFromIndex(app, abs, constraint, i - 1)
if i = 0 then any() else satisfiesConcreteTypesToIndex(app, abs, constraint, i - 1)
}
/** Holds if all the concrete types in `constraint` also occur in `app`. */
pragma[nomagic]
private predicate satisfiesConcreteTypes(App app, TypeAbstraction abs, Constraint constraint) {
satisfiesConcreteTypesFromIndex(app, abs, constraint,
satisfiesConcreteTypesToIndex(app, abs, constraint,
max(int i | exists(getNthPath(constraint, i))))
}
@@ -622,7 +622,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
}
pragma[nomagic]
private predicate typeParametersEqualFromIndexBase(
private predicate typeParametersEqualToIndexBase(
App app, TypeAbstraction abs, Constraint constraint, TypeParameter tp, TypePath path
) {
path = getNthTypeParameterPath(constraint, tp, 0) and
@@ -632,15 +632,15 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
}
pragma[nomagic]
private predicate typeParametersEqualFromIndex(
private predicate typeParametersEqualToIndex(
App app, TypeAbstraction abs, Constraint constraint, TypeParameter tp, Type t, int i
) {
exists(TypePath path |
t = app.getTypeAt(path) and
if i = 0
then typeParametersEqualFromIndexBase(app, abs, constraint, tp, path)
then typeParametersEqualToIndexBase(app, abs, constraint, tp, path)
else (
typeParametersEqualFromIndex(app, abs, constraint, tp, t, i - 1) and
typeParametersEqualToIndex(app, abs, constraint, tp, t, i - 1) and
path = getNthTypeParameterPath(constraint, tp, i)
)
)
@@ -657,19 +657,19 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
exists(int n | n = max(int i | exists(getNthTypeParameterPath(constraint, tp, i))) |
// If the largest index is 0, then there are no equalities to check as
// the type parameter only occurs once.
if n = 0 then any() else typeParametersEqualFromIndex(app, abs, constraint, tp, _, n)
if n = 0 then any() else typeParametersEqualToIndex(app, abs, constraint, tp, _, n)
)
)
}
private predicate typeParametersHaveEqualInstantiationFromIndex(
private predicate typeParametersHaveEqualInstantiationToIndex(
App app, TypeAbstraction abs, Constraint constraint, int i
) {
exists(TypeParameter tp | tp = getNthTypeParameter(abs, i) |
typeParametersEqual(app, abs, constraint, tp) and
if i = 0
then any()
else typeParametersHaveEqualInstantiationFromIndex(app, abs, constraint, i - 1)
else typeParametersHaveEqualInstantiationToIndex(app, abs, constraint, i - 1)
)
}
@@ -699,7 +699,7 @@ module Make1<LocationSig Location, InputSig1<Location> Input1> {
not exists(getNthTypeParameter(abs, _))
or
exists(int n | n = max(int i | exists(getNthTypeParameter(abs, i))) |
typeParametersHaveEqualInstantiationFromIndex(app, abs, constraint, n)
typeParametersHaveEqualInstantiationToIndex(app, abs, constraint, n)
)
)
}