error: add error classes

Co-authored-by: HoshinoTented <hoshinotented@qq.com>

base/src/main/java/org/aya/normalize/Normalizer.java

@@ -0,0 +1,14 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.normalize;
+
+import org.aya.syntax.core.term.Term;
+import org.aya.tyck.TyckState;
+import org.jetbrains.annotations.NotNull;
+
+public record Normalizer(@NotNull TyckState state) {
+  public @NotNull Term whnf(@NotNull Term term) {
+    // TODO
+    return term;
+  }
+}

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

@@ -0,0 +1,26 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) 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 org.aya.generic.AyaDocile;
+import org.aya.pretty.doc.Doc;
+import org.aya.syntax.core.term.Term;
+import org.aya.util.error.SourcePos;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+
+public record BadExprError(
+  @Override @NotNull AyaDocile expr,
+  @NotNull SourcePos sourcePos,
+  @NotNull Term expectedTy
+) implements TyckError {
+  @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+    return Doc.vcat(
+      Doc.english("The expected type is"),
+      Doc.par(1, expectedTy.toDoc(options)),
+      Doc.english("but the given expression"),
+      Doc.par(1, expr.toDoc(options)),
+      Doc.english("does not try to construct something into this type")
+    );
+  }
+}

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

@@ -0,0 +1,98 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) 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.mutable.MutableList;
+import org.aya.generic.AyaDocile;
+import org.aya.pretty.doc.Doc;
+import org.aya.syntax.concrete.Expr;
+import org.aya.syntax.core.term.Term;
+import org.aya.tyck.TyckState;
+import org.aya.util.error.SourcePos;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+
+public record BadTypeError(
+  @Override @NotNull Expr expr,
+  @Override @NotNull SourcePos sourcePos,
+  @NotNull Term actualType, @NotNull Doc action,
+  @NotNull Doc thing, @NotNull AyaDocile desired,
+  @NotNull TyckState state
+) implements TyckError {
+  @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+    var list = MutableList.of(
+      Doc.sep(Doc.english("Unable to"), action, Doc.english("the expression")),
+      Doc.par(1, expr.toDoc(options)),
+      Doc.sep(Doc.english("because the type"), thing, Doc.english("is not a"), Doc.cat(desired.toDoc(options), Doc.plain(",")), Doc.english("but instead:")));
+    UnifyInfo.exprInfo(actualType, options, state, list);
+    return Doc.vcat(list);
+  }
+
+  @Override public @NotNull Doc hint(@NotNull PrettierOptions options) {
+    // TODO: memberDef
+/*
+    if (expr instanceof Expr.App app && app.function() instanceof Expr.Ref ref
+      && ref.resolvedVar() instanceof DefVar<?, ?> defVar && defVar.core instanceof MemberDef) {
+      var fix = new Expr.Proj(SourcePos.NONE, app.argument().term(),
+        Either.right(new QualifiedID(SourcePos.NONE, defVar.name())));
+      return Doc.sep(Doc.english("Did you mean"),
+        Doc.code(fix.toDoc(options)),
+        Doc.english("?"));
+    }
+*/
+    return Doc.empty();
+  }
+
+  public static @NotNull BadTypeError pi(@NotNull TyckState state, @NotNull SourcePos pos, @NotNull Expr expr, @NotNull Term actualType) {
+    return new BadTypeError(expr, pos, actualType, Doc.plain("apply"),
+      Doc.english("of what you applied"), options -> Doc.english("Pi type"), state);
+  }
+
+  public static @NotNull BadTypeError sigmaAcc(@NotNull TyckState state, @NotNull SourcePos pos, @NotNull Expr expr, int ix, @NotNull Term actualType) {
+    return new BadTypeError(expr, pos, actualType,
+      Doc.sep(Doc.english("project the"), Doc.ordinal(ix), Doc.english("element of")),
+      Doc.english("of what you projected on"),
+      options -> Doc.english("Sigma type"),
+      state);
+  }
+
+  public static @NotNull BadTypeError sigmaCon(@NotNull TyckState state, @NotNull SourcePos pos, @NotNull Expr expr, @NotNull Term actualType) {
+    return new BadTypeError(expr, pos, actualType,
+      Doc.sep(Doc.plain("construct")),
+      Doc.english("you checked it against"),
+      options -> Doc.english("Sigma type"),
+      state);
+  }
+
+  public static @NotNull BadTypeError structAcc(@NotNull TyckState state, @NotNull SourcePos pos, @NotNull Expr expr, @NotNull String fieldName, @NotNull Term actualType) {
+    return new BadTypeError(expr, pos, actualType,
+      Doc.sep(Doc.english("access field"), Doc.code(fieldName), Doc.plain("of")),
+      Doc.english("of what you accessed"),
+      options -> Doc.english("struct type"),
+      state);
+  }
+
+  public static @NotNull BadTypeError structCon(@NotNull TyckState state, @NotNull SourcePos pos, @NotNull Expr expr, @NotNull Term actualType) {
+    return new BadTypeError(expr, pos, actualType,
+      Doc.sep(Doc.plain("construct")),
+      Doc.english("you gave"),
+      options -> Doc.english("struct type"),
+      state);
+  }
+
+  public static @NotNull BadTypeError univ(@NotNull TyckState state, @NotNull SourcePos pos, @NotNull Expr expr, @NotNull Term actual) {
+    return new BadTypeError(expr, pos, actual,
+      Doc.english("make sense of"),
+      Doc.english("provided"),
+      options -> Doc.english("universe"),
+      state);
+  }
+
+  public static @NotNull BadTypeError partTy(@NotNull TyckState state, @NotNull SourcePos pos, @NotNull Expr expr, @NotNull Term actualType) {
+    return new BadTypeError(expr, pos, actualType,
+      Doc.plain("fill the shape composed by"),
+      Doc.english("of the partial element"),
+      options -> Doc.english("Partial type"),
+      state);
+  }
+}

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

@@ -0,0 +1,19 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) 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 org.aya.pretty.doc.Doc;
+import org.aya.ref.AnyVar;
+import org.aya.util.error.SourcePos;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+
+public record CounterexampleError(@Override @NotNull SourcePos sourcePos, @NotNull AnyVar var) implements TyckError {
+  @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+    return Doc.sep(
+      Doc.english("The counterexample"),
+      // TODO
+      // BasePrettier.varDoc(var),
+      Doc.english("does not raise any type error"));
+  }
+}

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

@@ -0,0 +1,70 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) 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 org.aya.pretty.doc.Doc;
+import org.aya.syntax.concrete.Expr;
+import org.aya.util.error.SourcePos;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+
+public sealed interface CubicalError extends TyckError {
+  record BoundaryDisagree(
+    @Override @NotNull Expr expr,
+    @Override @NotNull SourcePos sourcePos,
+    @NotNull UnifyInfo.Comparison comparison,
+    @NotNull UnifyInfo info
+  ) implements CubicalError {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return info.describeUnify(options, comparison, Doc.english("The boundary"),
+        Doc.english("disagrees with"));
+    }
+  }
+
+/*
+  record FaceMismatch(
+    @NotNull Expr expr,
+    @Override @NotNull SourcePos sourcePos,
+    @NotNull Restr<Term> face,
+    @NotNull Restr<Term> cof
+  ) implements CubicalError {
+    @Override
+    public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.vcat(Doc.english("The face(s) in the partial element:"),
+        Doc.par(1, BasePrettier.restr(options, face)),
+        Doc.english("must cover the face(s) specified in type:"),
+        Doc.par(1, BasePrettier.restr(options, cof)));
+    }
+  }
+
+  record CoeVaryingType(
+    @NotNull Expr expr,
+    @NotNull Term type,
+    @Nullable Term typeInst,
+    @NotNull Restr<Term> restr,
+    boolean stuck
+  ) implements CubicalError {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      var typeDoc = type.toDoc(options);
+      var under = typeInst != null ? typeInst.toDoc(options) : null;
+      var buf = MutableList.of(
+        Doc.english("Under the cofibration:"),
+        Doc.par(1, BasePrettier.restr(options, restr)));
+      if (stuck)
+        buf.append(Doc.english("I am not sure if the type is constant, as my normalization is blocked for type:"));
+      else buf.append(Doc.english("The type in the body still depends on the interval parameter:"));
+      buf.append(Doc.par(1, typeDoc));
+      if (under != null && !typeDoc.equals(under)) buf.append(
+        Doc.par(1, Doc.parened(Doc.sep(Doc.plain("Normalized under cofibration:"), under))));
+      buf.append(Doc.english("which is not allowed in coercion"));
+      return Doc.vcat(buf);
+    }
+  }
+*/
+
+  record PathConDominateError(@NotNull SourcePos sourcePos) implements TyckError {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.english("The path constructor must not be a constant path");
+    }
+  }
+}

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

@@ -0,0 +1,43 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) 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;
+
+/*public record Goal(@NotNull TyckState state, @NotNull MetaTerm hole, @NotNull ImmutableSeq<LocalVar> scope) implements Problem {
+  @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+    var meta = hole.ref();
+    var nullableResult = meta.info.result();
+    var result = nullableResult != null ? nullableResult.freezeHoles(state)
+      : new ErrorTerm(Doc.plain("???"), false);
+    var doc = Doc.vcatNonEmpty(
+      Doc.english("Goal of type"),
+      Doc.par(1, result.toDoc(options)),
+      Doc.par(1, Doc.parened(Doc.sep(Doc.plain("Normalized:"), result.normalize(state, NormalizeMode.NF).toDoc(options)))),
+      Doc.plain("Context:"),
+      Doc.vcat(meta.fullTelescope().map(param -> {
+        param = new Term.Param(param, param.type().freezeHoles(state));
+        var paramDoc = param.toDoc(options);
+        return Doc.par(1, scope.contains(param.ref()) ? paramDoc : Doc.sep(paramDoc, Doc.parened(Doc.english("not in scope"))));
+      })),
+      meta.conditions.isNotEmpty() ? Doc.vcat(
+        ImmutableSeq.of(Doc.plain("To ensure confluence:"))
+          .concat(meta.conditions.toImmutableSeq().map(tup -> Doc.par(1, Doc.cat(
+            Doc.plain("Given "),
+            Doc.parened(tup.component1().toDoc(options)),
+            Doc.plain(", we should have: "),
+            tup.component2().freezeHoles(state).toDoc(options)
+          )))))
+        : Doc.empty()
+    );
+    var metas = state.metas();
+    return !metas.containsKey(meta) ? doc :
+      Doc.vcat(Doc.plain("Candidate exists:"), Doc.par(1, metas.get(meta).toDoc(options)), doc);
+  }
+
+  @Override public @NotNull SourcePos sourcePos() {
+    return hole.ref().sourcePos;
+  }
+
+  @Override public @NotNull Severity level() {return Severity.GOAL;}
+
+  @Override public @NotNull Stage stage() {return Stage.TYCK;}
+}*/

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

@@ -0,0 +1,104 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) 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;
+
+/** @author ice1000 */
+/*
+public sealed interface HoleProblem extends Problem {
+  @NotNull MetaTerm term();
+
+  @Override default @NotNull Severity level() {
+    return Severity.ERROR;
+  }
+
+  @Override default @NotNull SourcePos sourcePos() {
+    return term().ref().sourcePos;
+  }
+
+  */
+/** @author ice1000 *//*
+
+  record BadSpineError(
+    @Override @NotNull MetaTerm term
+  ) implements HoleProblem {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.vcat(
+        Doc.english("Can't perform pattern unification on hole with the following spine:"),
+        BasePrettier.argsDoc(options, term.args())
+      );
+    }
+  }
+
+  record IllTypedError(
+    @Override @NotNull MetaTerm term,
+    @NotNull TyckState state,
+    @Override @NotNull Term solution
+  ) implements HoleProblem {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      var list = MutableList.of(Doc.english("The meta (denoted ? below) is supposed to satisfy:"),
+        Doc.par(1, term.ref().info.toDoc(options)),
+        Doc.english("However, the solution below does not seem so:"));
+      UnifyInfo.exprInfo(solution, options, state, list);
+      return Doc.vcat(list);
+    }
+  }
+
+  record BadlyScopedError(
+    @Override @NotNull MetaTerm term,
+    @NotNull Term solved,
+    @NotNull Seq<LocalVar> scopeCheck
+  ) implements HoleProblem {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.vcat(
+        Doc.english("The solution"),
+        Doc.par(1, solved.toDoc(options)),
+        Doc.plain("is not well-scoped"),
+        Doc.cat(Doc.english("In particular, these variables are not in scope:"),
+          Doc.ONE_WS,
+          Doc.commaList(scopeCheck.view()
+            .map(BasePrettier::varDoc)
+            .map(Doc::code))));
+    }
+  }
+
+  */
+/**
+   * @author ice1000
+   *//*
+
+  record RecursionError(
+    @Override @NotNull MetaTerm term,
+    @NotNull Term sol
+  ) implements HoleProblem {
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.vcat(
+        Doc.sep(
+          Doc.english("Trying to solve hole"),
+          Doc.code(BasePrettier.linkDef(term.ref())),
+          Doc.plain("as")),
+        Doc.par(1, sol.toDoc(options)),
+        Doc.english("which is recursive"));
+    }
+  }
+
+  record CannotFindGeneralSolution(
+    @NotNull ImmutableSeq<TyckState.Eqn> eqns
+  ) implements Problem {
+    @Override public @NotNull SourcePos sourcePos() {
+      return eqns.getLast().pos();
+    }
+
+    @Override public @NotNull SeqView<WithPos<Doc>> inlineHints(@NotNull PrettierOptions options) {
+      return eqns.view().map(eqn -> new WithPos<>(eqn.pos(), eqn.toDoc(options)));
+    }
+
+    @Override public @NotNull Doc describe(@NotNull PrettierOptions options) {
+      return Doc.english("Solving equation(s) with not very general solution(s)");
+    }
+
+    @Override public @NotNull Severity level() {
+      return Severity.INFO;
+    }
+  }
+}
+*/