locally nameless with bind

base/build.gradle.kts

@@ -0,0 +1,69 @@
+// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang.
+// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
+import org.aya.gradle.CommonTasks
+import org.aya.gradle.GenerateReflectionConfigTask
+import org.aya.gradle.GenerateVersionTask
+
+CommonTasks.nativeImageConfig(project)
+
+dependencies {
+  api(project(":tools-kala"))
+  api(project(":tools-md"))
+  api(project(":pretty"))
+  implementation(libs.aya.commonmark)
+  implementation(libs.aya.ij.core)
+  testImplementation(libs.junit.params)
+  testImplementation(libs.junit.jupiter)
+  testImplementation(libs.hamcrest)
+}
+
+plugins {
+  id("org.graalvm.buildtools.native")
+}
+
+val genDir = file("src/main/gen")
+val generateVersion = tasks.register<GenerateVersionTask>("generateVersion") {
+  basePackage = "org.aya"
+  outputDir = genDir.resolve("org/aya/prelude")
+}
+
+idea.module.generatedSourceDirs.add(genDir)
+sourceSets.main {
+  java.srcDirs(genDir)
+}
+
+tasks.compileJava { dependsOn(generateVersion) }
+tasks.sourcesJar { dependsOn(generateVersion) }
+tasks.withType<GenerateReflectionConfigTask>().configureEach {
+//  extraDir = file("src/main/java/org/aya/core/serde")
+//  classPrefixes = listOf("SerTerm", "SerPat", "SerDef", "CompiledAya")
+//  excludeNamesSuffix = listOf("SerTerm\$DeState", "CompiledAya\$CompiledAya", "CompiledAya\$Serialization")
+//  packageName = "org.aya.core.serde"
+}
+
+val cleanGenerated = tasks.register("cleanGenerated") {
+  group = "build"
+  genDir.deleteRecursively()
+}
+
+tasks.named("clean") { dependsOn(cleanGenerated) }
+
+tasks.named<Test>("test") {
+  testLogging.showStandardStreams = true
+  testLogging.showCauses = true
+  inputs.dir(projectDir.resolve("src/test/resources"))
+}
+
+tasks.register<JavaExec>("runCustomTest") {
+  group = "Execution"
+  classpath = sourceSets.test.get().runtimeClasspath
+  mainClass.set("org.aya.test.TestRunner")
+}
+
+graalvmNative {
+  CommonTasks.nativeImageBinaries(
+    project, javaToolchains, this,
+    false,
+    true
+  )
+}

base/src/main/java/org/aya/base/core/FreeTerm.java

@@ -0,0 +1,11 @@
+package org.aya.base.core;
+
+import org.aya.base.generic.LocalVar;
+import org.jetbrains.annotations.NotNull;
+
+public record FreeTerm(@NotNull LocalVar name) implements Term {
+  @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
+    if (name == var) return new LocalTerm(depth);
+    return this;
+  }
+}

base/src/main/java/org/aya/base/core/LamTerm.java

@@ -0,0 +1,10 @@
+package org.aya.base.core;
+
+import org.aya.base.generic.LocalVar;
+import org.jetbrains.annotations.NotNull;
+
+public record LamTerm(Term body) implements Term {
+  @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
+    return new LamTerm(body.bindAt(var, depth + 1));
+  }
+}

base/src/main/java/org/aya/base/core/LocalTerm.java

@@ -0,0 +1,10 @@
+package org.aya.base.core;
+
+import org.aya.base.generic.LocalVar;
+import org.jetbrains.annotations.NotNull;
+
+public record LocalTerm(int index) implements Term {
+  @Override public @NotNull Term bindAt(@NotNull LocalVar var, int depth) {
+    return this;
+  }
+}

base/src/main/java/org/aya/base/core/Term.java

@@ -0,0 +1,17 @@
+package org.aya.base.core;
+
+import org.aya.base.generic.LocalVar;
+import org.jetbrains.annotations.ApiStatus;
+import org.jetbrains.annotations.NotNull;
+
+import java.io.Serializable;
+
+public sealed interface Term extends Serializable
+  permits FreeTerm, LamTerm, LocalTerm {
+  @ApiStatus.Internal
+  @NotNull Term bindAt(@NotNull LocalVar var, int depth);
+
+  default @NotNull Term bind(@NotNull LocalVar var) {
+    return bindAt(var, 0);
+  }
+}

base/src/main/java/org/aya/base/generic/LocalVar.java

@@ -0,0 +1,15 @@
+package org.aya.base.generic;
+
+import org.aya.util.error.SourcePos;
+import org.jetbrains.annotations.NotNull;
+import org.jetbrains.annotations.Nullable;
+
+public record LocalVar(@NotNull String name, @NotNull SourcePos definition) {
+  @Override public boolean equals(@Nullable Object o) {
+    return this == o;
+  }
+
+  @Override public int hashCode() {
+    return System.identityHashCode(this);
+  }
+}