add test

base/build.gradle.kts

@@ -1,10 +1,8 @@
 // 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)
+//CommonTasks.nativeImageConfig(project)
 
 dependencies {
   api(project(":tools-kala"))
@@ -34,12 +32,6 @@ sourceSets.main {
 
 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"
@@ -51,19 +43,13 @@ tasks.named("clean") { dependsOn(cleanGenerated) }
 tasks.named<Test>("test") {
   testLogging.showStandardStreams = true
   testLogging.showCauses = true
-  inputs.dir(projectDir.resolve("src/test/resources"))
+  val resources = projectDir.resolve("src/test/resources")
+  resources.mkdirs()
+  inputs.dir(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/AppTerm.java

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

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

@@ -7,7 +7,7 @@
 import java.io.Serializable;
 
 public sealed interface Term extends Serializable
-  permits FreeTerm, LamTerm, LocalTerm {
+    permits AppTerm, FreeTerm, LamTerm, LocalTerm {
   @ApiStatus.Internal
   @NotNull Term bindAt(@NotNull LocalVar var, int depth);
 

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

@@ -0,0 +1,21 @@
+package org.aya.base.core;
+
+import org.aya.base.generic.LocalVar;
+import org.aya.util.error.SourcePos;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.assertEquals;
+
+public class BindTest {
+  @Test public void simpleBind() {
+    // λx. λy. x y
+    var x = new LocalVar("x", SourcePos.NONE);
+    var y = new LocalVar("y", SourcePos.NONE);
+    var body = new AppTerm(new FreeTerm(x), new FreeTerm(y));
+    var lamYXY = new LamTerm(body.bind(y));
+    var lamXYXY = new LamTerm(lamYXY.bind(x));
+    // λ. λ. 1 0
+    var expect = new LamTerm(new LamTerm(new AppTerm(new LocalTerm(1), new LocalTerm(0))));
+    assertEquals(expect, lamXYXY);
+  }
+}