diff --git a/base/src/main/java/org/aya/primitive/PrimFactory.java b/base/src/main/java/org/aya/primitive/PrimFactory.java index 218fccf0c2..650847da18 100644 --- a/base/src/main/java/org/aya/primitive/PrimFactory.java +++ b/base/src/main/java/org/aya/primitive/PrimFactory.java @@ -8,9 +8,11 @@ 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; +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 +35,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 +47,11 @@ public PrimFactory() { ).map(seed -> Tuple.of(seed.name, seed))); } + public void definePrim(PrimDefLike prim) { + assert !isForbiddenRedefinition(prim.id(), prim instanceof JitPrim); + defs.put(prim.id(), prim); + } + @FunctionalInterface public interface Unfolder extends BiFunction<@NotNull PrimCall, @NotNull TyckState, @NotNull Term> { } @@ -96,7 +103,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 +160,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)); } @@ -183,11 +187,21 @@ public boolean have(@NotNull ID name) { return defs.containsKey(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)); + /** + * 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) { diff --git a/base/src/main/java/org/aya/resolve/ResolveInfo.java b/base/src/main/java/org/aya/resolve/ResolveInfo.java index 014548a7d1..34508753f5 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/base/src/main/java/org/aya/resolve/module/ModuleCallback.java b/base/src/main/java/org/aya/resolve/module/ModuleCallback.java index 87c8434d24..a8e8aa3974 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/main/java/org/aya/resolve/visitor/StmtBinder.java b/base/src/main/java/org/aya/resolve/visitor/StmtBinder.java index 42d007a4bd..831a0e69d1 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/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtPreResolver.java index 16453d5c6a..3d4cdd1c5c 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/base/src/main/java/org/aya/unify/TermComparator.java b/base/src/main/java/org/aya/unify/TermComparator.java index 9e22e1d338..cf5475ff92 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); }; diff --git a/base/src/test/java/org/aya/tyck/TyckTest.java b/base/src/test/java/org/aya/tyck/TyckTest.java index b70af57011..4f87d35f20 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/interactive/ReplCompiler.java b/cli-impl/src/main/java/org/aya/cli/interactive/ReplCompiler.java index fa496e5fe6..fc1068ab74 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/LibraryModuleLoader.java b/cli-impl/src/main/java/org/aya/cli/library/LibraryModuleLoader.java index 11f3aefb20..7408c1ec56 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,15 +74,22 @@ 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 - public boolean existsFileLevelModule(@NotNull ModulePath path) { + @Override public boolean existsFileLevelModule(@NotNull ModulePath path) { return owner.findModule(path) != null; } @@ -94,11 +101,11 @@ public boolean existsFileLevelModule(@NotNull ModulePath path) { } private void saveCompiledCore( - @NotNull LibrarySource file, - @NotNull ResolveInfo resolveInfo, - @NotNull ImmutableSeq defs + @NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, + @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 17aed8a39e..53b56fe949 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 + */ + @NotNull 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,25 @@ void doSaveCompiledCore( } } + /** + * @return possibly the compiled version of the {@link ResolveInfo} + * @see #doSaveCompiledCore + */ @ApiStatus.NonExtendable - default void saveCompiledCore( + default @NotNull ResolveInfo saveCompiledCore( @NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, - @NotNull ImmutableSeq defs + @NotNull ImmutableSeq defs, + @NotNull ModuleLoader recurseLoader ) { + assert recurseLoader instanceof CachedModuleLoader; 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 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 b19e48e178..5c54eb3b69 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 @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); } @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 2f66dff3ba..a7fdaeb17f 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; @@ -80,6 +81,28 @@ public void addURL(Path url) throws MalformedURLException { @Override public void clearModuleOutput(@NotNull LibrarySource source) throws IOException { 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, + @NotNull ModulePath mod, + @NotNull Path sourcePath, + @NotNull Path libraryRoot, + @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, primFactory); + } + @Override public @Nullable ResolveInfo doLoadCompiledCore( @NotNull Reporter reporter, @NotNull LibraryOwner owner, @NotNull ModulePath mod, @@ -90,30 +113,28 @@ 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, new PrimFactory()); } } - @Override public void doSaveCompiledCore( + @Override public @NotNull 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); @@ -140,7 +161,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, resolveInfo.primFactory() + ); } 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 8c07c0d3db..2110de4964 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,14 @@ public class InMemoryCompilerAdvisor implements CompilerAdvisor { return compiledCore.getOrNull(mod); } - @Override public void doSaveCompiledCore( + @Override public @NotNull 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/cli-impl/src/main/java/org/aya/cli/single/SingleFileCompiler.java b/cli-impl/src/main/java/org/aya/cli/single/SingleFileCompiler.java index 33865f190e..8bcefba36f 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/cli-impl/src/main/java/org/aya/cli/utils/CompilerUtil.java b/cli-impl/src/main/java/org/aya/cli/utils/CompilerUtil.java index 2591fd5c12..0a8755fd23 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 { 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 c946b3639b..ce37d8eda4 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; @@ -33,14 +34,15 @@ 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 void doSaveCompiledCore(@NotNull LibrarySource file, @NotNull ResolveInfo resolveInfo, @NotNull ImmutableSeq defs) { - super.doSaveCompiledCore(file, resolveInfo, defs); + @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/ide/src/main/java/org/aya/ide/LspPrimFactory.java b/ide/src/main/java/org/aya/ide/LspPrimFactory.java index d7d8f91382..872387c53e 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; @@ -33,9 +34,11 @@ * {@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; } - - @Override public @NotNull PrimDef factory(PrimDef.@NotNull ID name, @NotNull DefVar ref) { + /** 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 1456e31118..64a143a38f 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,17 +149,18 @@ 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); } } 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, @@ -167,14 +168,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 +206,7 @@ private void loadModule( shapeFactory.bonjour(fn, recognition); } } + case JitPrim prim -> primFactory.definePrim(prim); default -> { } } } 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 8b62f04817..8e568f2a59 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/jit-compiler/src/test/java/CompileTest.java b/jit-compiler/src/test/java/CompileTest.java index 0133372444..1ede4a8d37 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); diff --git a/syntax/src/main/java/org/aya/prettier/BasePrettier.java b/syntax/src/main/java/org/aya/prettier/BasePrettier.java index c980dcc955..bea03e247b 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); 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 a26e321978..2c940f4f19 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());