From ca78dbc62021b8343267cde1937d0f9b92f80afa Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sat, 30 Nov 2024 07:02:06 +0800 Subject: [PATCH 1/8] moduleLoader: extract --- .../incremental/DiskCompilerAdvisor.java | 26 ++++++++++++++----- .../java/org/aya/cli/utils/CompilerUtil.java | 4 ++- 2 files changed, 22 insertions(+), 8 deletions(-) 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 2f66dff3b..02a3cef1f 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 @@ -80,6 +80,22 @@ public void addURL(Path url) throws MalformedURLException { @Override public void clearModuleOutput(@NotNull LibrarySource source) throws IOException { Files.deleteIfExists(source.compiledCorePath()); } + + private @NotNull ResolveInfo doLoadCompiledCore( + @NotNull CompiledModule compiledAya, + @NotNull Reporter reporter, + @NotNull ModulePath mod, + @NotNull Path sourcePath, + @NotNull Path libraryRoot, + @NotNull ModuleLoader recurseLoader + ) throws ClassNotFoundException, MalformedURLException { + var context = new EmptyContext(reporter, sourcePath).derive(mod); + var coreDir = computeBaseDir(libraryRoot); + cl.addURL(coreDir); + cl.loadClass(NameSerializer.getModuleReference(QPath.fileLevel(mod))); + return compiledAya.toResolveInfo(recurseLoader, context, cl); + } + @Override public @Nullable ResolveInfo doLoadCompiledCore( @NotNull Reporter reporter, @NotNull LibraryOwner owner, @NotNull ModulePath mod, @@ -90,16 +106,12 @@ public void addURL(Path url) throws MalformedURLException { if (corePath == null || sourcePath == null) return null; if (!Files.exists(corePath)) return null; - var context = new EmptyContext(reporter, sourcePath).derive(mod); try (var inputStream = FileUtil.ois(corePath)) { var compiledAya = (CompiledModule) inputStream.readObject(); var parentCount = mod.size(); - var baseDir = corePath; - for (int i = 0; i < parentCount; i++) baseDir = baseDir.getParent(); - baseDir = computeBaseDir(baseDir); - cl.addURL(baseDir); - cl.loadClass(NameSerializer.getModuleReference(QPath.fileLevel(mod))); - return compiledAya.toResolveInfo(recurseLoader, context, cl); + var libraryRoot = corePath; + for (int i = 0; i < parentCount; i++) libraryRoot = libraryRoot.getParent(); + return doLoadCompiledCore(compiledAya, reporter, mod, sourcePath, libraryRoot, recurseLoader); } } diff --git a/cli-impl/src/main/java/org/aya/cli/utils/CompilerUtil.java b/cli-impl/src/main/java/org/aya/cli/utils/CompilerUtil.java index 2591fd5c1..0a8755fd2 100644 --- a/cli-impl/src/main/java/org/aya/cli/utils/CompilerUtil.java +++ b/cli-impl/src/main/java/org/aya/cli/utils/CompilerUtil.java @@ -44,7 +44,7 @@ public static int catching( } } - public static void saveCompiledCore( + public static @NotNull CompiledModule saveCompiledCore( @NotNull Path coreFile, @NotNull ImmutableSeq defs, @NotNull ResolveInfo resolveInfo ) throws IOException { @@ -52,6 +52,8 @@ public static void saveCompiledCore( try (var outputStream = coreWriter(coreFile)) { outputStream.writeObject(compiledAya); } + + return compiledAya; } private static @NotNull ObjectOutputStream coreWriter(@NotNull Path coreFile) throws IOException { From 3bfda228d7403738e645e28e9e2b75f183121aad Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Mon, 2 Dec 2024 03:13:05 +0800 Subject: [PATCH 2/8] lib: trying to use compiled ResolveInfo right after tyck --- .../java/org/aya/resolve/ResolveInfo.java | 4 +++ .../aya/cli/library/LibraryModuleLoader.java | 20 +++++++++---- .../library/incremental/CompilerAdvisor.java | 28 ++++++++++++++----- .../incremental/DelegateCompilerAdvisor.java | 6 ++-- .../incremental/DiskCompilerAdvisor.java | 24 ++++++++++++---- .../incremental/InMemoryCompilerAdvisor.java | 7 +++-- .../lsp/tester/LspTestCompilerAdvisor.java | 6 ++-- 7 files changed, 70 insertions(+), 25 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/ResolveInfo.java b/base/src/main/java/org/aya/resolve/ResolveInfo.java index 014548a7d..34508753f 100644 --- a/base/src/main/java/org/aya/resolve/ResolveInfo.java +++ b/base/src/main/java/org/aya/resolve/ResolveInfo.java @@ -116,6 +116,10 @@ public void open(@NotNull ResolveInfo other, @NotNull SourcePos sourcePos, @NotN }); } + public @NotNull Reporter reporter() { + return this.opSet.reporter; + } + @Debug.Renderer(text = "opInfo.name()") public record RenamedOpDecl(@NotNull OpInfo opInfo) implements OpDecl { } } diff --git a/cli-impl/src/main/java/org/aya/cli/library/LibraryModuleLoader.java b/cli-impl/src/main/java/org/aya/cli/library/LibraryModuleLoader.java index 11f3aefb2..0828270f6 100644 --- a/cli-impl/src/main/java/org/aya/cli/library/LibraryModuleLoader.java +++ b/cli-impl/src/main/java/org/aya/cli/library/LibraryModuleLoader.java @@ -74,11 +74,19 @@ record LibraryModuleLoader( assert program != null; var context = new EmptyContext(reporter, sourcePath).derive(mod); var resolveInfo = resolveModule(states.primFactory, context, program, recurseLoader); - source.resolveInfo().set(resolveInfo); - return tyckModule(resolveInfo, (moduleResolve, defs) -> { + tyckModule(resolveInfo, (moduleResolve, defs) -> { source.notifyTycked(moduleResolve, defs); - if (reporter.noError()) saveCompiledCore(source, moduleResolve, defs); + if (reporter.noError()) saveCompiledCore(source, moduleResolve, defs, recurseLoader); }); + + @Nullable var tyckedInfo = source.resolveInfo().get(); + // I know we can set resolveInfo before the tyckModule, but that doesn't tell the goal of the code. + if (tyckedInfo == null) { + // this happens if [saveCompiledCore] meets an exception, use fallback ResolveInfo + tyckedInfo = resolveInfo; + } + + return tyckedInfo; } @Override @@ -96,9 +104,11 @@ public boolean existsFileLevelModule(@NotNull ModulePath path) { private void saveCompiledCore( @NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, - @NotNull ImmutableSeq defs + @NotNull ImmutableSeq defs, + @NotNull ModuleLoader recurseLoader ) { - advisor.saveCompiledCore(file, resolveInfo, defs); + var info = advisor.saveCompiledCore(file, resolveInfo, defs, recurseLoader); + file.resolveInfo().set(info); } record United(@NotNull PrimFactory primFactory) { diff --git a/cli-impl/src/main/java/org/aya/cli/library/incremental/CompilerAdvisor.java b/cli-impl/src/main/java/org/aya/cli/library/incremental/CompilerAdvisor.java index 17aed8a39..604cf292b 100644 --- a/cli-impl/src/main/java/org/aya/cli/library/incremental/CompilerAdvisor.java +++ b/cli-impl/src/main/java/org/aya/cli/library/incremental/CompilerAdvisor.java @@ -69,11 +69,19 @@ default void notifyIncrementalJob( @NotNull ModuleLoader recurseLoader ) throws IOException, ClassNotFoundException; - void doSaveCompiledCore( + /** + * Save the well-typed defs as compiled defs + * + * @param file the source file + * @param resolveInfo the resolve info of the module + * @param defs the well-typed definitions + */ + @Nullable ResolveInfo doSaveCompiledCore( @NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, - @NotNull ImmutableSeq defs - ) throws IOException; + @NotNull ImmutableSeq defs, + @NotNull ModuleLoader recurseLoader + ) throws IOException, ClassNotFoundException; @ApiStatus.NonExtendable default @Nullable ResolveInfo loadCompiledCore( @@ -91,17 +99,23 @@ void doSaveCompiledCore( } } + /** + * @see #doSaveCompiledCore + */ @ApiStatus.NonExtendable - default void saveCompiledCore( + default @Nullable ResolveInfo saveCompiledCore( @NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, - @NotNull ImmutableSeq defs + @NotNull ImmutableSeq defs, + @NotNull ModuleLoader recurseLoader ) { try { - doSaveCompiledCore(file, resolveInfo, defs); + var info = doSaveCompiledCore(file, resolveInfo, defs, recurseLoader); updateLastModified(file); - } catch (IOException e) { + return info; + } catch (IOException | ClassNotFoundException e) { e.printStackTrace(); + return null; } } diff --git a/cli-impl/src/main/java/org/aya/cli/library/incremental/DelegateCompilerAdvisor.java b/cli-impl/src/main/java/org/aya/cli/library/incremental/DelegateCompilerAdvisor.java index b19e48e17..5e2f6c4ae 100644 --- a/cli-impl/src/main/java/org/aya/cli/library/incremental/DelegateCompilerAdvisor.java +++ b/cli-impl/src/main/java/org/aya/cli/library/incremental/DelegateCompilerAdvisor.java @@ -56,9 +56,9 @@ public void notifyIncrementalJob(@NotNull ImmutableSeq modified, return delegate.doLoadCompiledCore(reporter, owner, mod, sourcePath, corePath, recurseLoader); } - @Override public void - doSaveCompiledCore(@NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs) throws IOException { - delegate.doSaveCompiledCore(file, resolveInfo, defs); + @Override public @Nullable ResolveInfo + doSaveCompiledCore(@NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs, @NotNull ModuleLoader recurseLoader) throws IOException, ClassNotFoundException { + return delegate.doSaveCompiledCore(file, resolveInfo, defs, recurseLoader); } @Override public void close() throws Exception { delegate.close(); 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 02a3cef1f..d994c2d14 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 @@ -81,6 +81,11 @@ public void addURL(Path url) throws MalformedURLException { Files.deleteIfExists(source.compiledCorePath()); } + /** + * Load all core file to the ClassLoader + * + * @return a compiled ResolveInfo + */ private @NotNull ResolveInfo doLoadCompiledCore( @NotNull CompiledModule compiledAya, @NotNull Reporter reporter, @@ -115,17 +120,19 @@ public void addURL(Path url) throws MalformedURLException { } } - @Override public void doSaveCompiledCore( + @Override public @Nullable ResolveInfo doSaveCompiledCore( @NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, - @NotNull ImmutableSeq defs - ) throws IOException { + @NotNull ImmutableSeq defs, + @NotNull ModuleLoader recurseLoader + ) throws IOException, ClassNotFoundException { var javaCode = new FileSerializer(resolveInfo.shapeFactory()) .serialize(new ModuleSerializer.ModuleResult( QPath.fileLevel(file.moduleName()), defs.filterIsInstance(TopLevelDef.class))) .result(); - var baseDir = computeBaseDir(file.owner().outDir()).toAbsolutePath(); + var libraryRoot = file.owner().outDir(); + var baseDir = computeBaseDir(libraryRoot).toAbsolutePath(); var relativePath = NameSerializer.getReference(QPath.fileLevel(file.moduleName()), null, NameSerializer.NameType.ClassPath) + ".java"; var javaSrcPath = baseDir.resolve(relativePath); @@ -152,7 +159,14 @@ public void addURL(Path url) throws MalformedURLException { task.call(); if (Global.DELETE_JIT_JAVA_SOURCE) Files.delete(javaSrcPath); var coreFile = file.compiledCorePath(); - CompilerUtil.saveCompiledCore(coreFile, defs, resolveInfo); + + // save compiled core and load compiled ResolveInfo + var coreMod = CompilerUtil.saveCompiledCore(coreFile, defs, resolveInfo); + return doLoadCompiledCore( + coreMod, resolveInfo.reporter(), + resolveInfo.thisModule().modulePath(), file.underlyingFile(), libraryRoot, + recurseLoader + ); } private static @NotNull Path computeBaseDir(@NotNull Path outDir) { diff --git a/cli-impl/src/main/java/org/aya/cli/library/incremental/InMemoryCompilerAdvisor.java b/cli-impl/src/main/java/org/aya/cli/library/incremental/InMemoryCompilerAdvisor.java index 8c07c0d3d..bb9f6535e 100644 --- a/cli-impl/src/main/java/org/aya/cli/library/incremental/InMemoryCompilerAdvisor.java +++ b/cli-impl/src/main/java/org/aya/cli/library/incremental/InMemoryCompilerAdvisor.java @@ -71,12 +71,13 @@ public class InMemoryCompilerAdvisor implements CompilerAdvisor { return compiledCore.getOrNull(mod); } - @Override public void doSaveCompiledCore( + @Override public @Nullable ResolveInfo doSaveCompiledCore( @NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, - @NotNull ImmutableSeq defs - ) { + @NotNull ImmutableSeq defs, + @NotNull ModuleLoader recurseLoader) { // TODO: what if module name clashes? compiledCore.put(file.moduleName(), resolveInfo); + return resolveInfo; } } diff --git a/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java b/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java index c946b3639..442ad0637 100644 --- a/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java +++ b/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java @@ -8,6 +8,7 @@ import org.aya.cli.library.incremental.InMemoryCompilerAdvisor; import org.aya.cli.library.source.LibrarySource; import org.aya.resolve.ResolveInfo; +import org.aya.resolve.module.ModuleLoader; import org.aya.syntax.core.def.TyckDef; import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; @@ -39,8 +40,9 @@ public void notifyIncrementalJob(@NotNull ImmutableSeq modified, } @Override - public void doSaveCompiledCore(@NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs) { - super.doSaveCompiledCore(file, resolveInfo, defs); + public @Nullable ResolveInfo doSaveCompiledCore(@NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs, @NotNull ModuleLoader recurseLoader) { + var info = super.doSaveCompiledCore(file, resolveInfo, defs, recurseLoader); newlyCompiled.append(resolveInfo); + return info; } } From ff3aba5585dbecccbfce9acc09f3a21ce8cb29d0 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Sun, 1 Dec 2024 16:40:53 -0500 Subject: [PATCH 3/8] syntax: make bind block use `AnyDefVar` --- .../src/main/java/org/aya/compiler/CompiledModule.java | 6 +++--- .../main/java/org/aya/syntax/concrete/stmt/BindBlock.java | 7 +++---- 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java b/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java index 1456e3111..57f926584 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java +++ b/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java @@ -18,7 +18,7 @@ import org.aya.syntax.compile.JitFn; import org.aya.syntax.compile.JitPrim; import org.aya.syntax.concrete.stmt.*; -import org.aya.syntax.core.def.TyckAnyDef; +import org.aya.syntax.core.def.AnyDef; import org.aya.syntax.core.def.TyckDef; import org.aya.syntax.core.repr.AyaShape; import org.aya.syntax.core.repr.ShapeRecognition; @@ -149,8 +149,8 @@ private void serOp(@NotNull TyckDef def) { private @NotNull SerBind serBind(@NotNull BindBlock bindBlock) { if (bindBlock == BindBlock.EMPTY) return SerBind.EMPTY; - var loosers = bindBlock.resolvedLoosers().get().map(x -> TyckAnyDef.make(x.core).qualifiedName()); - var tighters = bindBlock.resolvedTighters().get().map(x -> TyckAnyDef.make(x.core).qualifiedName()); + var loosers = bindBlock.resolvedLoosers().get().map(x -> AnyDef.fromVar(x).qualifiedName()); + var tighters = bindBlock.resolvedTighters().get().map(x -> AnyDef.fromVar(x).qualifiedName()); return new SerBind(loosers, tighters); } } diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/BindBlock.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/BindBlock.java index a26e32197..2c940f4f1 100644 --- a/syntax/src/main/java/org/aya/syntax/concrete/stmt/BindBlock.java +++ b/syntax/src/main/java/org/aya/syntax/concrete/stmt/BindBlock.java @@ -4,7 +4,7 @@ import kala.collection.immutable.ImmutableSeq; import kala.value.MutableValue; -import org.aya.syntax.ref.DefVar; +import org.aya.syntax.ref.AnyDefVar; import org.aya.util.ForLSP; import org.aya.util.error.SourcePos; import org.jetbrains.annotations.NotNull; @@ -13,9 +13,8 @@ public record BindBlock( @Override @NotNull SourcePos sourcePos, @NotNull ImmutableSeq loosers, @NotNull ImmutableSeq tighters, - // TODO: make AnyVar - @ForLSP @NotNull MutableValue>> resolvedLoosers, - @ForLSP @NotNull MutableValue>> resolvedTighters + @ForLSP @NotNull MutableValue> resolvedLoosers, + @ForLSP @NotNull MutableValue> resolvedTighters ) { public static final @NotNull BindBlock EMPTY = new BindBlock(SourcePos.NONE, ImmutableSeq.empty(), ImmutableSeq.empty(), MutableValue.create(), MutableValue.create()); From 2246c4fec4f4c37c9bd24d7a35f6d7fd0b77b020 Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Mon, 2 Dec 2024 05:49:24 +0800 Subject: [PATCH 4/8] fix: compile (both java and aya) --- .../org/aya/resolve/visitor/StmtBinder.java | 5 ++-- .../org/aya/compiler/TermExprializer.java | 2 +- .../java/org/aya/prettier/BasePrettier.java | 29 +++++++++++++++++++ 3 files changed, 33 insertions(+), 3 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtBinder.java b/base/src/main/java/org/aya/resolve/visitor/StmtBinder.java index 42d007a4b..831a0e69d 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtBinder.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtBinder.java @@ -13,6 +13,7 @@ import org.aya.syntax.concrete.stmt.decl.DataDecl; import org.aya.syntax.concrete.stmt.decl.FnDecl; import org.aya.syntax.concrete.stmt.decl.PrimDecl; +import org.aya.syntax.ref.AnyDefVar; import org.aya.syntax.ref.DefVar; import org.aya.util.binop.OpDecl; import org.aya.util.error.Panic; @@ -37,7 +38,7 @@ public void bind(@NotNull Context ctx, @NotNull BindBlock bindBlock, OpDecl self bind(self, ctx, OpDecl.BindPred.Tighter, tighter))); } - private @Nullable DefVar bind( + private @Nullable AnyDefVar bind( @NotNull OpDecl self, @NotNull Context ctx, @NotNull OpDecl.BindPred pred, @NotNull QualifiedID id ) throws Context.ResolvingInterruptedException { @@ -45,7 +46,7 @@ public void bind(@NotNull Context ctx, @NotNull BindBlock bindBlock, OpDecl self var opDecl = info.resolveOpDecl(var); if (opDecl != null) { info.opSet().bind(self, pred, opDecl, id.sourcePos()); - return var instanceof DefVar defVar ? defVar : null; + return var instanceof AnyDefVar defVar ? defVar : null; } // make compiler happy 😥 diff --git a/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java b/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java index 8b62f0481..8e568f2a5 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java +++ b/jit-compiler/src/main/java/org/aya/compiler/TermExprializer.java @@ -221,7 +221,7 @@ case EqTerm(var A, var a, var b) -> ExprializeUtils.makeNew(ExprializeUtils.getJ case DimTyTerm _ -> ExprializeUtils.getInstance(ExprializeUtils.getJavaRef(DimTyTerm.class)); case DimTerm dim -> ExprializeUtils.makeSub(ExprializeUtils.getJavaRef(DimTerm.class), dim.name()); case TupTerm(var l, var r) -> ExprializeUtils.makeNew(ExprializeUtils.getJavaRef(TupTerm.class), - serializeToImmutableSeq(CLASS_TERM, ImmutableSeq.of(l, r)) + doSerialize(l), doSerialize(r) ); case PrimCall(var ref, var ulift, var args) -> ExprializeUtils.makeNew(CLASS_PRIMCALL, ExprializeUtils.getInstance(NameSerializer.getClassRef(ref)), diff --git a/syntax/src/main/java/org/aya/prettier/BasePrettier.java b/syntax/src/main/java/org/aya/prettier/BasePrettier.java index c980dcc95..bea03e247 100644 --- a/syntax/src/main/java/org/aya/prettier/BasePrettier.java +++ b/syntax/src/main/java/org/aya/prettier/BasePrettier.java @@ -309,6 +309,11 @@ protected boolean optionImplicit() { if (ref instanceof DefVar defVar && defVar.module != null) { return linkIdOf(currentFileModule, new TyckAnyDef<>(defVar)); } + + if (ref instanceof CompiledVar(JitDef core)) { + return linkIdOf(currentFileModule, core); + } + return Link.loc(ref.hashCode()); } @@ -334,22 +339,46 @@ protected boolean optionImplicit() { return Doc.linkDef(Doc.plain(ref.name()), linkIdOf(null, ref)); } + public static @NotNull Doc refVar(@NotNull AnyDefVar ref) { + return switch (ref) { + case CompiledVar compiledVar -> refVar(compiledVar); + case DefVar defVar -> refVar(defVar); + }; + } + public static @NotNull Doc refVar(DefVar ref) { var style = chooseStyle(ref); return style != null ? linkRef(ref, style) : varDoc(ref); } + public static @NotNull Doc refVar(CompiledVar ref) { + var style = chooseStyle(ref); + return style != null ? linkRef(ref, style) : varDoc(ref); + } + public static @NotNull Doc refVar(AnyDef ref) { var style = chooseStyle(ref); assert style != null; return linkRef(ref, style); } + public static @NotNull Doc defVar(@NotNull AnyDefVar ref) { + return switch (ref) { + case CompiledVar compiledVar -> defVar(compiledVar); + case DefVar defVar -> defVar(defVar); + }; + } + public static @NotNull Doc defVar(DefVar ref) { var style = chooseStyle(ref.concrete); return style != null ? linkDef(ref, style) : varDoc(ref); } + public static @NotNull Doc defVar(CompiledVar ref) { + var style = chooseStyle(ref.core()); + return style != null ? linkDef(ref, style) : varDoc(ref); + } + protected static @Nullable Style chooseStyle(Object obj) { return switch (obj) { case DefVar d -> chooseStyle(d.concrete); From a7a38b75caec10f9d3362ed7709e7657b3f23ed7 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Mon, 2 Dec 2024 23:57:54 -0500 Subject: [PATCH 5/8] compile: now `doSaveCompiledCore` returns `NotNull` --- .../main/java/org/aya/resolve/module/ModuleCallback.java | 2 +- base/src/test/java/org/aya/tyck/TyckTest.java | 2 +- .../java/org/aya/cli/library/LibraryModuleLoader.java | 9 +++------ .../org/aya/cli/library/incremental/CompilerAdvisor.java | 8 +++++--- .../cli/library/incremental/DelegateCompilerAdvisor.java | 2 +- .../aya/cli/library/incremental/DiskCompilerAdvisor.java | 2 +- .../cli/library/incremental/InMemoryCompilerAdvisor.java | 5 +++-- .../main/java/org/aya/cli/single/SingleFileCompiler.java | 8 ++++---- .../java/org/aya/lsp/tester/LspTestCompilerAdvisor.java | 8 ++++---- jit-compiler/src/test/java/CompileTest.java | 2 +- 10 files changed, 24 insertions(+), 24 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/module/ModuleCallback.java b/base/src/main/java/org/aya/resolve/module/ModuleCallback.java index 87c8434d2..a8e8aa397 100644 --- a/base/src/main/java/org/aya/resolve/module/ModuleCallback.java +++ b/base/src/main/java/org/aya/resolve/module/ModuleCallback.java @@ -9,6 +9,6 @@ @FunctionalInterface public interface ModuleCallback { - void onModuleTycked(@NotNull ResolveInfo moduleResolve, @NotNull ImmutableSeq defs) + void onModuleTycked(@NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs) throws E; } diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java index b70af5701..4f87d35f2 100644 --- a/base/src/test/java/org/aya/tyck/TyckTest.java +++ b/base/src/test/java/org/aya/tyck/TyckTest.java @@ -222,7 +222,7 @@ public static TyckResult tyck(@Language("Aya") @NotNull String code) { var moduleLoader = SyntaxTestUtil.moduleLoader(); var callback = new ModuleCallback() { ImmutableSeq ok; - @Override public void onModuleTycked(@NotNull ResolveInfo x, @NotNull ImmutableSeq defs) { ok = defs; } + @Override public void onModuleTycked(@NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs) { ok = defs; } }; var info = moduleLoader.tyckModule(moduleLoader.resolve(SyntaxTestUtil.parse(code)), callback); return new TyckResult(callback.ok, info); diff --git a/cli-impl/src/main/java/org/aya/cli/library/LibraryModuleLoader.java b/cli-impl/src/main/java/org/aya/cli/library/LibraryModuleLoader.java index 0828270f6..7408c1ec5 100644 --- a/cli-impl/src/main/java/org/aya/cli/library/LibraryModuleLoader.java +++ b/cli-impl/src/main/java/org/aya/cli/library/LibraryModuleLoader.java @@ -89,8 +89,7 @@ record LibraryModuleLoader( return tyckedInfo; } - @Override - public boolean existsFileLevelModule(@NotNull ModulePath path) { + @Override public boolean existsFileLevelModule(@NotNull ModulePath path) { return owner.findModule(path) != null; } @@ -102,10 +101,8 @@ public boolean existsFileLevelModule(@NotNull ModulePath path) { } private void saveCompiledCore( - @NotNull LibrarySource file, - @NotNull ResolveInfo resolveInfo, - @NotNull ImmutableSeq defs, - @NotNull ModuleLoader recurseLoader + @NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, + @NotNull ImmutableSeq defs, @NotNull ModuleLoader recurseLoader ) { var info = advisor.saveCompiledCore(file, resolveInfo, defs, recurseLoader); file.resolveInfo().set(info); diff --git a/cli-impl/src/main/java/org/aya/cli/library/incremental/CompilerAdvisor.java b/cli-impl/src/main/java/org/aya/cli/library/incremental/CompilerAdvisor.java index 604cf292b..53b56fe94 100644 --- a/cli-impl/src/main/java/org/aya/cli/library/incremental/CompilerAdvisor.java +++ b/cli-impl/src/main/java/org/aya/cli/library/incremental/CompilerAdvisor.java @@ -76,7 +76,7 @@ default void notifyIncrementalJob( * @param resolveInfo the resolve info of the module * @param defs the well-typed definitions */ - @Nullable ResolveInfo doSaveCompiledCore( + @NotNull ResolveInfo doSaveCompiledCore( @NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs, @@ -100,22 +100,24 @@ default void notifyIncrementalJob( } /** + * @return possibly the compiled version of the {@link ResolveInfo} * @see #doSaveCompiledCore */ @ApiStatus.NonExtendable - default @Nullable ResolveInfo saveCompiledCore( + default @NotNull ResolveInfo saveCompiledCore( @NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs, @NotNull ModuleLoader recurseLoader ) { + assert recurseLoader instanceof CachedModuleLoader; try { var info = doSaveCompiledCore(file, resolveInfo, defs, recurseLoader); updateLastModified(file); return info; } catch (IOException | ClassNotFoundException e) { e.printStackTrace(); - return null; + return resolveInfo; } } diff --git a/cli-impl/src/main/java/org/aya/cli/library/incremental/DelegateCompilerAdvisor.java b/cli-impl/src/main/java/org/aya/cli/library/incremental/DelegateCompilerAdvisor.java index 5e2f6c4ae..5c54eb3b6 100644 --- a/cli-impl/src/main/java/org/aya/cli/library/incremental/DelegateCompilerAdvisor.java +++ b/cli-impl/src/main/java/org/aya/cli/library/incremental/DelegateCompilerAdvisor.java @@ -56,7 +56,7 @@ public void notifyIncrementalJob(@NotNull ImmutableSeq modified, return delegate.doLoadCompiledCore(reporter, owner, mod, sourcePath, corePath, recurseLoader); } - @Override public @Nullable ResolveInfo + @Override public @NotNull ResolveInfo doSaveCompiledCore(@NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs, @NotNull ModuleLoader recurseLoader) throws IOException, ClassNotFoundException { return delegate.doSaveCompiledCore(file, resolveInfo, defs, recurseLoader); } 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 d994c2d14..2c1e64278 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 @@ -120,7 +120,7 @@ public void addURL(Path url) throws MalformedURLException { } } - @Override public @Nullable ResolveInfo doSaveCompiledCore( + @Override public @NotNull ResolveInfo doSaveCompiledCore( @NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs, diff --git a/cli-impl/src/main/java/org/aya/cli/library/incremental/InMemoryCompilerAdvisor.java b/cli-impl/src/main/java/org/aya/cli/library/incremental/InMemoryCompilerAdvisor.java index bb9f6535e..2110de496 100644 --- a/cli-impl/src/main/java/org/aya/cli/library/incremental/InMemoryCompilerAdvisor.java +++ b/cli-impl/src/main/java/org/aya/cli/library/incremental/InMemoryCompilerAdvisor.java @@ -71,11 +71,12 @@ public class InMemoryCompilerAdvisor implements CompilerAdvisor { return compiledCore.getOrNull(mod); } - @Override public @Nullable ResolveInfo doSaveCompiledCore( + @Override public @NotNull ResolveInfo doSaveCompiledCore( @NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs, - @NotNull ModuleLoader recurseLoader) { + @NotNull ModuleLoader recurseLoader + ) { // TODO: what if module name clashes? compiledCore.put(file.moduleName(), resolveInfo); return resolveInfo; diff --git a/cli-impl/src/main/java/org/aya/cli/single/SingleFileCompiler.java b/cli-impl/src/main/java/org/aya/cli/single/SingleFileCompiler.java index 33865f190..8bcefba36 100644 --- a/cli-impl/src/main/java/org/aya/cli/single/SingleFileCompiler.java +++ b/cli-impl/src/main/java/org/aya/cli/single/SingleFileCompiler.java @@ -1,4 +1,4 @@ -// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang. +// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang. // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.cli.single; @@ -58,12 +58,12 @@ public int compile( var ayaFile = fileManager.createAyaFile(locator, sourceFile); var program = ayaFile.parseMe(ayaParser); ayaFile.pretty(flags, program, reporter, CliEnums.PrettyStage.raw); - loader.tyckModule(new PrimFactory(), ctx, program, (moduleResolve, defs) -> { - ayaFile.tyckAdditional(moduleResolve); + loader.tyckModule(new PrimFactory(), ctx, program, (resolveInfo, defs) -> { + ayaFile.tyckAdditional(resolveInfo); ayaFile.pretty(flags, program, reporter, CliEnums.PrettyStage.scoped); ayaFile.pretty(flags, defs, reporter, CliEnums.PrettyStage.typed); ayaFile.pretty(flags, program, reporter, CliEnums.PrettyStage.literate); - if (moduleCallback != null) moduleCallback.onModuleTycked(moduleResolve, defs); + if (moduleCallback != null) moduleCallback.onModuleTycked(resolveInfo, defs); }); }); } diff --git a/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java b/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java index 442ad0637..ce37d8eda 100644 --- a/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java +++ b/ide-lsp/src/test/java/org/aya/lsp/tester/LspTestCompilerAdvisor.java @@ -34,13 +34,13 @@ public void prepareCompile() { newlyCompiled.clear(); } - @Override - public void notifyIncrementalJob(@NotNull ImmutableSeq modified, @NotNull ImmutableSeq> affected) { + @Override public void + notifyIncrementalJob(@NotNull ImmutableSeq modified, @NotNull ImmutableSeq> affected) { this.lastJob = affected; } - @Override - public @Nullable ResolveInfo doSaveCompiledCore(@NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs, @NotNull ModuleLoader recurseLoader) { + @Override public @NotNull ResolveInfo + doSaveCompiledCore(@NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs, @NotNull ModuleLoader recurseLoader) { var info = super.doSaveCompiledCore(file, resolveInfo, defs, recurseLoader); newlyCompiled.append(resolveInfo); return info; diff --git a/jit-compiler/src/test/java/CompileTest.java b/jit-compiler/src/test/java/CompileTest.java index 013337244..1ede4a8d3 100644 --- a/jit-compiler/src/test/java/CompileTest.java +++ b/jit-compiler/src/test/java/CompileTest.java @@ -107,7 +107,7 @@ public static TyckResult tyck(@Language("Aya") @NotNull String code) { var moduleLoader = new DumbModuleLoader(new EmptyContext(REPORTER, FILE)); var callback = new ModuleCallback() { ImmutableSeq ok; - @Override public void onModuleTycked(@NotNull ResolveInfo x, @NotNull ImmutableSeq defs) { ok = defs; } + @Override public void onModuleTycked(@NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs) { ok = defs; } }; var info = moduleLoader.tyckModule(moduleLoader.resolve(new AyaParserImpl(REPORTER).program( new SourceFile("", FILE, code))), callback); From 23b694db46993b6ad07727fca80ed11a616d7426 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 3 Dec 2024 00:17:24 -0500 Subject: [PATCH 6/8] compile: now deserialization inserts `PrimDef` into `PrimFactory` --- .../java/org/aya/primitive/PrimFactory.java | 29 +++++++++---------- .../main/java/org/aya/ide/LspPrimFactory.java | 3 +- .../java/org/aya/compiler/CompiledModule.java | 7 +++-- 3 files changed, 20 insertions(+), 19 deletions(-) diff --git a/base/src/main/java/org/aya/primitive/PrimFactory.java b/base/src/main/java/org/aya/primitive/PrimFactory.java index 218fccf0c..0d831fa89 100644 --- a/base/src/main/java/org/aya/primitive/PrimFactory.java +++ b/base/src/main/java/org/aya/primitive/PrimFactory.java @@ -11,6 +11,7 @@ import org.aya.syntax.concrete.stmt.decl.PrimDecl; import org.aya.syntax.core.Closure; import org.aya.syntax.core.def.PrimDef; +import org.aya.syntax.core.def.PrimDefLike; import org.aya.syntax.core.term.*; import org.aya.syntax.core.term.call.PrimCall; import org.aya.syntax.core.term.repr.StringTerm; @@ -33,7 +34,7 @@ public class PrimFactory { private final @NotNull Map<@NotNull ID, @NotNull PrimSeed> seeds; - private final @NotNull EnumMap<@NotNull ID, @NotNull PrimDef> defs = new EnumMap<>(ID.class); + private final @NotNull EnumMap<@NotNull ID, @NotNull PrimDefLike> defs = new EnumMap<>(ID.class); public PrimFactory() { seeds = ImmutableMap.from(ImmutableSeq.of( @@ -45,6 +46,11 @@ public PrimFactory() { ).map(seed -> Tuple.of(seed.name, seed))); } + public void definePrim(PrimDefLike prim) { + assert suppressRedefinition() || !have(prim.id()); + defs.put(prim.id(), prim); + } + @FunctionalInterface public interface Unfolder extends BiFunction<@NotNull PrimCall, @NotNull TyckState, @NotNull Term> { } @@ -96,7 +102,7 @@ public record PrimSeed( } final @NotNull PrimSeed stringType = - new PrimSeed(ID.STRING, this::primCall, + new PrimSeed(ID.STRING, (prim, _) -> prim, ref -> new PrimDef(ref, Type0, ID.STRING), ImmutableSeq.empty()); final @NotNull PrimSeed stringConcat = @@ -153,29 +159,26 @@ public record PrimSeed( } */ - private @NotNull PrimCall primCall(@NotNull PrimCall prim, @NotNull TyckState tyckState) { return prim; } - public final @NotNull PrimSeed intervalType = new PrimSeed(ID.I, ((_, _) -> DimTyTerm.INSTANCE), ref -> new PrimDef(ref, SortTerm.ISet, ID.I), ImmutableSeq.empty()); - public @NotNull PrimDef factory(@NotNull ID name, @NotNull DefVar ref) { - assert suppressRedefinition() || !have(name); - var rst = seeds.get(name).supply(ref); - defs.put(name, rst); + public @NotNull PrimDefLike factory(@NotNull ID name, @NotNull DefVar ref) { + var rst = new PrimDef.Delegate(seeds.get(name).supply(ref).ref); + definePrim(rst); return rst; } public @NotNull PrimCall getCall(@NotNull ID id, @NotNull ImmutableSeq args) { - return new PrimCall(getOption(id).get().ref(), 0, args); + return new PrimCall(getOption(id).get(), 0, args); } public @NotNull PrimCall getCall(@NotNull ID id) { - return getCall(id, ImmutableSeq.empty()); + return new PrimCall(getOption(id).get()); } - public @NotNull Option getOption(@NotNull ID name) { + public @NotNull Option getOption(@NotNull ID name) { return Option.ofNullable(defs.get(name)); } @@ -186,10 +189,6 @@ public boolean have(@NotNull ID name) { /** whether redefinition should be treated as error */ @ForLSP public boolean suppressRedefinition() { return false; } - public @NotNull PrimDef getOrCreate(@NotNull ID name, @NotNull DefVar ref) { - return getOption(name).getOrElse(() -> factory(name, ref)); - } - public @NotNull Option> checkDependency(@NotNull ID name) { return seeds.getOption(name).map(seed -> seed.dependency().filterNot(this::have)); } diff --git a/ide/src/main/java/org/aya/ide/LspPrimFactory.java b/ide/src/main/java/org/aya/ide/LspPrimFactory.java index d7d8f9138..b34f21d32 100644 --- a/ide/src/main/java/org/aya/ide/LspPrimFactory.java +++ b/ide/src/main/java/org/aya/ide/LspPrimFactory.java @@ -5,6 +5,7 @@ import org.aya.primitive.PrimFactory; import org.aya.syntax.concrete.stmt.decl.PrimDecl; import org.aya.syntax.core.def.PrimDef; +import org.aya.syntax.core.def.PrimDefLike; import org.aya.syntax.ref.DefVar; import org.jetbrains.annotations.NotNull; @@ -35,7 +36,7 @@ public class LspPrimFactory extends PrimFactory { @Override public boolean suppressRedefinition() { return true; } - @Override public @NotNull PrimDef factory(PrimDef.@NotNull ID name, @NotNull DefVar ref) { + @Override public @NotNull PrimDefLike factory(PrimDef.@NotNull ID name, @NotNull DefVar ref) { return getOption(name).getOrElse(() -> super.factory(name, ref)); } } diff --git a/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java b/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java index 57f926584..5d07fe4b7 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java +++ b/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java @@ -167,14 +167,14 @@ private void serOp(@NotNull TyckDef def) { ) { var resolveInfo = new ResolveInfo(context, primFactory, shapeFactory); shallowResolve(loader, resolveInfo); - loadModule(context, shapeFactory, state.topLevelClass(context.modulePath())); + loadModule(primFactory, shapeFactory, context, state.topLevelClass(context.modulePath())); deOp(state, resolveInfo); return resolveInfo; } private void loadModule( - @NotNull PhysicalModuleContext context, @NotNull ShapeFactory shapeFactory, - @NotNull Class rootClass + @NotNull PrimFactory primFactory, @NotNull ShapeFactory shapeFactory, + @NotNull PhysicalModuleContext context, @NotNull Class rootClass ) { for (var jitClass : rootClass.getDeclaredClasses()) { var jitDef = DeState.getJitDef(jitClass); @@ -205,6 +205,7 @@ private void loadModule( shapeFactory.bonjour(fn, recognition); } } + case JitPrim prim -> primFactory.definePrim(prim); default -> { } } } From d02b6296999ca4ad7b02b64ba3528df87a77f6b5 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 3 Dec 2024 00:35:19 -0500 Subject: [PATCH 7/8] unify: handle `PrimCall` --- base/src/main/java/org/aya/unify/TermComparator.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java index 9e22e1d33..cf5475ff9 100644 --- a/base/src/main/java/org/aya/unify/TermComparator.java +++ b/base/src/main/java/org/aya/unify/TermComparator.java @@ -4,10 +4,10 @@ import kala.collection.immutable.ImmutableSeq; import org.aya.generic.Renamer; +import org.aya.generic.term.DTKind; import org.aya.generic.term.SortKind; import org.aya.prettier.AyaPrettierOptions; import org.aya.syntax.core.term.*; -import org.aya.generic.term.DTKind; import org.aya.syntax.core.term.call.*; import org.aya.syntax.core.term.marker.Formation; import org.aya.syntax.core.term.repr.IntegerTerm; @@ -339,7 +339,7 @@ case ProjTerm(var lof, var ldx) -> { // We already compare arguments in compareApprox, if we arrive here, // it means their arguments don't match (even the ref don't match), // so we are unable to do more if we can't normalize them. - case FnCall _ -> null; + case FnCall _, PrimCall _ -> null; default -> throw noRules(lhs); }; From ec1a65ce88499c9d1678915245f635c959efeaf9 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Tue, 3 Dec 2024 01:04:54 -0500 Subject: [PATCH 8/8] compile: reuse `primFactory` --- .../java/org/aya/primitive/PrimFactory.java | 21 ++++++++++++++++--- .../aya/resolve/visitor/StmtPreResolver.java | 2 +- .../org/aya/cli/interactive/ReplCompiler.java | 5 ++++- .../incremental/DiskCompilerAdvisor.java | 10 +++++---- .../main/java/org/aya/ide/LspPrimFactory.java | 6 ++++-- .../java/org/aya/compiler/CompiledModule.java | 5 +++-- 6 files changed, 36 insertions(+), 13 deletions(-) diff --git a/base/src/main/java/org/aya/primitive/PrimFactory.java b/base/src/main/java/org/aya/primitive/PrimFactory.java index 0d831fa89..650847da1 100644 --- a/base/src/main/java/org/aya/primitive/PrimFactory.java +++ b/base/src/main/java/org/aya/primitive/PrimFactory.java @@ -8,6 +8,7 @@ import kala.control.Option; import kala.tuple.Tuple; import org.aya.normalize.Normalizer; +import org.aya.syntax.compile.JitPrim; import org.aya.syntax.concrete.stmt.decl.PrimDecl; import org.aya.syntax.core.Closure; import org.aya.syntax.core.def.PrimDef; @@ -47,7 +48,7 @@ public PrimFactory() { } public void definePrim(PrimDefLike prim) { - assert suppressRedefinition() || !have(prim.id()); + assert !isForbiddenRedefinition(prim.id(), prim instanceof JitPrim); defs.put(prim.id(), prim); } @@ -186,8 +187,22 @@ public boolean have(@NotNull ID name) { return defs.containsKey(name); } - /** whether redefinition should be treated as error */ - @ForLSP public boolean suppressRedefinition() { return false; } + /** + * Whether this definition is a redefinition that should be treated as error. + * There are two cases where a redefinition is allowed: + *
    + *
  • When we are working in an LSP, and users can reload a file to redefine things.
    • + *
  • When we are serializing a file, which we will deserialize immediately, and this will + * replace the existing PrimDefs with their JIT-compiled version.
    • + *
+ * + * @return true if redefinition is forbidden. + */ + @ForLSP public boolean isForbiddenRedefinition(@NotNull PrimDef.ID id, boolean isJit) { + if (isJit) + return have(id) && defs.get(id) instanceof JitPrim; + else return have(id); + } public @NotNull Option> checkDependency(@NotNull ID name) { return seeds.getOption(name).map(seed -> seed.dependency().filterNot(this::have)); diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java index 16453d5c6..3d4cdd1c5 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java @@ -132,7 +132,7 @@ public ImmutableSeq resolveStmt(@NotNull ImmutableSeq stmts var lack = factory.checkDependency(primID); if (lack.isNotEmpty() && lack.get().isNotEmpty()) context.reportAndThrow(new PrimResolveError.Dependency(name, lack.get(), sourcePos)); - else if (factory.have(primID) && !factory.suppressRedefinition()) + else if (factory.isForbiddenRedefinition(primID, false)) context.reportAndThrow(new PrimResolveError.Redefinition(name, sourcePos)); factory.factory(primID, decl.ref); var resolvedCtx = resolveTopLevelDecl(decl, context); diff --git a/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java b/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java index fa496e5fe..fc1068ab7 100644 --- a/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java +++ b/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java @@ -31,6 +31,7 @@ import org.aya.syntax.GenericAyaFile; import org.aya.syntax.concrete.Expr; import org.aya.syntax.concrete.stmt.Stmt; +import org.aya.syntax.core.def.PrimDef; import org.aya.syntax.core.def.TyckDef; import org.aya.syntax.core.term.Term; import org.aya.syntax.literate.CodeOptions.NormalizeMode; @@ -75,7 +76,9 @@ public ReplCompiler( reporter = CountingReporter.delegate(delegateReporter); this.locator = locator != null ? locator : new SourceFileLocator.Module(this.modulePaths); this.primFactory = new PrimFactory() { - @Override public boolean suppressRedefinition() { return true; } + @Override public boolean isForbiddenRedefinition(PrimDef.@NotNull ID id, boolean isJit) { + return false; + } }; this.shapeFactory = new ReplShapeFactory(); this.opSet = new AyaBinOpSet(reporter); 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 2c1e64278..a7fdaeb17 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 @@ -11,6 +11,7 @@ import org.aya.compiler.FileSerializer; import org.aya.compiler.ModuleSerializer; import org.aya.compiler.NameSerializer; +import org.aya.primitive.PrimFactory; import org.aya.resolve.ResolveInfo; import org.aya.resolve.context.EmptyContext; import org.aya.resolve.module.ModuleLoader; @@ -92,13 +93,14 @@ public void addURL(Path url) throws MalformedURLException { @NotNull ModulePath mod, @NotNull Path sourcePath, @NotNull Path libraryRoot, - @NotNull ModuleLoader recurseLoader + @NotNull ModuleLoader recurseLoader, + @NotNull PrimFactory primFactory ) throws ClassNotFoundException, MalformedURLException { var context = new EmptyContext(reporter, sourcePath).derive(mod); var coreDir = computeBaseDir(libraryRoot); cl.addURL(coreDir); cl.loadClass(NameSerializer.getModuleReference(QPath.fileLevel(mod))); - return compiledAya.toResolveInfo(recurseLoader, context, cl); + return compiledAya.toResolveInfo(recurseLoader, context, cl, primFactory); } @Override public @Nullable ResolveInfo doLoadCompiledCore( @@ -116,7 +118,7 @@ public void addURL(Path url) throws MalformedURLException { var parentCount = mod.size(); var libraryRoot = corePath; for (int i = 0; i < parentCount; i++) libraryRoot = libraryRoot.getParent(); - return doLoadCompiledCore(compiledAya, reporter, mod, sourcePath, libraryRoot, recurseLoader); + return doLoadCompiledCore(compiledAya, reporter, mod, sourcePath, libraryRoot, recurseLoader, new PrimFactory()); } } @@ -165,7 +167,7 @@ public void addURL(Path url) throws MalformedURLException { return doLoadCompiledCore( coreMod, resolveInfo.reporter(), resolveInfo.thisModule().modulePath(), file.underlyingFile(), libraryRoot, - recurseLoader + recurseLoader, resolveInfo.primFactory() ); } diff --git a/ide/src/main/java/org/aya/ide/LspPrimFactory.java b/ide/src/main/java/org/aya/ide/LspPrimFactory.java index b34f21d32..872387c53 100644 --- a/ide/src/main/java/org/aya/ide/LspPrimFactory.java +++ b/ide/src/main/java/org/aya/ide/LspPrimFactory.java @@ -34,8 +34,10 @@ * {@link org.aya.cli.library.incremental.InMemoryCompilerAdvisor} will be updated to the newest compilation result. */ public class LspPrimFactory extends PrimFactory { - @Override public boolean suppressRedefinition() { return true; } - + /** Allow all kinds of redefinition. */ + @Override public boolean isForbiddenRedefinition(PrimDef.@NotNull ID id, boolean isJit) { + return false; + } @Override public @NotNull PrimDefLike factory(PrimDef.@NotNull ID name, @NotNull DefVar ref) { return getOption(name).getOrElse(() -> super.factory(name, ref)); } diff --git a/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java b/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java index 5d07fe4b7..64a143a38 100644 --- a/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java +++ b/jit-compiler/src/main/java/org/aya/compiler/CompiledModule.java @@ -156,10 +156,11 @@ private void serOp(@NotNull TyckDef def) { } public @NotNull ResolveInfo toResolveInfo( - @NotNull ModuleLoader loader, @NotNull PhysicalModuleContext context, ClassLoader classLoader + @NotNull ModuleLoader loader, @NotNull PhysicalModuleContext context, + @NotNull ClassLoader classLoader, @NotNull PrimFactory primFactory ) { var state = new DeState(classLoader); - return toResolveInfo(loader, context, state, new PrimFactory(), new ShapeFactory()); + return toResolveInfo(loader, context, state, primFactory, new ShapeFactory()); } public @NotNull ResolveInfo toResolveInfo( @NotNull ModuleLoader loader, @NotNull PhysicalModuleContext context, @NotNull CompiledModule.DeState state,