in base/src/main/java/org/arend/typechecking/visitor/DefinitionTypechecker.java [245:363]
private void calculateParametersTypecheckingOrder(Definition definition) {
List<DependentLink> parametersList;
if (definition instanceof Constructor && ((Constructor) definition).getDataTypeParameters().hasNext()) {
parametersList = new ArrayList<>(2);
parametersList.add(((Constructor) definition).getDataTypeParameters());
parametersList.add(definition.getParameters());
} else {
parametersList = Collections.singletonList(definition.getParameters());
}
LinkedHashSet<Binding> processed = new LinkedHashSet<>();
for (DependentLink link : parametersList) {
boolean isDataTypeParameter = parametersList.size() > 1 && link == parametersList.get(0);
for (; link.hasNext(); link = link.getNext()) {
if (processed.contains(link)) {
continue;
}
if (link.isExplicit() && !isDataTypeParameter) {
processed.add(link);
} else {
FreeVariablesClassifier classifier = new FreeVariablesClassifier(link);
boolean isDataTypeParam = isDataTypeParameter;
DependentLink link1 = definition instanceof FunctionDefinition ? link : link.getNext(); // if link1 == link, check the result type
boolean found = false;
while (true) {
if (!link1.hasNext()) {
if (isDataTypeParam) {
link1 = parametersList.get(1);
isDataTypeParam = false;
}
if (!link1.hasNext()) {
break;
}
}
boolean checkResultType = link1 == link && definition instanceof FunctionDefinition;
DependentLink actualLink = checkResultType ? EmptyDependentLink.getInstance() : link1;
FreeVariablesClassifier.Result result;
if (checkResultType) {
Expression type = ((FunctionDefinition) definition).getResultType();
result = type instanceof ReferenceExpression && ((ReferenceExpression) type).getBinding() == link ? FreeVariablesClassifier.Result.BAD : type.accept(classifier, true);
} else {
result = classifier.checkBinding(link1);
}
if ((result == FreeVariablesClassifier.Result.GOOD || result == FreeVariablesClassifier.Result.BOTH) && processed.contains(actualLink)) {
found = true;
processed.add(link);
break;
}
if (result == FreeVariablesClassifier.Result.GOOD && (checkResultType || link1.isExplicit())) {
found = true;
processed.add(link);
Set<Binding> freeVars = new HashSet<>();
getFreeVariablesClosure(checkResultType ? ((FunctionDefinition) definition).getResultType() : link1.getTypeExpr(), freeVars);
for (DependentLink link2 : parametersList) {
for (; link2.hasNext() && link2 != actualLink; link2 = link2.getNext()) {
if (freeVars.contains(link2)) {
processed.add(link2);
}
}
if (!checkResultType && link2 == link1) {
break;
}
}
processed.add(actualLink);
break;
}
link1 = link1.getNext();
}
if (!found) {
processed.add(link);
}
}
}
}
boolean needReorder = false;
DependentLink link = parametersList.get(0);
boolean isDataTypeParameter = parametersList.size() > 1;
for (Binding binding : processed) {
if (binding != link) {
needReorder = true;
break;
}
if (link.hasNext()) {
link = link.getNext();
if (!link.hasNext() && isDataTypeParameter) {
link = parametersList.get(1);
isDataTypeParameter = false;
}
}
}
if (needReorder) {
Map<Binding,Integer> map = new HashMap<>();
if (definition instanceof FunctionDefinition) {
map.put(EmptyDependentLink.getInstance(), -1);
}
int i = 0;
for (DependentLink link1 : parametersList) {
for (; link1.hasNext(); link1 = link1.getNext()) {
map.put(link1,i);
i++;
}
}
List<Integer> order = new ArrayList<>(processed.size());
for (Binding binding : processed) {
order.add(map.get(binding));
}
if (order.get(order.size() - 1) == -1) {
order.remove(order.size() - 1);
}
definition.setParametersTypecheckingOrder(order);
}
}