merge: branch 'main' into fix-1035

aya-prover · Nov 30, 2024 · 92ca0f0 · 92ca0f0
2 parents 691e4f3 + ca44703
commit 92ca0f0
Show file tree

Hide file tree

Showing 8 changed files with 111 additions and 84 deletions.
diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java
@@ -224,7 +224,7 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
       ownerBinds = lhsResult.allBinds();
       TeleTycker.bindTele(ownerBinds, allTypedBinds);
       ownerTelePos = ownerBinds.map(LocalVar::definition);
-      ownerTele = allTypedBinds.toImmutableSeq();
+      ownerTele = allTypedBinds.map(Param::implicitize);
       if (wellPats.allMatch(pat -> pat instanceof Pat.Bind))
         wellPats = ImmutableSeq.empty();
     } else {

diff --git a/base/src/test/java/org/aya/syntax/core/PrettierTest.java b/base/src/test/java/org/aya/syntax/core/PrettierTest.java
@@ -0,0 +1,32 @@
+// 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.syntax.core;
+
+import org.aya.tyck.TyckTest;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+public class PrettierTest {
+  @Test public void clauses() {
+    var result = TyckTest.tyck("""
+      open inductive Nat | O | S Nat
+      
+      def plus (a : Nat) (b : Nat) : Nat
+      | 0  , c   => b
+      | S c, 0   => S (plus c b)
+      | S c, S d => S (plus c b)
+      """);
+
+    var fnPlus = result.defs()
+      .findFirst(x -> x.ref().name().equals("plus"))
+      .get();
+
+    assertEquals("""
+        def plus (a b : Nat) : Nat
+          | 0, c => c
+          | S c, 0 => S (plus c 0)
+          | S c, S d => S (plus c (S d))""",      // no new line here!!
+      fnPlus.debuggerOnlyToString());
+  }
+}
diff --git a/jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/PatternSerializer.java
@@ -6,7 +6,6 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.primitive.ImmutableIntSeq;
 import kala.range.primitive.IntRange;
-import org.aya.generic.AyaDocile;
 import org.aya.generic.State;
 import org.aya.syntax.core.pat.Pat;
 import org.aya.util.error.Panic;
@@ -68,8 +67,6 @@ public PatternSerializer(
   /// region Serializing
 
   private void doSerialize(@NotNull Pat pat, @NotNull String term, @NotNull Once continuation) {
-    buildComment(pat.debuggerOnlyToString());
-
     switch (pat) {
       case Pat.Absurd _ -> buildIfElse("Panic.unreachable()", State.Stuck, continuation);
       case Pat.Bind _ -> {
@@ -151,7 +148,6 @@ private void doSerialize(@NotNull SeqView<Pat> pats, @NotNull SeqView<String> te
       return;
     }
 
-    buildComment(pats.map(AyaDocile::debuggerOnlyToString).joinToString());
     var pat = pats.getFirst();
     var term = terms.getFirst();
     doSerialize(pat, term, Once.of(() -> doSerialize(pats.drop(1), terms.drop(1), continuation)));

diff --git a/syntax/src/main/java/org/aya/prettier/CorePrettier.java b/syntax/src/main/java/org/aya/prettier/CorePrettier.java
@@ -9,14 +9,15 @@
 import kala.collection.mutable.MutableList;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.Renamer;
+import org.aya.generic.term.DTKind;
 import org.aya.generic.term.ParamLike;
 import org.aya.pretty.doc.Doc;
 import org.aya.syntax.concrete.stmt.decl.DataCon;
+import org.aya.syntax.core.RichParam;
 import org.aya.syntax.core.def.*;
 import org.aya.syntax.core.pat.Pat;
 import org.aya.syntax.core.pat.PatToTerm;
 import org.aya.syntax.core.term.*;
-import org.aya.generic.term.DTKind;
 import org.aya.syntax.core.term.call.*;
 import org.aya.syntax.core.term.repr.IntegerTerm;
 import org.aya.syntax.core.term.repr.ListTerm;
@@ -126,10 +127,6 @@ yield visitCalls(null, fn, (_, t) -> t.toDoc(options), outer,
         );
       }
       case DimTyTerm _ -> KW_INTERVAL;
-      // case NewTerm(var inner) -> visitCalls(null, Doc.styled(KEYWORD, "new"), (nest, t) -> t.toDoc(options), outer,
-      //   SeqView.of(new Arg<>(o -> term(Outer.AppSpine, inner), true)),
-      //   options.map.get(AyaPrettierOptions.Key.ShowImplicitArgs)
-      // );
       case MemberCall term -> visitCoreApp(null, visitAccessHead(term),
         term.args().view(), outer,
         optionImplicit());
@@ -154,7 +151,6 @@ case ErrorTerm(var desc, var isReallyError) -> {
         yield visitCoreApp(null, term(Outer.AppHead, head), args.view(), outer, implicits);
       }
       case PrimCall prim -> visitCoreCalls(prim.ref(), prim.args(), outer, optionImplicit());
-      // case RefTerm.Field term -> linkRef(term.ref(), MEMBER);
       case ProjTerm(var of, var ix) -> Doc.cat(term(Outer.ProjHead, of), PROJ, Doc.plain(String.valueOf(ix)));
       // case MatchTerm match -> Doc.cblock(Doc.sep(Doc.styled(KEYWORD, "match"),
       //     Doc.commaList(match.discriminant().map(t -> term(Outer.Free, t)))), 2,
@@ -208,7 +204,7 @@ case EqTerm(var _, var a, var b) -> {
   }
 
   private @NotNull Doc visitDT(@NotNull Outer outer, DepTypeTerm.Unpi pair, Doc kw, Doc operator) {
-    var params = pair.names().zip(pair.params(), CoreParam::new);
+    var params = pair.names().zip(pair.params(), RichParam::ofExplicit);
     var body = pair.body().instantiateTeleVar(params.view().map(ParamLike::ref));
     var teleDoc = visitTele(params, body, FindUsage::free);
     var cod = term(Outer.Codomain, body);
@@ -275,7 +271,8 @@ private ImmutableSeq<Term> visibleArgsOf(Callable call) {
         var line1sep = Doc.sepNonEmpty(line1);
         yield def.body().fold(
           term -> Doc.sep(line1sep, FN_DEFINED_AS, term(Outer.Free, term.instantiateTele(subst))),
-          clauses -> Doc.vcat(line1sep, Doc.nest(2, visitClauses(clauses, subst))));
+          clauses -> Doc.vcat(line1sep,
+            Doc.nest(2, visitClauses(clauses, tele.view().map(ParamLike::explicit)))));
       }
       case MemberDef field -> Doc.sepNonEmpty(Doc.symbol("|"),
         defVar(field.ref()),
@@ -335,56 +332,41 @@ private ImmutableSeq<Term> visibleArgsOf(Callable call) {
     }
   }
 
+  public @NotNull Doc visitClauseLhs(@NotNull SeqView<Boolean> licits, @NotNull Term.Matching clause) {
+    var enrichPats = clause.patterns().zip(licits,
+      (pat, licit) -> pat(pat, licit, Outer.Free));
+    return Doc.commaList(enrichPats);
+  }
+
+  private @NotNull Doc visitClause(@NotNull Term.Matching clause, @NotNull SeqView<Boolean> licits) {
+    var patSubst = Pat.collectRichBindings(clause.patterns().view());
+    var lhsWithoutBar = visitClauseLhs(licits, clause);
+    var rhs = term(Outer.Free, clause.body().instantiateTele(patSubst.view().map(RichParam::toTerm)));
+
+    return Doc.sep(BAR, lhsWithoutBar, FN_DEFINED_AS, rhs);
+  }
+
   private @NotNull Doc visitClauses(
     @NotNull ImmutableSeq<Term.Matching> clauses,
-    @NotNull SeqView<Term> teleSubst
+    @NotNull SeqView<Boolean> licits
   ) {
-    // TODO: subset clause body with [teleSubst]
-    return Doc.vcat(clauses.view().map(matching ->
-      // TODO: toDoc use a new CorePrettier => new NameGenerator
-      Doc.sep(BAR, matching.toDoc(options))));
+    return Doc.vcat(clauses.view().map(matching -> visitClause(matching, licits)));
   }
 
   public @NotNull Doc visitParam(@NotNull Param param, @NotNull Outer outer) {
     return justType(
-      new CoreParam(new LocalVar(param.name(), SourcePos.SER, GenerateKind.Basic.Tyck), param.type()),
+      new RichParam(new LocalVar(param.name(), SourcePos.SER, GenerateKind.Basic.Tyck), param.type(), param.explicit()),
       outer);
   }
 
   /// region Name Generating
-  private record CoreParam(
-    @Override @NotNull LocalVar ref,
-    @Override @NotNull Term type
-  ) implements ParamLike<Term> {
-    @Override public boolean explicit() { return true; }
-  }
-
   private @NotNull ImmutableSeq<ParamLike<Term>> enrich(@NotNull SeqLike<Param> tele) {
     var richTele = MutableList.<ParamLike<Term>>create();
 
     for (var param : tele) {
-      var freeTy = param.type().instantiateTele(richTele.view()
-        .map(x -> new FreeTerm(x.ref())));
-      richTele.append(new CoreParam(LocalVar.generate(param.name(), SourcePos.SER), freeTy));
-    }
-
-    return richTele.toImmutableSeq();
-  }
-
-  /**
-   * Generate human friendly names for {@param tele}
-   *
-   * @return a {@link ParamLike} telescope
-   * @apiNote remember to instantiate body with corresponding {@link FreeTerm}
-   */
-  private @NotNull ImmutableSeq<ParamLike<Term>> generateNames(@NotNull ImmutableSeq<Term> tele) {
-    var richTele = MutableList.<ParamLike<Term>>create();
-    for (var param : tele) {
-      var freeTy = param.instantiateTeleVar(richTele.view().map(ParamLike::ref));
-      // mutable view!!😱
-      // perhaps we can obtain the whnf of ty as the name
-      // ice: just use freeTy I think it's ok
-      richTele.append(new CoreParam(generateName(freeTy), freeTy));
+      var freeTy = param.type().instantiateTeleVar(richTele.view()
+        .map(ParamLike::ref));
+      richTele.append(new RichParam(LocalVar.generate(param.name(), SourcePos.SER), freeTy, param.explicit()));
     }
 
     return richTele.toImmutableSeq();

diff --git a/syntax/src/main/java/org/aya/syntax/core/RichParam.java b/syntax/src/main/java/org/aya/syntax/core/RichParam.java
@@ -0,0 +1,29 @@
+// 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.syntax.core;
+
+import org.aya.generic.term.ParamLike;
+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.ref.LocalVar;
+import org.jetbrains.annotations.Contract;
+import org.jetbrains.annotations.NotNull;
+
+/**
+ * A enriched {@link org.aya.syntax.core.term.Param}, which is usually used for prettier.
+ */
+public record RichParam(
+  @Override @NotNull LocalVar ref,
+  @Override @NotNull Term type,
+  @Override boolean explicit
+) implements ParamLike<Term> {
+  public static @NotNull RichParam ofExplicit(@NotNull LocalVar ref, @NotNull Term type) {
+    return new RichParam(ref, type, true);
+  }
+
+  public @NotNull FreeTerm toTerm() { return new FreeTerm(ref); }
+  @Contract("-> new") public @NotNull Param degenerate() {
+    return new Param(ref.name(), type, explicit);
+  }
+}
diff --git a/syntax/src/main/java/org/aya/syntax/core/pat/Pat.java b/syntax/src/main/java/org/aya/syntax/core/pat/Pat.java
@@ -9,10 +9,7 @@
 import kala.value.MutableValue;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.stmt.Shaped;
-import org.aya.prettier.BasePrettier;
-import org.aya.prettier.CorePrettier;
-import org.aya.prettier.Tokens;
-import org.aya.pretty.doc.Doc;
+import org.aya.syntax.core.RichParam;
 import org.aya.syntax.core.def.ConDefLike;
 import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.Term;
@@ -26,12 +23,12 @@
 import org.aya.util.error.Panic;
 import org.aya.util.error.SourcePos;
 import org.aya.util.error.WithPos;
-import org.aya.util.prettier.PrettierOptions;
 import org.jetbrains.annotations.Debug;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 import java.util.function.BiConsumer;
+import java.util.function.BiFunction;
 import java.util.function.IntUnaryOperator;
 import java.util.function.UnaryOperator;
 
@@ -41,7 +38,7 @@
  * @author kiva, ice1000, HoshinoTented
  */
 @Debug.Renderer(text = "PatToTerm.visit(this).debuggerOnlyToString()")
-public sealed interface Pat extends AyaDocile {
+public sealed interface Pat {
   @NotNull Pat descent(@NotNull UnaryOperator<Pat> patOp, @NotNull UnaryOperator<Term> termOp);
 
   /**
@@ -57,20 +54,33 @@ public sealed interface Pat extends AyaDocile {
    */
   @NotNull Pat bind(MutableList<LocalVar> vars);
 
+  /**
+   * Traversal the patterns, collect and bind free variables.
+   *
+   * @param pats the patterns
+   * @return (free variables, bound patterns)
+   */
   static @NotNull Pair<MutableList<LocalVar>, ImmutableSeq<Pat>>
   collectVariables(@NotNull SeqView<Pat> pats) {
     var buffer = MutableList.<LocalVar>create();
     var newPats = pats.map(p -> p.bind(buffer)).toImmutableSeq();
     return new Pair<>(buffer, newPats);
   }
 
-  static @NotNull MutableList<Param> collectBindings(@NotNull SeqView<Pat> pats) {
-    var buffer = MutableList.<Param>create();
-    pats.forEach(p -> p.consumeBindings((var, type) ->
-      buffer.append(new Param(var.name(), type, false))));
+  static <U> @NotNull MutableList<U> collectBindings(@NotNull SeqView<Pat> pats, @NotNull BiFunction<LocalVar, Term, U> collector) {
+    var buffer = MutableList.<U>create();
+    pats.forEach(p -> p.consumeBindings((var, type) -> buffer.append(collector.apply(var, type))));
     return buffer;
   }
 
+  static @NotNull MutableList<Param> collectBindings(@NotNull SeqView<Pat> pats) {
+    return collectBindings(pats, (v, t) -> new Param(v.name(), t, true));
+  }
+
+  static @NotNull MutableList<RichParam> collectRichBindings(@NotNull SeqView<Pat> pats) {
+    return collectBindings(pats, RichParam::ofExplicit);
+  }
+
   /**
    * Replace {@link Pat.Meta} with {@link Pat.Meta#solution} (if there is) or {@link Pat.Bind}
    */
@@ -88,10 +98,6 @@ enum Absurd implements Pat {
     @Override public @NotNull Pat inline(@NotNull BiConsumer<LocalVar, Term> bind) { return this; }
   }
 
-  @Override default @NotNull Doc toDoc(@NotNull PrettierOptions options) {
-    return new CorePrettier(options).pat(this, true, BasePrettier.Outer.Free);
-  }
-
   /**
    * @param type of this bind, note that the type may refer to former binds (i.e. dependent type)
    *             by free {@link org.aya.syntax.core.term.LocalTerm}
@@ -264,21 +270,8 @@ record Preclause<T extends AyaDocile>(
     @NotNull SourcePos sourcePos,
     @NotNull ImmutableSeq<Pat> pats,
     int bindCount, @Nullable WithPos<T> expr
-  ) implements AyaDocile {
-    @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
-      var prettier = new CorePrettier(options);
-      var doc = Doc.emptyIf(pats.isEmpty(), () -> Doc.cat(Doc.ONE_WS, Doc.commaList(
-        pats.view().map(p -> prettier.pat(p, true, BasePrettier.Outer.Free)))));
-      return expr == null ? doc : Doc.sep(doc, Tokens.FN_DEFINED_AS, expr.data().toDoc(options));
-    }
-
-    public static @NotNull Preclause<Term> weaken(@NotNull Term.Matching clause) {
-      return new Preclause<>(clause.sourcePos(), clause.patterns(), clause.bindCount(),
-        WithPos.dummy(clause.body()));
-    }
-
-    public static @NotNull Option<Term.Matching>
-    lift(@NotNull Preclause<Term> clause) {
+  ) {
+    public static @NotNull Option<Term.Matching> lift(@NotNull Preclause<Term> clause) {
       if (clause.expr == null) return Option.none();
       var match = new Term.Matching(clause.sourcePos, clause.pats, clause.bindCount, clause.expr.data());
       return Option.some(match);

diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Param.java b/syntax/src/main/java/org/aya/syntax/core/term/Param.java
@@ -38,8 +38,7 @@ public record Param(@NotNull String name, @NotNull Term type, boolean explicit)
     return update(mapper.apply(type));
   }
 
-  @Override
-  public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
+  @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
     return new CorePrettier(options).visitParam(this, BasePrettier.Outer.Free);
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/Term.java b/syntax/src/main/java/org/aya/syntax/core/term/Term.java
@@ -182,11 +182,7 @@ record Matching(
     @NotNull SourcePos sourcePos,
     @NotNull ImmutableSeq<Pat> patterns,
     int bindCount, @NotNull Term body
-  ) implements AyaDocile {
-    @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
-      return Pat.Preclause.weaken(this).toDoc(options);
-    }
-
+  ) {
     public @NotNull Matching update(@NotNull ImmutableSeq<Pat> patterns, @NotNull Term body) {
       return body == body() && patterns.sameElements(patterns(), true) ? this
         : new Matching(sourcePos, patterns, bindCount, body);