Bump Gradle to 8.3 RC1

.github/workflows/commit-check.yml

@@ -10,7 +10,7 @@ jobs:
   commit-check:
     runs-on: ubuntu-20.04
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
         with:
           fetch-depth: 0
           ref: ${{ github.event.pull_request.head.sha }}

.github/workflows/gradle-check.yml

@@ -11,11 +11,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - uses: actions/checkout@v3
-      - name: Setup Java 19
+      - name: Setup Java 20
         uses: actions/setup-java@v3
         with:
           distribution: 'liberica'
-          java-version: '19'
+          java-version: '20'
       - uses: gradle/gradle-build-action@v2
         with:
           arguments: testCodeCoverageReport --no-daemon --stacktrace --warning-mode all

.github/workflows/nightly-build.yml

@@ -21,7 +21,7 @@ jobs:
     outputs:
       isSnapshot: ${{ steps.check.outputs.isSnapshot }}
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
       - name: Check snapshot version
         id: check
         run: |
@@ -39,12 +39,12 @@ jobs:
       ossrhUsername: ${{ secrets.OSSRHUSERNAME }}
       ossrhPassword: ${{ secrets.OSSRHPASSWORD }}
     steps:
-      - uses: actions/checkout@v2
-      - name: Setup Java 19
+      - uses: actions/checkout@v3
+      - name: Setup Java 20
         uses: actions/setup-java@v3
         with:
           distribution: 'liberica'
-          java-version: '19'
+          java-version: '20'
       - name: gradle publish
         uses: gradle/gradle-build-action@v2
         with:
@@ -70,13 +70,13 @@ jobs:
             platform: 'windows-x64'
             binaryExt: '.exe'
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v3
 
-      - name: Setup Java 19
+      - name: Setup Java 20
         uses: actions/setup-java@v3
         with:
           distribution: 'liberica'
-          java-version: '19'
+          java-version: '20'
 
       - name: Run task jlinkAyaZip
         uses: gradle/gradle-build-action@v2
@@ -93,9 +93,8 @@ jobs:
       - name: Setup GraalVM
         uses: graalvm/setup-graalvm@v1
         with:
-          # Switch back when Java 20
-          version: '22.3.1'
-          java-version: '19'
+          version: 'latest'
+          java-version: '20'
           components: 'native-image'
           set-java-home: 'false'
           github-token: ${{ secrets.GH_TOKEN }}

base/src/main/java/org/aya/concrete/remark/CodeOptions.java

@@ -20,10 +20,9 @@ public record CodeOptions(
   @NotNull ShowCode showCode
 ) {
   public static @NotNull Literate analyze(@NotNull Code code, @NotNull SourcePos sourcePos) {
-    return switch (code.getFirstChild()) {
-      case CodeAttrProcessor.Attr attr -> new AyaLiterate.AyaInlineCode(code.getLiteral(), sourcePos, attr.options);
-      case default, null -> new Literate.Raw(Doc.code(Language.Builtin.Plain, Doc.plain(code.getLiteral())));
-    };
+    return code.getFirstChild() instanceof CodeAttrProcessor.Attr attr
+      ? new AyaLiterate.AyaInlineCode(code.getLiteral(), sourcePos, attr.options)
+      : new Literate.Raw(Doc.code(Language.Builtin.Plain, Doc.plain(code.getLiteral())));
   }
 
   public enum ShowCode {

base/src/main/java/org/aya/core/pat/PatUnify.java

@@ -6,12 +6,12 @@
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.core.term.RefTerm;
 import org.aya.core.visitor.Subst;
-import org.aya.util.error.InternalException;
 import org.aya.prettier.AyaPrettierOptions;
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.LocalVar;
 import org.aya.tyck.env.LocalCtx;
 import org.aya.util.Arg;
+import org.aya.util.error.InternalException;
 import org.jetbrains.annotations.NotNull;
 
 /**
@@ -23,7 +23,6 @@
 public record PatUnify(@NotNull Subst lhsSubst, @NotNull Subst rhsSubst, @NotNull LocalCtx ctx) {
   private void unify(@NotNull Pat lhs, @NotNull Pat rhs) {
     switch (lhs) {
-      default -> throw new InternalException();
       case Pat.Bind bind -> visitAs(bind.bind(), rhs);
       case Pat.Meta meta -> visitAs(meta.fakeBind(), rhs);
       case Pat.Tuple tuple -> {
@@ -52,6 +51,7 @@ private void unify(@NotNull Pat lhs, @NotNull Pat rhs) {
           default -> unify(lhsInt.constructorForm(), rhs);
         }
       }
+      default -> throw new InternalException();
     }
   }
 

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

@@ -85,9 +85,6 @@ public record PathTerm(
     while (true) {
       if (args.isEmpty()) return pLam;
       switch (pLam) {
-        case default -> {
-          break loop;
-        }
         case PLamTerm lam -> {
           assert lam.params().sizeLessThanOrEquals(args);
           pLam = lam.body().subst(new Subst(lam.params(), args.take(lam.params().size())));
@@ -99,6 +96,9 @@ public record PathTerm(
           pLam = AppTerm.make(lam, new Arg<>(args.first(), true));
           args = args.drop(1);
         }
+        default -> {
+          break loop;
+        }
       }
     }
     var newArgs = args.map(x -> new Arg<Term>(x, true)).toImmutableSeq();

base/src/main/java/org/aya/prettier/Codifier.java

@@ -111,7 +111,7 @@ case FormulaTerm(var mula) -> {
         builder.append(sort.lift());
         builder.append(")");
       }
-      case default -> throw new UnsupportedOperationException("TODO: " + term.getClass().getCanonicalName());
+      default -> throw new UnsupportedOperationException("TODO: " + term.getClass().getCanonicalName());
     }
   }
 

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

@@ -186,8 +186,9 @@ public void enterBody() {
         }
         case AnyVar var -> new Expr.Ref(pos, var);
       };
-      case Expr.Let(var $, var letBind, var body) let -> {
+      case Expr.Let let -> {
         // resolve letBind
+        var letBind = let.bind();
 
         var mCtx = MutableValue.create(ctx);
         // visit telescope
@@ -203,18 +204,19 @@ public void enterBody() {
 
         // resolve body
         var newBody = enter(ctx.bind(letBind.bindName()))
-          .apply(body);
+          .apply(let.body());
 
         yield let.update(
           letBind.update(telescope, result, definedAs),
           newBody
         );
       }
-      case Expr.LetOpen(var pos, var component, var useHide, var body) letOpen -> {
+      case Expr.LetOpen letOpen -> {
         var innerCtx = new NoExportContext(ctx);
         // open module
-        innerCtx.openModule(component, Stmt.Accessibility.Private, pos, useHide);
-        yield letOpen.update(enter(innerCtx).apply(body));
+        innerCtx.openModule(letOpen.componentName(), Stmt.Accessibility.Private,
+          letOpen.sourcePos(), letOpen.useHide());
+        yield letOpen.update(enter(innerCtx).apply(letOpen.body()));
       }
       default -> EndoExpr.super.apply(expr);
     };

base/src/main/java/org/aya/tyck/env/LocalCtx.java

@@ -17,10 +17,10 @@
 import org.aya.core.term.Term;
 import org.aya.core.visitor.VarConsumer;
 import org.aya.generic.Constants;
-import org.aya.util.error.InternalException;
 import org.aya.ref.AnyVar;
 import org.aya.ref.LocalVar;
 import org.aya.tyck.tycker.TyckState;
+import org.aya.util.error.InternalException;
 import org.aya.util.error.SourcePos;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.Debug;
@@ -84,7 +84,7 @@ default void forward(@NotNull LocalCtx dest, @NotNull Term term, @NotNull TyckSt
             var sol = state.metas().getOrNull(meta);
             if (sol != null) forward(dest, sol, state);
           }
-          case default -> {}
+          default -> {}
         }
       }
     }.accept(term);

base/src/main/java/org/aya/tyck/pat/PatClassifier.java

@@ -99,8 +99,6 @@
     var whnfTy = whnf(param.type());
     final var explicit = param.explicit();
     switch (whnfTy) {
-      default -> {
-      }
       // Note that we cannot have ill-typed patterns such as constructor patterns,
       // since patterns here are already well-typed
       case SigmaTerm(var params) -> {
@@ -180,6 +178,8 @@
         }
         return buffer.toImmutableSeq();
       }
+      default -> {
+      }
     }
     return ImmutableSeq.of(new PatClass<>(param.toArg(), Indexed.indices(clauses)));
   }

base/src/main/java/org/aya/tyck/unify/DoubleChecker.java

@@ -78,7 +78,7 @@ case PiTerm(var dom, var cod) -> {
         unifier.solveMeta(meta, new MetaTerm(newMeta, meta.contextArgs(), meta.args()), lr, rl, expected);
         yield true;
       }
-      case default -> compare(synthesizer.press(preterm), expected);
+      default -> compare(synthesizer.press(preterm), expected);
     };
   }
 

base/src/main/java/org/aya/tyck/unify/Synthesizer.java

@@ -11,13 +11,13 @@
 import org.aya.core.visitor.DeltaExpander;
 import org.aya.core.visitor.Subst;
 import org.aya.generic.SortKind;
-import org.aya.util.error.InternalException;
 import org.aya.generic.util.NormalizeMode;
 import org.aya.guest0x0.cubical.Partial;
 import org.aya.prettier.AyaPrettierOptions;
 import org.aya.tyck.env.LocalCtx;
 import org.aya.tyck.tycker.TyckState;
 import org.aya.util.Arg;
+import org.aya.util.error.InternalException;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
@@ -169,7 +169,7 @@
         var piRaw = tryPress(of);
         yield piRaw instanceof PiTerm pi ? pi.substBody(arg.term()) : null;
       }
-      case default -> null;
+      default -> null;
     };
   }
 

base/src/main/java/org/aya/tyck/unify/TermComparator.java

@@ -14,7 +14,6 @@
 import org.aya.core.visitor.AyaRestrSimplifier;
 import org.aya.core.visitor.Subst;
 import org.aya.generic.SortKind;
-import org.aya.util.error.InternalException;
 import org.aya.guest0x0.cubical.CofThy;
 import org.aya.guest0x0.cubical.Partial;
 import org.aya.prettier.AyaPrettierOptions;
@@ -28,6 +27,7 @@
 import org.aya.tyck.tycker.TyckState;
 import org.aya.util.Arg;
 import org.aya.util.Ordering;
+import org.aya.util.error.InternalException;
 import org.aya.util.error.SourcePos;
 import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.Debug;
@@ -88,11 +88,11 @@
     return switch (l.kind()) {
       case Type -> switch (r.kind()) {
         case Type, Set -> lift <= rift;
-        case default -> false;
+        default -> false;
       };
       case ISet -> switch (r.kind()) {
         case ISet, Set -> true;
-        case default -> false;
+        default -> false;
       };
       case Prop -> r.kind() == SortKind.Prop;
       case Set -> r.kind() == SortKind.Set && lift <= rift;
@@ -247,7 +247,7 @@
     else return null;
   }
 
-  /** TODO: Revise when JDK 20 is released. */
+  /** 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) {
@@ -259,7 +259,6 @@
     traceEntrance(new Trace.UnifyT(lhs.freezeHoles(state), rhs.freezeHoles(state),
       pos, type.freezeHoles(state)));
     var ret = switch (type) {
-      default -> compareUntyped(lhs, rhs, lr, rl) != null;
       case ClassCall type1 -> {
         var fieldSigs = type1.ref().core.members;
         var fieldSubst = new Subst();
@@ -289,8 +288,10 @@
         ctx.remove(paramsSeq.view().map(Term.Param::ref));
         yield true;
       }
-      case PiTerm pi -> ctx.with(pi.param(), () -> switch (new Pair(lhs, rhs)) {
-        case Pair(LamTerm(var lp, var lb), LamTerm(var rp, var rb)) -> {
+      // https://stackoverflow.com/q/75971020/7083401
+      case PiTerm pi -> ctx.with(pi.param(), () -> {
+        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());
           lr.map.put(ref, rp.toTerm());
@@ -299,12 +300,14 @@
           var res = compare(lb.subst(lp.ref(), piParam), rb.subst(rp.ref(), piParam), lr, rl, pi.body());
           lr.map.remove(ref);
           rl.map.remove(ref);
-          yield res;
+          return res;
+        } else if (pair instanceof Pair(var $, LamTerm rambda)) {
+          return compareLambdaBody(rambda, lhs, rl, lr, pi);
+        } else if (pair instanceof Pair(LamTerm lambda, var $)) {
+          return compareLambdaBody(lambda, rhs, lr, rl, pi);
+        } else {
+          return compare(lhs, rhs, lr, rl, null);
         }
-        case Pair(var $, LamTerm rambda) -> compareLambdaBody(rambda, lhs, rl, lr, pi);
-        case Pair(LamTerm lambda, var $) -> compareLambdaBody(lambda, rhs, lr, rl, pi);
-        // Question: do we need a unification for Pi.body?
-        case default -> compare(lhs, rhs, lr, rl, null);
       });
       // In this case, both sides have the same type (I hope)
       case PathTerm cube -> ctx.withIntervals(cube.params().view(), () -> {
@@ -337,6 +340,7 @@
           yield compare(lU, rU, lr, rl, A);
         } else yield compare(lhs, rhs, lr, rl, A);
       }
+      default -> compareUntyped(lhs, rhs, lr, rl) != null;
     };
     traceExit();
     return ret;
@@ -394,7 +398,6 @@
     record Pair(Formation lhs, Formation rhs) {
     }
     return switch (new Pair(preLhs, (Formation) preRhs)) {
-      default -> throw noRules(preLhs);
       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()));
@@ -413,13 +416,13 @@
         compare(lTy, rTy, lr, rl, null) && compareRestr(lR, rR);
       case Pair(PathTerm lCube, PathTerm rCube) -> compareCube(lCube, rCube, lr, rl);
       case Pair(IntervalTerm lhs, IntervalTerm rhs) -> true;
+      default -> throw noRules(preLhs);
     };
   }
 
   private Term doCompareUntyped(@NotNull Term preLhs, @NotNull Term preRhs, Sub lr, Sub rl) {
     if (preLhs instanceof Formation lhs) return doCompareType(lhs, preRhs, lr, rl) ? SortTerm.Type0 : null;
     return switch (preLhs) {
-      default -> throw noRules(preLhs);
       case ErrorTerm term -> ErrorTerm.typeOf(term);
       case MetaPatTerm(var lhsRef) -> {
         if (preRhs instanceof MetaPatTerm(var rRef) && lhsRef == rRef) yield lhsRef.type();
@@ -468,11 +471,11 @@
       }
       // See compareApprox for why we don't compare these
       case FnCall lhs -> null;
-      case CoeTerm(var lType, var lR, var lS) coe -> {
+      case CoeTerm coe -> {
         if (!(preRhs instanceof CoeTerm(var rType, var rR, var rS))) yield null;
-        if (!compare(lR, rR, lr, rl, IntervalTerm.INSTANCE)) yield null;
-        if (!compare(lS, rS, lr, rl, IntervalTerm.INSTANCE)) yield null;
-        yield compare(lType, rType, lr, rl, PrimDef.intervalToType()) ?
+        if (!compare(coe.r(), rR, lr, rl, IntervalTerm.INSTANCE)) yield null;
+        if (!compare(coe.s(), rS, lr, rl, IntervalTerm.INSTANCE)) yield null;
+        yield compare(coe.type(), rType, lr, rl, PrimDef.intervalToType()) ?
           coe.family() : null;
       }
       case ConCall lhs -> switch (preRhs) {
@@ -532,6 +535,7 @@
         yield null;
       }
       case MetaTerm lhs -> solveMeta(lhs, preRhs, lr, rl, null);
+      default -> throw noRules(preLhs);
     };
   }