tele: improve code

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

@@ -90,7 +90,7 @@ yield switch (fnDecl.body) {
               patResult = clauseTycker.checkNoClassify();
               def = factory.apply(Either.right(patResult.wellTyped()));
               if (!patResult.hasLhsError()) {
-                var rawParams = signature.rawBoundParams();
+                var rawParams = signature.boundParams();
                 var confluence = new YouTrack(rawParams, tycker, fnDecl.sourcePos());
                 confluence.check(patResult, signature.boundResult(),
                   PatClassifier.classify(patResult.clauses().view(), rawParams.view(), tycker, fnDecl.sourcePos()));
@@ -134,7 +134,7 @@ public ExprTycker checkHeader(@NotNull TeleDecl decl) {
         if (signature.boundResult() instanceof SortTerm userSort) sort = userSort;
         else fail(BadTypeError.doNotLike(tycker.state, result, signature.boundResult(),
           _ -> Doc.plain("universe")));
-        data.ref.signature = new PosedTele(new AbstractTele.Locns(signature.telescope().telescope(), sort), signature.pos());
+        data.ref.signature = new PosedTele(new AbstractTele.Locns(signature.boundParams(), sort), signature.pos());
       }
       case FnDecl fn -> {
         var teleTycker = new TeleTycker.Default(tycker);
@@ -147,7 +147,7 @@ else fail(BadTypeError.doNotLike(tycker.state, result, signature.boundResult(),
         if (fn.body instanceof FnBody.BlockBody(var cls, _, _)) {
           tycker.solveMetas();
           fnRef.signature = fnRef.signature.pusheen(tycker::whnf).descent(tycker::zonk);
-          if (fnRef.signature.rawBoundParams().isEmpty() && cls.isEmpty())
+          if (fnRef.signature.boundParams().isEmpty() && cls.isEmpty())
             fail(new NobodyError(decl.sourcePos(), fn.ref));
         }
       }
@@ -279,7 +279,7 @@ private void checkPrim(@NotNull ExprTycker tycker, PrimDecl prim) {
     var core = primRef.core;
     if (prim.telescope.isEmpty() && prim.result == null) {
       var pos = prim.sourcePos();
-      primRef.signature = PosedTele.fromSig(core.telescope().map(param -> new WithPos<>(pos, param)), core.result());
+      primRef.signature = new PosedTele(TyckDef.defSignature(core), ImmutableSeq.fill(core.telescope().size(), pos));
       return;
     }
     if (prim.telescope.isNotEmpty()) {
@@ -291,7 +291,7 @@ private void checkPrim(@NotNull ExprTycker tycker, PrimDecl prim) {
     assert prim.result != null;
     var tele = teleTycker.checkSignature(prim.telescope, prim.result);
     tycker.unifyTermReported(
-      PiTerm.make(tele.rawBoundParams().view().map(Param::type), tele.boundResult()),
+      PiTerm.make(tele.boundParams().view().map(Param::type), tele.boundResult()),
       // No checks, slightly faster than TeleDef.defType
       PiTerm.make(core.telescope.view().map(Param::type), core.result),
       null, prim.entireSourcePos(),

base/src/main/java/org/aya/tyck/pat/ClauseTycker.java

@@ -80,7 +80,7 @@ public record Worker(
 
       if (lhsResult.noneMatch(r -> r.hasError)) {
         var classes = PatClassifier.classify(lhsResult.view().map(LhsResult::clause),
-          signature.rawBoundParams().view(), parent.exprTycker, overallPos);
+          signature.boundParams().view(), parent.exprTycker, overallPos);
         if (clauses.isNotEmpty()) {
           var usages = PatClassifier.firstMatchDomination(clauses, parent.reporter(), classes);
           // refinePatterns(lhsResults, usages, classes);
@@ -148,7 +148,7 @@ public record Worker(
     @NotNull Pattern.Clause clause,
     boolean isFn
   ) {
-    var tycker = newPatternTycker(indices, signature.rawBoundParams().view());
+    var tycker = newPatternTycker(indices, signature.boundParams().view());
     return exprTycker.subscoped(() -> {
       // If a pattern occurs in elimination environment, then we check if it contains absurd pattern.
       // If it is not the case, the pattern must be accompanied by a body.

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

@@ -99,7 +99,7 @@ static void loadTele(
     assert binds.sizeEquals(signature.telescope().telescopeSize());
     var tele = MutableList.<LocalVar>create();
 
-    binds.forEachWith(signature.rawBoundParams(), (ref, param) -> {
+    binds.forEachWith(signature.boundParams(), (ref, param) -> {
       tycker.localCtx().put(ref, param.type().instantiateTeleVar(tele.view()));
       tele.append(ref);
     });

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

@@ -100,7 +100,7 @@ protected BasePrettier(@NotNull PrettierOptions options) {
     var licit = switch (var) {
       case TyckAnyDef<?> inner -> inner.core() instanceof SubLevelDef sub ?
         sub.selfTele.mapToBoolean(MutableBooleanList.factory(), Param::explicit) :
-        Objects.requireNonNull(inner.ref.signature).rawBoundParams()
+        Objects.requireNonNull(inner.ref.signature).boundParams()
           .mapToBooleanTo(MutableBooleanList.create(), Param::explicit);
       case JitDef jit -> MutableBooleanList.from(jit.telescopeLicit);
       default -> throw new UnsupportedOperationException("TODO");

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

@@ -10,7 +10,6 @@
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.core.term.xtt.DimTyTerm;
 import org.aya.syntax.ref.DefVar;
-import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NonNls;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
@@ -44,7 +43,7 @@ public PrimDef(@NotNull DefVar<@NotNull PrimDef, @NotNull PrimDecl> ref, @NotNul
   @Override public @NotNull ImmutableSeq<Param> telescope() {
     if (telescope.isEmpty()) return telescope;
     var signature = ref.signature;
-    if (signature != null) return signature.rawBoundParams();
+    if (signature != null) return signature.boundParams();
     return telescope;
   }
 

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

@@ -5,7 +5,6 @@
 import kala.collection.immutable.ImmutableSeq;
 import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.Term;
-import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.NotNull;
 
 /**
@@ -15,7 +14,7 @@ public sealed interface TopLevelDef extends TyckDef permits ClassDef, DataDef, F
   @Override default @NotNull ImmutableSeq<Param> telescope() {
     var signature = ref().signature;
     assert signature != null;
-    return signature.rawBoundParams();
+    return signature.boundParams();
   }
 
   @Override default @NotNull Term result() {

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

@@ -45,13 +45,16 @@ public sealed interface TyckDef extends AyaDocile permits MemberDef, SubLevelDef
   /**
    * @see AnyDef#signature()
    */
-  static @NotNull AbstractTele defSignature(@NotNull DefVar<?, ?> defVar) {
-    if (defVar.core != null) return new AbstractTele.Locns(defVar.core.telescope(), defVar.core.result());
+  static @NotNull AbstractTele.Locns defSignature(@NotNull DefVar<?, ?> defVar) {
+    if (defVar.core != null) return defSignature(defVar.core);
     // guaranteed as this is already a core term
     var signature = defVar.signature;
     assert signature != null : defVar.name();
     return signature.telescope();
   }
+  static @NotNull AbstractTele.Locns defSignature(@NotNull TyckDef core) {
+    return new AbstractTele.Locns(core.telescope(), core.result());
+  }
 
   @NotNull DefVar<?, ?> ref();
   @NotNull Term result();

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

@@ -13,25 +13,14 @@
 import java.util.function.UnaryOperator;
 
 public record PosedTele(@NotNull AbstractTele.Locns telescope, @NotNull ImmutableSeq<SourcePos> pos) {
-  public PosedTele {
-    assert telescope.telescopeSize() == pos.size();
-  }
+  public PosedTele { assert telescope.telescopeSize() == pos.size(); }
 
   public static @NotNull PosedTele fromSig(@NotNull ImmutableSeq<WithPos<Param>> param, @NotNull Term result) {
     return new PosedTele(new AbstractTele.Locns(param.map(WithPos::data), result), param.map(WithPos::sourcePos));
   }
 
-  public @NotNull ImmutableSeq<Param> rawBoundParams() {
-    return telescope.telescope();
-  }
-
-  public @NotNull ImmutableSeq<WithPos<Param>> boundParam() {
-    return rawBoundParams().zip(pos, (p, s) -> new WithPos<>(s, p));
-  }
-
-  public @NotNull Term boundResult() {
-    return telescope.result();
-  }
+  public @NotNull ImmutableSeq<Param> boundParams() { return telescope.telescope(); }
+  public @NotNull Term boundResult() { return telescope.result(); }
 
   public @NotNull PosedTele descent(@NotNull UnaryOperator<Term> f) {
     return new PosedTele(new AbstractTele.Locns(telescope.telescope().map(x -> x.descent(f)), f.apply(telescope.result())), pos);
@@ -44,7 +33,7 @@ public record PosedTele(@NotNull AbstractTele.Locns telescope, @NotNull Immutabl
   public @NotNull PosedTele pusheen(UnaryOperator<Term> pre) {
     var resultPushed = PiTerm.unpiDBI(boundResult(), pre);
     return new PosedTele(
-      new AbstractTele.Locns(rawBoundParams().appendedAll(resultPushed.params().view()), resultPushed.body()),
+      new AbstractTele.Locns(boundParams().appendedAll(resultPushed.params().view()), resultPushed.body()),
       pos.appendedAll(ImmutableSeq.fill(resultPushed.params().size(), SourcePos.NONE)));
   }
 }