more files

base/src/main/java/module-info.java

@@ -12,6 +12,9 @@
   requires org.commonmark;
 
   exports org.aya.prelude;
-  exports org.aya.syntax.core;
+  exports org.aya.syntax.concrete.decl;
+  exports org.aya.syntax.core.def;
+  exports org.aya.syntax.core.term;
   exports org.aya.syntax.ref;
+  exports org.aya.syntax.concrete.expr;
 }

base/src/main/java/org/aya/syntax/concrete/decl/Decl.java

@@ -0,0 +1,4 @@
+package org.aya.syntax.concrete.decl;
+
+public interface Decl {
+}

base/src/main/java/org/aya/syntax/concrete/expr/Expr.java

@@ -0,0 +1,16 @@
+package org.aya.syntax.concrete.expr;
+
+import org.aya.syntax.ref.LocalVar;
+import org.aya.util.error.SourceNode;
+import org.aya.util.error.SourcePos;
+import org.jetbrains.annotations.NotNull;
+
+public sealed interface Expr {
+  record Node(@NotNull SourcePos sourcePos, @NotNull Expr expr) implements SourceNode {}
+
+  record Lam(@NotNull LocalVar var, @NotNull Node body) implements Expr {}
+
+  record Ref(@NotNull LocalVar var) implements Expr {}
+
+  record App(@NotNull Node fun, @NotNull Node arg) implements Expr {}
+}

base/src/main/java/org/aya/syntax/core/def/Def.java

@@ -0,0 +1,4 @@
+package org.aya.syntax.core.def;
+
+public interface Def {
+}

base/src/main/java/org/aya/syntax/core/AppTerm.java → base/src/main/java/org/aya/syntax/core/term/AppTerm.java

@@ -1,4 +1,4 @@
-package org.aya.syntax.core;
+package org.aya.syntax.core.term;
 
 import org.aya.syntax.ref.LocalVar;
 import org.jetbrains.annotations.NotNull;

base/src/main/java/org/aya/syntax/core/FreeTerm.java → base/src/main/java/org/aya/syntax/core/term/FreeTerm.java

@@ -1,4 +1,4 @@
-package org.aya.syntax.core;
+package org.aya.syntax.core.term;
 
 import org.aya.syntax.ref.LocalVar;
 import org.jetbrains.annotations.NotNull;

base/src/main/java/org/aya/syntax/core/LamTerm.java → base/src/main/java/org/aya/syntax/core/term/LamTerm.java

@@ -1,9 +1,9 @@
-package org.aya.syntax.core;
+package org.aya.syntax.core.term;
 
 import org.aya.syntax.ref.LocalVar;
 import org.jetbrains.annotations.NotNull;
 
-public record LamTerm(Term body) implements Term {
+public record LamTerm(Term body) implements Term, Term.StableWHNF {
   @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
     var newBody = body.bindAt(var, depth + 1);
     if (newBody == body) return this;

base/src/main/java/org/aya/syntax/core/LocalTerm.java → base/src/main/java/org/aya/syntax/core/term/LocalTerm.java

@@ -1,4 +1,4 @@
-package org.aya.syntax.core;
+package org.aya.syntax.core.term;
 
 import org.aya.syntax.ref.LocalVar;
 import org.jetbrains.annotations.NotNull;

base/src/main/java/org/aya/syntax/core/Term.java → base/src/main/java/org/aya/syntax/core/term/Term.java

@@ -1,4 +1,4 @@
-package org.aya.syntax.core;
+package org.aya.syntax.core.term;
 
 import org.aya.syntax.ref.LocalVar;
 import org.jetbrains.annotations.ApiStatus;
@@ -35,4 +35,6 @@ public sealed interface Term extends Serializable
   default @NotNull Term instantiate(Term arg) {
     return replace(0, arg);
   }
+
+  interface StableWHNF {}
 }

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

@@ -0,0 +1,12 @@
+package org.aya.syntax.ref;
+
+import org.jetbrains.annotations.Debug;
+import org.jetbrains.annotations.NotNull;
+
+/**
+ * @author kiva
+ */
+@Debug.Renderer(hasChildren = "false", text = "name()")
+public interface AnyVar {
+  @NotNull String name();
+}

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

@@ -0,0 +1,67 @@
+package org.aya.syntax.ref;
+
+import kala.collection.immutable.ImmutableSeq;
+import org.aya.syntax.concrete.decl.Decl;
+import org.aya.syntax.core.def.Def;
+import org.aya.util.binop.Assoc;
+import org.aya.util.binop.OpDecl;
+import org.jetbrains.annotations.Contract;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+import org.jetbrains.annotations.UnknownNullability;
+
+public final class DefVar<Core extends Def, Concrete extends Decl> implements AnyVar {
+  private final @NotNull String name;
+  /** Initialized in parsing, so it might be null for deserialized user definitions. */
+  public @UnknownNullability Concrete concrete;
+  /** Initialized in type checking or core deserialization, so it might be null for unchecked user definitions. */
+  public @UnknownNullability Core core;
+  /** Initialized in the resolver or core deserialization */
+  public @Nullable ImmutableSeq<String> module;
+  public @Nullable ImmutableSeq<String> fileModule; // TODO: unify `module` and `fileModule`
+  /** Initialized in the resolver or core deserialization */
+  public @Nullable OpDecl opDecl;
+
+  @Contract(pure = true) public @Nullable Assoc assoc() {
+    if (opDecl == null) return null;
+    if (opDecl.opInfo() == null) return null;
+    return opDecl.opInfo().assoc();
+  }
+
+  @Contract(pure = true) public @NotNull String name() {
+    return name;
+  }
+
+  private DefVar(Concrete concrete, Core core, @NotNull String name) {
+    this.concrete = concrete;
+    this.core = core;
+    this.name = name;
+  }
+
+  /** Used in user definitions. */
+  public static <Core extends Def, Concrete extends Decl>
+  @NotNull DefVar<Core, Concrete> concrete(@NotNull Concrete concrete, @NotNull String name) {
+    return new DefVar<>(concrete, null, name);
+  }
+
+  /** Used in the serialization of core and primitive definitions. */
+  public static <Core extends Def, Concrete extends Decl>
+  @NotNull DefVar<Core, Concrete> empty(@NotNull String name) {
+    return new DefVar<>(null, null, name);
+  }
+
+  @Override public boolean equals(Object o) {
+    return this == o;
+  }
+
+  public boolean isInModule(@NotNull ImmutableSeq<String> moduleName) {
+    var maybeSubmodule = module;
+    if (maybeSubmodule == null) return false;
+    if (maybeSubmodule.sizeLessThan(moduleName.size())) return false;
+    return maybeSubmodule.sliceView(0, moduleName.size()).sameElements(moduleName);
+  }
+
+  public @NotNull ImmutableSeq<String> qualifiedName() {
+    return module == null ? ImmutableSeq.of(name) : module.appended(name);
+  }
+}

base/src/test/java/org/aya/syntax/core/BindTest.java

@@ -1,5 +1,9 @@
 package org.aya.syntax.core;
 
+import org.aya.syntax.core.term.AppTerm;
+import org.aya.syntax.core.term.FreeTerm;
+import org.aya.syntax.core.term.LamTerm;
+import org.aya.syntax.core.term.LocalTerm;
 import org.aya.syntax.ref.LocalVar;
 import org.aya.util.error.SourcePos;
 import org.junit.jupiter.api.Test;