private void calculateParametersTypecheckingOrder()

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);
    }
  }