matcher: delete def

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

Hide file tree

Showing 2 changed files with 2 additions and 16 deletions.
diff --git a/base/src/main/java/org/aya/core/repr/ShapeMatcher.java b/base/src/main/java/org/aya/core/repr/ShapeMatcher.java
@@ -32,7 +32,6 @@
  * @author kiva
  */
 public record ShapeMatcher(
-  @NotNull MutableLinkedList<DefVar<? extends Def, ? extends TeleDecl<?>>> def,
   @NotNull MutableMap<CodeShape.MomentId, DefVar<?, ?>> captures,
   @NotNull MutableMap<AnyVar, AnyVar> teleSubst,
   // --------
@@ -42,11 +41,11 @@ public record ShapeMatcher(
 ) {
 
   public ShapeMatcher() {
-    this(MutableLinkedList.create(), MutableMap.create(), MutableMap.create(), ImmutableMap.empty(), MutableList.create(), MutableMap.create());
+    this(MutableMap.create(), MutableMap.create(), ImmutableMap.empty(), MutableList.create(), MutableMap.create());
   }
 
   public ShapeMatcher(@NotNull ImmutableMap<DefVar<?, ?>, ShapeRecognition> discovered) {
-    this(MutableLinkedList.create(), MutableMap.create(), MutableMap.create(), discovered, MutableList.create(), MutableMap.create());
+    this(MutableMap.create(), MutableMap.create(), discovered, MutableList.create(), MutableMap.create());
   }
 
   public Option<ShapeRecognition> match(@NotNull AyaShape shape, @NotNull GenericDef def) {
@@ -211,15 +210,6 @@ private boolean matchTerm(@NotNull TermShape shape, @NotNull Term term) {
       result = callable.ref();
     }
 
-    if (shape instanceof TermShape.TeleRef ref && term instanceof RefTerm refTerm) {
-      var superLevel = def.getOrNull(ref.superLevel());
-      if (superLevel == null) return false;
-      var tele = Def.defTele(superLevel).getOrNull(ref.nth());
-      if (tele == null) return false;
-      var teleVar = teleSubst.getOrNull(tele.ref());
-      return teleVar == refTerm.var() || tele.ref() == refTerm.var();
-    }
-
     if (shape instanceof TermShape.Sort sort && term instanceof SortTerm sortTerm) {
       // kind is null -> any sort
       if (sort.kind() == null) return true;
@@ -283,9 +273,7 @@ private boolean matchInside(@NotNull DefVar<? extends Def, ? extends TeleDecl<?>
 
     bind(names, defVar);
 
-    def.push(defVar);
     var result = matcher.getAsBoolean();
-    def.pop();
 
     resolved.clear();
     resolved.putAll(snapshot);

diff --git a/base/src/main/java/org/aya/core/repr/TermShape.java b/base/src/main/java/org/aya/core/repr/TermShape.java
@@ -16,8 +16,6 @@ enum Any implements TermShape {
     INSTANCE;
   }
 
-  record TeleRef(int superLevel, int nth) implements TermShape {}
-
   /**
    * The shape to Sort term, I am not very work well at type theory, so improve this feel free!
    *
-Original file line number
+Diff line change
@@ Expand Up / @@ -16,8 +16,6 @@ enum Any implements TermShape { @@
         INSTANCE;
       }
-      record TeleRef(int superLevel, int nth) implements TermShape {}
       /**
        * The shape to Sort term, I am not very work well at type theory, so improve this feel free!
        *
@@ Expand Down @@