tycker

base/src/main/java/org/aya/syntax/concrete/Pattern.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// 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.syntax.concrete;
 
@@ -56,12 +56,10 @@ record CalmFace(@Override @NotNull SourcePos sourcePos) implements Pattern {
   }
 
   /**
-   * @param userType only generated when a typed lambda is pushed into the patterns
-   * @param type     used in the LSP server
+   * @param type used in the LSP server
    */
   record Bind(
     @NotNull LocalVar bind
-    // @Nullable Expr userType
     // @ForLSP @NotNull MutableValue<@Nullable Term> type
   ) implements Pattern {
     @Override public @NotNull Bind descent(@NotNull UnaryOperator<@NotNull Pattern> f) {

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

@@ -0,0 +1,14 @@
+// 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.syntax.ref;
+
+import kala.collection.mutable.MutableMap;
+import org.aya.syntax.core.term.Term;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+public record LocalCtx(
+  @NotNull MutableMap<LocalVar, Term> binds,
+  @Nullable LocalCtx parent
+) {
+}

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

@@ -1,4 +1,7 @@
+// 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;
 
 public class ExprTycker {
+  public TyckState state;
 }

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

@@ -0,0 +1,11 @@
+// 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;
+
+import org.aya.syntax.ref.LocalCtx;
+import org.jetbrains.annotations.NotNull;
+
+public record TyckState(
+  @NotNull LocalCtx ctx
+) {
+}