merge: #991

991: Use Java 20 language features r=ice1000 a=ice1000 bors r+ Written under the supervision of `@imkiva` and `@HoshinoTented` Co-authored-by: ice1000 <ice1000kotlin@foxmail.com>
aya-prover · Aug 5, 2023 · 89e400e · 89e400e
2 parents 01256ee + 641de84
commit 89e400e
Show file tree

Hide file tree

Showing 10 changed files with 45 additions and 43 deletions.
diff --git a/base/src/main/java/org/aya/core/term/FormulaTerm.java b/base/src/main/java/org/aya/core/term/FormulaTerm.java
@@ -1,7 +1,8 @@
-// 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.Seq;
 import kala.collection.SeqView;
 import org.aya.core.pat.Pat;
 import org.aya.guest0x0.cubical.Formula;
@@ -44,9 +45,9 @@ public record FormulaTerm(@NotNull Formula<Term> asFormula) implements Term {
 
   public @NotNull SeqView<Term> view() {
     return switch (asFormula) {
-      case Formula.Conn<Term> cnn -> SeqView.of(cnn.l()).appended(cnn.r());
-      case Formula.Inv<Term> inv -> SeqView.of(inv.i());
-      case Formula.Lit<Term> lit -> SeqView.empty();
+      case Formula.Conn(var $, var l, var r) -> Seq.of(l, r).view();
+      case Formula.Inv(var i) -> SeqView.of(i);
+      case Formula.Lit<?> $ -> SeqView.empty();
     };
   }
 }
diff --git a/base/src/main/java/org/aya/core/term/PartialTerm.java b/base/src/main/java/org/aya/core/term/PartialTerm.java
@@ -55,7 +55,7 @@ public static Partial<Term> amendTerms(Partial<Term> p, UnaryOperator<Term> appl
     return switch (p) {
       case Partial.Split<Term> s -> new Split<>(s.clauses().map(c ->
         new Restr.Side<>(c.cof(), applyDimsTo.apply(c.u()))));
-      case Partial.Const<Term> c -> new Const<>(applyDimsTo.apply(c.u()));
+      case Partial.Const(var c) -> new Const<>(applyDimsTo.apply(c));
     };
   }
 

diff --git a/base/src/main/java/org/aya/core/visitor/BetaExpander.java b/base/src/main/java/org/aya/core/visitor/BetaExpander.java
@@ -50,15 +50,15 @@ case PAppTerm(var of, var args, PathTerm(var xi, var type, var partial)) -> {
         }
         yield switch (partial(partial)) {
           case Partial.Split<Term> hap -> new PAppTerm(of, args, new PathTerm(xi, type, hap));
-          case Partial.Const<Term> sad -> sad.u();
+          case Partial.Const(var sad) -> sad;
         };
       }
       case PartialTerm(var partial, var rhsTy) -> new PartialTerm(partial(partial), rhsTy);
       // TODO[coe]: temporary hack
       case CoeTerm(
         var ty,
-        FormulaTerm(Formula.Lit<Term>(var r)),
-        FormulaTerm(Formula.Lit<Term>(var s))
+        FormulaTerm(Formula.Lit(var r)),
+        FormulaTerm(Formula.Lit(var s))
       ) when r == s -> identity("x");
       case CoeTerm(var ty, RefTerm(var r), RefTerm(var s)) when r == s -> identity("x");
       case CoeTerm coe -> {

diff --git a/base/src/main/java/org/aya/core/visitor/DeltaExpander.java b/base/src/main/java/org/aya/core/visitor/DeltaExpander.java
@@ -10,10 +10,10 @@
 import org.aya.core.pat.PatMatcher;
 import org.aya.core.term.*;
 import org.aya.generic.Modifier;
-import org.aya.util.error.InternalException;
 import org.aya.guest0x0.cubical.Partial;
 import org.aya.tyck.tycker.TyckState;
 import org.aya.util.Arg;
+import org.aya.util.error.InternalException;
 import org.jetbrains.annotations.NotNull;
 
 /**
@@ -36,7 +36,7 @@ public interface DeltaExpander extends EndoTerm {
         if (def == null) yield con;
         var sat = AyaRestrSimplifier.INSTANCE.mapSplit(def.clauses, t ->
           t.subst(buildSubst(def.fullTelescope(), con.args())));
-        if (sat instanceof Partial.Const<Term> c) yield apply(c.u());
+        if (sat instanceof Partial.Const(var c)) yield apply(c);
         yield con;
       }
       case FnCall fn -> {

diff --git a/base/src/main/java/org/aya/core/visitor/Subst.java b/base/src/main/java/org/aya/core/visitor/Subst.java
@@ -101,7 +101,7 @@ public boolean isEmpty() {
     // In an and-only cofibration, every variable appears uniquely in a cond.
     if (!map.containsKey(i)) return false;
     // check whether if the cond is self-contradictory
-    if (!(map.get(i).asFormula() instanceof Formula.Lit<Term> end)) return false;
+    if (!(map.get(i).asFormula() instanceof Formula.Lit<?> end)) return false;
     return end.isOne() != newIsOne;
   }
 

diff --git a/base/src/main/java/org/aya/prettier/BasePrettier.java b/base/src/main/java/org/aya/prettier/BasePrettier.java
@@ -293,25 +293,25 @@ private Doc mutableListNames(MutableList<LocalVar> names, ParamLike<?> param) {
 
   public @NotNull Doc formula(@NotNull Outer outer, @NotNull Formula<Term> formula) {
     return switch (formula) {
-      case Formula.Conn<Term> cnn -> {
-        var here = cnn.isAnd() ? Outer.IMin : Outer.IMax;
+      case Formula.Conn(var isAnd, var l, var r) -> {
+        var here = isAnd ? Outer.IMin : Outer.IMax;
         yield checkParen(outer, Doc.sep(
-            term(here, cnn.l()),
-            cnn.isAnd() ? Doc.symbol("/\\") : Doc.symbol("\\/"),
-            term(here, cnn.r())),
-          cnn.isAnd() ? Outer.AppHead : Outer.IMin);
+            term(here, l),
+            isAnd ? Doc.symbol("/\\") : Doc.symbol("\\/"),
+            term(here, r)),
+          isAnd ? Outer.AppHead : Outer.IMin);
       }
-      case Formula.Inv<Term> inv -> checkParen(outer,
-        Doc.sep(Doc.symbol("~"), term(Outer.AppSpine, inv.i())),
+      case Formula.Inv(var i) -> checkParen(outer,
+        Doc.sep(Doc.symbol("~"), term(Outer.AppSpine, i)),
         Outer.AppSpine);
-      case Formula.Lit<Term>(var one) -> Doc.plain(one ? "1" : "0");
+      case Formula.Lit(var one) -> Doc.plain(one ? "1" : "0");
     };
   }
 
   public static <T extends Restr.TermLike<T> & AyaDocile> @NotNull Doc
   partial(@NotNull PrettierOptions options, @NotNull Partial<T> partial, boolean showEmpty, @NotNull Doc lb, @NotNull Doc rb) {
     return switch (partial) {
-      case Partial.Const<T> sad -> Doc.sepNonEmpty(lb, sad.u().toDoc(options), rb);
+      case Partial.Const(var sad) -> Doc.sepNonEmpty(lb, sad.toDoc(options), rb);
       case Partial.Split<T> hap when !showEmpty && hap.clauses().isEmpty() -> Doc.empty();
       case Partial.Split<T> hap -> Doc.sepNonEmpty(lb,
         Doc.join(Doc.spaced(Doc.symbol("|")), hap.clauses().map(s -> side(options, s))),

diff --git a/base/src/main/java/org/aya/prettier/Codifier.java b/base/src/main/java/org/aya/prettier/Codifier.java
@@ -174,9 +174,9 @@ private void partial(Partial<Term> par) {
         });
         builder.append("))");
       }
-      case Partial.Const<Term> c -> {
+      case Partial.Const(var c) -> {
         builder.append("new Partial.Const<>(");
-        term(c.u());
+        term(c);
         builder.append(")");
       }
     }
@@ -207,19 +207,19 @@ private void restr(Restr<Term> restr) {
 
   private void formula(Formula<Term> mula) {
     switch (mula) {
-      case Formula.Conn<Term> conn -> {
-        builder.append("new Formula.Conn<>(").append(conn.isAnd()).append(",");
-        term(conn.l());
+      case Formula.Conn(var isAnd, var l, var r) -> {
+        builder.append("new Formula.Conn<>(").append(isAnd).append(",");
+        term(l);
         builder.append(",");
-        term(conn.r());
+        term(r);
         builder.append(")");
       }
-      case Formula.Inv<Term> inv -> {
+      case Formula.Inv(var i) -> {
         builder.append("new Formula.Inv<>(");
-        term(inv.i());
+        term(i);
         builder.append(")");
       }
-      case Formula.Lit<Term>(var one) -> builder.append("new Formula.Lit<>(").append(one).append(")");
+      case Formula.Lit(var one) -> builder.append("new Formula.Lit<>(").append(one).append(")");
     }
   }
 

diff --git a/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java b/base/src/main/java/org/aya/tyck/tycker/UnifiedTycker.java
@@ -154,7 +154,7 @@ protected final Result.Default checkBoundaries(Expr expr, PathTerm path, Subst s
     var applied = path.applyDimsTo(lambda);
     return ctx.withIntervals(path.params().view(), () -> {
       var happy = switch (path.partial()) {
-        case Partial.Const<Term> sad -> boundary(expr, applied, sad.u(), path.type(), subst);
+        case Partial.Const(var sad) -> boundary(expr, applied, sad, path.type(), subst);
         case Partial.Split<Term> hap -> hap.clauses().allMatch(c ->
           CofThy.conv(c.cof(), subst, s -> boundary(expr, applied, c.u(), path.type(), s)));
       };

diff --git a/base/src/main/java/org/aya/tyck/unify/TermComparator.java b/base/src/main/java/org/aya/tyck/unify/TermComparator.java
@@ -27,6 +27,7 @@
 import org.aya.tyck.tycker.TyckState;
 import org.aya.util.Arg;
 import org.aya.util.Ordering;
+import org.aya.util.Pair;
 import org.aya.util.error.InternalException;
 import org.aya.util.error.SourcePos;
 import org.aya.util.reporter.Reporter;
@@ -247,9 +248,6 @@ private boolean visitLists(SeqView<Term> l, SeqView<Term> r, Sub lr, Sub rl, @No
     else return null;
   }
 
-  /** TODO: Revise when JDK 21 is released. */
-  private record Pair(Term lhs, Term rhs) {}
-
   private boolean doCompareTyped(@NotNull Term type, @NotNull Term lhs, @NotNull Term rhs, Sub lr, Sub rl) {
     // Skip tracing, because too easy.
     // Note that it looks tempting to apply some unification here, but it is not correct:
@@ -290,7 +288,7 @@ case SigmaTerm(var paramsSeq) -> {
       }
       // https://stackoverflow.com/q/75971020/7083401
       case PiTerm pi -> ctx.with(pi.param(), () -> {
-        var pair = new Pair(lhs, rhs);
+        var pair = new Pair<>(lhs, rhs);
         if (pair instanceof Pair(LamTerm(var lp, var lb), LamTerm(var rp, var rb))) {
           var ref = pi.param().ref();
           if (ref == LocalVar.IGNORED) ref = new LocalVar(lp.ref().name() + rp.ref().name());
@@ -335,7 +333,7 @@ case SigmaTerm(var paramsSeq) -> {
       case PrimCall prim when prim.id() == PrimDef.ID.SUB -> {
         // See PrimDef.Factory.Initializer.sub
         var A = prim.args().get(0).term();
-        if (new Pair(lhs, rhs) instanceof Pair(InTerm(var lPhi, var lU), InTerm(var rPhi, var rU))) {
+        if (new Pair<>(lhs, rhs) instanceof Pair(InTerm(var lPhi, var lU), InTerm(var rPhi, var rU))) {
           if (!compare(lPhi, rPhi, lr, rl, IntervalTerm.INSTANCE)) yield false;
           yield compare(lU, rU, lr, rl, A);
         } else yield compare(lhs, rhs, lr, rl, A);
@@ -367,10 +365,9 @@ private boolean comparePartial(
     @NotNull PartialTerm lhs, @NotNull PartialTerm rhs,
     @NotNull PartialTyTerm type, Sub lr, Sub rl
   ) {
-    record P(Partial<Term> l, Partial<Term> r) {}
-    return switch (new P(lhs.partial(), rhs.partial())) {
-      case P(Partial.Const<Term>(var ll), Partial.Const<Term>(var rr)) -> compare(ll, rr, lr, rl, type.type());
-      case P(Partial.Split<Term> ll, Partial.Split<Term> rr) -> CofThy.conv(type.restr(), new Subst(),
+    return switch (new Pair<>(lhs.partial(), rhs.partial())) {
+      case Pair(Partial.Const(var ll), Partial.Const(var rr)) -> compare(ll, rr, lr, rl, type.type());
+      case Pair(Partial.Split<?> ll, Partial.Split<?> rr) -> CofThy.conv(type.restr(), new Subst(),
         subst -> compare(lhs.subst(subst), rhs.subst(subst), lr, rl, type.subst(subst)));
       default -> false;
     };
@@ -395,9 +392,7 @@ private boolean compareCube(@NotNull PathTerm lhs, @NotNull PathTerm rhs, Sub lr
    */
   private boolean doCompareType(@NotNull Formation preLhs, @NotNull Term preRhs, Sub lr, Sub rl) {
     if (preLhs.getClass() != preRhs.getClass()) return false;
-    record Pair(Formation lhs, Formation rhs) {
-    }
-    return switch (new Pair(preLhs, (Formation) preRhs)) {
+    return switch (new Pair<>(preLhs, (Formation) preRhs)) {
       case Pair(DataCall lhs, DataCall rhs) -> {
         if (lhs.ref() != rhs.ref()) yield false;
         yield visitArgs(lhs.args(), rhs.args(), lr, rl, Term.Param.subst(Def.defTele(lhs.ref()), lhs.ulift()));

diff --git a/tools/src/main/java/org/aya/util/Pair.java b/tools/src/main/java/org/aya/util/Pair.java
@@ -0,0 +1,6 @@
+// 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.util;
+
+public record Pair<A, B>(A component1, B component2) {
+}