merge: Class call code (#1113)

base/src/main/java/org/aya/resolve/visitor/StmtBinder.java

@@ -9,7 +9,7 @@
 import org.aya.resolve.error.NameProblem;
 import org.aya.syntax.concrete.stmt.BindBlock;
 import org.aya.syntax.concrete.stmt.QualifiedID;
-import org.aya.syntax.concrete.stmt.decl.DataCon;
+import org.aya.syntax.concrete.stmt.decl.ClassDecl;
 import org.aya.syntax.concrete.stmt.decl.DataDecl;
 import org.aya.syntax.concrete.stmt.decl.FnDecl;
 import org.aya.syntax.concrete.stmt.decl.PrimDecl;
@@ -70,16 +70,15 @@ case TopDecl(DataDecl decl, var innerCtx) -> {
         decl.body.forEach(con -> resolveBind(innerCtx, new MiscDecl(con)));
         visitBind(ctx, decl.ref, decl.bindBlock());
       }
+      case TopDecl(ClassDecl decl, var innerCtx) -> {
+        decl.members.forEach(field -> resolveBind(innerCtx, new MiscDecl(field)));
+        visitBind(ctx, decl.ref, decl.bindBlock());
+      }
       case TopDecl(FnDecl fn, var innerCtx) -> visitBind(innerCtx, fn.ref, fn.bindBlock());
-      case MiscDecl(DataCon con) -> visitBind(ctx, con.ref, con.bindBlock());
+      case MiscDecl(var decl) -> visitBind(ctx, decl.ref(), decl.bindBlock());
       case TopDecl(PrimDecl _, _), GenStmt _ -> { }
-      case TopDecl _, MiscDecl _ -> Panic.unreachable();
+      case TopDecl _ -> Panic.unreachable();
       case ModStmt(var stmts) -> resolveBind(stmts);
-      // case TeleDecl.ClassMember field -> visitBind(field.ref, field.bindBlock());
-      // case ClassDecl decl -> {
-      //   decl.members.forEach(field -> resolveBind(field));
-      //   visitBind(decl.ref, decl.bindBlock());
-      // }
     }
   }
 }

base/src/main/java/org/aya/resolve/visitor/StmtResolver.java

@@ -107,6 +107,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
         var resolver = new ExprResolver(ctx, false);
         resolver.enter(Where.Head);
         decl.members.forEach(field -> {
+          // TODO: how does a field refer to a former member? DefVar or LocalVar?
           var bodyResolver = resolver.member(decl, ExprResolver.Where.Head);
           var mCtx = MutableValue.create(resolver.ctx());
           resolveMemberSignature(field, bodyResolver, mCtx);
@@ -117,7 +118,7 @@ private static void resolveDecl(@NotNull ResolvingStmt.ResolvingDecl predecl, @N
           // field.body = field.body.map(bodyResolver.enter(mCtx.get()));
           // addReferences(info, new TyckOrder.Body(field), bodyResolver);
         });
-        addReferences(info, new TyckOrder.Head(decl), resolver.reference().view()
+        addReferences(info, new TyckOrder.Body(decl), resolver.reference().view()
           .concat(decl.members.map(TyckOrder.Head::new)));
       }
       case ResolvingStmt.TopDecl(PrimDecl decl, var ctx) -> {

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

@@ -324,10 +324,10 @@ yield subscoped(param.ref(), wellParam, () ->
       case LocalVar lVar -> generateApplication(args,
         new Jdg.Default(new FreeTerm(lVar), localCtx().get(lVar))).lift(lift);
       case CompiledVar(var content) -> AppTycker.checkCompiledApplication(content,
-        new AppTycker.CheckAppData<>(state, lift, (params, k) ->
+        new AppTycker.CheckAppData<>(state, args.size(), lift, (params, k) ->
           computeArgs(sourcePos, args, params, k)));
       case DefVar<?, ?> defVar -> AppTycker.checkDefApplication(defVar,
-        new AppTycker.CheckAppData<>(state, lift, (params, k) ->
+        new AppTycker.CheckAppData<>(state, args.size(), lift, (params, k) ->
           computeArgs(sourcePos, args, params, k)));
       default -> throw new UnsupportedOperationException("TODO");
     };

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

@@ -104,7 +104,6 @@ yield switch (fnDecl.body) {
       case DataCon _, PrimDecl _, ClassMember _ ->
         Objects.requireNonNull(predecl.ref().core);   // see checkHeader
       case ClassDecl clazz -> {
-        assert clazz.ref.signature != null;
         for (var member : clazz.members) checkHeader(member);
         yield new ClassDef(clazz.ref, clazz.members.map(member -> member.ref.core));
       }
@@ -121,7 +120,15 @@ public ExprTycker checkHeader(@NotNull TeleDecl decl) {
     switch (decl) {
       case DataCon con -> checkKitsune(con, tycker);
       case PrimDecl prim -> checkPrim(tycker, prim);
-      case ClassMember member -> throw new UnsupportedOperationException("TODO");
+      case ClassMember member -> {
+        var teleTycker = new TeleTycker.Default(tycker);
+        var result = member.result;
+        assert result != null; // See AyaProducer
+        var signature = teleTycker.checkSignature(member.telescope, result);
+        tycker.solveMetas();
+        signature = signature.pusheen(tycker::whnf).descent(tycker::zonk);
+        member.ref.signature = signature;
+      }
       case DataDecl data -> {
         var teleTycker = new TeleTycker.Default(tycker);
         var result = data.result;
@@ -138,15 +145,14 @@ else fail(BadTypeError.doNotLike(tycker.state, result, signature.result(),
       case FnDecl fn -> {
         var teleTycker = new TeleTycker.Default(tycker);
         var result = fn.result;
-        if (result == null) result = new WithPos<>(fn.sourcePos(), new Expr.Hole(false, null));
+        assert result != null; // See AyaProducer
         var fnRef = fn.ref;
         fnRef.signature = teleTycker.checkSignature(fn.telescope, result);
 
         // For ExprBody, they will be zonked later
         if (fn.body instanceof FnBody.BlockBody(var cls, _, _)) {
-          fnRef.signature = fnRef.signature.pusheen(tycker::whnf);
           tycker.solveMetas();
-          fnRef.signature = fnRef.signature.descent(tycker::zonk);
+          fnRef.signature = fnRef.signature.pusheen(tycker::whnf).descent(tycker::zonk);
           if (fnRef.signature.param().isEmpty() && cls.isEmpty())
             fail(new NobodyError(decl.sourcePos(), fn.ref));
         }

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

@@ -9,10 +9,7 @@
 import org.aya.syntax.compile.JitData;
 import org.aya.syntax.compile.JitFn;
 import org.aya.syntax.compile.JitPrim;
-import org.aya.syntax.concrete.stmt.decl.DataCon;
-import org.aya.syntax.concrete.stmt.decl.DataDecl;
-import org.aya.syntax.concrete.stmt.decl.FnDecl;
-import org.aya.syntax.concrete.stmt.decl.PrimDecl;
+import org.aya.syntax.concrete.stmt.decl.*;
 import org.aya.syntax.core.def.*;
 import org.aya.syntax.core.repr.AyaShape;
 import org.aya.syntax.core.term.Term;
@@ -32,7 +29,7 @@ interface Factory<Ex extends Exception> extends
     CheckedBiFunction<AbstractTele, Function<Term[], Jdg>, Jdg, Ex> {
   }
   record CheckAppData<Ex extends Exception>(
-    @NotNull TyckState state, int lift, @NotNull Factory<Ex> makeArgs
+    @NotNull TyckState state, int argsCount, int lift, @NotNull Factory<Ex> makeArgs
   ) { }
 
   static <Ex extends Exception> @NotNull Jdg
@@ -67,7 +64,9 @@ record CheckAppData<Ex extends Exception>(
         new PrimDef.Delegate((DefVar<PrimDef, PrimDecl>) defVar));
       case DataCon _ -> checkConCall(input.state, input.makeArgs, input.lift,
         new ConDef.Delegate((DefVar<ConDef, DataCon>) defVar));
-      default -> Panic.unreachable();
+      case ClassDecl _ -> checkClassCall(input.makeArgs, input.argsCount, input.lift,
+        new ClassDef.Delegate((DefVar<ClassDef, ClassDecl>) defVar));
+      case Decl any -> throw new Panic(any.getClass().getCanonicalName());
     };
   }
 
@@ -123,4 +122,15 @@ record CheckAppData<Ex extends Exception>(
       return new Jdg.Default(fnCall, result);
     });
   }
+
+  private static <Ex extends Exception> Jdg
+  checkClassCall(@NotNull Factory<Ex> makeArgs, int argsCount, int lift, ClassDefLike clazz) throws Ex {
+    var appliedParams = clazz.takeMembers(argsCount).lift(lift);
+    return makeArgs.applyChecked(appliedParams, args -> {
+      return new Jdg.Default(
+        new ClassCall(clazz, 0, ImmutableArray.from(args)),
+        appliedParams.result(args)
+      );
+    });
+  }
 }

base/src/main/java/org/aya/unify/Synthesizer.java

@@ -8,6 +8,7 @@
 import org.aya.syntax.core.def.PrimDef;
 import org.aya.syntax.core.term.*;
 import org.aya.syntax.core.term.call.Callable;
+import org.aya.syntax.core.term.call.ClassCall;
 import org.aya.syntax.core.term.call.ConCall;
 import org.aya.syntax.core.term.call.MetaCall;
 import org.aya.syntax.core.term.repr.IntegerTerm;
@@ -134,6 +135,7 @@ case MetaCall(var ref, var args) when ref.req() instanceof MetaVar.OfType(var ty
       case DimTyTerm _ -> SortTerm.ISet;
       case MetaLitTerm mlt -> mlt.type();
       case StringTerm str -> state().primFactory().getCall(PrimDef.ID.STRING);
+      case ClassCall classCall -> throw new UnsupportedOperationException("TODO");
     };
   }
 

base/src/test/java/org/aya/tyck/TyckTest.java

@@ -66,7 +66,7 @@ def letExample (A : Type) (B : A -> Type) (f : Fn (a : A) -> B a) (a : A) : B a
       prim I : ISet
       prim Path (A : I -> Type) (a : A 0) (b : A 1) : Type
       prim coe (r s : I) (A : I -> Type) : A r -> A s
-            
+
       def transp (A : I -> Type) (a : A 0) : A 1 => coe 0 1 A a
       def transpInv (A : I -> Type) (a : A 1) : A 0 => coe 1 0 A a
       def coeFill0 (A : I -> Type) (u : A 0) : Path A u (transp A u) => \\i => coe 0 i A u
@@ -135,8 +135,7 @@ def test (a : Nat) => a = 114514
       """).defs.isNotEmpty());
   }
 
-  @Test
-  public void elimResolve() {
+  @Test public void elimResolve() {
     assertTrue(tyck("""
       open inductive Nat | O | S Nat
       open inductive Phantom Nat Nat (A : Type) | mk A
@@ -147,6 +146,14 @@ open inductive Phantom Nat Nat (A : Type) | mk A
       """).defs.isNotEmpty());
   }
 
+  @Test public void classTyck() {
+    // 🦀
+    assertTrue(tyck("""
+      class Monoid
+      | classifying carrier : Type
+      """).defs.isNotEmpty());
+  }
+
   @SuppressWarnings("unchecked") private static <T extends AnyDef> T
   getDef(@NotNull ImmutableSeq<TyckDef> defs, @NotNull String name) {
     return (T) TyckAnyDef.make(defs.find(x -> x.ref().name().equals(name)).get());

jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java

@@ -120,8 +120,7 @@ public TermExprializer(@NotNull NameGenerator nameGen, @NotNull ImmutableSeq<Str
     return STR."\{reducible}.invoke(\{finalArgs})\{elevate}";
   }
 
-  @Override
-  protected @NotNull String doSerialize(@NotNull Term term) {
+  @Override protected @NotNull String doSerialize(@NotNull Term term) {
     return switch (term) {
       case FreeTerm(var bind) -> {
         // It is possible that we meet bind here,
@@ -136,6 +135,7 @@ case FreeTerm(var bind) -> {
       case TyckInternal i -> throw new Panic(i.getClass().toString());
       case Callable.SharableCall call when call.ulift() == 0 && call.args().isEmpty() ->
         NameSerializer.getClassReference(call.ref()) + ".ourCall";
+      case ClassCall classCall -> throw new UnsupportedOperationException("TODO");
       case AppTerm appTerm -> makeAppNew(CLASS_APPTERM, appTerm.fun(), appTerm.arg());
       case LocalTerm _ when !allowLocalTerm -> throw new Panic("LocalTerm");
       case LocalTerm(var index) -> ExprializeUtils.makeNew(CLASS_LOCALTERM, Integer.toString(index));

producer/src/main/java/org/aya/producer/AyaProducer.java

@@ -296,7 +296,7 @@ private record DeclParseData(
       reporter.report(new ModifierProblem(overlap, ModifierParser.CModifier.Overlap, ModifierProblem.Reason.Duplicative));
     }
 
-    var ty = typeOrNull(node.peekChild(TYPE));
+    var ty = typeOrHole(node.peekChild(TYPE), info.info.sourcePos());
     var fnDecl = new FnDecl(info.info, fnMods, name, tele, ty, dynamite);
     if (info.modifier.isExample()) fnDecl.isExample = true;
     return fnDecl;

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

@@ -103,6 +103,7 @@ protected BasePrettier(@NotNull PrettierOptions options) {
         Objects.requireNonNull(inner.ref.signature).param()
           .mapToBooleanTo(MutableBooleanList.create(), p -> p.data().explicit());
       case JitDef jit -> MutableBooleanList.from(jit.telescopeLicit);
+      default -> throw new UnsupportedOperationException("TODO");
     };
 
     // licited args, note that this may not include all [var] args since [preArgs.size()] may less than [licit.size()]

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

@@ -195,7 +195,7 @@ 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 -> visitArgsCalls(classCall.ref(), CLAZZ, classCall.orderedArgs(), outer);
+      case ClassCall classCall -> visitCoreCalls(classCall.ref(), classCall.args(), 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/concrete/stmt/decl/ClassMember.java

@@ -8,14 +8,13 @@
 import org.aya.syntax.ref.DefVar;
 import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
-import org.jetbrains.annotations.Nullable;
 
 public final class ClassMember extends TeleDecl {
   public final @NotNull DefVar<MemberDef, ClassMember> ref;
 
   public ClassMember(
     @NotNull String name, @NotNull DeclInfo info,
-    @NotNull ImmutableSeq<Expr.Param> telescope, @Nullable WithPos<Expr> result
+    @NotNull ImmutableSeq<Expr.Param> telescope, @NotNull WithPos<Expr> result
   ) {
     super(info, telescope, result);
     ref = DefVar.concrete(this, name);

syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/FnDecl.java

@@ -11,7 +11,6 @@
 import org.aya.util.error.PosedUnaryOperator;
 import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
-import org.jetbrains.annotations.Nullable;
 
 import java.util.EnumSet;
 
@@ -31,7 +30,7 @@ public FnDecl(
     @NotNull EnumSet<Modifier> modifiers,
     @NotNull String name,
     @NotNull ImmutableSeq<Expr.Param> telescope,
-    @Nullable WithPos<Expr> result,
+    @NotNull WithPos<Expr> result,
     @NotNull FnBody body
   ) {
     super(info, telescope, result);

syntax/src/main/java/org/aya/syntax/core/def/AnyDef.java

@@ -30,7 +30,7 @@
  * </ul>
  * Note that {@link ConDef.Delegate} <b>contains</b> a {@link ConDef} rather than a super class of.
  */
-public sealed interface AnyDef extends OpDecl permits JitDef, ConDefLike, DataDefLike, FnDefLike, PrimDefLike, TyckAnyDef {
+public sealed interface AnyDef extends OpDecl permits JitDef, ClassDefLike, ConDefLike, DataDefLike, FnDefLike, MemberDefLike, PrimDefLike, TyckAnyDef {
   /**
    * Returns which file level module this def lives in.
    */
@@ -56,6 +56,7 @@ public sealed interface AnyDef extends OpDecl permits JitDef, ConDefLike, DataDe
     return switch (defVar) {
       case JitDef jitDef -> new CompiledVar(jitDef);
       case TyckAnyDef<?> tyckAnyDef -> tyckAnyDef.ref;
+      default -> throw new UnsupportedOperationException("TODO");
     };
   }
 

syntax/src/main/java/org/aya/syntax/core/def/ClassDef.java

@@ -2,17 +2,68 @@
 // 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.def;
 
+import kala.collection.Seq;
+import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
+import kala.value.LazyValue;
 import org.aya.syntax.concrete.stmt.decl.ClassDecl;
+import org.aya.syntax.core.term.PiTerm;
+import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.DefVar;
+import org.aya.syntax.telescope.AbstractTele;
 import org.jetbrains.annotations.NotNull;
 
+/**
+ * <pre>
+ * class Cat
+ * | A : Type
+ * | Hom (a b : A) : Type
+ * | id (a : A) : Hom a a
+ * </pre>
+ *
+ * <ul>
+ *   <li>{@code Cat : Type1}, the type of all categories</li>
+ *   <li>{@code Cat A : Type1}, the type of all categories where the object type is A</li>
+ *   <li>{@code Cat A (->) : Type0}, essentially type of {@code A -> A}</li>
+ * </ul>
+ */
 public record ClassDef(
   @Override @NotNull DefVar<ClassDef, ClassDecl> ref,
   @NotNull ImmutableSeq<MemberDef> members
 ) implements TopLevelDef {
   public ClassDef { ref.initialize(this); }
-  public static class Delegate extends TyckAnyDef<ClassDef> {
+  public static final class Delegate extends TyckAnyDef<ClassDef> implements ClassDefLike {
+    private final @NotNull LazyValue<ImmutableSeq<MemberDefLike>> members = LazyValue.of(() ->
+      core().members.map(x -> new MemberDef.Delegate(x.ref())));
+
     public Delegate(@NotNull DefVar<ClassDef, ?> ref) { super(ref); }
+    @Override public @NotNull ImmutableSeq<MemberDefLike> members() { return members.get(); }
+    @Override public @NotNull AbstractTele takeMembers(int size) {
+      return new TakeMembers(core(), size);
+    }
+  }
+
+  record TakeMembers(@NotNull ClassDef clazz, @Override int telescopeSize) implements AbstractTele {
+    @Override public boolean telescopeLicit(int i) { return true; }
+    @Override public @NotNull String telescopeName(int i) {
+      assert i < telescopeSize;
+      return clazz.members.get(i).ref().name();
+    }
+    @Override public @NotNull Term telescope(int i, Seq<Term> teleArgs) {
+      assert i < telescopeSize;
+      var member = clazz.members.get(i);
+      // FIXME: duplicated with somewhere, abstract!
+      var instedParam = member.telescope().mapIndexed((idx, param) ->
+        param.type().replaceTeleFrom(idx, teleArgs.view()));
+      var instedResult = member.result().replaceTeleFrom(instedParam.size(), teleArgs.view());
+      return PiTerm.make(instedParam.view(), instedResult);
+    }
+    @Override public @NotNull Term result(Seq<Term> teleArgs) {
+      // Use SigmaTerm::lub
+      throw new UnsupportedOperationException("TODO");
+    }
+    @Override public @NotNull SeqView<String> namesView() {
+      return clazz.members.sliceView(0, telescopeSize).map(i -> i.ref().name());
+    }
   }
 }

syntax/src/main/java/org/aya/syntax/core/def/ClassDefLike.java

@@ -0,0 +1,12 @@
+// 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.def;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.syntax.telescope.AbstractTele;
+import org.jetbrains.annotations.NotNull;
+
+public sealed interface ClassDefLike extends AnyDef permits ClassDef.Delegate {
+  @NotNull ImmutableSeq<MemberDefLike> members();
+  @NotNull AbstractTele takeMembers(int size);
+}