fn-shape: so is IntegerTerm

aya-prover · Dec 11, 2023 · 4e1d5c4 · 4e1d5c4
1 parent 3968376
commit 4e1d5c4
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/base/src/main/java/org/aya/core/term/IntegerOps.java b/base/src/main/java/org/aya/core/term/IntegerOps.java
@@ -17,6 +17,11 @@
 
 import java.io.Serializable;
 
+/**
+ * IntegerOps acts like a DefVar with special reduce rule. So it is not a {@link Term}.
+ *
+ * @see RuleReducer
+ */
 public sealed interface IntegerOps<Core extends Def, Concrete extends TeleDecl<?>>
   extends Shaped.Applicable<Term, Core, Concrete> {
   @Override default @NotNull Term type() {

diff --git a/base/src/main/java/org/aya/core/term/IntegerTerm.java b/base/src/main/java/org/aya/core/term/IntegerTerm.java
@@ -47,12 +47,8 @@ public record IntegerTerm(
     return ImmutableSeq.of(new Arg<>(new IntegerTerm(repr - 1, recognition, type), ctorTele.first().explicit()));
   }
 
-  public IntegerTerm update(DataCall type) {
-    return type == type() ? this : new IntegerTerm(repr, recognition, type);
-  }
-
   @Override public @NotNull IntegerTerm descent(@NotNull UnaryOperator<Term> f, @NotNull UnaryOperator<Pat> g) {
-    return update((DataCall) f.apply(type));
+    return this;
   }
 
   @Override
@@ -62,8 +58,7 @@ public IntegerTerm update(DataCall type) {
   }
 
   @Override public @NotNull Term makeZero(@NotNull CtorDef zero) {
-    return new RuleReducer.Con(new IntegerOps.ConRule(zero.ref, recognition, type),
-      0, ImmutableSeq.empty(), ImmutableSeq.empty());
+    return map(x -> 0);
   }
 
   @Override public @NotNull Term makeSuc(@NotNull CtorDef suc, @NotNull Arg<Term> term) {