merge: Classes are now kinda working (#1118)

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

@@ -16,6 +16,7 @@
 import org.aya.syntax.core.def.PrimDef;
 import org.aya.syntax.core.repr.AyaShape;
 import org.aya.syntax.core.term.*;
+import org.aya.syntax.core.term.call.ClassCall;
 import org.aya.syntax.core.term.call.DataCall;
 import org.aya.syntax.core.term.call.MetaCall;
 import org.aya.syntax.core.term.repr.IntegerTerm;
@@ -331,6 +332,13 @@ case CompiledVar(var content) -> new AppTycker<>(state, sourcePos, args.size(),
     };
   }
 
+  private @NotNull Term insertImplicit(@NotNull Param param, @NotNull SourcePos pos) {
+    if (param.type() instanceof ClassCall clazz) {
+      // TODO: type checking
+      return new FreeTerm(state.classThis.peek());
+    } else return mockTerm(param, pos);
+  }
+
   private Jdg computeArgs(
     @NotNull SourcePos pos, @NotNull ImmutableSeq<Expr.NamedArg> args,
     @NotNull AbstractTele params, @NotNull Function<Term[], Jdg> k
@@ -347,12 +355,12 @@ private Jdg computeArgs(
           break;
         } else if (arg.name() == null) {
           // here, arg.explicit() == true and param.explicit() == false
-          result[paramIx++] = mockTerm(param, arg.sourcePos());
+          result[paramIx++] = insertImplicit(param, arg.sourcePos());
           continue;
         }
       }
       if (arg.name() != null && !param.nameEq(arg.name())) {
-        result[paramIx++] = mockTerm(param, arg.sourcePos());
+        result[paramIx++] = insertImplicit(param, arg.sourcePos());
         continue;
       }
       result[paramIx++] = inherit(arg.arg(), param.type()).wellTyped();
@@ -362,7 +370,7 @@ private Jdg computeArgs(
     while (paramIx < params.telescopeSize()) {
       if (params.telescopeLicit(paramIx)) break;
       var param = params.telescopeRich(paramIx, result);
-      result[paramIx++] = mockTerm(param, pos);
+      result[paramIx++] = insertImplicit(param, pos);
     }
     var extraParams = MutableStack.<Pair<LocalVar, Term>>create();
     if (argIx < args.size()) {

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

@@ -17,6 +17,7 @@
 import org.aya.syntax.core.pat.Pat;
 import org.aya.syntax.core.pat.PatToTerm;
 import org.aya.syntax.core.term.*;
+import org.aya.syntax.core.term.call.ClassCall;
 import org.aya.syntax.core.term.call.DataCall;
 import org.aya.syntax.core.term.xtt.DimTyTerm;
 import org.aya.syntax.core.term.xtt.EqTerm;
@@ -155,7 +156,10 @@ else fail(BadTypeError.doNotLike(tycker.state, result, signature.result(),
   private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker) {
     if (member.ref.core != null) return;
     var classRef = member.classRef;
-    tycker.state.classThis.push(classRef.concrete.self);
+    var self = classRef.concrete.self;
+    tycker.state.classThis.push(self);
+    var classCall = new ClassCall(new ClassDef.Delegate(classRef), 0, ImmutableSeq.empty());
+    tycker.localCtx().put(self, classCall);
     var teleTycker = new TeleTycker.Default(tycker);
     var result = member.result;
     assert result != null; // See AyaProducer
@@ -164,8 +168,9 @@ private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker
     signature = signature.pusheen(tycker::whnf)
       .descent(tycker::zonk)
       .bindTele(SeqView.of(tycker.state.classThis.pop()));
-    // TODO: prepend {this: Class} to the telescope
-    new MemberDef(classRef, member.ref, signature.rawParams(), signature.result());
+    // TODO: reconsider these `self` references, they should be locally nameless!
+    var selfParam = new Param("this", classCall, false);
+    new MemberDef(classRef, member.ref, signature.rawParams().prepended(selfParam), signature.result());
     member.ref.signature = signature;
   }
 

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

@@ -5,7 +5,6 @@
 import kala.collection.Seq;
 import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableArray;
-import kala.collection.immutable.ImmutableSeq;
 import kala.function.CheckedBiFunction;
 import org.aya.generic.stmt.Shaped;
 import org.aya.syntax.compile.JitCon;
@@ -139,29 +138,23 @@ public interface Factory<Ex extends Exception> extends
 
   private @NotNull Jdg checkClassCall(@NotNull ClassDefLike clazz) throws Ex {
     var appliedParams = ofClassMembers(clazz, argsCount).lift(lift);
-    // TODO: We may just accept a LocalVar and do subscopedClass in ExprTycker as long as appliedParams won't be affected.
     var self = LocalVar.generate("self");
     state.classThis.push(self);
     var result = makeArgs.applyChecked(appliedParams, args -> new Jdg.Default(
-      new ClassCall(self, clazz, 0, ImmutableArray.from(args)),
+      new ClassCall(clazz, 0, ImmutableArray.from(args)),
       appliedParams.result(args)
-    ));
+    ).bindTele(SeqView.of(self)));
     state.classThis.pop();
     return result;
   }
 
   private @NotNull Jdg checkProjCall(@NotNull MemberDefLike member) throws Ex {
-    var self = new FreeTerm(state.classThis.peek());
-    var signature = member.signature().inst(ImmutableSeq.of(self)).lift(lift);
+    var signature = member.signature().lift(lift);
     return makeArgs.applyChecked(signature, args -> {
-      // assert args.length >= 1;
-      // var fieldArgs = ImmutableArray.fill(args.length - 1, i -> args[i + 1]);
-      // return new Jdg.Default(
-      //   new FieldCall(args[0], member, 0, fieldArgs),
-      //   signature.result(args)
-      // );
+      assert args.length >= 1;
+      var fieldArgs = ImmutableArray.fill(args.length - 1, i -> args[i + 1]);
       return new Jdg.Default(
-        new MemberCall(self, member, 0, ImmutableArray.from(args)),
+        new MemberCall(args[0], member, 0, fieldArgs),
         signature.result(args)
       );
     });

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

@@ -61,7 +61,7 @@ default <R> R subscoped(@NotNull LocalVar var, @NotNull Term type, @NotNull Supp
   /**
    * Generate a fresh {@link MetaCall} with type {@link Param#type()}
    */
-  default @NotNull Term mockTerm(@NotNull Param param, @NotNull SourcePos pos) {
+  default @NotNull MetaCall mockTerm(@NotNull Param param, @NotNull SourcePos pos) {
     return freshMeta(param.name(), pos, new MetaVar.OfType(param.type()));
   }
 

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

@@ -37,7 +37,7 @@ public class TyckTest {
     var result = tyck("""
       inductive Nat | O | S Nat
       inductive FreeMonoid (A : Type) | e | cons A (FreeMonoid A)
-            
+      
       def id {A : Type} (a : A) => a
       def lam (A : Type) : Fn (a : A) -> Type => fn a => A
       def tup (A : Type) (B : A -> Type) (a : A) (b : Fn (a : A) -> B a)
@@ -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
@@ -149,10 +149,15 @@ open inductive Phantom Nat Nat (A : Type) | mk A
   @Test public void classTyck() {
     // 🦀
     assertTrue(tyck("""
+      prim I prim Path prim coe
+      variable A : Type
+      def infix = (a b : A) => Path (\\i => A) a b
+      
       class Monoid
-      | classifying carrier : Type
+      | carrier : Type
       | unit : carrier
       | op : carrier -> carrier -> carrier
+      | idl (x : carrier) : op unit x = x
       """).defs.isNotEmpty());
   }
 

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

@@ -8,7 +8,6 @@
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.marker.Formation;
 import org.aya.syntax.core.term.marker.StableWHNF;
-import org.aya.syntax.ref.LocalVar;
 import org.jetbrains.annotations.NotNull;
 
 /**
@@ -22,21 +21,20 @@
  * @author kiva, ice1000
  */
 public record ClassCall(
-  @NotNull LocalVar self,
   @NotNull ClassDefLike ref,
   @Override int ulift,
   @NotNull ImmutableSeq<Term> args
 ) implements StableWHNF, Formation {
   public @NotNull ClassCall update(@NotNull ImmutableSeq<Term> args) {
     return this.args.sameElements(args, true)
-      ? this : new ClassCall(self, ref, ulift, args);
+      ? 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)));
   }
 
   @Override public @NotNull Term doElevate(int level) {
-    return new ClassCall(self, ref, ulift + level, args);
+    return new ClassCall(ref, ulift + level, args);
   }
 }

syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java

@@ -141,14 +141,14 @@ record Inst(
     @NotNull ImmutableSeq<Term> args
   ) implements AbstractTele {
     @Override public @NotNull Term telescope(int i, Seq<Term> teleArgs) {
-      return signature.telescope(i, args.appendedAll(teleArgs));
+      return signature.telescope(i + args.size(), args.appendedAll(teleArgs));
     }
 
     @Override public @NotNull Term result(Seq<Term> teleArgs) {
       return signature.result(args.appendedAll(teleArgs));
     }
-    @Override public int telescopeSize() { return signature.telescopeSize(); }
-    @Override public boolean telescopeLicit(int i) { return signature.telescopeLicit(i); }
-    @Override public @NotNull String telescopeName(int i) { return signature.telescopeName(i); }
+    @Override public int telescopeSize() { return signature.telescopeSize() - args.size(); }
+    @Override public boolean telescopeLicit(int i) { return signature.telescopeLicit(i + args.size()); }
+    @Override public @NotNull String telescopeName(int i) { return signature.telescopeName(i + args.size()); }
   }
 }