term: def (unable to pass the compilation though)

base/src/main/java/org/aya/syntax/core/def/Def.java

@@ -1,4 +1,25 @@
+// Copyright (c) 2020-2023 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;
 
-public interface Def {
+import org.aya.generic.AyaDocile;
+import org.aya.pretty.doc.Doc;
+import org.aya.syntax.core.term.Term;
+import org.aya.syntax.ref.DefVar;
+import org.aya.util.prettier.PrettierOptions;
+import org.jetbrains.annotations.NotNull;
+
+import java.util.function.Consumer;
+
+/**
+ * @author zaoqi
+ */
+public sealed interface Def extends AyaDocile permits ClassDef, TeleDef {
+  @NotNull DefVar<?, ?> ref();
+
+  void descentConsume(@NotNull Consumer<Term> f, @NotNull Consumer<Pat> g);
+
+  @Override default @NotNull Doc toDoc(@NotNull PrettierOptions options) {
+    throw new UnsupportedOperationException("TODO");
+  }
 }

base/src/main/java/org/aya/syntax/core/def/TeleDef.java

@@ -0,0 +1,50 @@
+// Copyright (c) 2020-2023 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.Seq;
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.syntax.concrete.stmt.decl.Decl;
+import org.aya.syntax.concrete.stmt.decl.TeleDecl;
+import org.aya.syntax.core.term.PiTerm;
+import org.aya.syntax.core.term.Term;
+import org.aya.syntax.ref.DefVar;
+import org.aya.util.Arg;
+import org.jetbrains.annotations.Contract;
+import org.jetbrains.annotations.NotNull;
+
+import java.util.Objects;
+
+/**
+ * @author ice1000
+ */
+public sealed interface TeleDef extends Def permits SubLevelDef, TopLevelDef {
+  static @NotNull Term defType(@NotNull DefVar<? extends TeleDef, ? extends TeleDecl<?>> defVar) {
+    return PiTerm.make(defTele(defVar), defResult(defVar));
+  }
+
+  static @NotNull ImmutableSeq<Arg<Term>> defTele(@NotNull DefVar<? extends TeleDef, ? extends TeleDecl<?>> defVar) {
+    if (defVar.core != null) return defVar.core.telescope();
+    // guaranteed as this is already a core term
+    var signature = defVar.concrete.signature;
+    assert signature != null : defVar.name();
+    return signature.param();
+  }
+  static @NotNull Seq<CtorDef> dataBody(@NotNull DefVar<? extends DataDef, ? extends TeleDecl.DataDecl> defVar) {
+    if (defVar.core != null) return defVar.core.body;
+      // guaranteed as this is already a core term
+    else return defVar.concrete.checkedBody;
+  }
+
+  @SuppressWarnings("unchecked") @Contract(pure = true)
+  static <T extends Term> @NotNull T
+  defResult(@NotNull DefVar<? extends TeleDef, ? extends TeleDecl<? extends T>> defVar) {
+    if (defVar.core != null) return (T) defVar.core.result();
+      // guaranteed as this is already a core term
+    else return Objects.requireNonNull(defVar.concrete.signature).result();
+  }
+
+  @Override @NotNull DefVar<? extends TeleDef, ? extends Decl> ref();
+  @NotNull Term result();
+  @NotNull ImmutableSeq<Arg<Term>> telescope();
+}