Skip to content

Commit

Permalink
pattern: only report unimported con when the con is no-arg
Browse files Browse the repository at this point in the history
  • Loading branch information
ice1000 committed Dec 22, 2024
1 parent 4d67d48 commit 43fb355
Show file tree
Hide file tree
Showing 6 changed files with 19 additions and 14 deletions.
12 changes: 8 additions & 4 deletions base/src/main/java/org/aya/tyck/pat/PatternTycker.java
Original file line number Diff line number Diff line change
Expand Up @@ -157,7 +157,7 @@ public record TyckResult(

// report after tyRef.set, the error message requires it
if (whnf(type) instanceof DataCall call) {
var unimportedCon = collectConNames(call.ref())
var unimportedCon = collectNoParamConNames(call.ref())
.anyMatch(it -> it.equalsIgnoreCase(bind.name()));
if (unimportedCon) {
fail(new PatternProblem.UnimportedConName(pattern.replace(bindPat)));
Expand Down Expand Up @@ -479,13 +479,17 @@ private record Selection(
};
}

private static @NotNull SeqView<String> collectConNames(@NotNull DataDefLike call) {
private static @NotNull SeqView<String> collectNoParamConNames(@NotNull DataDefLike call) {
return switch (call) {
case JitData jitData -> jitData.body().view().map(AnyDef::name);
case JitData jitData -> jitData.body().view()
.filter(it -> it.selfTeleSize() == 0)
.map(AnyDef::name);
case DataDef.Delegate delegate -> {
// the core may be unchecked!
var concrete = (DataDecl) delegate.ref.concrete;
yield concrete.body.view().map(it -> it.ref.name());
yield concrete.body.view()
.filter(it -> it.telescope.isEmpty())
.map(it -> it.ref.name());
}
};
}
Expand Down
4 changes: 2 additions & 2 deletions cli-impl/src/main/java/org/aya/cli/single/CompilerFlags.java
Original file line number Diff line number Diff line change
Expand Up @@ -2,7 +2,7 @@
// 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;

import kala.collection.SeqLike;
import kala.collection.SeqView;
import org.aya.cli.render.RenderOptions;
import org.aya.cli.utils.CliEnums;
import org.aya.prettier.AyaPrettierOptions;
Expand All @@ -18,7 +18,7 @@ public record CompilerFlags(
boolean interruptedTrace,
boolean remake,
@Nullable CompilerFlags.PrettyInfo prettyInfo,
@NotNull SeqLike<Path> modulePaths,
@NotNull SeqView<Path> modulePaths,
@Nullable Path outputFile
) {
public static @Nullable CompilerFlags.PrettyInfo prettyInfoFromOutput(
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -38,8 +38,9 @@ public SingleFileCompiler(
ayaParser = new AyaParserImpl(reporter);
fileManager = new SingleAyaFile.Factory(reporter);
loader = new CachedModuleLoader<>(new ModuleListLoader(this.reporter,
flags.modulePaths().view().map(path ->
new FileModuleLoader(locator, path, reporter, ayaParser, fileManager)).toImmutableSeq()));
flags.modulePaths().map(path ->
new FileModuleLoader(locator, path, reporter, ayaParser, fileManager))
.toImmutableSeq()));
}

public <E extends IOException> int compile(
Expand Down
3 changes: 2 additions & 1 deletion cli-impl/src/test/java/org/aya/test/LibraryTest.java
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,7 @@
// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
package org.aya.test;

import kala.collection.SeqView;
import kala.collection.immutable.ImmutableSeq;
import kala.collection.mutable.MutableSet;
import org.aya.cli.library.LibraryCompiler;
Expand Down Expand Up @@ -74,7 +75,7 @@ public static void main(String... args) throws IOException {
true, false, false, false, CliEnums.PrettyStage.literate,
CliEnums.PrettyFormat.html, AyaPrettierOptions.pretty(), new RenderOptions(), null
);
return new CompilerFlags(CompilerFlags.Message.ASCII, false, false, prettyInfo, ImmutableSeq.empty(), null);
return new CompilerFlags(CompilerFlags.Message.ASCII, false, false, prettyInfo, SeqView.empty(), null);
}

@Test public void testInMemoryAndPrim() throws IOException {
Expand Down
4 changes: 2 additions & 2 deletions cli-impl/src/test/java/org/aya/test/TestRunner.java
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@

import com.intellij.openapi.util.text.Strings;
import kala.collection.Seq;
import kala.collection.immutable.ImmutableSeq;
import kala.collection.SeqView;
import org.aya.cli.single.CompilerFlags;
import org.aya.cli.single.SingleFileCompiler;
import org.aya.test.fixtures.*;
Expand Down Expand Up @@ -141,7 +141,7 @@ private static void runSingleCase(String code, SingleFileCompiler compiler) thro
}

public static @NotNull CompilerFlags flags() {
var modulePaths = ImmutableSeq.of(DEFAULT_TEST_DIR.resolve("shared/src"));
var modulePaths = SeqView.of(DEFAULT_TEST_DIR.resolve("shared/src"));
return new CompilerFlags(CompilerFlags.Message.ASCII,
false, false, null, modulePaths, null);
}
Expand Down
5 changes: 2 additions & 3 deletions producer/src/main/java/org/aya/producer/AyaProducer.java
Original file line number Diff line number Diff line change
Expand Up @@ -539,7 +539,7 @@ private record DeclNameOrInfix(@NotNull WithPos<String> name, @Nullable OpDecl.O
}
if (node.is(ULIFT_ATOM)) {
var expr = expr(node.child(EXPR));
var lifts = node.childrenOfType(ULIFT_PREFIX).collect(Collectors.summingInt(kw -> {
int lifts = node.childrenOfType(ULIFT_PREFIX).collect(Collectors.summingInt(kw -> {
var text = kw.tokenText();
if ("ulift".contentEquals(text)) return 1;
else return text.length();
Expand Down Expand Up @@ -872,8 +872,7 @@ private Arg<WithPos<Pattern>> unitPattern(@NotNull GenericNode<?> node) {
if (node == null) return null;
var child = node.peekChild(EXPR);
if (child == null) {
reporter.report(new ParseError(sourcePosOf(node), "Expect the return type expression"));
return null;
return error(node, "Expect the return type expression");

Check warning on line 875 in producer/src/main/java/org/aya/producer/AyaProducer.java

View check run for this annotation

Codecov / codecov/patch

producer/src/main/java/org/aya/producer/AyaProducer.java#L875

Added line #L875 was not covered by tests
}
return expr(child);
}
Expand Down

0 comments on commit 43fb355

Please sign in to comment.