tyck: siblings

base/src/main/java/org/aya/syntax/ref/LocalCtx.java

@@ -4,11 +4,16 @@
 
 import kala.collection.mutable.MutableMap;
 import org.aya.syntax.core.term.Term;
+import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
 public record LocalCtx(
   @NotNull MutableMap<LocalVar, Term> binds,
   @Nullable LocalCtx parent
 ) {
+  @Contract("-> new")
+  public @NotNull LocalCtx derive() {
+    return new LocalCtx(MutableMap.create(), this);
+  }
 }

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

@@ -2,6 +2,19 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck;
 
-public class ExprTycker {
-  public TyckState state;
+import org.aya.syntax.core.term.Term;
+import org.aya.syntax.ref.LocalCtx;
+import org.aya.tyck.tycker.AbstractExprTycker;
+import org.aya.util.reporter.Reporter;
+import org.jetbrains.annotations.NotNull;
+
+public final class ExprTycker extends AbstractExprTycker {
+  public ExprTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @NotNull Reporter reporter) {
+    super(state, ctx, reporter);
+  }
+
+  @Override
+  public @NotNull Term whnf(@NotNull Term term) {
+    throw new UnsupportedOperationException("TODO");
+  }
 }

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

@@ -0,0 +1,42 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.tyck.tycker;
+
+import org.aya.syntax.ref.LocalCtx;
+import org.aya.tyck.ExprTycker;
+import org.aya.tyck.TyckState;
+import org.aya.util.reporter.Reporter;
+import org.jetbrains.annotations.NotNull;
+
+public sealed abstract class AbstractExprTycker implements StatedTycker, ContextTycker, Problematic permits ExprTycker {
+  public @NotNull TyckState state;
+  private @NotNull LocalCtx localCtx;
+  public final @NotNull Reporter reporter;
+
+  protected AbstractExprTycker(@NotNull TyckState state, @NotNull LocalCtx ctx, @NotNull Reporter reporter) {
+    this.state = state;
+    this.localCtx = ctx;
+    this.reporter = reporter;
+  }
+
+  @Override
+  public @NotNull LocalCtx localCtx() {
+    return this.localCtx;
+  }
+
+  @Override public @NotNull LocalCtx setLocalCtx(@NotNull LocalCtx ctx) {
+    var old = this.localCtx;
+    this.localCtx = ctx;
+    return old;
+  }
+
+  @Override
+  public @NotNull TyckState state() {
+    return this.state;
+  }
+
+  @Override
+  public @NotNull Reporter reporter() {
+    return this.reporter;
+  }
+}

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

@@ -0,0 +1,27 @@
+// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+package org.aya.tyck.tycker;
+
+import org.aya.syntax.ref.LocalCtx;
+import org.jetbrains.annotations.NotNull;
+
+import java.util.function.Supplier;
+
+public sealed interface ContextTycker permits AbstractExprTycker {
+  @NotNull LocalCtx localCtx();
+
+  /**
+   * Update {@code localCtx} with the given one
+   *
+   * @param ctx new {@link LocalCtx}
+   * @return old context
+   */
+  @NotNull LocalCtx setLocalCtx(@NotNull LocalCtx ctx);
+
+  default <R> R subscoped(@NotNull Supplier<R> action) {
+    var parentCtx = setLocalCtx(localCtx().derive());
+    var result = action.get();
+    setLocalCtx(parentCtx);
+    return result;
+  }
+}

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

@@ -25,30 +25,16 @@
  * @see #defCall
  * @see #conOwnerSubst(ConCall)
  */
-public abstract sealed class StatedTycker implements Problematic {
-  public final @NotNull TyckState state;
-  private final @NotNull Reporter reporter;
-
-  protected StatedTycker(@NotNull Reporter reporter, @NotNull TyckState state) {
-    this.reporter = reporter;
-    this.state = state;
-  }
-
-  @Override
-  public @NotNull Reporter reporter() {
-    return reporter;
-  }
-
-  public @NotNull Term whnf(@NotNull Term term) {
-    throw new UnsupportedOperationException("TODO");    // TODO
-  }
+public sealed interface StatedTycker permits AbstractExprTycker {
+  @NotNull TyckState state();
 
+  @NotNull Term whnf(@NotNull Term term);
 
   /**
    * Elaborate partial applied call
    * {@code someCtor} -> {@code \ params -> someCtor params }
    */
-  protected final <D extends TeleDef, S extends TeleDecl<? extends Term>> @NotNull Result
+  default <D extends TeleDef, S extends TeleDecl<? extends Term>> @NotNull Result
   defCall(DefVar<D, S> defVar, Callable.Factory<D, S> function) {
     var tele = TeleDef.defTele(defVar);
     var spine = tele.mapIndexed((i, type) -> type.<Term>map(_ -> new LocalTerm(tele.size() - 1 - i)));    // λ. λ. λ. someCtor 2 1 0