From ff50b0c15d34059a5f5b81ee69dac301b2ea9f52 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Wed, 17 Jan 2024 00:09:54 +0800
Subject: [PATCH] misc: rename

---
 .../main/java/org/aya/tyck/tycker/AbstractExprTycker.java    | 2 +-
 .../tyck/tycker/{ContextTycker.java => ContextBased.java}    | 5 ++++-
 .../aya/tyck/tycker/{StatedTycker.java => StateBased.java}   | 4 ++--
 3 files changed, 7 insertions(+), 4 deletions(-)
 rename base/src/main/java/org/aya/tyck/tycker/{ContextTycker.java => ContextBased.java} (80%)
 rename base/src/main/java/org/aya/tyck/tycker/{StatedTycker.java => StateBased.java} (93%)

diff --git a/base/src/main/java/org/aya/tyck/tycker/AbstractExprTycker.java b/base/src/main/java/org/aya/tyck/tycker/AbstractExprTycker.java
index e7ab8647..7d3fab1d 100644
--- 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/base/src/main/java/org/aya/tyck/tycker/ContextTycker.java b/base/src/main/java/org/aya/tyck/tycker/ContextBased.java
similarity index 80%
rename from base/src/main/java/org/aya/tyck/tycker/ContextTycker.java
rename to base/src/main/java/org/aya/tyck/tycker/ContextBased.java
index b6d099aa..f102cc68 100644
--- a/base/src/main/java/org/aya/tyck/tycker/ContextTycker.java
+++ b/base/src/main/java/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/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java b/base/src/main/java/org/aya/tyck/tycker/StateBased.java
similarity index 93%
rename from base/src/main/java/org/aya/tyck/tycker/StatedTycker.java
rename to base/src/main/java/org/aya/tyck/tycker/StateBased.java
index 5ae56d7c..5a3d7698 100644
--- a/base/src/main/java/org/aya/tyck/tycker/StatedTycker.java
+++ b/base/src/main/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);