misc: refactorings

aya-prover · Dec 13, 2023 · 01ce520 · 01ce520
1 parent 90303ec
commit 01ce520
Show file tree

Hide file tree

Showing 5 changed files with 8 additions and 16 deletions.
diff --git a/base/src/main/java/org/aya/core/pat/PatUnify.java b/base/src/main/java/org/aya/core/pat/PatUnify.java
@@ -84,7 +84,7 @@ private void visitAs(@NotNull LocalVar as, Pat rhs) {
 
   private void reportError(@NotNull Pat lhs, @NotNull Pat pat) {
     var doc = Doc.sep(lhs.toDoc(AyaPrettierOptions.debug()), Doc.plain("and"), pat.toDoc(AyaPrettierOptions.debug()));
-    throw new InternalException(doc.debugRender() + " are patterns of different types!");
+    throw new InternalException(STR."\{doc.debugRender()} are patterns of different types!");
   }
 
   private static void unifyPat(Pat lhs, Pat rhs, Subst lhsSubst, Subst rhsSubst, LocalCtx ctx) {

diff --git a/base/src/main/java/org/aya/core/term/Term.java b/base/src/main/java/org/aya/core/term/Term.java
@@ -19,7 +19,6 @@
 import org.aya.pretty.doc.Doc;
 import org.aya.ref.AnyVar;
 import org.aya.ref.LocalVar;
-import org.aya.tyck.env.LocalCtx;
 import org.aya.tyck.tycker.TyckState;
 import org.aya.tyck.unify.Synthesizer;
 import org.aya.util.Arg;
@@ -50,7 +49,7 @@ public sealed interface Term extends AyaDocile, Restr.TermLike<Term>
   permits Callable, CoeTerm, Elimination, Formation, FormulaTerm, HCompTerm, InTerm, MatchTerm, MetaLitTerm, MetaPatTerm, PartialTerm, RefTerm, RefTerm.Field, StableWHNF {
   /**
    * Descending an operation to the term AST. NOTE: Currently we require the operation `f` to preserve:
-   * {@link StructCall}, {@link DataCall}, {@link SortTerm}, {@link org.aya.generic.Shaped.Applicable}.
+   * {@link ClassCall}, {@link DataCall}, {@link SortTerm}, {@link org.aya.generic.Shaped.Applicable}.
    */
   @NotNull Term descent(@NotNull UnaryOperator<Term> f, @NotNull UnaryOperator<Pat> g);
 
@@ -114,13 +113,6 @@ default VarConsumer.ScopeChecker scopeCheck(@NotNull ImmutableSeq<LocalVar> allo
   default @NotNull Term lift(int ulift) {
     return new EndoTerm.Elevator(ulift).apply(this);
   }
-  /**
-   * @return WHNF
-   * @throws NullPointerException if the term is an introduction rule
-   */
-  default @NotNull Term computeType(@NotNull TyckState state, @NotNull LocalCtx ctx) {
-    return new Synthesizer(state, ctx).press(this);
-  }
 
   /**
    * @author re-xyr

diff --git a/base/src/main/java/org/aya/core/visitor/BetaExpander.java b/base/src/main/java/org/aya/core/visitor/BetaExpander.java
@@ -56,24 +56,24 @@ yield switch (partial(partial)) {
       case PartialTerm(var partial, var rhsTy) -> new PartialTerm(partial(partial), rhsTy);
       // TODO[coe]: temporary hack
       case CoeTerm(
-        var ty,
+        _,
         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(_, RefTerm(var r), RefTerm(var s)) when r == s -> identity("x");
       case CoeTerm coe -> {
         var varI = new LamTerm.Param(new LocalVar("i"), true);
         var codom = apply(AppTerm.make(coe.type(), varI.toArg()));
 
         yield switch (codom) {
-          case PathTerm path -> term;
+          case PathTerm _ -> term;
           case PiTerm pi -> pi.coe(coe, varI);
           case SigmaTerm sigma -> sigma.coe(coe, varI);
           case DataCall data when data.args().isEmpty() -> identity(String.valueOf(data.ref()
             .name().chars()
             .filter(Character::isAlphabetic)
             .findFirst()).toLowerCase(Locale.ROOT));
-          case SortTerm type -> identity("A");
+          case SortTerm _ -> identity("A");
           default -> term;
         };
       }

diff --git a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
@@ -256,7 +256,7 @@ private void addReference(@NotNull DefVar<?, ?> defVar) {
               addReference(maybe);
               yield new Pattern.Ctor(bind, maybe);
             }
-            ctx.set(ctx.get().bind(bind.bind(), var -> false));
+            ctx.set(ctx.get().bind(bind.bind(), _ -> false));
             yield bind;
           }
           case Pattern.QualifiedRef qref -> {

diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml
@@ -2,7 +2,7 @@
 # The Version of this project, aka, The Aya Theorem Prover.
 # Remove "-SNAPSHOT" suffix and run gradle publish to release a new version.
 # After that, increase the version number and add "-SNAPSHOT" suffix back for next cycle.
-project = "0.30"
+project = "0.29.4"
 
 # https://openjdk.org/
 java = "21"