call: Con

base/src/main/java/org/aya/syntax/core/term/call/Callable.java

@@ -24,7 +24,7 @@ public sealed interface Callable extends Term permits Callable.Common {
   /**
    * Call to a {@link TeleDecl}.
    */
-  sealed interface Tele extends Common permits DataCall, FnCall {
+  sealed interface Tele extends Common permits ConCallLike, DataCall, FnCall {
     @Override @NotNull DefVar<? extends TeleDef, ? extends TeleDecl<?>> ref();
     int ulift();
   }

base/src/main/java/org/aya/syntax/core/term/call/ConCall.java

@@ -0,0 +1,37 @@
+// Copyright (c) 2020-2023 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.call;
+
+import kala.collection.immutable.ImmutableSeq;
+import kala.function.IndexedFunction;
+import org.aya.syntax.concrete.stmt.decl.TeleDecl;
+import org.aya.syntax.core.def.CtorDef;
+import org.aya.syntax.core.def.DataDef;
+import org.aya.syntax.core.term.Term;
+import org.aya.syntax.ref.DefVar;
+import org.aya.util.Arg;
+import org.jetbrains.annotations.NotNull;
+
+public record ConCall(
+  @Override @NotNull ConCall.Head head,
+  @Override @NotNull ImmutableSeq<Arg<Term>> conArgs
+) implements ConCallLike {
+  public @NotNull ConCall update(@NotNull Head head, @NotNull ImmutableSeq<Arg<Term>> conArgs) {
+    return head == head() && conArgs.sameElements(conArgs(), true) ? this : new ConCall(head, conArgs);
+  }
+
+  @Override
+  public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
+    return update(head.descent(x -> f.apply(0, x)), conArgs.map(x -> x.descent(t -> f.apply(0, t))));
+  }
+
+  public ConCall(
+    @NotNull DefVar<DataDef, TeleDecl.DataDecl> dataRef,
+    @NotNull DefVar<CtorDef, TeleDecl.DataCtor> ref,
+    @NotNull ImmutableSeq<Arg<@NotNull Term>> dataArgs,
+    int ulift,
+    @NotNull ImmutableSeq<Arg<@NotNull Term>> conArgs
+  ) {
+    this(new Head(dataRef, ref, ulift, dataArgs), conArgs);
+  }
+}

base/src/main/java/org/aya/syntax/core/term/call/ConCallLike.java

@@ -0,0 +1,67 @@
+// Copyright (c) 2020-2023 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.call;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.syntax.concrete.stmt.decl.TeleDecl;
+import org.aya.syntax.core.def.CtorDef;
+import org.aya.syntax.core.def.DataDef;
+import org.aya.syntax.core.term.Term;
+import org.aya.syntax.ref.DefVar;
+import org.aya.util.Arg;
+import org.jetbrains.annotations.NotNull;
+
+import java.util.function.UnaryOperator;
+
+/**
+ * Terms that behave like a {@link ConCall}, for example:
+ * <ul>
+ *   <li>{@link IntegerTerm} behaves like a {@link ConCall}, in a efficient way</li>
+ *   <li>{@link RuleReducer.Con} behaves like a {@link ConCall}, but it produce a special term</li>
+ *   <li>Of course, {@link ConCall} haves like a {@link ConCall}</li>
+ * </ul>
+ */
+public sealed interface ConCallLike extends Callable.Tele permits ConCall {
+  /**
+   * @param dataArgs the arguments to the data type, NOT the constructor patterns!!
+   *                 They need to be turned implicit when used as arguments.
+   * @see org.aya.tyck.pat.PatternTycker#mischa
+   */
+  record Head(
+    @NotNull DefVar<DataDef, TeleDecl.DataDecl> dataRef,
+    @NotNull DefVar<CtorDef, TeleDecl.DataCtor> ref,
+    int ulift,
+    @NotNull ImmutableSeq<Arg<@NotNull Term>> dataArgs
+  ) {
+    public @NotNull DataCall underlyingDataCall() {
+      return new DataCall(dataRef, ulift, dataArgs);
+    }
+
+    public @NotNull Head descent(@NotNull UnaryOperator<@NotNull Term> f) {
+      var args = dataArgs.map(arg -> arg.descent(f));
+      if (args.sameElements(dataArgs, true)) return this;
+      return new Head(dataRef, ref, ulift, args);
+    }
+  }
+
+  @NotNull ConCallLike.Head head();
+  @NotNull ImmutableSeq<Arg<Term>> conArgs();
+
+  @Override
+  default @NotNull DefVar<CtorDef, TeleDecl.DataCtor> ref() {
+    return head().ref();
+  }
+
+  @Override
+  default @NotNull ImmutableSeq<Arg<@NotNull Term>> args() {
+    return head().dataArgs().view()
+      .map(Arg::implicitify)
+      .concat(conArgs())
+      .toImmutableSeq();
+  }
+
+  @Override
+  default int ulift() {
+    return head().ulift();
+  }
+}

base/src/main/java/org/aya/tyck/tycker/ContextBased.java

@@ -9,7 +9,7 @@
 
 import java.util.function.Supplier;
 
-public sealed interface ContextBased permits AbstractExprTycker {
+public interface ContextBased {
   @NotNull LocalCtx localCtx();
 
   /**

base/src/main/java/org/aya/tyck/tycker/StateBased.java

@@ -25,7 +25,7 @@
  * @see #defCall
  * @see #conOwnerSubst(ConCall)
  */
-public sealed interface StateBased permits AbstractExprTycker {
+public interface StateBased {
   @NotNull TyckState state();
 
   @NotNull Term whnf(@NotNull Term term);

base/src/test/java/org/aya/syntax/core/BindTest.java

@@ -1,17 +1,12 @@
 package org.aya.syntax.core;
 
-import kala.collection.mutable.MutableMap;
-import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.core.term.AppTerm;
 import org.aya.syntax.core.term.FreeTerm;
 import org.aya.syntax.core.term.LamTerm;
 import org.aya.syntax.core.term.LocalTerm;
-import org.aya.syntax.ref.LocalCtx;
 import org.aya.syntax.ref.LocalVar;
-import org.aya.tyck.ExprTycker;
 import org.aya.util.Arg;
 import org.aya.util.error.SourcePos;
-import org.aya.util.error.WithPos;
 import org.junit.jupiter.api.Test;
 
 import static org.junit.jupiter.api.Assertions.assertEquals;