review: cosmetics changes

aya-prover · Jan 4, 2025 · 33065af · 33065af
1 parent 148a827
commit 33065af
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 17 deletions.
diff --git a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
@@ -69,7 +69,7 @@ public record LhsResult(
     boolean hasError
   ) {
     public @NotNull Term instType() {
-      // I guess we need not to inline this term even we did before. The [paramSubst] is already inlined.
+      // We need not to inline this term even we did before. The [paramSubst] is already inlined.
       return newSignature.result().instTele(paramSubst.view().map(Jdg::wellTyped));
     }
 

diff --git a/base/src/main/java/org/aya/tyck/pat/PatternTycker.java b/base/src/main/java/org/aya/tyck/pat/PatternTycker.java
@@ -13,7 +13,6 @@
 import org.aya.normalize.Normalizer;
 import org.aya.syntax.compile.JitCon;
 import org.aya.syntax.compile.JitData;
-import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.concrete.Pattern;
 import org.aya.syntax.concrete.stmt.decl.DataDecl;
 import org.aya.syntax.core.Jdg;
@@ -33,7 +32,6 @@
 import org.aya.tyck.error.PatternProblem;
 import org.aya.tyck.pat.iter.ConstPusheen;
 import org.aya.tyck.pat.iter.PatternIterator;
-import org.aya.tyck.pat.iter.PusheenIterator;
 import org.aya.tyck.pat.iter.SignatureIterator;
 import org.aya.tyck.tycker.Problematic;
 import org.aya.tyck.tycker.Stateful;
@@ -106,11 +104,7 @@ public record TyckResult(
     @NotNull ImmutableSeq<Jdg> paramSubst,
     @NotNull LocalLet asSubst,
     boolean hasError
-  ) {
-    public @NotNull SeqView<Term> paramSubstObj() {
-      return paramSubst.view().map(Jdg::wellTyped);
-    }
-  }
+  ) { }
 
   /**
    * Tyck a {@param type} against {@param type}
@@ -298,7 +292,7 @@ public enum Kind {
 
       if (!currentPat.explicit() && !allowImplicit) {
         foundError(new PatternProblem.ImplicitDisallowed(currentPat.term()));
-        // TODO: return or continue tyck?
+        return done(wellTyped);
       }
 
       // find the next appropriate parameter
@@ -342,9 +336,7 @@ public enum Kind {
 
   private final Closer CLOSER = new Closer();
   private class Closer implements AutoCloseable {
-    @Override public void close() {
-      consumeParam();
-    }
+    @Override public void close() { consumeParam(); }
   }
 
   /**

diff --git a/tools-kala/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java b/tools-kala/src/main/java/org/aya/util/tyck/pat/ClassifierUtil.java
@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 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.tyck.pat;
 
@@ -22,8 +22,7 @@ public interface ClassifierUtil<Subst, Term, Param, Pat> {
     @NotNull ImmutableSeq<Indexed<Pat>> clauses, int fuel
   );
 
-  @ApiStatus.Internal default @NotNull ImmutableSeq<PatClass<ImmutableSeq<Term>>>
-  classifyN(
+  @ApiStatus.Internal default @NotNull ImmutableSeq<PatClass<ImmutableSeq<Term>>> classifyN(
     @NotNull Subst subst, @NotNull SeqView<Param> telescope,
     @NotNull ImmutableSeq<Indexed<SeqView<Pat>>> clauses, int fuel
   ) {
@@ -41,8 +40,7 @@ public interface ClassifierUtil<Subst, Term, Param, Pat> {
         .map(args -> args.map(ls -> ls.prepended(subclauses.term()))));
   }
 
-  @ApiStatus.Internal default @NotNull ImmutableSeq<PatClass<Pair<Term, Term>>>
-  classify2(
+  @ApiStatus.Internal default @NotNull ImmutableSeq<PatClass<Pair<Term, Term>>> classify2(
     @NotNull Subst subst, @NotNull Param tele1, @NotNull Function<Term, Param> tele2,
     @NotNull ImmutableSeq<Indexed<Pair<Pat, Pat>>> clauses, int fuel
   ) {