sig: remove Signature, rename later (for review).

aya-prover · Jun 25, 2024 · 76ea37d · 76ea37d
1 parent 68dd2d4
commit 76ea37d
Show file tree

Hide file tree

Showing 6 changed files with 0 additions and 99 deletions.
diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/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;
@@ -25,7 +24,6 @@
 import org.aya.syntax.ref.MapLocalCtx;
 import org.aya.syntax.telescope.AbstractTele;
 import org.aya.syntax.telescope.PosedTele;
-import org.aya.syntax.telescope.Signature;
 import org.aya.tyck.ctx.LocalLet;
 import org.aya.tyck.error.*;
 import org.aya.tyck.pat.ClauseTycker;

diff --git a/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java b/base/src/main/java/org/aya/tyck/pat/ClauseTycker.java
@@ -18,7 +18,6 @@
 import org.aya.syntax.ref.LocalCtx;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.syntax.telescope.PosedTele;
-import org.aya.syntax.telescope.Signature;
 import org.aya.tyck.ExprTycker;
 import org.aya.tyck.Jdg;
 import org.aya.tyck.TyckState;

diff --git a/base/src/main/java/org/aya/tyck/tycker/TeleTycker.java b/base/src/main/java/org/aya/tyck/tycker/TeleTycker.java
@@ -14,7 +14,6 @@
 import org.aya.syntax.ref.LocalCtx;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.syntax.telescope.PosedTele;
-import org.aya.syntax.telescope.Signature;
 import org.aya.tyck.ExprTycker;
 import org.aya.tyck.Jdg;
 import org.aya.tyck.error.UnifyError;
@@ -91,21 +90,6 @@ static void bindTele(ImmutableSeq<LocalVar> binds, MutableSeq<Param> tele) {
     }
   }
 
-  @Contract(mutates = "param3")
-  static void loadTele(
-    @NotNull SeqView<LocalVar> binds,
-    @NotNull Signature signature,
-    @NotNull ExprTycker tycker
-  ) {
-    assert binds.sizeEquals(signature.param());
-    var tele = MutableList.<LocalVar>create();
-
-    binds.forEachWith(signature.param(), (ref, param) -> {
-      tycker.localCtx().put(ref, param.data().type().instantiateTeleVar(tele.view()));
-      tele.append(ref);
-    });
-  }
-
   @Contract(mutates = "param3")
   static void loadTele(
     @NotNull SeqView<LocalVar> binds,

diff --git a/syntax/src/main/java/org/aya/syntax/ref/DefVar.java b/syntax/src/main/java/org/aya/syntax/ref/DefVar.java
@@ -5,7 +5,6 @@
 import org.aya.syntax.concrete.stmt.decl.Decl;
 import org.aya.syntax.core.def.TyckDef;
 import org.aya.syntax.telescope.PosedTele;
-import org.aya.syntax.telescope.Signature;
 import org.aya.util.binop.Assoc;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;

diff --git a/syntax/src/main/java/org/aya/syntax/telescope/PosedTele.java b/syntax/src/main/java/org/aya/syntax/telescope/PosedTele.java
@@ -21,10 +21,6 @@ public record PosedTele(@NotNull AbstractTele.Locns telescope, @NotNull Immutabl
     return new PosedTele(new AbstractTele.Locns(param.map(WithPos::data), result), param.map(WithPos::sourcePos));
   }
 
-  public static @NotNull PosedTele fromSig(@NotNull Signature sig) {
-    return new PosedTele(new AbstractTele.Locns(sig.rawParams(), sig.result()), sig.param().map(WithPos::sourcePos));
-  }
-
   public @NotNull ImmutableSeq<Param> rawBoundParams() {
     return telescope.telescope();
   }

diff --git a/syntax/src/main/java/org/aya/syntax/telescope/Signature.java b/syntax/src/main/java/org/aya/syntax/telescope/Signature.java