term: FnCall

base/src/main/java/module-info.java

@@ -20,4 +20,5 @@
   exports org.aya.syntax.core.term;
   exports org.aya.syntax.ref;
   exports org.aya.resolve.context;
+  exports org.aya.syntax.core.term.call;
 }

base/src/main/java/org/aya/syntax/concrete/stmt/decl/TeleDecl.java

@@ -13,7 +13,7 @@
 import org.aya.syntax.core.def.DataDef;
 import org.aya.syntax.core.def.FnDef;
 import org.aya.syntax.core.def.TeleDef;
-import org.aya.syntax.core.term.DataCall;
+import org.aya.syntax.core.term.call.DataCall;
 import org.aya.syntax.core.term.SortTerm;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.DefVar;

base/src/main/java/org/aya/syntax/core/term/Formation.java

@@ -2,6 +2,8 @@
 // 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;
 
+import org.aya.syntax.core.term.call.DataCall;
+
 /**
  * Term formers, definitely.
  * Note that {@link PrimCall} may also be term formers, but not necessarily.

base/src/main/java/org/aya/syntax/core/term/StableWHNF.java

@@ -2,6 +2,8 @@
 // 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;
 
+import org.aya.syntax.core.term.call.DataCall;
+
 /**
  * Cubical-stable WHNF: those who will not change to other term formers
  * after a substitution (this usually happens under face restrictions (aka cofibrations)).

base/src/main/java/org/aya/syntax/core/term/Term.java

@@ -5,6 +5,7 @@
 import org.aya.generic.AyaDocile;
 import org.aya.pretty.doc.Doc;
 import org.aya.syntax.core.pat.Pat;
+import org.aya.syntax.core.term.call.Callable;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.util.Arg;
 import org.aya.util.error.SourcePos;

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

@@ -1,11 +1,13 @@
 // Copyright (c) 2020-2024 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;
+package org.aya.syntax.core.term.call;
 
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.syntax.concrete.stmt.decl.Decl;
 import org.aya.syntax.concrete.stmt.decl.TeleDecl;
 import org.aya.syntax.core.def.TeleDef;
+import org.aya.syntax.core.term.AppTerm;
+import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.AnyVar;
 import org.aya.syntax.ref.DefVar;
 import org.aya.util.Arg;
@@ -22,7 +24,7 @@ public sealed interface Callable extends Term permits Callable.Common {
   /**
    * Call to a {@link TeleDecl}.
    */
-  sealed interface Tele extends Common permits DataCall {
+  sealed interface Tele extends Common permits DataCall, FnCall {
     @Override @NotNull DefVar<? extends TeleDef, ? extends TeleDecl<?>> ref();
     int ulift();
   }

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

@@ -1,11 +1,14 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2024 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;
+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.DataDef;
+import org.aya.syntax.core.term.Formation;
+import org.aya.syntax.core.term.StableWHNF;
+import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.DefVar;
 import org.aya.util.Arg;
 import org.jetbrains.annotations.NotNull;

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

@@ -0,0 +1,27 @@
+// 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.FnDef;
+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 FnCall(
+  @Override @NotNull DefVar<FnDef, TeleDecl.FnDecl> ref,
+  @Override int ulift,
+  @Override @NotNull ImmutableSeq<Arg<@NotNull Term>> args
+) implements Callable.Tele {
+  public @NotNull FnCall update(@NotNull ImmutableSeq<Arg<Term>> args) {
+    return args.sameElements(args(), true) ? this : new FnCall(ref, ulift, args);
+  }
+
+  @Override
+  public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
+    return update(args.map(x -> x.descent(t -> f.apply(0, t))));
+  }
+}