tyck: class signature

Co-authored-by: HoshinoTented <[email protected]>

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

@@ -2,13 +2,31 @@
 // 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
@@ -21,7 +39,31 @@ public static final class Delegate extends TyckAnyDef<ClassDef> implements Class
     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 null;
+      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/MemberDef.java

@@ -10,6 +10,9 @@
 import org.aya.syntax.ref.DefVar;
 import org.jetbrains.annotations.NotNull;
 
+/**
+ * @apiNote the telescope/result of a member probably need to be instantiated, they may refer to the former members.
+ */
 public record MemberDef(
   @NotNull DefVar<ClassDef, ClassDecl> classRef,
   @Override @NotNull DefVar<MemberDef, ClassMember> ref,

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

@@ -71,10 +71,7 @@ record Lift(
     @Override public @NotNull AbstractTele lift(int i) { return new Lift(signature, lift + i); }
     @Override public @NotNull SeqView<String> namesView() { return signature.namesView(); }
   }
-  record Locns(
-    @NotNull ImmutableSeq<Param> telescope,
-    @NotNull Term result
-  ) implements AbstractTele {
+  record Locns(@NotNull ImmutableSeq<Param> telescope, @NotNull Term result) implements AbstractTele {
     @Override public int telescopeSize() { return telescope.size(); }
     @Override public boolean telescopeLicit(int i) { return telescope.get(i).explicit(); }
     @Override public @NotNull String telescopeName(int i) { return telescope.get(i).name(); }