merge: Pretty print/literate mode features (#1094)

base/src/main/java/org/aya/resolve/visitor/ExprResolver.java

@@ -102,9 +102,10 @@ public ExprResolver(@NotNull Context ctx, @NotNull Options options) {
         // if (resolvedIx == null) ctx.reportAndThrow(new FieldError.UnknownField(projName.sourcePos(), projName.join()));
         yield new Expr.Proj(tup, ix, resolvedIx, theCore);
       }
-      case Expr.Hole(var expl, var fill, var local) -> {
+      case Expr.Hole(var expl, var fill, var core, var local) -> {
         assert local.isEmpty();
-        yield new Expr.Hole(expl, fill, ctx.collect(MutableList.create()).toImmutableSeq());
+        yield new Expr.Hole(expl, fill, core,
+          ctx.collect(MutableList.create()).toImmutableSeq());
       }
       default -> expr;
     };

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

@@ -51,6 +51,7 @@
 public final class ExprTycker extends AbstractTycker implements Unifiable {
   public final @NotNull MutableTreeSet<WithPos<Expr.WithTerm>> withTerms =
     MutableTreeSet.create(Comparator.comparing(SourceNode::sourcePos));
+  public final @NotNull MutableList<WithPos<Expr.Hole>> userHoles = MutableList.create();
   private @NotNull LocalLet localLet;
 
   public void addWithTerm(@NotNull Expr.WithTerm with, @NotNull SourcePos pos, @NotNull Term type) {
@@ -73,6 +74,7 @@ public ExprTycker(@NotNull TyckState state, @NotNull Reporter reporter) {
   public void solveMetas() {
     state.solveMetas(reporter);
     withTerms.forEach(with -> with.data().theCoreType().update(this::freezeHoles));
+    userHoles.forEach(hole -> hole.data().solution().update(this::freezeHoles));
   }
 
   /**
@@ -102,6 +104,8 @@ case PiTerm(var dom, var cod) -> {
       };
       case Expr.Hole hole -> {
         var freshHole = freshMeta(Constants.randomName(hole), expr.sourcePos(), new MetaVar.OfType(type));
+        hole.solution().set(freshHole);
+        userHoles.append(new WithPos<>(expr.sourcePos(), hole));
         if (hole.explicit()) fail(new Goal(state, freshHole, hole.accessibleLocal()));
         yield new Jdg.Default(freshHole, type);
       }
@@ -149,6 +153,8 @@ case PiTerm(var dom, var cod) -> {
           : new Closure.Jit(i -> new AppTerm(result.wellTyped(), i));
         checkBoundaries(eq, closure, expr.sourcePos(), msg ->
           new CubicalError.BoundaryDisagree(expr, msg, new UnifyInfo(state)));
+        if (expr.data() instanceof Expr.WithTerm with)
+          addWithTerm(with, expr.sourcePos(), eq);
         return new Jdg.Default(new LamTerm(closure), eq);
       }
     }

base/src/main/java/org/aya/tyck/tycker/TeleTycker.java

@@ -18,6 +18,7 @@
 import org.aya.tyck.Jdg;
 import org.aya.tyck.error.UnifyError;
 import org.aya.unify.Synthesizer;
+import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
@@ -29,6 +30,7 @@ public sealed interface TeleTycker extends Contextful {
    * @return well-typed type or {@link ErrorTerm}
    */
   @NotNull Term checkType(@NotNull WithPos<Expr> typeExpr, boolean isResult);
+  void addWithTerm(@NotNull Expr.WithTerm with, @NotNull SourcePos pos, @NotNull Term type);
 
   /**
    * @return a locally nameless signature computed from what's in the localCtx.
@@ -63,6 +65,7 @@ public sealed interface TeleTycker extends Contextful {
   default @NotNull MutableSeq<Param> checkTeleFree(ImmutableSeq<Expr.Param> cTele) {
     return MutableSeq.from(cTele.view().map(p -> {
       var pTy = checkType(p.typeExpr(), false);
+      addWithTerm(p, p.sourcePos(), pTy);
       localCtx().put(p.ref(), pTy);
       return new Param(p.ref().name(), pTy, p.explicit());
     }));
@@ -112,6 +115,9 @@ record Default(@Override @NotNull ExprTycker tycker) implements Impl {
     @Override public @NotNull Term checkType(@NotNull WithPos<Expr> typeExpr, boolean isResult) {
       return tycker.ty(typeExpr);
     }
+    @Override public void addWithTerm(Expr.@NotNull WithTerm with, @NotNull SourcePos pos, @NotNull Term type) {
+      tycker.addWithTerm(with, pos, type);
+    }
   }
 
   final class InlineCode implements Impl {
@@ -129,6 +135,9 @@ final class InlineCode implements Impl {
       result = jdg;
       return jdg.wellTyped();
     }
+    @Override public void addWithTerm(Expr.@NotNull WithTerm with, @NotNull SourcePos pos, @NotNull Term type) {
+      tycker.addWithTerm(with, pos, type);
+    }
     @Override public @NotNull ExprTycker tycker() { return tycker; }
   }
 
@@ -140,5 +149,8 @@ record Con(@NotNull ExprTycker tycker, @NotNull SortTerm dataResult) implements
       }
       return result;
     }
+    @Override public void addWithTerm(Expr.@NotNull WithTerm with, @NotNull SourcePos pos, @NotNull Term type) {
+      tycker.addWithTerm(with, pos, type);
+    }
   }
 }

cli-impl/src/main/java/org/aya/cli/literate/FaithfulPrettier.java

@@ -74,19 +74,21 @@ static void checkHighlights(@NotNull ImmutableSeq<HighlightInfo> highlights) {
       case HighlightInfo.Def def -> Doc.linkDef(highlightVar(raw, def.kind()), def.target(), hover(def.type()));
       case HighlightInfo.Ref ref -> Doc.linkRef(highlightVar(raw, ref.kind()), ref.target(), hover(ref.type()));
       case HighlightInfo.Lit lit -> highlightLit(raw, lit.kind());
-      case HighlightInfo.Err err -> {
-        var doc = doHighlight(StringSlice.of(raw), base, err.children());
-        var style = switch (err.problem().level()) {
+      case HighlightInfo.Err(var problem, var children) -> {
+        var doc = doHighlight(StringSlice.of(raw), base, children);
+        var style = switch (problem.level()) {
           case ERROR -> BasePrettier.ERROR;
           case WARN -> BasePrettier.WARNING;
           case GOAL -> BasePrettier.GOAL;
           case INFO -> null;
         };
         yield style == null ? doc : new Doc.Tooltip(Doc.styled(style, doc), () -> Doc.codeBlock(
           Language.Builtin.Aya,
-          err.problem().brief(options()).toDoc()
+          problem.brief(options()).toDoc()
         ));
       }
+      case HighlightInfo.UserMeta meta -> new Doc.Tooltip(Doc.plain(raw),
+        () -> Doc.codeBlock(Language.Builtin.Aya, meta.hover().toDoc(options())));
     };
   }
 

cli-impl/src/main/java/org/aya/cli/literate/HighlightInfo.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// 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.cli.literate;
 
@@ -88,4 +88,7 @@ record Err(
 
   /** A literal */
   record Lit(@NotNull SourcePos sourcePos, @NotNull LitKind kind) implements HighlightInfo { }
+
+  /** Usually metavariables */
+  record UserMeta(@NotNull SourcePos sourcePos, @NotNull AyaDocile hover) implements HighlightInfo { }
 }

cli-impl/src/main/java/org/aya/cli/literate/SyntaxHighlight.java

@@ -22,7 +22,10 @@
 import org.aya.syntax.concrete.stmt.ModuleName;
 import org.aya.syntax.concrete.stmt.Stmt;
 import org.aya.syntax.concrete.stmt.StmtVisitor;
-import org.aya.syntax.concrete.stmt.decl.*;
+import org.aya.syntax.concrete.stmt.decl.DataCon;
+import org.aya.syntax.concrete.stmt.decl.DataDecl;
+import org.aya.syntax.concrete.stmt.decl.FnDecl;
+import org.aya.syntax.concrete.stmt.decl.PrimDecl;
 import org.aya.syntax.core.def.ConDef;
 import org.aya.syntax.core.def.DataDef;
 import org.aya.syntax.core.def.FnDef;
@@ -80,14 +83,18 @@ else if (SPECIAL_SYMBOL.contains(tokenType))
     return prettier.info.toImmutableSeq();
   }
 
-  @Override
-  public void visitVarRef(@NotNull SourcePos pos, @NotNull AnyVar var, @NotNull LazyValue<@Nullable Term> type) {
+  @Override public void
+  visitVarRef(@NotNull SourcePos pos, @NotNull AnyVar var, @NotNull LazyValue<@Nullable Term> type) {
     info.append(linkRef(pos, var, type.get()));
   }
   @Override public void visitExpr(@NotNull SourcePos pos, @NotNull Expr expr) {
     switch (expr) {
       case Expr.LitInt _ -> info.append(LitKind.Int.toLit(pos));
       case Expr.LitString _ -> info.append(LitKind.String.toLit(pos));
+      case Expr.Hole hole when hole.filling() == null -> {
+        var hover = hole.solution().get();
+        if (hover != null) info.append(new HighlightInfo.UserMeta(pos, hover));
+      }
       default -> StmtVisitor.super.visitExpr(pos, expr);
     }
   }

cli-impl/src/test/resources/shared/src/type-theory/qiit.aya

@@ -40,7 +40,6 @@ open inductive infix << (Γ : Con) (Δ : Con) : Type
   : (σ ∷ t) ∘ δ = (σ ∘ δ) ∷ transport (Tm _) SubAss (sub t)
 | _, • => εη {δ : Γ << •} : δ = ε
 
-// Incomplete
 open inductive Tm (Γ : Con) (Ty Γ) : Type
 | _, Π A B => λ (Tm (Γ ▷ A) B)
 | Γ' ▷ A, B => app (Tm Γ' (Π A B))

ide-lsp/src/main/java/org/aya/lsp/models/HighlightResult.java

@@ -64,8 +64,9 @@ public record Symbol(
           case Prim -> Option.some(Kind.PrimRef);
           case Unknown -> Option.none();
         };
-        case HighlightInfo.Lit _ -> Option.none();   // handled by client
+        case HighlightInfo.Lit _ -> Option.none(); // handled by client
         case HighlightInfo.Err _ -> Option.none(); // handled by client
+        case HighlightInfo.UserMeta _ -> Option.none(); // handled by something else
       };
     }
   }

syntax/src/main/java/org/aya/syntax/concrete/Expr.java

@@ -78,14 +78,15 @@ public Param(@NotNull SourcePos sourcePos, @NotNull LocalVar ref, @NotNull WithP
   record Hole(
     boolean explicit,
     @Nullable WithPos<Expr> filling,
-    ImmutableSeq<LocalVar> accessibleLocal
+    @NotNull MutableValue<Term> solution,
+    @NotNull ImmutableSeq<LocalVar> accessibleLocal
   ) implements Expr {
     public Hole(boolean explicit, @Nullable WithPos<Expr> filling) {
-      this(explicit, filling, ImmutableSeq.empty());
+      this(explicit, filling, MutableValue.create(), ImmutableSeq.empty());
     }
 
     public @NotNull Hole update(@Nullable WithPos<Expr> filling) {
-      return filling == filling() ? this : new Hole(explicit, filling, accessibleLocal);
+      return filling == filling() ? this : new Hole(explicit, filling, solution, accessibleLocal);
     }
 
     @Override public @NotNull Hole descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {

syntax/src/main/java/org/aya/syntax/concrete/stmt/StmtVisitor.java

@@ -100,9 +100,8 @@ default void accept(@NotNull Stmt stmt) {
             fn.body.forEach(this::visitExpr, cl -> cl.forEach(this::visitExpr,
               this::visitPattern));
             if (fn.body instanceof FnBody.BlockBody block) {
-              if (block.elims() != null) {
-                block.elims().forEachWith(block.rawElims(), (var, name) -> visitVar(name.sourcePos(), var, noType));
-              }
+              if (block.elims() != null) block.elims().forEachWith(block.rawElims(), (var, name) ->
+                visitVarRef(name.sourcePos(), var, noType));
             }
           }
           case DataCon con -> con.patterns.forEach(cl -> visitPattern(cl.term()));

syntax/src/main/java/org/aya/syntax/core/def/TyckDef.java

@@ -6,12 +6,15 @@
 import org.aya.generic.AyaDocile;
 import org.aya.prettier.CorePrettier;
 import org.aya.pretty.doc.Doc;
-import org.aya.syntax.compile.JitDef;
 import org.aya.syntax.concrete.stmt.decl.Decl;
+import org.aya.syntax.core.Closure;
+import org.aya.syntax.core.term.FreeTerm;
 import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.Term;
+import org.aya.syntax.core.term.xtt.EqTerm;
 import org.aya.syntax.ref.DefVar;
 import org.aya.syntax.telescope.AbstractTele;
+import org.aya.util.ForLSP;
 import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -27,17 +30,18 @@ public sealed interface TyckDef extends AyaDocile permits SubLevelDef, TopLevelD
     return new CorePrettier(options).def(this);
   }
 
-  //region Pretty & IDE only APIs
-  static @Nullable Term defType(@NotNull AnyDef var) {
-    return switch (var) {
-      case TyckAnyDef<?> tyckDef -> {
-        var sig = tyckDef.ref.signature;
-        yield sig == null ? null : sig.result();
-      }
-      case JitDef jitDef -> jitDef.makePi();
-    };
+  @ForLSP static @Nullable Term defType(@NotNull AnyDef var) {
+    if (var instanceof TyckAnyDef<?> def && def.ref.signature == null) return null;
+    var sig = var.signature();
+    var names = sig.namesView().<Term>map(FreeTerm::new).toSeq();
+    var result = sig.result(names);
+    if (var instanceof ConDefLike con && con.hasEq()) result = new EqTerm(
+      Closure.mkConst(result),
+      con.equality(names, true),
+      con.equality(names, false)
+    );
+    return result;
   }
-  //endregion
 
   /**
    * @see AnyDef#signature()

syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java

@@ -2,9 +2,12 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.telescope;
 
+import kala.collection.ArraySeq;
 import kala.collection.Seq;
-import kala.collection.immutable.ImmutableArray;
+import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
+import kala.collection.immutable.primitive.ImmutableIntSeq;
+import kala.range.primitive.IntRange;
 import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.term.ErrorTerm;
 import org.aya.syntax.core.term.Param;
@@ -17,7 +20,7 @@ public interface AbstractTele {
    * @param teleArgs the arguments before {@param i}, for constructor, it also contains the arguments to the data
    */
   default @NotNull Term telescope(int i, Term[] teleArgs) {
-    return telescope(i, ImmutableArray.Unsafe.wrap(teleArgs));
+    return telescope(i, ArraySeq.wrap(teleArgs));
   }
 
   @NotNull Term telescope(int i, Seq<Term> teleArgs);
@@ -30,7 +33,12 @@ public interface AbstractTele {
   }
 
   default @NotNull Term result(Term... teleArgs) {
-    return result(ImmutableArray.Unsafe.wrap(teleArgs));
+    return result(ArraySeq.wrap(teleArgs));
+  }
+
+  default @NotNull SeqView<String> namesView() {
+    return ImmutableIntSeq.from(IntRange.closedOpen(0, telescopeSize()))
+      .view().mapToObj(this::telescopeName);
   }
 
   default @NotNull Term makePi() {
@@ -58,6 +66,7 @@ record Lift(
       return signature.result(teleArgs).elevate(lift);
     }
     @Override public @NotNull AbstractTele lift(int i) { return new Lift(signature, lift + i); }
+    @Override public @NotNull SeqView<String> namesView() { return signature.namesView(); }
   }
   record Locns(
     @NotNull ImmutableSeq<Param> telescope,
@@ -73,6 +82,9 @@ record Locns(
       assert teleArgs.size() == telescopeSize();
       return result.instantiateTele(teleArgs.view());
     }
+    @Override public @NotNull SeqView<String> namesView() {
+      return telescope.view().map(Param::name);
+    }
   }
   default @NotNull AbstractTele prefix(int i) {
     return i == telescopeSize() ? this : new Slice(this, i);
@@ -92,5 +104,8 @@ record Slice(
     @Override public @NotNull AbstractTele prefix(int i) {
       return new Slice(signature, i);
     }
+    @Override public @NotNull SeqView<String> namesView() {
+      return signature.namesView().sliceView(0, telescopeSize);
+    }
   }
 }

syntax/src/main/java/org/aya/syntax/telescope/JitTele.java

@@ -2,6 +2,8 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.syntax.telescope;
 
+import kala.collection.ArraySeq;
+import kala.collection.SeqView;
 import org.jetbrains.annotations.NotNull;
 
 /**
@@ -21,4 +23,7 @@ protected JitTele(int telescopeSize, boolean[] telescopeLicit, String[] telescop
   @Override public int telescopeSize() { return telescopeSize; }
   @Override public boolean telescopeLicit(int i) { return telescopeLicit[i]; }
   @Override public @NotNull String telescopeName(int i) { return telescopeNames[i]; }
+  @Override public @NotNull SeqView<String> namesView() {
+    return ArraySeq.wrap(telescopeNames).view();
+  }
 }