pat: code cleanup

aya-prover · Jan 4, 2025 · 050171c · 050171c
1 parent 757f7a1
commit 050171c
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 28 deletions.
diff --git a/syntax/src/main/java/org/aya/syntax/core/pat/PatToTerm.java b/syntax/src/main/java/org/aya/syntax/core/pat/PatToTerm.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.syntax.core.pat;
 
@@ -12,32 +12,23 @@
 import org.aya.util.error.Panic;
 import org.jetbrains.annotations.NotNull;
 
-import java.util.function.Consumer;
 import java.util.function.Function;
 
 public interface PatToTerm {
   static @NotNull Term visit(@NotNull Pat pat) {
-    return new Unary(_ -> { }).apply(pat);
-  }
-  record Unary(@NotNull Consumer<Pat.Bind> freshCallback) implements Function<Pat, Term> {
-    @Override public Term apply(Pat pat) {
-      return switch (pat) {
-        case Pat.Misc misc -> switch (misc) {
-          // We expect this to be never used, but this needs to not panic because
-          // absurd clauses need to finish type checking
-          case Absurd -> SortTerm.Type0;
-          case UntypedBind -> Panic.unreachable();
-        };
-        case Pat.Bind bind -> {
-          freshCallback.accept(bind);
-          yield new FreeTerm(bind.bind());
-        }
-        case Pat.Con con -> new ConCall(con.head(), con.args().map(this));
-        case Pat.Tuple(var l, var r) -> new TupTerm(apply(l), apply(r));
-        case Pat.Meta meta -> new MetaPatTerm(meta);
-        case Pat.ShapedInt si -> si.toTerm();
+    return switch (pat) {
+      case Pat.Misc misc -> switch (misc) {
+        // We expect this to be never used, but this needs to not panic because
+        // absurd clauses need to finish type checking
+        case Absurd -> SortTerm.Type0;
+        case UntypedBind -> Panic.unreachable();
       };
-    }
+      case Pat.Bind bind -> new FreeTerm(bind.bind());
+      case Pat.Con con -> new ConCall(con.head(), con.args().map(PatToTerm::visit));
+      case Pat.Tuple(var l, var r) -> new TupTerm(visit(l), visit(r));
+      case Pat.Meta meta -> new MetaPatTerm(meta);
+      case Pat.ShapedInt si -> si.toTerm();
+    };
   }
 
   record Monadic(@NotNull LocalCtx ctx) implements Function<Pat, ImmutableSeq<Term>> {
@@ -69,11 +60,10 @@ record Monadic(@NotNull LocalCtx ctx) implements Function<Pat, ImmutableSeq<Term
           ctx.put(bind.bind(), bind.type());
           yield ImmutableSeq.of(new FreeTerm(bind.bind()));
         }
-        case Pat.Con con when con.ref().hasEq() ->
-          list(con.args().view().dropLast(1), BOUNDARIES)
-            .map(args -> {
-              return new ConCall(con.head(), args);
-            });
+        case Pat.Con con when con.ref().hasEq() -> list(con.args().view().dropLast(1), BOUNDARIES)
+          .map(args -> {
+            return new ConCall(con.head(), args);
+          });
         case Pat.Con con -> list(con.args().view())
           .map(args -> {
             return new ConCall(con.head(), args);

diff --git a/syntax/src/main/java/org/aya/syntax/core/term/LamTerm.java b/syntax/src/main/java/org/aya/syntax/core/term/LamTerm.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.syntax.core.term;