misc: rename

aya-prover · Jan 16, 2024 · ff50b0c · ff50b0c
1 parent ebeba8e
commit ff50b0c
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 4 deletions.
diff --git a/base/src/main/java/org/aya/tyck/tycker/AbstractExprTycker.java b/base/src/main/java/org/aya/tyck/tycker/AbstractExprTycker.java
@@ -8,7 +8,7 @@
 import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.NotNull;
 
-public sealed abstract class AbstractExprTycker implements StatedTycker, ContextTycker, Problematic permits ExprTycker {
+public sealed abstract class AbstractExprTycker implements StateBased, ContextBased, Problematic permits ExprTycker {
   public @NotNull TyckState state;
   private @NotNull LocalCtx localCtx;
   public final @NotNull Reporter reporter;

diff --git a/...va/org/aya/tyck/tycker/ContextTycker.java → ...ava/org/aya/tyck/tycker/ContextBased.java b/...va/org/aya/tyck/tycker/ContextTycker.java → ...ava/org/aya/tyck/tycker/ContextBased.java
@@ -3,11 +3,12 @@
 package org.aya.tyck.tycker;
 
 import org.aya.syntax.ref.LocalCtx;
+import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
 
 import java.util.function.Supplier;
 
-public sealed interface ContextTycker permits AbstractExprTycker {
+public sealed interface ContextBased permits AbstractExprTycker {
   @NotNull LocalCtx localCtx();
 
   /**
@@ -16,8 +17,10 @@ public sealed interface ContextTycker permits AbstractExprTycker {
    * @param ctx new {@link LocalCtx}
    * @return old context
    */
+  @Contract(mutates = "this")
   @NotNull LocalCtx setLocalCtx(@NotNull LocalCtx ctx);
 
+  @Contract(mutates = "this")
   default <R> R subscoped(@NotNull Supplier<R> action) {
     var parentCtx = setLocalCtx(localCtx().derive());
     var result = action.get();

diff --git a/...ava/org/aya/tyck/tycker/StatedTycker.java → .../java/org/aya/tyck/tycker/StateBased.java b/...ava/org/aya/tyck/tycker/StatedTycker.java → .../java/org/aya/tyck/tycker/StateBased.java
@@ -7,11 +7,11 @@
 import org.aya.syntax.core.def.FnDef;
 import org.aya.syntax.core.def.TeleDef;
 import org.aya.syntax.core.term.*;
+import org.aya.syntax.core.term.call.Callable;
 import org.aya.syntax.ref.DefVar;
 import org.aya.tyck.Result;
 import org.aya.tyck.TyckState;
 import org.aya.util.Arg;
-import org.aya.util.reporter.Reporter;
 import org.jetbrains.annotations.NotNull;
 
 /**
@@ -25,7 +25,7 @@
  * @see #defCall
  * @see #conOwnerSubst(ConCall)
  */
-public sealed interface StatedTycker permits AbstractExprTycker {
+public sealed interface StateBased permits AbstractExprTycker {
   @NotNull TyckState state();
 
   @NotNull Term whnf(@NotNull Term term);