From b4889a6f1da565ca7a14570f06158bf00192a344 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Tue, 9 Jan 2024 12:52:26 -0500
Subject: [PATCH] tycker

---
 .../main/java/org/aya/syntax/concrete/Pattern.java |  6 ++----
 .../src/main/java/org/aya/syntax/ref/LocalCtx.java | 14 ++++++++++++++
 base/src/main/java/org/aya/tyck/ExprTycker.java    |  3 +++
 base/src/main/java/org/aya/tyck/TyckState.java     | 11 +++++++++++
 4 files changed, 30 insertions(+), 4 deletions(-)
 create mode 100644 base/src/main/java/org/aya/syntax/ref/LocalCtx.java
 create mode 100644 base/src/main/java/org/aya/tyck/TyckState.java

diff --git a/base/src/main/java/org/aya/syntax/concrete/Pattern.java b/base/src/main/java/org/aya/syntax/concrete/Pattern.java
index 8939c82b..3dc61554 100644
--- a/base/src/main/java/org/aya/syntax/concrete/Pattern.java
+++ b/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) {
diff --git a/base/src/main/java/org/aya/syntax/ref/LocalCtx.java b/base/src/main/java/org/aya/syntax/ref/LocalCtx.java
new file mode 100644
index 00000000..db3c6af1
--- /dev/null
+++ b/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
+) {
+}
diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index 98326dca..81f28435 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/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;
 }
diff --git a/base/src/main/java/org/aya/tyck/TyckState.java b/base/src/main/java/org/aya/tyck/TyckState.java
new file mode 100644
index 00000000..7d0ab348
--- /dev/null
+++ b/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
+) {
+}