merge: #874

874: Reimplement sort system: step 1 r=ice1000 a=ice1000

Support `piDom` checks.

Co-authored-by: ice1000 <ice1000kotlin@foxmail.com>

base/src/main/java/module-info.java

@@ -17,6 +17,7 @@
   exports org.aya.concrete.visitor;
   exports org.aya.concrete;
   exports org.aya.core.def;
+  exports org.aya.core.meta;
   exports org.aya.core.ops;
   exports org.aya.core.pat;
   exports org.aya.core.repr;

base/src/main/java/org/aya/core/Meta.java → base/src/main/java/org/aya/core/meta/Meta.java

@@ -1,21 +1,21 @@
 // Copyright (c) 2020-2023 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.core;
+package org.aya.core.meta;
 
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.mutable.MutableList;
 import kala.tuple.Tuple2;
 import org.aya.core.term.MetaTerm;
 import org.aya.core.term.PiTerm;
+import org.aya.core.term.SortTerm;
 import org.aya.core.term.Term;
 import org.aya.core.visitor.Subst;
 import org.aya.generic.Constants;
 import org.aya.ref.AnyVar;
 import org.aya.util.Arg;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.NotNull;
-import org.jetbrains.annotations.Nullable;
 
 /**
  * @author ice1000, re-xyr
@@ -26,13 +26,8 @@ public final class Meta implements AnyVar {
   public final @NotNull ImmutableSeq<Term.Param> contextTele;
   public final @NotNull ImmutableSeq<Term.Param> telescope;
   public final @NotNull String name;
-  public final @Nullable Term result;
+  public final @NotNull MetaInfo info;
   public final @NotNull SourcePos sourcePos;
-  /**
-   * Usually implies {@link Meta#result} == null,
-   * asserts that the current meta is a type meta.
-   */
-  public final boolean isType;
   public final @NotNull MutableList<Tuple2<Subst, Term>> conditions = MutableList.create();
 
   public SeqView<Term.Param> fullTelescope() {
@@ -42,22 +37,21 @@ public SeqView<Term.Param> fullTelescope() {
   private Meta(
     @NotNull ImmutableSeq<Term.Param> contextTele,
     @NotNull ImmutableSeq<Term.Param> telescope,
-    @NotNull String name, @Nullable Term result,
-    boolean isType, @NotNull SourcePos sourcePos
+    @NotNull String name, @NotNull MetaInfo info,
+    @NotNull SourcePos sourcePos
   ) {
     this.contextTele = contextTele;
     this.telescope = telescope;
     this.name = name;
-    this.result = result;
-    this.isType = isType;
+    this.info = info;
     this.sourcePos = sourcePos;
   }
 
   public static @NotNull Meta from(
     @NotNull ImmutableSeq<Term.Param> contextTele, @NotNull String name,
     @NotNull SourcePos sourcePos
   ) {
-    return new Meta(contextTele, ImmutableSeq.empty(), name, null, true, sourcePos);
+    return new Meta(contextTele, ImmutableSeq.empty(), name, new MetaInfo.AnyType(), sourcePos);
   }
 
   public static @NotNull Meta from(
@@ -66,24 +60,38 @@ private Meta(
   ) {
     if (result instanceof PiTerm pi) {
       var buf = MutableList.<Term.Param>create();
-      var r = pi.parameters(buf);
-      return new Meta(contextTele, buf.toImmutableSeq(), name, r, false, sourcePos);
-    } else return new Meta(contextTele, ImmutableSeq.empty(), name, result, false, sourcePos);
+      var r = new MetaInfo.Result(pi.parameters(buf));
+      return new Meta(contextTele, buf.toImmutableSeq(), name, r, sourcePos);
+    } else return new Meta(contextTele, ImmutableSeq.empty(), name, new MetaInfo.Result(result), sourcePos);
   }
 
   public @NotNull PiTerm asPi(
     @NotNull String domName, @NotNull String codName, boolean explicit,
     @NotNull ImmutableSeq<Arg<Term>> contextArgs
   ) {
     assert telescope.isEmpty();
-    var domVar = new Meta(contextTele, ImmutableSeq.empty(), domName, result, isType, sourcePos);
-    var codVar = new Meta(contextTele, ImmutableSeq.empty(), codName, result, isType, sourcePos);
+    var knownDomInfo = info;
+    // TODO[isType]: deal with piCod
+    var knownCodInfo = info;
+    if (knownDomInfo instanceof MetaInfo.Result(var result)) {
+      if (!(result instanceof SortTerm sort)) throw new AssertionError("This should be unreachable");
+      knownDomInfo = new MetaInfo.PiDom(sort);
+    }
+    var domVar = new Meta(contextTele, ImmutableSeq.empty(), domName, knownDomInfo, sourcePos);
+    var codVar = new Meta(contextTele, ImmutableSeq.empty(), codName, knownCodInfo, sourcePos);
     var dom = new MetaTerm(domVar, contextArgs, ImmutableSeq.empty());
     var cod = new MetaTerm(codVar, contextArgs, ImmutableSeq.empty());
     var domParam = new Term.Param(Constants.randomlyNamed(sourcePos), dom, explicit);
     return new PiTerm(domParam, cod);
   }
 
+  public @NotNull MetaTerm asPiDom(@NotNull SortTerm sort, @NotNull ImmutableSeq<Arg<Term>> contextArgs) {
+    assert telescope.isEmpty();
+    assert info instanceof MetaInfo.AnyType;
+    var typed = new Meta(contextTele, ImmutableSeq.empty(), name, new MetaInfo.PiDom(sort), sourcePos);
+    return new MetaTerm(typed, contextArgs, ImmutableSeq.empty());
+  }
+
   @Override public @NotNull String name() {
     return name;
   }

base/src/main/java/org/aya/core/meta/MetaInfo.java

@@ -0,0 +1,72 @@
+// Copyright (c) 2020-2023 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.core.meta;
+
+import org.aya.core.term.SortTerm;
+import org.aya.core.term.Term;
+import org.aya.generic.AyaDocile;
+import org.aya.pretty.doc.Doc;
+import org.aya.tyck.unify.Synthesizer;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+/**
+ * Constraints on a meta variable.
+ *
+ * @author ice1000
+ */
+public sealed interface MetaInfo extends AyaDocile {
+  @Nullable Term result();
+  boolean isType(@NotNull Synthesizer synthesizer);
+  /**
+   * The type of the meta is known.
+   * We shall check the solution against this type.
+   */
+  record Result(@NotNull Term result) implements MetaInfo {
+    @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
+      return Doc.sep(Doc.symbol("?"), Doc.symbol(":"), result.toDoc(options));
+    }
+
+    @Override public boolean isType(@NotNull Synthesizer synthesizer) {
+      return synthesizer.tryPress(result) instanceof SortTerm;
+    }
+  }
+
+  /**
+   * The meta variable is a type.
+   * It should be able to appear on the RHS of a judgment.
+   */
+  record AnyType() implements MetaInfo {
+    @Override public @Nullable Term result() {
+      return null;
+    }
+
+    @Override public boolean isType(@NotNull Synthesizer synthesizer) {
+      return true;
+    }
+
+    @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
+      return Doc.sep(Doc.plain("_"), Doc.symbols(":", "?"));
+    }
+  }
+
+  /**
+   * The meta variable is the domain of a pi type which is of a known type.
+   * <p>
+   * See: <code>notes/sort-system.md</code>
+   */
+  record PiDom(@NotNull SortTerm sort) implements MetaInfo {
+    @Override public @Nullable Term result() {
+      return null;
+    }
+
+    @Override public boolean isType(@NotNull Synthesizer synthesizer) {
+      return true;
+    }
+
+    @Override public @NotNull Doc toDoc(@NotNull PrettierOptions options) {
+      return Doc.sep(Doc.symbols("?", "->", "_", ":"), sort.toDoc(options));
+    }
+  }
+}

base/src/main/java/org/aya/core/term/MetaTerm.java

@@ -1,10 +1,10 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 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.core.term;
 
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
-import org.aya.core.Meta;
+import org.aya.core.meta.Meta;
 import org.aya.util.Arg;
 import org.jetbrains.annotations.NotNull;
 
@@ -31,6 +31,10 @@ public record MetaTerm(
     return ref.asPi(ref.name() + "dom", ref.name() + "cod", explicit, contextArgs);
   }
 
+  public @NotNull MetaTerm asPiDom(@NotNull SortTerm result) {
+    return ref.asPiDom(result, contextArgs);
+  }
+
   public @NotNull SeqView<@NotNull Arg<Term>> fullArgs() {
     return contextArgs.view().concat(args);
   }

base/src/main/java/org/aya/core/term/PiTerm.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 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.core.term;
 
@@ -11,7 +11,6 @@
 import org.aya.tyck.Result;
 import org.aya.util.Arg;
 import org.jetbrains.annotations.NotNull;
-import org.jetbrains.annotations.Nullable;
 
 import java.util.function.UnaryOperator;
 
@@ -62,7 +61,7 @@ case PiTerm(var param, var body)when param.explicit() -> {
     };
   }
 
-  public static @Nullable SortTerm max(@NotNull SortTerm domain, @NotNull SortTerm codomain) {
+  public static @NotNull SortTerm max(@NotNull SortTerm domain, @NotNull SortTerm codomain) {
     var alift = domain.lift();
     var blift = codomain.lift();
     return switch (domain.kind()) {
@@ -72,18 +71,16 @@ case PiTerm(var param, var body)when param.explicit() -> {
         case Prop -> codomain;
       };
       case ISet -> switch (codomain.kind()) {
-        case ISet -> SortTerm.Set0;
+        case ISet, Prop -> SortTerm.Set0;
         case Set, Type -> codomain;
-        default -> null;
       };
       case Set -> switch (codomain.kind()) {
         case Set, Type -> new SortTerm(SortKind.Set, Math.max(alift, blift));
-        case ISet -> new SortTerm(SortKind.Set, alift);
-        default -> null;
+        case ISet, Prop -> new SortTerm(SortKind.Set, alift);
       };
       case Prop -> switch (codomain.kind()) {
         case Prop, Type -> codomain;
-        default -> null;
+        default -> new SortTerm(SortKind.Set, blift);
       };
     };
   }

base/src/main/java/org/aya/core/term/SortTerm.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2023 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.core.term;
 
@@ -27,6 +27,9 @@ public SortTerm(@NotNull SortKind kind, int lift) {
   public static final @NotNull SortTerm ISet = new SortTerm(SortKind.ISet, 0);
   public static final @NotNull SortTerm Prop = new SortTerm(SortKind.Prop, 0);
 
+  /**
+   * <a href="https://github.com/agda/agda/blob/6a92d584c70a615fdc3f364975814d75a0e31bf7/src/full/Agda/TypeChecking/Substitute.hs#L1541-L1558">Agda</a>
+   */
   public @NotNull SortTerm succ() {
     return switch (kind) {
       case Type, Set -> new SortTerm(kind, lift + 1);

base/src/main/java/org/aya/core/term/Term.java

@@ -19,9 +19,9 @@
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.AnyVar;
 import org.aya.ref.LocalVar;
-import org.aya.tyck.Synthesizer;
 import org.aya.tyck.env.LocalCtx;
 import org.aya.tyck.tycker.TyckState;
+import org.aya.tyck.unify.Synthesizer;
 import org.aya.util.Arg;
 import org.aya.util.error.SourcePos;
 import org.aya.util.prettier.PrettierOptions;