REFACTOR: replace visitor with pattern matching

Fix typo for accept

Put @NotNull annotations back and replace Boolean with boolean

Delete some redundant lines and comments

Delete doAccept functions

Delete BiVisitor and relevant accept function usage

Delete BiVisitor and relevant accept function Declaration

Delete comments

Change usage of previous visitxxx to visit function

Add implementation of visit with pattern matching, try to match multiple pattern in one case but seems not supported yet

Add new visit function declaration

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

@@ -57,11 +57,6 @@ record Fn(
     @Override public <P, R> R doAccept(@NotNull Visitor<P, R> visitor, P p) {
       return visitor.visitFnCall(this, p);
     }
-
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitFnCall(this, p, q);
-    }
-
   }
 
   record Prim(
@@ -72,11 +67,6 @@ record Prim(
     @Override public <P, R> R doAccept(@NotNull Visitor<P, R> visitor, P p) {
       return visitor.visitPrimCall(this, p);
     }
-
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitPrimCall(this, p, q);
-    }
-
   }
 
   record Data(
@@ -88,10 +78,6 @@ record Data(
       return visitor.visitDataCall(this, p);
     }
 
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitDataCall(this, p, q);
-    }
-
     public @NotNull ConHead conHead(@NotNull DefVar<CtorDef, Decl.DataCtor> ctorRef) {
       return new ConHead(ref, ctorRef, sortArgs, args);
     }
@@ -108,11 +94,6 @@ record Struct(
     @Override public <P, R> R doAccept(@NotNull Visitor<P, R> visitor, P p) {
       return visitor.visitStructCall(this, p);
     }
-
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitStructCall(this, p, q);
-    }
-
   }
 
   record ConHead(
@@ -152,14 +133,9 @@ public Con(
       return visitor.visitConCall(this, p);
     }
 
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitConCall(this, p, q);
-    }
-
     @Override public @NotNull ImmutableSeq<Arg<@NotNull Term>> args() {
       return head.dataArgs.view().concat(conArgs).toImmutableSeq();
     }
-
   }
 
   /**
@@ -182,10 +158,6 @@ public Hole(@NotNull HoleVar<Meta> var, @NotNull ImmutableSeq<@NotNull Arg<@NotN
       return visitor.visitHole(this, p);
     }
 
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitHole(this, p, q);
-    }
-
     @Override public @NotNull ImmutableSeq<@NotNull Sort> sortArgs() {
       return ImmutableSeq.empty();
     }
@@ -205,13 +177,8 @@ record Access(
       return visitor.visitAccess(this, p);
     }
 
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitAccess(this, p, q);
-    }
-
     @Override public @NotNull ImmutableSeq<@NotNull Arg<Term>> args() {
       return structArgs.concat(fieldArgs);
     }
-
   }
 }

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

@@ -32,19 +32,11 @@ record Proj(@NotNull Term of, int ix) implements ElimTerm {
     @Override public <P, R> R doAccept(@NotNull Visitor<P, R> visitor, P p) {
       return visitor.visitProj(this, p);
     }
-
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitProj(this, p, q);
-    }
   }
 
   record App(@NotNull Term of, @NotNull Arg<@NotNull Term> arg) implements ElimTerm {
     @Override public <P, R> R doAccept(@NotNull Visitor<P, R> visitor, P p) {
       return visitor.visitApp(this, p);
     }
-
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitApp(this, p, q);
-    }
   }
 }

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

@@ -31,10 +31,6 @@ public ErrorTerm(@NotNull Doc description, boolean isReallyError) {
     return visitor.visitError(this, p);
   }
 
-  @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-    return visitor.visitError(this, p, q);
-  }
-
   public static @NotNull ErrorTerm typeOf(@NotNull Term origin) {
     return typeOf((AyaDocile) origin.freezeHoles(null));
   }

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

@@ -23,10 +23,6 @@ record Pi(@NotNull Term.Param param, @NotNull Term body) implements FormTerm {
       return visitor.visitPi(this, p);
     }
 
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitPi(this, p, q);
-    }
-
     public @NotNull Term substBody(@NotNull Term term) {
       return body.subst(param.ref(), term);
     }
@@ -53,10 +49,6 @@ record Sigma(@NotNull ImmutableSeq<@NotNull Param> params) implements FormTerm {
     @Override public <P, R> R doAccept(@NotNull Visitor<P, R> visitor, P p) {
       return visitor.visitSigma(this, p);
     }
-
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitSigma(this, p, q);
-    }
   }
 
   /**
@@ -70,8 +62,5 @@ record Univ(@NotNull Sort sort) implements FormTerm {
       return visitor.visitUniv(this, p);
     }
 
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitUniv(this, p, q);
-    }
   }
 }

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

@@ -24,10 +24,6 @@ record Lambda(@NotNull Term.Param param, @NotNull Term body) implements IntroTer
       return visitor.visitLam(this, p);
     }
 
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitLam(this, p, q);
-    }
-
     public static @NotNull Term make(@NotNull SeqLike<@NotNull Param> telescope, @NotNull Term body) {
       return telescope.view().foldRight(body, Lambda::new);
     }
@@ -43,10 +39,6 @@ record New(
     @Override public <P, R> R doAccept(@NotNull Visitor<P, R> visitor, P p) {
       return visitor.visitNew(this, p);
     }
-
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitNew(this, p, q);
-    }
   }
 
   /**
@@ -56,10 +48,5 @@ record Tuple(@NotNull ImmutableSeq<Term> items) implements IntroTerm {
     @Override public <P, R> R doAccept(@NotNull Visitor<P, R> visitor, P p) {
       return visitor.visitTup(this, p);
     }
-
-    @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-      return visitor.visitTup(this, p, q);
-    }
   }
-
 }

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

@@ -12,8 +12,4 @@ public record RefTerm(@NotNull LocalVar var, @NotNull Term type) implements Term
   @Override public <P, R> R doAccept(@NotNull Visitor<P, R> visitor, P p) {
     return visitor.visitRef(this, p);
   }
-
-  @Override public <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-    return visitor.visitRef(this, p, q);
-  }
 }

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

@@ -40,19 +40,14 @@
  */
 public sealed interface Term extends CoreTerm permits CallTerm, ElimTerm, FormTerm, IntroTerm, RefTerm, ErrorTerm {
   <P, R> R doAccept(@NotNull Visitor<P, R> visitor, P p);
-  <P, Q, R> R doAccept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q);
+
   default <P, R> R accept(@NotNull Visitor<P, R> visitor, P p) {
     visitor.traceEntrance(this, p);
     var ret = doAccept(visitor, p);
     visitor.traceExit(ret);
     return ret;
   }
-  default <P, Q, R> R accept(@NotNull BiVisitor<P, Q, R> visitor, P p, Q q) {
-    visitor.traceEntrance(this, p, q);
-    var ret = doAccept(visitor, p, q);
-    visitor.traceExit(ret);
-    return ret;
-  }
+
   @Override default @Nullable Pat toPat() {
     return accept(TermToPat.INSTANCE, Unit.unit());
   }
@@ -133,30 +128,6 @@ default void traceExit(R r) {
     R visitError(@NotNull ErrorTerm term, P p);
   }
 
-  interface BiVisitor<P, Q, R> {
-    default void traceEntrance(@NotNull Term term, P p, Q q) {
-    }
-    default void traceExit(R r) {
-    }
-    R visitRef(@NotNull RefTerm term, P p, Q q);
-    R visitLam(@NotNull IntroTerm.Lambda term, P p, Q q);
-    R visitPi(@NotNull FormTerm.Pi term, P p, Q q);
-    R visitSigma(@NotNull FormTerm.Sigma term, P p, Q q);
-    R visitUniv(@NotNull FormTerm.Univ term, P p, Q q);
-    R visitApp(@NotNull ElimTerm.App term, P p, Q q);
-    R visitFnCall(CallTerm.@NotNull Fn fnCall, P p, Q q);
-    R visitDataCall(CallTerm.@NotNull Data dataCall, P p, Q q);
-    R visitConCall(CallTerm.@NotNull Con conCall, P p, Q q);
-    R visitStructCall(CallTerm.@NotNull Struct structCall, P p, Q q);
-    R visitPrimCall(@NotNull CallTerm.Prim prim, P p, Q q);
-    R visitTup(@NotNull IntroTerm.Tuple term, P p, Q q);
-    R visitNew(@NotNull IntroTerm.New newTerm, P p, Q q);
-    R visitProj(@NotNull ElimTerm.Proj term, P p, Q q);
-    R visitAccess(@NotNull CallTerm.Access term, P p, Q q);
-    R visitHole(@NotNull CallTerm.Hole term, P p, Q q);
-    R visitError(@NotNull ErrorTerm term, P p, Q q);
-  }
-
   /**
    * @author re-xyr
    */