matcher: use Java language features

aya-prover · Oct 20, 2023 · f48c65e · f48c65e
1 parent ad0e18b
commit f48c65e
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 29 deletions.
diff --git a/base/src/main/java/org/aya/core/repr/AyaShape.java b/base/src/main/java/org/aya/core/repr/AyaShape.java
@@ -158,7 +158,7 @@ public void bonjour(@NotNull GenericDef def, @NotNull ShapeRecognition shape) {
     /** Discovery of shaped literals */
     public void bonjour(@NotNull GenericDef def) {
       AyaShape.LITERAL_SHAPES.view()
-        .flatMap(shape -> shape.match(def))
+        .flatMap(shape -> new ShapeMatcher().match(shape, def))
         .forEach(shape -> bonjour(def, shape));
     }
 

diff --git a/base/src/main/java/org/aya/core/repr/ShapeMatcher.java b/base/src/main/java/org/aya/core/repr/ShapeMatcher.java
@@ -49,28 +49,26 @@ public ShapeMatcher(@NotNull ImmutableMap<DefVar<?, ?>, ShapeRecognition> discov
   }
 
   public Option<ShapeRecognition> match(@NotNull AyaShape shape, @NotNull GenericDef def) {
-    if (matchDecl(shape.codeShape(), def)) {
+    if (matchDecl(new MatchDecl(shape.codeShape(), def))) {
       return Option.some(new ShapeRecognition(shape, ImmutableMap.from(captures)));
     }
 
     return Option.none();
   }
 
-  private boolean matchDecl(@NotNull CodeShape shape, @NotNull GenericDef def) {
-    if (shape instanceof CodeShape.Named named) {
-      names.append(named.name());
-      return matchDecl(named.shape(), def);
-    }
-
-    if (shape instanceof CodeShape.DataShape dataShape && def instanceof DataDef data) {
-      return matchData(dataShape, data);
-    }
-
-    if (shape instanceof CodeShape.FnShape fnShape && def instanceof FnDef fn) {
-      return matchFn(fnShape, fn);
-    }
+  record MatchDecl(@NotNull CodeShape shape, @NotNull GenericDef def) {
+  }
 
-    return false;
+  private boolean matchDecl(@NotNull MatchDecl params) {
+    return switch (params) {
+      case MatchDecl(CodeShape.Named named, var def) -> {
+        names.append(named.name());
+        yield matchDecl(new MatchDecl(named.shape(), def));
+      }
+      case MatchDecl(CodeShape.DataShape dataShape, DataDef data) -> matchData(dataShape, data);
+      case MatchDecl(CodeShape.FnShape fnShape, FnDef fn) -> matchFn(fnShape, fn);
+      default -> false;
+    };
   }
 
   private boolean matchFn(@NotNull CodeShape.FnShape shape, @NotNull FnDef def) {
@@ -82,13 +80,11 @@ private boolean matchFn(@NotNull CodeShape.FnShape shape, @NotNull FnDef def) {
     if (!teleResult) return false;
 
     // match body
-    return shape.body().fold(
-      termShape -> {
+    return shape.body().fold(termShape -> {
         if (!def.body.isLeft()) return false;
         var term = def.body.getLeftValue();
         return matchInside(def.ref, names, () -> matchTerm(termShape, term));
-      },
-      clauseShapes -> {
+      }, clauseShapes -> {
         if (!def.body.isRight()) return false;
         var clauses = def.body.getRightValue();
         var mode = def.modifiers.contains(Modifier.Overlap) ? MatchMode.Sub : MatchMode.Eq;
@@ -123,15 +119,9 @@ private boolean matchPat(@NotNull PatShape shape, @NotNull Pat pat) {
           throw new InternalException("Invalid name: " + shapedCtor.name());
         }
 
-        var recognition = discovered.getOrNull(defVar);
-        if (recognition == null) {
-          throw new InternalException("Not a shaped data");
-        }
-
-        var realShapedCtor = recognition.captures().getOrNull(shapedCtor.id());
-        if (realShapedCtor == null) {
-          throw new InternalException("Invalid moment id: " + shapedCtor.id() + " in recognition" + recognition);
-        }
+        var recognition = discovered.getOrThrow(defVar, () -> new InternalException("Not a shaped data"));
+        var realShapedCtor = recognition.captures().getOrThrow(shapedCtor.id(), () ->
+          new InternalException("Invalid moment id: " + shapedCtor.id() + " in recognition" + recognition));
 
         matched = realShapedCtor == ctor.ref();
       }