TYCK: SCC tycker

Signed-off-by: imkiva <imkiva@islovely.icu>

api/src/main/java/org/aya/api/error/CollectingReporter.java

@@ -5,7 +5,7 @@
 import kala.collection.mutable.Buffer;
 import org.jetbrains.annotations.NotNull;
 
-public record CollectingReporter(@NotNull Buffer<@NotNull Problem> problems) implements Reporter {
+public record CollectingReporter(@NotNull Buffer<@NotNull Problem> problems) implements StoringReporter {
   public CollectingReporter() {
     this(Buffer.create());
   }

api/src/main/java/org/aya/api/error/DelayedReporter.java

@@ -8,7 +8,7 @@
 public record DelayedReporter(
   @NotNull Reporter delegated,
   @NotNull Buffer<Problem> problems
-) implements Reporter, AutoCloseable {
+) implements StoringReporter, AutoCloseable {
   public DelayedReporter(@NotNull Reporter delegated) {
     this(delegated, Buffer.create());
   }

api/src/main/java/org/aya/api/error/StoringReporter.java

@@ -0,0 +1,10 @@
+// Copyright (c) 2020-2021 Yinsen (Tesla) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.api.error;
+
+import kala.collection.mutable.Buffer;
+import org.jetbrains.annotations.NotNull;
+
+public interface StoringReporter extends Reporter {
+  @NotNull Buffer<Problem> problems();
+}

api/src/main/java/org/aya/api/util/InterruptException.java

@@ -13,5 +13,6 @@ public abstract class InterruptException extends RuntimeException {
   public enum InterruptStage {
     Parsing,
     Resolving,
+    Tycking,
   }
 }

base/src/main/java/org/aya/concrete/desugar/error/OperatorProblem.java

@@ -96,7 +96,7 @@ public record Circular(
 
     @Override public @NotNull Doc describe(@NotNull DistillerOptions options) {
       return Doc.sep(
-        Doc.english("Precedence circle found between"),
+        Doc.english("Circular precedence found between"),
         Doc.commaList(items.view().map(BinOpSet.BinOP::name).toImmutableSeq()
           .sorted().view().map(Doc::plain))
       );

base/src/main/java/org/aya/concrete/resolve/module/FileModuleLoader.java

@@ -8,25 +8,22 @@
 import kala.collection.mutable.MutableMap;
 import kala.function.CheckedConsumer;
 import org.aya.api.error.DelayedReporter;
-import org.aya.api.error.Problem;
 import org.aya.api.error.Reporter;
 import org.aya.api.error.SourceFileLocator;
 import org.aya.api.ref.Var;
 import org.aya.api.util.InternalException;
 import org.aya.concrete.Expr;
 import org.aya.concrete.desugar.BinOpSet;
 import org.aya.concrete.parse.AyaParsing;
-import org.aya.concrete.remark.Remark;
 import org.aya.concrete.resolve.ResolveInfo;
 import org.aya.concrete.resolve.ShallowResolveInfo;
 import org.aya.concrete.resolve.context.EmptyContext;
 import org.aya.concrete.resolve.context.ModuleContext;
 import org.aya.concrete.resolve.visitor.StmtShallowResolver;
-import org.aya.concrete.stmt.Decl;
-import org.aya.concrete.stmt.Sample;
 import org.aya.concrete.stmt.Stmt;
 import org.aya.core.def.Def;
 import org.aya.tyck.ExprTycker;
+import org.aya.tyck.order.SCCTycker;
 import org.aya.tyck.trace.Trace;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -91,13 +88,14 @@ public static <E extends Exception> void tyckModule(
     program.forEach(s -> s.desugar(reporter, resolveInfo.opSet()));
     // in case we have un-messaged TyckException
     try (var delayedReporter = new DelayedReporter(reporter)) {
+      var sccTycker = new SCCTycker(builder, delayedReporter);
       var SCCs = resolveInfo.declGraph().topologicalOrder()
         .view().appendedAll(resolveInfo.sampleGraph().topologicalOrder());
       var wellTyped = SCCs
-        .flatMap(scc -> tyckSCC(scc, builder, delayedReporter))
+        .flatMap(sccTycker::tyckSCC)
         .toImmutableSeq();
       onTycked.acceptChecked(wellTyped);
-    } catch (GroupTyckingFailed ignored) {
+    } catch (SCCTycker.SCCTyckingFailed ignored) {
       // stop tycking the rest of groups since some of their dependencies are failed.
       // Random thought: we may assume their signatures are correct and try to tyck
       // the rest of program as much as possible, which can make LSP more user-friendly?
@@ -106,24 +104,6 @@ public static <E extends Exception> void tyckModule(
     }
   }
 
-  /**
-   * Tyck a group of statements in an SCC.
-   */
-  private static @NotNull ImmutableSeq<Def> tyckSCC(@NotNull ImmutableSeq<Stmt> scc, Trace.@Nullable Builder builder, DelayedReporter reporter) {
-    // TODO[kiva]: check signatures first, then bodies
-    var wellTyped = Buffer.<Def>create();
-    for (var stmt : scc) {
-      if (stmt instanceof Decl decl) wellTyped.append(decl.tyck(reporter, builder));
-      else if (stmt instanceof Sample sample) wellTyped.append(sample.tyck(reporter, builder));
-      else if (stmt instanceof Remark remark) {
-        var literate = remark.literate;
-        if (literate != null) literate.tyck(new ExprTycker(reporter, builder));
-      }
-      if (reporter.problems().anyMatch(Problem::isError)) throw new GroupTyckingFailed();
-    }
-    return wellTyped.toImmutableSeq();
-  }
-
   /**
    * Copied and adapted.
    *
@@ -150,7 +130,4 @@ public static void handleInternalError(@NotNull InternalException e) {
       Please report the stacktrace to the developers so a better error handling could be made.
       Don't forget to inform the version of Aya you're using and attach your code for reproduction.""");
   }
-
-  private static class GroupTyckingFailed extends RuntimeException {
-  }
 }

base/src/main/java/org/aya/concrete/stmt/Decl.java

@@ -53,8 +53,8 @@ protected Decl(
 
   protected abstract <P, R> R doAccept(@NotNull Visitor<P, R> visitor, P p);
 
-  public @NotNull Def tyck(@NotNull Reporter reporter, Trace.@Nullable Builder builder) {
-    return new StmtTycker(reporter, builder).tyck(this);
+  public @NotNull Def tyck(@NotNull Reporter reporter, Trace.@Nullable Builder builder, boolean headerOnly) {
+    return new StmtTycker(reporter, builder, headerOnly).tyck(this);
   }
 
   @Override public final <P, R> R accept(Stmt.@NotNull Visitor<P, R> visitor, P p) {

base/src/main/java/org/aya/concrete/stmt/Sample.java

@@ -18,7 +18,7 @@ public sealed interface Sample extends Stmt {
   @NotNull Stmt delegate();
 
   /** @return <code>null</code> if the delegate is a command (not a definition) */
-  @Nullable Def tyck(@NotNull Reporter reporter, Trace.@Nullable Builder traceBuilder);
+  @Nullable Def tyck(@NotNull Reporter reporter, Trace.@Nullable Builder traceBuilder, boolean headerOnly);
 
   @Override default @NotNull SourcePos sourcePos() {
     return delegate().sourcePos();
@@ -35,10 +35,11 @@ record Working(@NotNull Stmt delegate) implements Sample {
 
     @Override public @Nullable Def tyck(
       @NotNull Reporter reporter,
-      Trace.@Nullable Builder traceBuilder
+      Trace.@Nullable Builder traceBuilder,
+      boolean headerOnly
     ) {
       return delegate instanceof Decl decl ?
-        new StmtTycker(reporter, traceBuilder).tyck(decl) : null;
+        new StmtTycker(reporter, traceBuilder, headerOnly).tyck(decl) : null;
     }
   }
 
@@ -53,9 +54,10 @@ public Counter(@NotNull Decl delegate) {
 
     @Override public @Nullable Def tyck(
       @NotNull Reporter reporter,
-      Trace.@Nullable Builder traceBuilder
+      Trace.@Nullable Builder traceBuilder,
+      boolean headerOnly
     ) {
-      var stmtTycker = new StmtTycker(reporter, traceBuilder);
+      var stmtTycker = new StmtTycker(reporter, traceBuilder, headerOnly);
       var def = stmtTycker.tyck(delegate, new ExprTycker(this.reporter, stmtTycker.traceBuilder()));
       var problems = this.reporter.problems().toImmutableSeq();
       if (problems.isEmpty()) {

base/src/main/java/org/aya/tyck/StmtTycker.java

@@ -43,7 +43,8 @@
  */
 public record StmtTycker(
   @NotNull Reporter reporter,
-  Trace.@Nullable Builder traceBuilder
+  Trace.@Nullable Builder traceBuilder,
+  boolean headerOnly
 ) {
   public @NotNull ExprTycker newTycker() {
     return new ExprTycker(reporter, traceBuilder);

base/src/main/java/org/aya/tyck/error/CircularSignatureError.java

@@ -0,0 +1,46 @@
+// Copyright (c) 2020-2021 Yinsen (Tesla) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.tyck.error;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.api.distill.DistillerOptions;
+import org.aya.api.error.Problem;
+import org.aya.api.error.SourcePos;
+import org.aya.concrete.remark.Remark;
+import org.aya.concrete.stmt.Decl;
+import org.aya.concrete.stmt.Sample;
+import org.aya.concrete.stmt.Stmt;
+import org.aya.pretty.doc.Doc;
+import org.jetbrains.annotations.NotNull;
+
+import java.util.Comparator;
+
+public record CircularSignatureError(
+  @NotNull ImmutableSeq<Stmt> cycles
+) implements Problem {
+  @Override public @NotNull SourcePos sourcePos() {
+    return cycles.view().map(Stmt::sourcePos)
+      .max(Comparator.comparingInt(SourcePos::endLine));
+  }
+
+  @Override public @NotNull Doc describe(@NotNull DistillerOptions options) {
+    return Doc.sep(
+      Doc.english("Circular signature dependency found between"),
+      Doc.commaList(cycles.view().map(this::nameOf).toImmutableSeq()
+        .sorted().view().map(Doc::plain))
+    );
+  }
+
+  private @NotNull String nameOf(@NotNull Stmt stmt) {
+    return switch (stmt) {
+      case Decl decl -> decl.ref().name();
+      case Sample sample -> nameOf(sample.delegate());
+      case Remark remark -> remark.raw;
+      default -> throw new IllegalStateException("Unexpected stmt seen in SCCTycker: " + stmt);
+    };
+  }
+
+  @Override public @NotNull Severity level() {
+    return Severity.ERROR;
+  }
+}