diff --git a/base/src/main/java/org/aya/concrete/Expr.java b/base/src/main/java/org/aya/concrete/Expr.java index df4d9ff87b..905ff7af5a 100644 --- a/base/src/main/java/org/aya/concrete/Expr.java +++ b/base/src/main/java/org/aya/concrete/Expr.java @@ -98,6 +98,8 @@ public Error(@NotNull SourcePos sourcePos, @NotNull Doc description) { } /** + * @param explicit whether the hole is a type-directed programming goal or + * a to-be-solved by tycking hole. * @author ice1000 */ record Hole( diff --git a/base/src/main/java/org/aya/concrete/error/ParseError.java b/base/src/main/java/org/aya/concrete/error/ParseError.java index 4f6103de2e..7fe45048fa 100644 --- a/base/src/main/java/org/aya/concrete/error/ParseError.java +++ b/base/src/main/java/org/aya/concrete/error/ParseError.java @@ -1,16 +1,16 @@ -// Copyright (c) 2020-2022 Yinsen (Tesla) Zhang. +// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang. // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.concrete.error; import org.aya.pretty.doc.Doc; -import org.aya.util.prettier.PrettierOptions; import org.aya.util.error.SourcePos; +import org.aya.util.prettier.PrettierOptions; import org.aya.util.reporter.Problem; import org.jetbrains.annotations.NotNull; public record ParseError(@Override @NotNull SourcePos sourcePos, @NotNull String message) implements Problem { @Override public @NotNull Doc describe(@NotNull PrettierOptions options) { - return Doc.plain("Parser error: " + message); + return Doc.english(message); } @Override public @NotNull Severity level() { diff --git a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java index 71c18531df..c679fdd46e 100644 --- a/base/src/main/java/org/aya/tyck/unify/Synthesizer.java +++ b/base/src/main/java/org/aya/tyck/unify/Synthesizer.java @@ -62,7 +62,7 @@ public boolean inheritPiDom(@NotNull Term type, @NotNull SortTerm expected) { */ public @Nullable Term synthesize(@NotNull Term preterm) { return switch (preterm) { - case RefTerm term -> ctx.get(term.var()); + case RefTerm(var var) -> ctx.get(var); case ConCall conCall -> conCall.head().underlyingDataCall(); case Callable.DefCall call -> Def.defResult(call.ref()) .subst(DeltaExpander.buildSubst(Def.defTele(call.ref()), call.args())) @@ -72,8 +72,7 @@ public boolean inheritPiDom(@NotNull Term type, @NotNull SortTerm expected) { if (result == null) { preterm = whnf(preterm); yield preterm instanceof MetaTerm ? null : synthesize(preterm); - } - else yield result; + } else yield result; } case RefTerm.Field field -> Def.defType(field.ref()); case FieldTerm access -> { diff --git a/base/src/test/resources/failure/syntax/implicit-element-list-pattern.aya.txt b/base/src/test/resources/failure/syntax/implicit-element-list-pattern.aya.txt index 9a5cdece85..e1bfce847a 100644 --- a/base/src/test/resources/failure/syntax/implicit-element-list-pattern.aya.txt +++ b/base/src/test/resources/failure/syntax/implicit-element-list-pattern.aya.txt @@ -5,7 +5,7 @@ In file $FILE:11:8 -> 11 │ | [ _, {y} ], default => y │ ╰╯ -Error: Parser error: Implicit elements in a list pattern is disallowed +Error: Implicit elements in a list pattern is disallowed 1 error(s), 0 warning(s). What are you doing? diff --git a/base/src/test/resources/failure/syntax/incomplete-code.aya b/base/src/test/resources/failure/syntax/incomplete-code.aya new file mode 100644 index 0000000000..893fdbd20d --- /dev/null +++ b/base/src/test/resources/failure/syntax/incomplete-code.aya @@ -0,0 +1,4 @@ +prim +def +def k => +data diff --git a/base/src/test/resources/failure/syntax/incomplete-code.aya.txt b/base/src/test/resources/failure/syntax/incomplete-code.aya.txt new file mode 100644 index 0000000000..dcd9bfd7f1 --- /dev/null +++ b/base/src/test/resources/failure/syntax/incomplete-code.aya.txt @@ -0,0 +1,38 @@ +In file $FILE:1:0 -> + + 1 │ prim + │ ╰──╯ + 2 │ def + 3 │ def k => + +Error: Expect a primitive's name + +In file $FILE:2:0 -> + + 1 │ prim + 2 │ def + │ ╰─╯ + 3 │ def k => + +Error: Expect a function name + +In file $FILE:3:6 -> + + 1 │ prim + 2 │ def + 3 │ def k => + │ ╰╯ + +Error: Expect function body + +In file $FILE:4:0 -> + + 2 │ def + 3 │ def k => + 4 │ data + │ ╰──╯ + +Error: Expect a data name + +4 error(s), 0 warning(s). +What are you doing? diff --git a/base/src/test/resources/failure/syntax/issue164.aya.txt b/base/src/test/resources/failure/syntax/issue164.aya.txt index c743a2b00c..354f6bfd5a 100644 --- a/base/src/test/resources/failure/syntax/issue164.aya.txt +++ b/base/src/test/resources/failure/syntax/issue164.aya.txt @@ -5,7 +5,7 @@ In file $FILE:3:26 -> 3 │ (p : Sig A B) : C │ ╰╯ -Error: Parser error: Cannot parse +Error: Cannot parse In file $FILE:8:29 -> @@ -14,7 +14,7 @@ In file $FILE:8:29 -> 8 │ (p : Sig A B C) : D │ ╰╯ -Error: Parser error: Cannot parse +Error: Cannot parse In file $FILE:1:4 -> diff --git a/base/src/test/resources/failure/syntax/issue165.aya.txt b/base/src/test/resources/failure/syntax/issue165.aya.txt index f4265b14d7..a53056bbab 100644 --- a/base/src/test/resources/failure/syntax/issue165.aya.txt +++ b/base/src/test/resources/failure/syntax/issue165.aya.txt @@ -1,9 +1,9 @@ -In file $FILE:1:3 -> +In file $FILE:1:0 -> 1 │ def - │ ╰╯ + │ ╰─╯ -Error: Parser error: Cannot parse +Error: Expect a function name 1 error(s), 0 warning(s). What are you doing? diff --git a/base/src/test/resources/failure/syntax/literal-too-large.aya.txt b/base/src/test/resources/failure/syntax/literal-too-large.aya.txt index c2527941ff..9faf336fea 100644 --- a/base/src/test/resources/failure/syntax/literal-too-large.aya.txt +++ b/base/src/test/resources/failure/syntax/literal-too-large.aya.txt @@ -5,7 +5,7 @@ In file $FILE:3:17 -> 3 │ def too-large => 2147483648 │ ╰────────╯ -Error: Parser error: Unsupported integer literal `2147483648` +Error: Unsupported integer literal `2147483648` Parsing interrupted due to: 1 error(s), 0 warning(s). diff --git a/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java b/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java index 4825894935..f23de14244 100644 --- a/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java +++ b/cli/src/main/java/org/aya/cli/parse/AyaGKProducer.java @@ -1,4 +1,4 @@ -// Copyright (c) 2020-2022 Tesla (Yinsen) Zhang. +// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang. // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.cli.parse; @@ -10,6 +10,7 @@ import com.intellij.psi.tree.TokenSet; import kala.collection.SeqView; import kala.collection.immutable.ImmutableSeq; +import kala.collection.mutable.MutableList; import kala.collection.mutable.MutableSinglyLinkedList; import kala.control.Either; import kala.control.Option; @@ -95,10 +96,11 @@ public record AyaGKProducer( if (node.is(MODULE)) return ImmutableSeq.of(module(node)); if (node.is(OPEN_CMD)) return openCmd(node); if (node.is(DECL)) { - var result = decl(node); - var stmts = result.component2().view().prepended(result.component1()); - if (result.component1() instanceof Decl.TopLevel top && top.personality() == Decl.Personality.COUNTEREXAMPLE) { - result.component2().firstOption(stmt -> !(stmt instanceof Decl)) + var stmts = MutableList.create(); + var result = decl(node, stmts); + if (result != null) stmts.prepend(result); + if (result instanceof Decl.TopLevel top && top.personality() == Decl.Personality.COUNTEREXAMPLE) { + stmts.firstOption(stmt -> !(stmt instanceof Decl)) .ifDefined(stmt -> reporter.report(new BadCounterexampleWarn(stmt))); return stmts.filterIsInstance(Decl.class).toImmutableSeq(); } @@ -222,11 +224,11 @@ public SeqView useIdsComma(@NotNull GenericNode node) { node.childrenOfType(STMT).flatMap(this::stmt).toImmutableSeq()); } - public Tuple2> decl(@NotNull GenericNode node) { - if (node.is(FN_DECL)) return Tuple.of(fnDecl(node), ImmutableSeq.empty()); - if (node.is(PRIM_DECL)) return Tuple.of(primDecl(node), ImmutableSeq.empty()); - if (node.is(DATA_DECL)) return dataDecl(node); - if (node.is(STRUCT_DECL)) return structDecl(node); + public @Nullable Decl decl(@NotNull GenericNode node, @NotNull MutableList additional) { + if (node.is(FN_DECL)) return fnDecl(node); + if (node.is(PRIM_DECL)) return primDecl(node); + if (node.is(DATA_DECL)) return dataDecl(node, additional); + if (node.is(STRUCT_DECL)) return structDecl(node, additional); return unreachable(node); } @@ -256,7 +258,18 @@ public Tuple2> decl(@NotNull GenericNode n return declModifiersOf(node, x -> true); } - public TeleDecl.FnDecl fnDecl(@NotNull GenericNode node) { + public @Nullable TeleDecl.FnDecl fnDecl(@NotNull GenericNode node) { + var nameOrInfix = declNameOrInfix(node.peekChild(DECL_NAME_OR_INFIX)); + if (nameOrInfix == null) { + error(node.childrenView().first(), "Expect a function name"); + return null; + } + var fnBodyNode = node.peekChild(FN_BODY); + if (fnBodyNode == null) { + error(node.childrenView().first(), "Expect a function body"); + return null; + } + var modifier = commonDeclModifiersOf(node); var acc = modifier.accessibility().data(); var sample = modifier.personality().data(); @@ -270,9 +283,9 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode node) { } var tele = telescope(node.childrenOfType(TELE).map(x -> x)); // make compiler happy var bind = node.peekChild(BIND_BLOCK); - var nameOrInfix = declNameOrInfix(node.child(DECL_NAME_OR_INFIX)); - var dynamite = fnBody(node.child(FN_BODY)); + var dynamite = fnBody(fnBodyNode); + if (dynamite == null) return null; if (dynamite.isRight() && inline.isDefined()) { var gelatin = inline.get(); reporter.report(new BadModifierWarn(sourcePosOf(gelatin.component1()), gelatin.component2())); @@ -293,16 +306,22 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode node) { ); } - public @NotNull Either> fnBody(@NotNull GenericNode node) { + public @Nullable Either> + fnBody(@NotNull GenericNode node) { var expr = node.peekChild(EXPR); + var implies = node.peekChild(IMPLIES); + if (expr == null && implies != null) { + error(implies, "Expect function body"); + return null; + } if (expr != null) return Either.left(expr(expr)); return Either.right(node.childrenOfType(BARRED_CLAUSE).map(this::bareOrBarredClause).toImmutableSeq()); } - private @NotNull ImmutableSeq giveMeOpen(@NotNull ModifierSet modiSet, @NotNull TeleDecl decl) { - if (!modiSet.isReExport().data()) return ImmutableSeq.empty(); + private void giveMeOpen(@NotNull ModifierSet modiSet, @NotNull TeleDecl decl, @NotNull MutableList additional) { + if (!modiSet.isReExport().data()) return; - return ImmutableSeq.of(new Command.Open( + additional.append(new Command.Open( modiSet.isReExport().sourcePos(), modiSet.accessibility().data(), new QualifiedID(decl.sourcePos(), decl.ref().name()), @@ -312,19 +331,21 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode node) { )); } - public @NotNull Tuple2> - dataDecl(GenericNode node) { + public @Nullable TeleDecl.DataDecl dataDecl(GenericNode node, @NotNull MutableList additional) { + var nameOrInfix = declNameOrInfix(node.peekChild(DECL_NAME_OR_INFIX)); + if (nameOrInfix == null) { + error(node.childrenView().first(), "Expect a data name"); + return null; + } var modifier = moduleLikeDeclModifiersOf(node); var acc = modifier.accessibility().data(); var sample = modifier.personality().data(); var bind = node.peekChild(BIND_BLOCK); - var body = node.childrenOfType(DATA_BODY).map(this::dataBody).toImmutableSeq(); + var body = node.childrenOfType(DATA_BODY).mapNotNull(this::dataBody).toImmutableSeq(); var tele = telescope(node.childrenOfType(TELE).map(x -> x)); - var nameOrInfix = declNameOrInfix(node.child(DECL_NAME_OR_INFIX)); - var entire = sourcePosOf(node); var decl = new TeleDecl.DataDecl( nameOrInfix.component1().sourcePos(), - entire, + sourcePosOf(node), sample == Decl.Personality.NORMAL ? acc : Stmt.Accessibility.Private, nameOrInfix.component2(), nameOrInfix.component1().data(), @@ -335,22 +356,24 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode node) { sample ); - return Tuple.of(decl, giveMeOpen(modifier, decl)); + giveMeOpen(modifier, decl, additional); + return decl; } - public @NotNull TeleDecl.DataCtor dataBody(@NotNull GenericNode node) { + public @Nullable TeleDecl.DataCtor dataBody(@NotNull GenericNode node) { var dataCtorClause = node.peekChild(DATA_CTOR_CLAUSE); if (dataCtorClause != null) return dataCtorClause(dataCtorClause); var dataCtor = node.peekChild(DATA_CTOR); if (dataCtor != null) return dataCtor(ImmutableSeq.empty(), dataCtor); - return unreachable(node); + error(node.childrenView().first(), "Expect a data constructor"); + return null; } public @NotNull TeleDecl.DataCtor dataCtorClause(@NotNull GenericNode node) { return dataCtor(patterns(node.child(PATTERNS).child(COMMA_SEP)), node.child(DATA_CTOR)); } - public @NotNull Tuple2> structDecl(@NotNull GenericNode node) { + public @NotNull TeleDecl.StructDecl structDecl(@NotNull GenericNode node, @NotNull MutableList additional) { var modifier = moduleLikeDeclModifiersOf(node); var acc = modifier.accessibility().data(); var sample = modifier.personality().data(); @@ -370,7 +393,8 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode node) { bind == null ? BindBlock.EMPTY : bindBlock(bind), sample ); - return Tuple.of(decl, giveMeOpen(modifier, decl)); + giveMeOpen(modifier, decl, additional); + return decl; } public @NotNull TeleDecl.StructField structField(GenericNode node) { @@ -390,8 +414,17 @@ public TeleDecl.FnDecl fnDecl(@NotNull GenericNode node) { ); } - public @NotNull TeleDecl.PrimDecl primDecl(@NotNull GenericNode node) { - var id = primName(node.child(PRIM_NAME)); + private void error(@NotNull GenericNode node, @NotNull String message) { + reporter.report(new ParseError(sourcePosOf(node), message)); + } + + public @Nullable TeleDecl.PrimDecl primDecl(@NotNull GenericNode node) { + var nameEl = node.peekChild(PRIM_NAME); + if (nameEl == null) { + error(node.childrenView().first(), "Expect a primitive's name"); + return null; + } + var id = weakId(nameEl.child(WEAK_ID)); return new TeleDecl.PrimDecl( id.sourcePos(), sourcePosOf(node), @@ -496,7 +529,9 @@ private interface LicitParser extends BooleanObjBiFunction, T> LocalVar.from(teleParamName(node)), typeOrHole(null, pos), explicit)); } - public Tuple2<@NotNull WithPos, OpDecl.@Nullable OpInfo> declNameOrInfix(@NotNull GenericNode node) { + public @Nullable Tuple2<@NotNull WithPos, OpDecl.@Nullable OpInfo> + declNameOrInfix(@Nullable GenericNode node) { + if (node == null) return null; var assoc = node.peekChild(ASSOC); var id = weakId(node.child(WEAK_ID)); if (assoc == null) return Tuple.of(id, null); @@ -506,6 +541,9 @@ private interface LicitParser extends BooleanObjBiFunction, T> public @NotNull Expr expr(@NotNull GenericNode node) { var pos = sourcePosOf(node); + // if (node.is(TokenType.ERROR_ELEMENT)) { + // return new Expr.Hole(pos, true, null); + // } if (node.is(REF_EXPR)) { var qid = qualifiedId(node.child(QUALIFIED_ID)); return new Expr.Unresolved(qid.sourcePos(), qid); @@ -850,7 +888,12 @@ private Arg unitPattern(@NotNull GenericNode node) { public @Nullable Expr typeOrNull(@Nullable GenericNode node) { if (node == null) return null; - return expr(node.child(EXPR)); + var child = node.peekChild(EXPR); + if (child == null) { + reporter.report(new ParseError(sourcePosOf(node), "Expect the return type expression")); + return null; + } + return expr(child); } public @NotNull Expr typeOrHole(@Nullable GenericNode node, SourcePos sourcePos) { @@ -871,10 +914,6 @@ private Arg unitPattern(@NotNull GenericNode node) { return weakId(node.child(WEAK_ID)); } - public @NotNull WithPos primName(@NotNull GenericNode node) { - return weakId(node.child(WEAK_ID)); - } - public @NotNull WithPos newArgField(@NotNull GenericNode node) { return weakId(node.child(WEAK_ID)); } diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java index 1a49485dcd..a6294606ff 100644 --- a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java +++ b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java @@ -1,3 +1,6 @@ +// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang. +// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. + // This is a generated file. Not intended for manual editing. package org.aya.parser; @@ -85,7 +88,6 @@ public interface AyaPsiElementTypes { IElementType PROJ_FIX_ID = new AyaPsiElementType("PROJ_FIX_ID"); IElementType QUALIFIED_ID = new AyaPsiElementType("QUALIFIED_ID"); IElementType REF_EXPR = new AyaPsiElementType("REF_EXPR"); - IElementType SAMPLE_MODIFIERS = new AyaPsiElementType("SAMPLE_MODIFIERS"); IElementType SIGMA_EXPR = new AyaPsiElementType("SIGMA_EXPR"); IElementType STMT = new AyaPsiElementType("STMT"); IElementType STRUCT_DECL = new AyaPsiElementType("STRUCT_DECL"); diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java index 64da8b5184..c0606b7383 100644 --- a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java +++ b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java @@ -1,3 +1,6 @@ +// Copyright (c) 2020-2023 Tesla (Yinsen) Zhang. +// Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. + // This is a generated file. Not intended for manual editing. package org.aya.parser; @@ -436,12 +439,13 @@ private static boolean commaSep_1_0(PsiBuilder b, int l, Parser _param) { public static boolean dataBody(PsiBuilder b, int l) { if (!recursion_guard_(b, l, "dataBody")) return false; if (!nextTokenIs(b, BAR)) return false; - boolean r; - Marker m = enter_section_(b); + boolean r, p; + Marker m = enter_section_(b, l, _NONE_, DATA_BODY, null); r = consumeToken(b, BAR); + p = r; // pin = 1 r = r && dataBody_1(b, l + 1); - exit_section_(b, m, DATA_BODY, r); - return r; + exit_section_(b, l, m, r, p, null); + return r || p; } // dataCtorClause | dataCtor @@ -522,20 +526,23 @@ public static boolean dataCtorClause(PsiBuilder b, int l) { } /* ********************************************************** */ - // declModifiers* KW_DATA declNameOrInfix tele* type? dataBody* bindBlock? + // declModifiers* + // KW_DATA declNameOrInfix + // tele* type? dataBody* bindBlock? public static boolean dataDecl(PsiBuilder b, int l) { if (!recursion_guard_(b, l, "dataDecl")) return false; - boolean r; + boolean r, p; Marker m = enter_section_(b, l, _NONE_, DATA_DECL, ""); r = dataDecl_0(b, l + 1); r = r && consumeToken(b, KW_DATA); - r = r && declNameOrInfix(b, l + 1); - r = r && dataDecl_3(b, l + 1); - r = r && dataDecl_4(b, l + 1); - r = r && dataDecl_5(b, l + 1); - r = r && dataDecl_6(b, l + 1); - exit_section_(b, l, m, r, false, null); - return r; + p = r; // pin = 2 + r = r && report_error_(b, declNameOrInfix(b, l + 1)); + r = p && report_error_(b, dataDecl_3(b, l + 1)) && r; + r = p && report_error_(b, dataDecl_4(b, l + 1)) && r; + r = p && report_error_(b, dataDecl_5(b, l + 1)) && r; + r = p && dataDecl_6(b, l + 1) && r; + exit_section_(b, l, m, r, p, null); + return r || p; } // declModifiers* @@ -669,29 +676,18 @@ static boolean exprList(PsiBuilder b, int l) { } /* ********************************************************** */ - // IMPLIES expr + // simpleBody // | barredClause* public static boolean fnBody(PsiBuilder b, int l) { if (!recursion_guard_(b, l, "fnBody")) return false; boolean r; Marker m = enter_section_(b, l, _NONE_, FN_BODY, ""); - r = fnBody_0(b, l + 1); + r = simpleBody(b, l + 1); if (!r) r = fnBody_1(b, l + 1); exit_section_(b, l, m, r, false, null); return r; } - // IMPLIES expr - private static boolean fnBody_0(PsiBuilder b, int l) { - if (!recursion_guard_(b, l, "fnBody_0")) return false; - boolean r; - Marker m = enter_section_(b); - r = consumeToken(b, IMPLIES); - r = r && expr(b, l + 1, -1); - exit_section_(b, m, null, r); - return r; - } - // barredClause* private static boolean fnBody_1(PsiBuilder b, int l) { if (!recursion_guard_(b, l, "fnBody_1")) return false; @@ -704,21 +700,24 @@ private static boolean fnBody_1(PsiBuilder b, int l) { } /* ********************************************************** */ - // declModifiers* KW_DEF fnModifiers* declNameOrInfix tele* type? fnBody bindBlock? + // declModifiers* + // KW_DEF fnModifiers* declNameOrInfix + // tele* type? fnBody bindBlock? public static boolean fnDecl(PsiBuilder b, int l) { if (!recursion_guard_(b, l, "fnDecl")) return false; - boolean r; + boolean r, p; Marker m = enter_section_(b, l, _NONE_, FN_DECL, ""); r = fnDecl_0(b, l + 1); r = r && consumeToken(b, KW_DEF); - r = r && fnDecl_2(b, l + 1); - r = r && declNameOrInfix(b, l + 1); - r = r && fnDecl_4(b, l + 1); - r = r && fnDecl_5(b, l + 1); - r = r && fnBody(b, l + 1); - r = r && fnDecl_7(b, l + 1); - exit_section_(b, l, m, r, false, null); - return r; + p = r; // pin = 2 + r = r && report_error_(b, fnDecl_2(b, l + 1)); + r = p && report_error_(b, declNameOrInfix(b, l + 1)) && r; + r = p && report_error_(b, fnDecl_4(b, l + 1)) && r; + r = p && report_error_(b, fnDecl_5(b, l + 1)) && r; + r = p && report_error_(b, fnBody(b, l + 1)) && r; + r = p && fnDecl_7(b, l + 1) && r; + exit_section_(b, l, m, r, p, null); + return r || p; } // declModifiers* @@ -1434,14 +1433,15 @@ public static boolean patterns(PsiBuilder b, int l) { public static boolean primDecl(PsiBuilder b, int l) { if (!recursion_guard_(b, l, "primDecl")) return false; if (!nextTokenIs(b, KW_PRIM)) return false; - boolean r; - Marker m = enter_section_(b); + boolean r, p; + Marker m = enter_section_(b, l, _NONE_, PRIM_DECL, null); r = consumeToken(b, KW_PRIM); - r = r && primName(b, l + 1); - r = r && primDecl_2(b, l + 1); - r = r && primDecl_3(b, l + 1); - exit_section_(b, m, PRIM_DECL, r); - return r; + p = r; // pin = 1 + r = r && report_error_(b, primName(b, l + 1)); + r = p && report_error_(b, primDecl_2(b, l + 1)) && r; + r = p && primDecl_3(b, l + 1) && r; + exit_section_(b, l, m, r, p, null); + return r || p; } // tele* @@ -1624,16 +1624,17 @@ private static boolean repl_0(PsiBuilder b, int l) { } /* ********************************************************** */ - // KW_EXAMPLE | KW_COUNTEREXAMPLE - public static boolean sampleModifiers(PsiBuilder b, int l) { - if (!recursion_guard_(b, l, "sampleModifiers")) return false; - if (!nextTokenIs(b, "", KW_COUNTEREXAMPLE, KW_EXAMPLE)) return false; - boolean r; - Marker m = enter_section_(b, l, _NONE_, SAMPLE_MODIFIERS, ""); - r = consumeToken(b, KW_EXAMPLE); - if (!r) r = consumeToken(b, KW_COUNTEREXAMPLE); - exit_section_(b, l, m, r, false, null); - return r; + // IMPLIES expr + static boolean simpleBody(PsiBuilder b, int l) { + if (!recursion_guard_(b, l, "simpleBody")) return false; + if (!nextTokenIs(b, IMPLIES)) return false; + boolean r, p; + Marker m = enter_section_(b, l, _NONE_); + r = consumeToken(b, IMPLIES); + p = r; // pin = 1 + r = r && expr(b, l + 1, -1); + exit_section_(b, l, m, r, p, null); + return r || p; } /* ********************************************************** */ diff --git a/parser/src/main/grammar/AyaPsiParser.bnf b/parser/src/main/grammar/AyaPsiParser.bnf index f9a73c32a6..08dc76bdda 100644 --- a/parser/src/main/grammar/AyaPsiParser.bnf +++ b/parser/src/main/grammar/AyaPsiParser.bnf @@ -1,5 +1,5 @@ /* - * Copyright (c) 2020-2022 Tesla (Yinsen) Zhang. + * Copyright (c) 2020-2023 Tesla (Yinsen) Zhang. * Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. */ @@ -159,7 +159,7 @@ program ::= repl | stmts private stmts ::= stmt_with_recover* private stmt_with_recover ::= !(<>) stmt { - pin = 1 + pin=1 recoverWhile = stmt_recover } private stmt_recover ::= !(stmt_first) @@ -191,8 +191,6 @@ generalize ::= KW_VARIABLE generalizeParamName+ type // declarations -sampleModifiers ::= KW_EXAMPLE | KW_COUNTEREXAMPLE - decl ::= fnDecl | primDecl | structDecl | dataDecl { mixin="org.aya.intellij.psi.impl.AyaPsiGenericDeclImpl" implements="org.aya.intellij.psi.AyaPsiGenericDecl" @@ -206,9 +204,12 @@ bindBlock ::= (tighters | loosers)+ tighters ::= KW_TIGHTER qualifiedId+ loosers ::= KW_LOOSER qualifiedId+ -fnDecl ::= declModifiers* KW_DEF fnModifiers* declNameOrInfix tele* type? fnBody bindBlock? +fnDecl ::= declModifiers* + KW_DEF fnModifiers* declNameOrInfix + tele* type? fnBody bindBlock? { pin=2 } -fnBody ::= IMPLIES expr +private simpleBody ::= IMPLIES expr { pin=1 } +fnBody ::= simpleBody | barredClause* fnModifiers ::= KW_OPAQUE @@ -223,7 +224,7 @@ openKw ::= KW_OPEN // This rule is used for convenience in semantic highlight. // see: SemanticHighlight, AyaGenericDeclImpl, AyaRunLineMarkerContributor primName ::= weakId -primDecl ::= KW_PRIM primName tele* type? +primDecl ::= KW_PRIM primName tele* type? { pin=1 } declModifiers ::= KW_PRIVATE | openKw | KW_EXAMPLE | KW_COUNTEREXAMPLE @@ -239,11 +240,14 @@ structField implements="org.aya.intellij.psi.AyaPsiGenericDecl" } -dataDecl ::= declModifiers* KW_DATA declNameOrInfix tele* type? dataBody* bindBlock? +dataDecl ::= declModifiers* + KW_DATA declNameOrInfix + tele* type? dataBody* bindBlock? { pin=2 } dataBody ::= BAR (dataCtorClause | dataCtor) { mixin="org.aya.intellij.psi.impl.AyaPsiGenericDeclImpl" implements="org.aya.intellij.psi.AyaPsiGenericDecl" + pin=1 } dataCtor ::= KW_COERCE? declNameOrInfix tele* type? partialBlock? bindBlock? @@ -397,7 +401,7 @@ pathTele ::= teleParamName // utilities private exprList ::= <> barred ::= expr BAR -type ::= COLON expr { pin = 1 } +type ::= COLON expr { pin=1 } doBinding ::= weakId LARROW expr { mixin="org.aya.intellij.psi.impl.AyaPsiNamedWeakIdImpl" implements="org.aya.intellij.psi.AyaPsiNamedWeakId"