diff --git a/cli-impl/src/main/java/org/aya/cli/library/incremental/DiskCompilerAdvisor.java b/cli-impl/src/main/java/org/aya/cli/library/incremental/DiskCompilerAdvisor.java index ec0a130ee3..5682f48635 100644 --- a/cli-impl/src/main/java/org/aya/cli/library/incremental/DiskCompilerAdvisor.java +++ b/cli-impl/src/main/java/org/aya/cli/library/incremental/DiskCompilerAdvisor.java @@ -19,11 +19,13 @@ import org.jetbrains.annotations.Nullable; import javax.tools.ToolProvider; +import java.io.File; import java.io.IOException; import java.net.URL; import java.net.URLClassLoader; import java.nio.file.Files; import java.nio.file.Path; +import java.util.List; public class DiskCompilerAdvisor implements CompilerAdvisor { @Override public boolean isSourceModified(@NotNull LibrarySource source) { @@ -87,14 +89,18 @@ public class DiskCompilerAdvisor implements CompilerAdvisor { .serialize(new FileSerializer.FileResult(file.moduleName().dropLast(1), new ModuleSerializer.ModuleResult( name, defs.filterIsInstance(TopLevelDef.class), ImmutableSeq.empty()))) .result(); - var javaSrcPath = FileUtil.resolveFile(computeBaseDir(file.owner()).resolve(AyaSerializer.PACKAGE_BASE), + var baseDir = computeBaseDir(file.owner()).toAbsolutePath(); + var javaSrcPath = FileUtil.resolveFile(baseDir.resolve(AyaSerializer.PACKAGE_BASE), file.moduleName().module(), ".java"); FileUtil.writeString(javaSrcPath, javaCode); var compiler = ToolProvider.getSystemJavaCompiler(); var fileManager = compiler.getStandardFileManager(null, null, null); var compilationUnits = fileManager.getJavaFileObjects(javaSrcPath); - var task = compiler.getTask(null, fileManager, null, null, null, compilationUnits); + var classpath = System.getProperty("java.class.path"); + var options = List.of("-classpath", baseDir + File.pathSeparator + classpath); + var task = compiler.getTask(null, fileManager, null, options, null, compilationUnits); task.call(); + Files.delete(javaSrcPath); var coreFile = file.compiledCorePath(); CompilerUtil.saveCompiledCore(coreFile, resolveInfo); } diff --git a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java index 4154a817b7..5d56f2901f 100644 --- a/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java +++ b/cli-impl/src/test/java/org/aya/test/cli/ReplCompilerTest.java @@ -29,9 +29,9 @@ public class ReplCompilerTest { @Test public void library() throws IOException { compiler.loadToContext(Paths.get("../ide-lsp", "src", "test", "resources", "lsp-test-lib")); - assertNotNull(findContext("NatCore::zero")); - assertNotNull(findContext("Vec::vnil")); - assertNotNull(findContext("Vec:::>")); + assertNotNull(findContext("Nat::Core::zero")); + assertNotNull(findContext("VecCore::vnil")); + assertNotNull(findContext("VecCore:::>")); } @Test public void simpleExpr() { compile("Set"); } @@ -51,15 +51,15 @@ public class ReplCompilerTest { assertNull(findContext("a")); } - // /** Bug report */ - // @Test public void reportedInSpace() { - // // success cases, we can find the definition in the context - // compile("data Unit | unit"); - // assertNotNull(findContext("Unit")); - // compile("data What | what : Unit"); - // assertNotNull(findContext("What")); - // assertNotNull(findContext("Unit")); - // } + /** Bug report */ + @Test public void reportedInSpace() { + // success cases, we can find the definition in the context + compile("data Unit | unit"); + assertNotNull(findContext("Unit")); + compile("data What | what"); + assertNotNull(findContext("What")); + assertNotNull(findContext("Unit")); + } private @Nullable AnyVar findContext(@NotNull String name) { try { diff --git a/ide-lsp/src/test/java/org/aya/lsp/LspTest.java b/ide-lsp/src/test/java/org/aya/lsp/LspTest.java index f04a973f21..c5d43ce5c9 100644 --- a/ide-lsp/src/test/java/org/aya/lsp/LspTest.java +++ b/ide-lsp/src/test/java/org/aya/lsp/LspTest.java @@ -52,7 +52,7 @@ public class LspTest { @Test public void test541() { launch(TEST_LIB).execute(compile((a, _) -> { var testOpt = a.lastCompiled() - .filter(x -> x.moduleName().module().getLast().equals("Vec")) + .filter(x -> x.moduleName().module().getLast().equals("VecCore")) .flatMap(x -> x.program().get()) .filterIsInstance(FnDecl.class) .filter(x -> x.ref.name().equals("test")) @@ -74,8 +74,8 @@ public class LspTest { compile((_, _) -> {}), mutate("HelloWorld"), compile((a, e) -> assertRemake(a, e, "HelloWorld")), - mutate("NatCore"), - compile((a, e) -> assertRemake(a, e, "NatCore", "Vec", "HelloWorld")), + mutate("Nat::Core"), + compile((a, e) -> assertRemake(a, e, "Nat::Core", "VecCore", "HelloWorld")), mutate("PathPrims"), compile((a, e) -> assertRemake(a, e, "PathPrims", "Path", "HelloWorld")) ); @@ -90,19 +90,19 @@ public class LspTest { client.execute(compile((_, _) -> {})); var param = new TextDocumentPositionParams(new TextDocumentIdentifier( - TEST_LIB.resolve("src").resolve("NatCore.aya").toUri()), + TEST_LIB.resolve("src/Nat/Core.aya").toUri()), new Position(0, 18) ); var result0 = client.service.hover(param); assertTrue(result0.isPresent()); - assertEquals("Nat", result0.get().contents.getFirst().value); + assertEquals("Nat", result0.get().contents.getFirst().value); client.service.updateServerOptions(new ServerOptions(new ServerRenderOptions("IntelliJ", null, RenderOptions.OutputTarget.HTML))); var result1 = client.service.hover(param); assertTrue(result1.isPresent()); - assertEquals("Nat", result1.get().contents.getFirst().value); + assertEquals("Nat", result1.get().contents.getFirst().value); } private void logTime(long time) { diff --git a/ide-lsp/src/test/resources/lsp-test-lib/src/HelloWorld.aya b/ide-lsp/src/test/resources/lsp-test-lib/src/HelloWorld.aya index a4ab1e49e8..f2f184d828 100644 --- a/ide-lsp/src/test/resources/lsp-test-lib/src/HelloWorld.aya +++ b/ide-lsp/src/test/resources/lsp-test-lib/src/HelloWorld.aya @@ -1,4 +1,4 @@ -open import NatCore +open import Nat::Core open import Path open import StringPrims using ( String diff --git a/ide-lsp/src/test/resources/lsp-test-lib/src/NatCore.aya b/ide-lsp/src/test/resources/lsp-test-lib/src/Nat/Core.aya similarity index 100% rename from ide-lsp/src/test/resources/lsp-test-lib/src/NatCore.aya rename to ide-lsp/src/test/resources/lsp-test-lib/src/Nat/Core.aya diff --git a/ide-lsp/src/test/resources/lsp-test-lib/src/Vec.aya b/ide-lsp/src/test/resources/lsp-test-lib/src/VecCore.aya similarity index 94% rename from ide-lsp/src/test/resources/lsp-test-lib/src/Vec.aya rename to ide-lsp/src/test/resources/lsp-test-lib/src/VecCore.aya index d07a82ac1c..cc0a95b7cd 100644 --- a/ide-lsp/src/test/resources/lsp-test-lib/src/Vec.aya +++ b/ide-lsp/src/test/resources/lsp-test-lib/src/VecCore.aya @@ -1,4 +1,4 @@ -open import NatCore +open import Nat::Core open data Vec Type Nat : Type | A, 0 => vnil diff --git a/jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java index ae168d2473..a7d6291d33 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java +++ b/jit-compiler/src/main/java/org/aya/compiler/JitTeleSerializer.java @@ -123,7 +123,7 @@ protected void buildConstructor(@NotNull T def, @NotNull ImmutableSeq ex buildSuperCall(ImmutableSeq.of( Integer.toString(size), makeArrayFrom("boolean", licit.toImmutableSeq()), - makeArrayFrom("String", names.toImmutableArray()) + makeArrayFrom("java.lang.String", names.toImmutableArray()) ).appendedAll(ext)); } diff --git a/jit-compiler/src/main/java/org/aya/compiler/PrimSerializer.java b/jit-compiler/src/main/java/org/aya/compiler/PrimSerializer.java index 7468081fea..471faa49ad 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/PrimSerializer.java +++ b/jit-compiler/src/main/java/org/aya/compiler/PrimSerializer.java @@ -12,7 +12,7 @@ public PrimSerializer(@NotNull AbstractSerializer parent) { super(parent, JitPrim.class); } @Override protected void buildConstructor(PrimDef unit) { - super.buildConstructor(unit, ImmutableSeq.of("id")); + super.buildConstructor(unit, ImmutableSeq.of(STR."org.aya.syntax.core.def.PrimDef.ID.\{unit.id.name()}")); } @Override public AyaSerializer serialize(PrimDef unit) { buildFramework(unit, () -> { }); diff --git a/syntax/src/main/java/org/aya/syntax/compile/JitPrim.java b/syntax/src/main/java/org/aya/syntax/compile/JitPrim.java index 9b1a41ec71..756eb53499 100644 --- a/syntax/src/main/java/org/aya/syntax/compile/JitPrim.java +++ b/syntax/src/main/java/org/aya/syntax/compile/JitPrim.java @@ -7,6 +7,7 @@ import org.aya.syntax.core.def.PrimDef; import org.aya.syntax.core.def.PrimDefLike; import org.aya.syntax.core.term.Term; +import org.aya.util.error.Panic; import org.jetbrains.annotations.NotNull; public abstract non-sealed class JitPrim extends JitDef implements PrimDefLike, Reducible { @@ -17,8 +18,7 @@ protected JitPrim(int telescopeSize, boolean[] telescopeLicit, String[] telescop this.id = id; } - /** - * Unfold this function - */ - @Override public abstract Term invoke(Term stuck, @NotNull Seq args); + @Override public Term invoke(Term stuck, @NotNull Seq args) { + throw new Panic("Should not be called"); + } }