diff --git a/syntax/src/main/java/org/aya/syntax/core/def/ClassDef.java b/syntax/src/main/java/org/aya/syntax/core/def/ClassDef.java
index 2e6b40de4..3a8eed139 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/ClassDef.java
+++ b/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;
+/**
+ *
+ * class Cat
+ * | A : Type
+ * | Hom (a b : A) : Type
+ * | id (a : A) : Hom a a
+ *
+ *
+ *
+ * - {@code Cat : Type1}, the type of all categories
+ * - {@code Cat A : Type1}, the type of all categories where the object type is A
+ * - {@code Cat A (->) : Type0}, essentially type of {@code A -> A}
+ *
+ */
public record ClassDef(
@Override @NotNull DefVar ref,
@NotNull ImmutableSeq members
@@ -21,7 +39,31 @@ public static final class Delegate extends TyckAnyDef implements Class
public Delegate(@NotNull DefVar ref) { super(ref); }
@Override public @NotNull ImmutableSeq 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 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 teleArgs) {
+ // Use SigmaTerm::lub
+ throw new UnsupportedOperationException("TODO");
+ }
+ @Override public @NotNull SeqView namesView() {
+ return clazz.members.sliceView(0, telescopeSize).map(i -> i.ref().name());
}
}
}
diff --git a/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java b/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
index e7012be82..66786b8ba 100644
--- a/syntax/src/main/java/org/aya/syntax/core/def/MemberDef.java
+++ b/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 classRef,
@Override @NotNull DefVar ref,
diff --git a/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java b/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java
index b4b79c2cb..855923fd4 100644
--- a/syntax/src/main/java/org/aya/syntax/telescope/AbstractTele.java
+++ b/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 namesView() { return signature.namesView(); }
}
- record Locns(
- @NotNull ImmutableSeq telescope,
- @NotNull Term result
- ) implements AbstractTele {
+ record Locns(@NotNull ImmutableSeq 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(); }