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