public void bodiesFound()

in base/src/main/java/org/arend/typechecking/order/listener/TypecheckingOrderingListener.java [360:497]
123 lines of code
38 McCabe index (conditional complexity)

  public void bodiesFound(List<Concrete.ResolvableDefinition> definitions) {
    Map<FunctionDefinition,Concrete.Definition> functionDefinitions = new HashMap<>();
    Map<FunctionDefinition, List<? extends ElimClause<ExpressionPattern>>> clausesMap = new HashMap<>();
    Set<DataDefinition> dataDefinitions = new HashSet<>();
    List<Concrete.ResolvableDefinition> orderedDefinitions = new ArrayList<>(definitions.size());
    List<Concrete.ResolvableDefinition> otherDefs = new ArrayList<>();
    Set<TCDefReferable> refs = new HashSet<>();
    for (Concrete.ResolvableDefinition definition : definitions) {
      Concrete.ResolvableDefinition newDef = myDesugaredDefinitions.get(definition.getData());
      if (newDef == null) newDef = definition;
      Definition typechecked = newDef.getData().getTypechecked();
      if (typechecked instanceof DataDefinition) {
        dataDefinitions.add((DataDefinition) typechecked);
        orderedDefinitions.add(newDef);
      } else {
        otherDefs.add(newDef);
      }
      refs.add(definition.getData());
    }
    orderedDefinitions.addAll(otherDefs);

    DefinitionTypechecker typechecking = new DefinitionTypechecker(null, refs);
    myCurrentDefinitions = new ArrayList<>();
    for (Concrete.ResolvableDefinition definition : orderedDefinitions) {
      myCurrentDefinitions.add(definition.getData());
    }

    Set<Definition> newDefs = new HashSet<>();
    List<Pair<Definition, DefinitionListener>> listeners = new ArrayList<>();
    for (Concrete.ResolvableDefinition definition : orderedDefinitions) {
      Definition def = definition.getData().getTypechecked();
      if (def instanceof TopLevelDefinition) {
        Suspension suspension = mySuspensions.get(definition.getData());
        if (suspension != null) {
          ((TopLevelDefinition) def).setUniverseKind(suspension.universeKind);
        }
      }
    }

    for (Concrete.ResolvableDefinition definition : orderedDefinitions) {
      typecheckingBodyStarted(definition.getData());

      Definition def = definition.getData().getTypechecked();
      Suspension suspension = mySuspensions.remove(definition.getData());
      if (suspension != null && suspension.isNew) {
        newDefs.add(def);
      }
      if (myHeadersAreOK && suspension != null) {
        typechecking.setTypechecker(suspension.typechecker);
        typechecking.updateState(suspension.isNew);
        List<? extends ElimClause<ExpressionPattern>> clauses = typechecking.typecheckBody(def, definition, dataDefinitions);
        if (def instanceof FunctionDefinition && definition instanceof Concrete.Definition) {
          functionDefinitions.put((FunctionDefinition) def, (Concrete.Definition) definition);
          if (clauses != null) {
            clausesMap.put((FunctionDefinition) def, clauses);
          }
        }

        ArendExtension extension = suspension.typechecker.getExtension();
        if (extension != null) {
          DefinitionListener listener = extension.getDefinitionListener();
          if (listener != null) {
            listeners.add(new Pair<>(def, listener));
          }
        }
      }
    }
    myCurrentDefinitions = Collections.emptyList();

    myHeadersAreOK = true;

    boolean fixLevels = true;
    Set<TopLevelDefinition> allDefinitions = new LinkedHashSet<>();
    for (Concrete.ResolvableDefinition definition : orderedDefinitions) {
      Definition typechecked = definition.getData().getTypechecked();
      if (!newDefs.contains(typechecked)) continue;
      if (typechecked instanceof FunctionDefinition) {
        ((FunctionDefinition) typechecked).setRecursiveDefinitions(allDefinitions);
        allDefinitions.add((FunctionDefinition) typechecked);
      } else if (typechecked instanceof DataDefinition) {
        ((DataDefinition) typechecked).setRecursiveDefinitions(allDefinitions);
        allDefinitions.add((DataDefinition) typechecked);
      }
      if (definition instanceof Concrete.FunctionDefinition && ((Concrete.FunctionDefinition) definition).getKind().isCoclause()) {
        fixLevels = false;
      }
    }

    if (fixLevels) {
      FixLevelParameters.fix(allDefinitions, newDefs);
    }

    if (!functionDefinitions.isEmpty()) {
      FindDefCallVisitor<DataDefinition> visitor = new FindDefCallVisitor<>(dataDefinitions, false);
      Iterator<Map.Entry<FunctionDefinition, Concrete.Definition>> it = functionDefinitions.entrySet().iterator();
      while (it.hasNext()) {
        Map.Entry<FunctionDefinition, Concrete.Definition> entry = it.next();
        visitor.visitBody(entry.getKey().getActualBody(), null);
        Definition found = visitor.getFoundDefinition();
        if (found != null) {
          entry.getKey().setBody(null);
          entry.getKey().addStatus(Definition.TypeCheckingStatus.HAS_ERRORS);
          myErrorReporter.report(new TypecheckingError("Mutually recursive function refers to data type '" + found.getName() + "'", entry.getValue()).withDefinition(entry.getKey().getReferable()));
          it.remove();
          visitor.clear();
        }
      }

      if (!functionDefinitions.isEmpty()) {
        checkRecursiveFunctions(functionDefinitions, clausesMap);
      }
    }

    for (Concrete.ResolvableDefinition definition : orderedDefinitions) {
      if (definition.getData().getTypechecked().accept(new SearchVisitor<Void>() {
        @Override
        protected CoreExpression.FindAction processDefCall(DefCallExpression expr, Void param) {
          return expr instanceof LeveledDefCallExpression && expr.getDefinition() instanceof TopLevelDefinition && allDefinitions.contains((TopLevelDefinition) expr.getDefinition()) && !((LeveledDefCallExpression) expr).getLevels().compare(expr.getDefinition().makeIdLevels(), CMP.EQ, DummyEquations.getInstance(), null) ? CoreExpression.FindAction.STOP : CoreExpression.FindAction.CONTINUE;
        }
      }, null)) {
        myErrorReporter.report(new TypecheckingError("Recursive call must have the same levels as the definition", definition));
      }
    }

    for (TopLevelDefinition definition : allDefinitions) {
      setParametersOriginalDefinitionsDependency(definition);
    }

    findAxiomsAndGoals(orderedDefinitions, newDefs);

    for (Definition definition : allDefinitions) {
      typecheckingBodyFinished(definition.getReferable(), definition);
    }

    for (Pair<Definition, DefinitionListener> pair : listeners) {
      pair.proj2.typechecked(pair.proj1);
    }
  }