review: cosmetics changes

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

Hide file tree

Showing 9 changed files with 27 additions and 83 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/base/src/main/java/org/aya/tyck/pat/iter/ConstPusheen.java b/base/src/main/java/org/aya/tyck/pat/iter/ConstPusheen.java
@@ -6,23 +6,8 @@
 import org.jetbrains.annotations.NotNull;
 
 public record ConstPusheen<T, R>(@NotNull R body) implements Pusheenable<T, R> {
-  @Override
-  public @NotNull T peek() {
-    return Panic.unreachable();
-  }
-
-  @Override
-  public R body() {
-    return body;
-  }
-
-  @Override
-  public boolean hasNext() {
-    return false;
-  }
-
-  @Override
-  public T next() {
-    return Panic.unreachable();
-  }
+  @Override public @NotNull T peek() { return Panic.unreachable(); }
+  @Override public @NotNull R body() { return body; }
+  @Override public boolean hasNext() { return false; }
+  @Override public T next() { return Panic.unreachable(); }
 }
diff --git a/base/src/main/java/org/aya/tyck/pat/iter/LambdaPusheen.java b/base/src/main/java/org/aya/tyck/pat/iter/LambdaPusheen.java
@@ -17,27 +17,18 @@ public LambdaPusheen(@NotNull WithPos<Expr> body) {
     this.body = body;
   }
 
-  @Override
-  public @NotNull Arg<WithPos<Pattern>> peek() {
+  @Override public @NotNull Arg<WithPos<Pattern>> peek() {
     if (peek != null) return peek;
 
     var bind = ((Expr.Lambda) body.data()).ref();
     peek = Arg.ofExplicitly(new WithPos<>(bind.definition(), new Pattern.Bind(bind)));
     return peek;
   }
 
-  @Override
-  public @NotNull WithPos<Expr> body() {
-    return body;
-  }
-
-  @Override
-  public boolean hasNext() {
-    return body.data() instanceof Expr.Lambda;
-  }
+  @Override public @NotNull WithPos<Expr> body() { return body; }
+  @Override public boolean hasNext() { return body.data() instanceof Expr.Lambda; }
 
-  @Override
-  public Arg<WithPos<Pattern>> next() {
+  @Override public Arg<WithPos<Pattern>> next() {
     if (peek == null) peek();
     body = ((Expr.Lambda) body.data()).body();
 

diff --git a/base/src/main/java/org/aya/tyck/pat/iter/PiPusheen.java b/base/src/main/java/org/aya/tyck/pat/iter/PiPusheen.java
@@ -3,12 +3,10 @@
 package org.aya.tyck.pat.iter;
 
 import kala.collection.immutable.ImmutableSeq;
-import org.aya.generic.term.DTKind;
 import org.aya.syntax.core.term.DepTypeTerm;
 import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.Term;
 import org.jetbrains.annotations.NotNull;
-import org.jetbrains.annotations.Nullable;
 
 public final class PiPusheen implements Pusheenable<Param, @NotNull Term> {
   private final @NotNull ImmutableSeq<Param> unpi;
@@ -22,23 +20,13 @@ public PiPusheen(@NotNull DepTypeTerm.UnpiRaw unpi) {
     this.result = unpi.body();
   }
 
-  @Override
-  public @NotNull Param peek() {
-    return unpi.get(pusheenIdx);
-  }
-
-  @Override
-  public @NotNull Term body() {
+  @Override public @NotNull Param peek() { return unpi.get(pusheenIdx); }
+  @Override public @NotNull Term body() {
     return DepTypeTerm.makePi(unpi.sliceView(pusheenIdx, unpi.size()).map(Param::type), result);
   }
 
-  @Override
-  public boolean hasNext() {
-    return pusheenIdx < unpi.size();
-  }
-
-  @Override
-  public @NotNull Param next() {
+  @Override public boolean hasNext() { return pusheenIdx < unpi.size(); }
+  @Override public @NotNull Param next() {
     var result = peek();
     pusheenIdx += 1;
     return result;

diff --git a/base/src/main/java/org/aya/tyck/pat/iter/PusheenIterator.java b/base/src/main/java/org/aya/tyck/pat/iter/PusheenIterator.java
@@ -19,13 +19,11 @@ public PusheenIterator(Iterator<T> iter, @NotNull Pusheenable<T, R> cat) {
     this.cat = cat;
   }
 
-  @Override
-  public boolean hasNext() {
+  @Override public boolean hasNext() {
     return peek != null || iter.hasNext() || cat.hasNext();
   }
 
-  @Override
-  public @NotNull T peek() {
+  @Override public @NotNull T peek() {
     if (peek != null) return peek;
     if (iter.hasNext()) return peek = postDoPeek(iter.next());
 
@@ -39,8 +37,7 @@ public boolean hasNext() {
     return peeked;
   }
 
-  @Override
-  public T next() {
+  @Override public T next() {
     if (peek == null) peek();
 
     if (fromPusheen) {
@@ -53,13 +50,8 @@ public T next() {
     return result;
   }
 
-  @Override
-  public @NotNull Pusheenable<T, R> body() {
-    return cat;
-  }
+  @Override public @NotNull Pusheenable<T, R> body() { return cat; }
 
   ///  Whether the last element comes from {@link #cat}
-  public boolean isFromPusheen() {
-    return fromPusheen;
-  }
+  public boolean isFromPusheen() { return fromPusheen; }
 }
diff --git a/base/src/main/java/org/aya/tyck/pat/iter/Pusheenable.java b/base/src/main/java/org/aya/tyck/pat/iter/Pusheenable.java
@@ -10,6 +10,5 @@
 /// A Pusheenable is a functional list.
 public interface Pusheenable<T, R> extends Iterator<T> {
   @NotNull T peek();
-
   @NotNull R body();
 }
diff --git a/base/src/main/java/org/aya/tyck/pat/iter/SignatureIterator.java b/base/src/main/java/org/aya/tyck/pat/iter/SignatureIterator.java
@@ -22,6 +22,7 @@ public class SignatureIterator extends PusheenIterator<Param, Term> {
       return new ConstPusheen<>(unpi.body());
     } else {
       return new PiPusheen(unpi);
+
     }
   }
 
@@ -63,13 +64,11 @@ public SignatureIterator(Iterator<Param> iter, @NotNull Pusheenable<Param, Term>
     this.elims = elims;
   }
 
-  @Override
-  public @NotNull Pusheenable<Param, Term> body() {
+  @Override public @NotNull Pusheenable<Param, Term> body() {
     return Objects.requireNonNull(super.body());
   }
 
-  @Override
-  public Param next() {
+  @Override public Param next() {
     var theNext = super.next();
     consumed.append(theNext);
     return theNext;

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
   ) {