Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -351,7 +351,7 @@ module ArgsAreInstantiationsOf<ArgsAreInstantiationsOfInputSig Input> {
|
rnk = 0
or
argsAreInstantiationsOfFromIndex(call, abs, f, rnk - 1)
argsAreInstantiationsOfToIndex(call, abs, f, rnk - 1)
)
}

Expand All @@ -360,15 +360,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)
)
Expand All @@ -381,7 +381,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))
)
}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -578,21 +578,21 @@ 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 |
t = resolveNthTypeAt(app, abs, constraint, i, path) and
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))))
}

Expand Down Expand Up @@ -620,7 +620,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
Expand All @@ -630,15 +630,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)
)
)
Expand All @@ -655,19 +655,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)
)
}

Expand Down Expand Up @@ -697,7 +697,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)
)
)
}
Expand Down
Loading