normalize: MemberCall extends BetaRedex

aya-prover · Jul 8, 2024 · a1247a7 · a1247a7
1 parent 8e33f0c
commit a1247a7
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 14 deletions.
diff --git a/base/src/main/java/org/aya/normalize/Normalizer.java b/base/src/main/java/org/aya/normalize/Normalizer.java
@@ -82,11 +82,6 @@ case FnCall(var fn, int ulift, var args) -> switch (fn) {
           ? apply(fnRule.toFnCall())
           : reduceRule;
       }
-      case MemberCall memberCall -> {
-        var result = MemberCall.make(memberCall);
-        if (result != memberCall) yield apply(result);
-        yield defaultValue;
-      }
       case ConCall(var head, _) when !head.ref().hasEq() -> defaultValue;
       case ConCall call when call.conArgs().getLast() instanceof DimTerm dim ->
         call.head().ref().equality(call.args(), dim == DimTerm.I0);

diff --git a/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java b/syntax/src/main/java/org/aya/syntax/core/term/call/MemberCall.java
@@ -8,14 +8,15 @@
 import org.aya.syntax.core.term.ClassCastTerm;
 import org.aya.syntax.core.term.NewTerm;
 import org.aya.syntax.core.term.Term;
+import org.aya.syntax.core.term.marker.BetaRedex;
 import org.jetbrains.annotations.NotNull;
 
 public record MemberCall(
   @NotNull Term of,
   @Override @NotNull MemberDefLike ref,
   @Override int ulift,
   @Override @NotNull ImmutableSeq<@NotNull Term> args
-) implements Callable.Tele {
+) implements Callable.Tele, BetaRedex {
   private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
     return clazz == of && newArgs.sameElements(args, true) ? this
       : new MemberCall(clazz, ref, ulift, newArgs);
@@ -34,23 +35,23 @@ private MemberCall update(Term clazz, ImmutableSeq<Term> newArgs) {
   ) {
     var impl = typeOfOf.get(ref);
     if (impl != null) return impl.apply(of);
-    return make(new MemberCall(of, ref, ulift, args));
+    return new MemberCall(of, ref, ulift, args).make();
   }
 
-  public static @NotNull Term make(@NotNull MemberCall call) {
-    return switch (call.of()) {
+  public @NotNull Term make() {
+    return switch (of()) {
       case NewTerm neu -> {
-        var impl = neu.inner().get(call.ref);
+        var impl = neu.inner().get(ref);
         assert impl != null;    // NewTerm is always fully applied
         yield impl.apply(neu);
       }
       case ClassCastTerm cast -> {
-        var impl = cast.get(call.ref);
+        var impl = cast.get(ref);
         if (impl != null) yield impl.apply(cast);
         // no impl, try inner
-        yield call.update(cast.subterm(), call.args);
+        yield update(cast.subterm(), args);
       }
-      default -> call;
+      default -> this;
     };
   }
 }
diff --git a/syntax/src/main/java/org/aya/syntax/core/term/marker/BetaRedex.java b/syntax/src/main/java/org/aya/syntax/core/term/marker/BetaRedex.java
@@ -5,9 +5,10 @@
 import org.aya.syntax.core.term.AppTerm;
 import org.aya.syntax.core.term.ProjTerm;
 import org.aya.syntax.core.term.Term;
+import org.aya.syntax.core.term.call.MemberCall;
 import org.aya.syntax.core.term.xtt.PAppTerm;
 import org.jetbrains.annotations.NotNull;
 
-public sealed interface BetaRedex extends Term permits AppTerm, PAppTerm, ProjTerm {
+public sealed interface BetaRedex extends Term permits AppTerm, ProjTerm, MemberCall, PAppTerm {
   @NotNull Term make();
 }