merge: Use closures in classes (#1119)

base/src/main/java/org/aya/tyck/Jdg.java

@@ -16,6 +16,10 @@ public sealed interface Jdg {
   @NotNull Term type();
 
   default @NotNull Jdg bindTele(@NotNull SeqView<LocalVar> vars) { return map(t -> t.bindTele(vars)); }
+
+  /**
+   * @apiNote the mapper {@param f} may not executed immediately, so make sure that {@param f} is pure.
+   */
   @NotNull Jdg map(@NotNull UnaryOperator<Term> f);
   default Jdg lift(int lift) { return map(t -> t.elevate(lift)); }
 

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

@@ -141,9 +141,9 @@ public interface Factory<Ex extends Exception> extends
     var self = LocalVar.generate("self");
     state.classThis.push(self);
     var result = makeArgs.applyChecked(appliedParams, args -> new Jdg.Default(
-      new ClassCall(clazz, 0, ImmutableArray.from(args)),
+      new ClassCall(clazz, 0, ImmutableArray.from(args).map(x -> x.bind(self))),
       appliedParams.result(args)
-    ).bindTele(SeqView.of(self)));
+    ));
     state.classThis.pop();
     return result;
   }

syntax/src/main/java/org/aya/prettier/CorePrettier.java

@@ -44,6 +44,7 @@
  * @see ConcretePrettier
  */
 public class CorePrettier extends BasePrettier<Term> {
+  private static final @NotNull LocalVar SELF = LocalVar.generate("self");
   private final Renamer nameGen = new Renamer();
 
   public CorePrettier(@NotNull PrettierOptions options) { super(options); }
@@ -196,7 +197,8 @@ case ErrorTerm(var desc, var isReallyError) -> {
         // Add paren when it's not free or a codomain
         yield checkParen(outer, doc, Outer.BinOp);
       }
-      case ClassCall classCall -> visitCoreCalls(classCall.ref(), classCall.args(), outer, true);
+      case ClassCall classCall ->
+        visitCoreCalls(classCall.ref(), classCall.args().map(x -> x.apply(SELF)), outer, true);
       case DataCall dataCall -> visitCoreCalls(dataCall.ref(), dataCall.args(), outer, optionImplicit());
       case StringTerm(var str) -> Doc.plain("\"" + StringUtil.escapeStringCharacters(str) + "\"");
       case PAppTerm app -> visitCalls(null, term(Outer.AppHead, app.fun()),

syntax/src/main/java/org/aya/syntax/core/term/call/ClassCall.java

@@ -4,6 +4,7 @@
 
 import kala.collection.immutable.ImmutableSeq;
 import kala.function.IndexedFunction;
+import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.def.ClassDefLike;
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.marker.Formation;
@@ -18,20 +19,29 @@
  *   <li>It can be applied like a function, which essentially inserts the nearest missing field.</li>
  * </ul>
  *
+ * As the type of some class instance {@link NewTerm}, the {@param args} may refer to other member
+ * (not just former members!), therefore the value of members depend on the class instance.
+ * In order to check a class instance against to a ClassCall, you need to supply the class instance
+ * to obtain the actual arguments of the ClassCall, see {@link #args(Term)}
+ *
  * @author kiva, ice1000
  */
 public record ClassCall(
   @NotNull ClassDefLike ref,
   @Override int ulift,
-  @NotNull ImmutableSeq<Term> args
+  @NotNull ImmutableSeq<Closure> args
 ) implements StableWHNF, Formation {
-  public @NotNull ClassCall update(@NotNull ImmutableSeq<Term> args) {
+  public @NotNull ImmutableSeq<Term> args(@NotNull Term self) {
+    return this.args.map(x -> x.apply(self));
+  }
+
+  public @NotNull ClassCall update(@NotNull ImmutableSeq<Closure> args) {
     return this.args.sameElements(args, true)
       ? this : new ClassCall(ref, ulift, args);
   }
 
   @Override public @NotNull Term descent(@NotNull IndexedFunction<Term, Term> f) {
-    return update(args.map(t -> f.apply(0, t)));
+    return update(args.map(t -> t.descent(f)));
   }
 
   @Override public @NotNull Term doElevate(int level) {