protected void sccFound()

in base/src/main/java/org/arend/typechecking/order/Ordering.java [200:333]


  protected void sccFound(List<Concrete.ResolvableDefinition> scc) {
    if (myStage.ordinal() >= Stage.WITHOUT_BODIES.ordinal()) {
      myOrderingListener.cycleFound(scc, false);
      return;
    }
    if (scc.isEmpty()) {
      return;
    }
    if (scc.size() == 1) {
      myOrderingListener.unitFound(scc.get(0), true);
      return;
    }

    boolean hasUse = false;
    boolean hasInstances = false;
    for (Concrete.ResolvableDefinition definition : scc) {
      if (definition instanceof Concrete.FunctionDefinition && ((Concrete.FunctionDefinition) definition).getKind() == FunctionKind.INSTANCE) {
        if (myStage.ordinal() >= Stage.WITHOUT_INSTANCES.ordinal()) {
          myOrderingListener.cycleFound(scc, false);
          return;
        }
        hasInstances = true;
        break;
      }
      if (definition instanceof Concrete.UseDefinition && ((Concrete.UseDefinition) definition).getKind() != FunctionKind.FUNC_COCLAUSE) {
        if (myStage.ordinal() >= Stage.WITHOUT_USE.ordinal()) {
          myOrderingListener.cycleFound(scc, false);
          return;
        }
        hasUse = true;
      }
    }

    Set<TCReferable> dependencies = new HashSet<>();
    for (Concrete.ResolvableDefinition definition : scc) {
      dependencies.add(definition.getData());
    }

    if (hasInstances) {
      Map<TCDefReferable, Concrete.FunctionDefinition> instanceMap = new HashMap<>();
      for (Concrete.ResolvableDefinition definition : scc) {
        if (definition instanceof Concrete.FunctionDefinition funDef && funDef.getKind() == FunctionKind.INSTANCE) {
          instanceMap.put(definition.getData(), funDef);
        }
      }

      TarjanSCC<TCDefReferable> tarjan = new TarjanSCC<>() {
        @Override
        protected boolean forDependencies(TCDefReferable unit, Consumer<TCDefReferable> consumer) {
          boolean[] withLoops = new boolean[] { false };
          InstanceProvider instanceProvider = myInstanceProviderSet.get(unit);
          if (instanceProvider != null) {
            instanceProvider.findInstance(instance -> {
              if (instanceMap.containsKey(instance)) {
                consumer.accept(instance);
                if (unit.equals(instance)) {
                  withLoops[0] = true;
                }
              }
              return false;
            });
          }
          return withLoops[0];
        }

        @Override
        protected void sccFound(List<TCDefReferable> scc) {
          List<Concrete.ResolvableDefinition> defs = new ArrayList<>(scc.size());
          for (TCDefReferable ref : scc) {
            Concrete.FunctionDefinition def = instanceMap.get(ref);
            if (def != null) defs.add(def);
          }
          if (!defs.isEmpty()) {
            myOrderingListener.cycleFound(defs, true);
          }
        }
      };
      for (Concrete.ResolvableDefinition definition : scc) {
        if (definition instanceof Concrete.FunctionDefinition funDef && funDef.getKind() == FunctionKind.INSTANCE) {
          tarjan.order(definition.getData());
        }
      }

      Ordering ordering = new Ordering(this, dependencies, Stage.WITHOUT_INSTANCES);
      for (Concrete.ResolvableDefinition definition : scc) {
        ordering.order(definition);
      }
      return;
    }

    if (hasUse) {
      Ordering ordering = new Ordering(this, dependencies, Stage.WITHOUT_USE);
      for (Concrete.ResolvableDefinition definition : scc) {
        ordering.order(definition);
      }

      List<Concrete.UseDefinition> useDefinitions = new ArrayList<>();
      for (Concrete.ResolvableDefinition definition : scc) {
        if (definition instanceof Concrete.UseDefinition) {
          useDefinitions.add((Concrete.UseDefinition) definition);
        } else if (definition instanceof Concrete.ClassDefinition) {
          myOrderingListener.classFinished((Concrete.ClassDefinition) definition);
        }
      }
      myOrderingListener.useFound(useDefinitions);
      return;
    }

    for (Concrete.ResolvableDefinition definition : scc) {
      if (definition instanceof Concrete.ClassDefinition) {
        myOrderingListener.cycleFound(scc, false);
        return;
      }
    }

    Set<TCDefReferable> defSet = new HashSet<>();
    List<Concrete.ResolvableDefinition> defs = new ArrayList<>(scc.size());
    for (Concrete.ResolvableDefinition def : scc) {
      defs.add(def);
      defSet.add(def.getData());
      if (def instanceof Concrete.Definition) {
        ((Concrete.Definition) def).setRecursiveDefinitions(defSet);
      }
    }

    myOrderingListener.preBodiesFound(defs);
    Ordering ordering = new Ordering(this, dependencies, Stage.WITHOUT_BODIES);
    for (Concrete.ResolvableDefinition definition : scc) {
      ordering.order(definition);
    }

    new DefinitionComparator(myComparator).sort(defs);
    myOrderingListener.bodiesFound(defs);
  }