in meta/src/main/java/org/arend/lib/meta/closure/CongruenceClosure.java [412:471]
public List<VarId> getVarIds(CoreExpression value) {
int prefixSize = 0;
List<VarId> result = new ArrayList<>();
int index = getIndex(value);
if (index == -1) {
return result;
}
if (!(value instanceof CoreDefCallExpression)) {
return result;
}
List<Integer> argInds = new ArrayList<>();
for (CoreExpression arg : ((CoreDefCallExpression) value).getDefCallArguments()) {
int argInd = getIndex(arg);
argInds.add(argInd);
}
int numArgs = argInds.size();
for (int i = 0; i < values.size(); i++) {
if (i == index) continue;
CoreExpression element = values.get(i);
if (element instanceof CoreDefCallExpression && ((CoreDefCallExpression) value).getDefinition().equals(((CoreDefCallExpression) element).getDefinition())) {
if (((CoreDefCallExpression) element).getDefCallArguments().size() != numArgs) return Collections.emptyList();
if (prefixSize == 0) {
result.add(new VarId(i, numArgs - prefixSize - 1));
++prefixSize;
}
for (int j = 0; j < numArgs; ++j) {
if (argInds.get(j) == -1) {
break;
}
int elementArg = getIndex(((CoreDefCallExpression) element).getDefCallArguments().get(j));
if (argInds.get(j) == elementArg) {
if (prefixSize <= j + 1) {
result.add(new VarId(i, numArgs - prefixSize - 1));
++prefixSize;
}
} else {
break;
}
}
if (prefixSize > argInds.size() || prefixSize > 0 && argInds.get(prefixSize - 1) == -1) {
break;
}
}
}
for (int i = 0; i < numArgs - prefixSize; ++i) {
result.add(null);
}
result.add(new VarId(index, -1));
Collections.reverse(result);
return result;
}