Unify Signature with AbstractTele.Locns

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

@@ -2,7 +2,6 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck;
 
-import kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.control.Either;
 import kala.control.Option;
@@ -21,7 +20,9 @@
 import org.aya.syntax.core.term.call.DataCall;
 import org.aya.syntax.core.term.xtt.DimTyTerm;
 import org.aya.syntax.core.term.xtt.EqTerm;
+import org.aya.syntax.ref.LocalVar;
 import org.aya.syntax.ref.MapLocalCtx;
+import org.aya.syntax.telescope.AbstractTele;
 import org.aya.syntax.telescope.Signature;
 import org.aya.tyck.ctx.LocalLet;
 import org.aya.tyck.error.*;
@@ -89,7 +90,7 @@ yield switch (fnDecl.body) {
               patResult = clauseTycker.checkNoClassify();
               def = factory.apply(Either.right(patResult.wellTyped()));
               if (!patResult.hasLhsError()) {
-                var rawParams = signature.rawParams();
+                var rawParams = signature.params();
                 var confluence = new YouTrack(rawParams, tycker, fnDecl.sourcePos());
                 confluence.check(patResult, signature.result(),
                   PatClassifier.classify(patResult.clauses().view(), rawParams.view(), tycker, fnDecl.sourcePos()));
@@ -133,7 +134,7 @@ public ExprTycker checkHeader(@NotNull TeleDecl decl) {
         if (signature.result() instanceof SortTerm userSort) sort = userSort;
         else fail(BadTypeError.doNotLike(tycker.state, result, signature.result(),
           _ -> Doc.plain("universe")));
-        data.ref.signature = new Signature(signature.param(), sort);
+        data.ref.signature = new Signature(new AbstractTele.Locns(signature.params(), sort), signature.pos());
       }
       case FnDecl fn -> {
         var teleTycker = new TeleTycker.Default(tycker);
@@ -146,7 +147,7 @@ else fail(BadTypeError.doNotLike(tycker.state, result, signature.result(),
         if (fn.body instanceof FnBody.BlockBody(var cls, _, _)) {
           tycker.solveMetas();
           fnRef.signature = fnRef.signature.pusheen(tycker::whnf).descent(tycker::zonk);
-          if (fnRef.signature.param().isEmpty() && cls.isEmpty())
+          if (fnRef.signature.params().isEmpty() && cls.isEmpty())
             fail(new NobodyError(decl.sourcePos(), fn.ref));
         }
       }
@@ -167,10 +168,12 @@ private void checkMember(@NotNull ClassMember member, @NotNull ExprTycker tycker
     tycker.solveMetas();
     signature = signature.pusheen(tycker::whnf)
       .descent(tycker::zonk)
-      .bindTele(SeqView.of(tycker.state.classThis.pop()));
-    // 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());
+      .bindTele(
+        tycker.state.classThis.pop(),
+        new Param("self", classCall, false),
+        classRef.concrete.sourcePos()
+      );
+    new MemberDef(classRef, member.ref, signature.params(), signature.result());
     member.ref.signature = signature;
   }
 
@@ -187,7 +190,8 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
     var dataSig = dataRef.signature;
     assert dataSig != null : "the header of data should be tycked";
     // Intended to be indexed, not free
-    var ownerTele = dataSig.param().map(x -> x.descent((_, p) -> p.implicitize()));
+    var ownerTele = dataSig.telescope().telescope().map(Param::implicitize);
+    var ownerTelePos = dataSig.pos();
     var ownerBinds = dataRef.concrete.telescope.map(Expr.Param::ref);
     // dataTele already in localCtx
     // The result that a con should be, unless it is a Path result
@@ -207,8 +211,8 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
       var allTypedBinds = Pat.collectBindings(wellPats.view());
       ownerBinds = lhsResult.allBinds();
       TeleTycker.bindTele(ownerBinds, allTypedBinds);
-      ownerTele = ownerBinds.zip(allTypedBinds,
-        (bind, param) -> new WithPos<>(bind.definition(), param));
+      ownerTelePos = ownerBinds.map(LocalVar::definition);
+      ownerTele = allTypedBinds.toImmutableSeq();
       if (wellPats.allMatch(pat -> pat instanceof Pat.Bind))
         wellPats = ImmutableSeq.empty();
     } else {
@@ -217,25 +221,30 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
 
     var teleTycker = new TeleTycker.Con(tycker, (SortTerm) dataSig.result());
     var selfTele = teleTycker.checkTele(con.telescope);
-    var selfTeleVars = con.teleVars();
+    var selfTelePos = con.telescope.map(Expr.Param::sourcePos);
+    var selfBinds = con.teleVars();
 
     var conTy = con.result;
     EqTerm boundaries = null;
     if (conTy != null) {
       var pusheenResult = PiTerm.unpi(tycker.ty(conTy), tycker::whnf);
+
       selfTele = selfTele.appendedAll(pusheenResult.params().zip(pusheenResult.names(),
-        (param, name) -> new WithPos<>(conTy.sourcePos(), new Param(name.name(), param, true))));
-      selfTeleVars = selfTeleVars.appendedAll(pusheenResult.names());
+        (param, name) -> new Param(name.name(), param, true)));
+      selfTelePos = selfTelePos.appendedAll(ImmutableSeq.fill(pusheenResult.params().size(), conTy.sourcePos()));
+
+      selfBinds = selfBinds.appendedAll(pusheenResult.names());
       var tyResult = tycker.whnf(pusheenResult.body());
       if (tyResult instanceof EqTerm eq) {
         var state = tycker.state;
         var fresh = new FreeTerm("i");
         tycker.unifyTermReported(eq.appA(fresh), freeDataCall, null, conTy.sourcePos(),
           cmp -> new UnifyError.ConReturn(con, cmp, new UnifyInfo(state)));
 
-        selfTele = selfTele.appended(new WithPos<>(conTy.sourcePos(),
-          new Param("i", DimTyTerm.INSTANCE, true)));
-        selfTeleVars = selfTeleVars.appended(fresh.name());
+        selfTele = selfTele.appended(new Param("i", DimTyTerm.INSTANCE, true));
+        selfTelePos = selfTelePos.appended(conTy.sourcePos());
+
+        selfBinds = selfBinds.appended(fresh.name());
         boundaries = eq;
       } else {
         var state = tycker.state;
@@ -247,22 +256,24 @@ private void checkKitsune(@NotNull DataCon con, @NotNull ExprTycker tycker) {
 
     // the result will refer to the telescope of con if it has patterns,
     // the path result may also refer to it, so we need to bind both
-    var boundDataCall = (DataCall) tycker.zonk(freeDataCall).bindTele(selfTeleVars);
-    if (boundaries != null) boundaries = (EqTerm) tycker.zonk(boundaries).bindTele(selfTeleVars);
+    var boundDataCall = (DataCall) tycker.zonk(freeDataCall).bindTele(selfBinds);
+    if (boundaries != null) boundaries = (EqTerm) tycker.zonk(boundaries).bindTele(selfBinds);
     var boundariesWithDummy = boundaries != null ? boundaries : ErrorTerm.DUMMY;
-    var selfSig = new Signature(tycker.zonk(selfTele), new TupTerm(
+    var wholeSig = new AbstractTele.Locns(tycker.zonk(selfTele), new TupTerm(
       // This is a silly hack that allows two terms to appear in the result of a Signature
       // I considered using `AppTerm` but that is more disgraceful
-      ImmutableSeq.of(boundDataCall, boundariesWithDummy))).bindTele(ownerBinds.view());
-    var selfSigResult = ((TupTerm) selfSig.result()).items();
-    boundDataCall = (DataCall) selfSigResult.get(0);
-    if (boundaries != null) boundaries = (EqTerm) selfSigResult.get(1);
+      ImmutableSeq.of(boundDataCall, boundariesWithDummy)))
+      .bindTele(ownerBinds.zip(ownerTele).view());
+    var wholeSigResult = ((TupTerm) wholeSig.result()).items();
+    boundDataCall = (DataCall) wholeSigResult.get(0);
+    if (boundaries != null) boundaries = (EqTerm) wholeSigResult.get(1);
 
     // The signature of con should be full (the same as [konCore.telescope()])
-    ref.signature = new Signature(ownerTele.concat(selfSig.param()), boundDataCall);
+    ref.signature = new Signature(new AbstractTele.Locns(wholeSig.telescope(), boundDataCall),
+      ownerTelePos.appendedAll(selfTelePos));
     new ConDef(dataDef, ref, wellPats, boundaries,
-      ownerTele.map(WithPos::data),
-      selfSig.rawParams(),
+      ownerTele,
+      wholeSig.telescope().drop(ownerTele.size()),
       boundDataCall, false);
   }
 
@@ -275,7 +286,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 = new Signature(core.telescope().map(param -> new WithPos<>(pos, param)), core.result());
+      primRef.signature = new Signature(TyckDef.defSignature(core), ImmutableSeq.fill(core.telescope().size(), pos));
       return;
     }
     if (prim.telescope.isNotEmpty()) {
@@ -287,7 +298,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.param().view().map(p -> p.data().type()), tele.result()),
+      PiTerm.make(tele.params().view().map(Param::type), tele.result()),
       // 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.param().view().map(WithPos::data), parent.exprTycker, overallPos);
+          signature.params().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.rawParams().view());
+    var tycker = newPatternTycker(indices, signature.params().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/AbstractTycker.java

@@ -58,7 +58,7 @@ public <R> R subscoped(@NotNull Term type, @NotNull Function<LocalVar, R> action
   public @NotNull Term zonk(Term t) {
     return new Finalizer.Zonk<>(this).zonk(t);
   }
-  public ImmutableSeq<WithPos<Param>> zonk(ImmutableSeq<WithPos<Param>> tele) {
-    return tele.map(wp -> wp.map(p -> p.descent(this::zonk)));
+  public ImmutableSeq<Param> zonk(ImmutableSeq<Param> tele) {
+    return tele.map(wp -> wp.descent(this::zonk));
   }
 }

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

@@ -13,6 +13,7 @@
 import org.aya.syntax.core.term.Term;
 import org.aya.syntax.ref.LocalCtx;
 import org.aya.syntax.ref.LocalVar;
+import org.aya.syntax.telescope.AbstractTele;
 import org.aya.syntax.telescope.Signature;
 import org.aya.tyck.ExprTycker;
 import org.aya.tyck.Jdg;
@@ -43,18 +44,17 @@ public sealed interface TeleTycker extends Contextful {
     var locals = cTele.view().map(Expr.Param::ref).toImmutableSeq();
     var checkedParam = checkTele(cTele);
     var checkedResult = checkType(result, true).bindTele(locals.view());
-    return new Signature(checkedParam, checkedResult);
+    return new Signature(new AbstractTele.Locns(checkedParam, checkedResult), cTele.map(Expr.Param::sourcePos));
   }
 
   /**
    * Does not zonk the result. Need <emph>you</emph> to zonk them.
    */
-  default @NotNull ImmutableSeq<WithPos<Param>> checkTele(@NotNull ImmutableSeq<Expr.Param> cTele) {
+  default @NotNull ImmutableSeq<Param> checkTele(@NotNull ImmutableSeq<Expr.Param> cTele) {
     var tele = checkTeleFree(cTele);
     var locals = cTele.view().map(Expr.Param::ref).toImmutableSeq();
     bindTele(locals, tele);
-    return tele.zip(cTele, (param, sp) -> new WithPos<>(sp.sourcePos(), param))
-      .toImmutableSeq();
+    return tele.toImmutableSeq();
   }
 
   /**
@@ -96,11 +96,11 @@ static void loadTele(
     @NotNull Signature signature,
     @NotNull ExprTycker tycker
   ) {
-    assert binds.sizeEquals(signature.param());
+    assert binds.sizeEquals(signature.telescope().telescopeSize());
     var tele = MutableList.<LocalVar>create();
 
-    binds.forEachWith(signature.param(), (ref, param) -> {
-      tycker.localCtx().put(ref, param.data().type().instantiateTeleVar(tele.view()));
+    binds.forEachWith(signature.params(), (ref, param) -> {
+      tycker.localCtx().put(ref, param.type().instantiateTeleVar(tele.view()));
       tele.append(ref);
     });
   }

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

@@ -100,8 +100,8 @@ 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).param()
-          .mapToBooleanTo(MutableBooleanList.create(), p -> p.data().explicit());
+        Objects.requireNonNull(inner.ref.signature).params()
+          .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.param().map(WithPos::data);
+    if (signature != null) return signature.params();
     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.param().map(WithPos::data);
+    return signature.params();
   }
 
   @Override default @NotNull Term result() {

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

@@ -45,12 +45,15 @@ 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 new AbstractTele.Locns(signature.rawParams(), signature.result());
+    return signature.telescope();
+  }
+  static @NotNull AbstractTele.Locns defSignature(@NotNull TyckDef core) {
+    return new AbstractTele.Locns(core.telescope(), core.result());
   }
 
   @NotNull DefVar<?, ?> ref();

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

@@ -8,10 +8,12 @@
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.primitive.ImmutableIntSeq;
 import kala.range.primitive.IntRange;
+import kala.tuple.Tuple2;
 import org.aya.syntax.core.Closure;
 import org.aya.syntax.core.term.Param;
 import org.aya.syntax.core.term.PiTerm;
 import org.aya.syntax.core.term.Term;
+import org.aya.syntax.ref.LocalVar;
 import org.jetbrains.annotations.NotNull;
 
 /**
@@ -109,6 +111,36 @@ record Locns(@NotNull ImmutableSeq<Param> telescope, @NotNull Term result) imple
     @Override public @NotNull SeqView<String> namesView() {
       return telescope.view().map(Param::name);
     }
+
+    public @NotNull Locns bind(@NotNull LocalVar var, @NotNull Param type) {
+      var boundTele = telescope.view().mapIndexed((idx, p) -> p.descent(t -> t.bindAt(var, idx)));
+      return new Locns(boundTele.prepended(type).toImmutableSeq(), result.bindAt(var, telescope.size()));
+    }
+
+    public @NotNull Locns bindTele(@NotNull SeqView<Tuple2<LocalVar, Param>> tele) {
+      return tele.foldRight(this, (pair, acc) -> {
+        var var = pair.component1();
+        var type = pair.component2();
+        return acc.bind(var, type);
+      });
+    }
+
+    // public @NotNull Locns drop(int count) {
+    //   assert count <= telescopeSize();
+    //   return new Locns(telescope.drop(count), result);
+    // }
+
+    @Override public @NotNull Locns inst(ImmutableSeq<Term> preArgs) {
+      if (preArgs.isEmpty()) return this;
+      assert preArgs.size() <= telescopeSize();
+      var view = preArgs.view();
+      var cope = telescope.view()
+        .drop(preArgs.size())
+        .mapIndexed((idx, p) -> p.descent(t -> t.replaceTeleFrom(idx, view)))
+        .toImmutableSeq();
+      var result = this.result.replaceTeleFrom(cope.size(), view);
+      return new Locns(cope, result);
+    }
   }
 
   record Lift(