diff --git a/base/build.gradle.kts b/base/build.gradle.kts index bc3c7504..dd519b61 100644 --- a/base/build.gradle.kts +++ b/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().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,7 +43,9 @@ tasks.named("clean") { dependsOn(cleanGenerated) } tasks.named("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("runCustomTest") { @@ -59,11 +53,3 @@ tasks.register("runCustomTest") { classpath = sourceSets.test.get().runtimeClasspath mainClass.set("org.aya.test.TestRunner") } - -graalvmNative { - CommonTasks.nativeImageBinaries( - project, javaToolchains, this, - false, - true - ) -} diff --git a/base/src/main/java/org/aya/base/core/AppTerm.java b/base/src/main/java/org/aya/base/core/AppTerm.java new file mode 100644 index 00000000..b78c8bf6 --- /dev/null +++ b/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)); + } +} diff --git a/base/src/main/java/org/aya/base/core/Term.java b/base/src/main/java/org/aya/base/core/Term.java index 4190b276..09faa86e 100644 --- a/base/src/main/java/org/aya/base/core/Term.java +++ b/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); diff --git a/base/src/test/java/org/aya/base/core/BindTest.java b/base/src/test/java/org/aya/base/core/BindTest.java new file mode 100644 index 00000000..168cddda --- /dev/null +++ b/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); + } +}