From a8964deba19f1eb79ae88f2c78e39dc753caf15b Mon Sep 17 00:00:00 2001 From: HoshinoTented Date: Sun, 29 Dec 2024 02:59:45 +0800 Subject: [PATCH] elim data: done --- .../org/aya/resolve/visitor/StmtResolver.java | 4 -- .../org/aya/syntax/concrete/SyntaxTest.java | 3 ++ .../test/resources/negative/GoalAndMeta.txt | 9 ++++ .../test/resources/negative/PatTyckError.txt | 11 ++++- .../resources/shared/src/data/vec/base.aya | 6 +-- .../org/aya/parser/AyaPsiElementTypes.java | 1 + .../main/gen/org/aya/parser/AyaPsiParser.java | 45 +++++++++++++------ parser/src/main/grammar/AyaPsiParser.bnf | 4 +- .../java/org/aya/producer/AyaProducer.java | 14 ++++-- .../org/aya/prettier/ConcretePrettier.java | 4 +- .../syntax/concrete/stmt/decl/DataDecl.java | 5 +-- .../syntax/concrete/stmt/decl/MatchBody.java | 2 +- 12 files changed, 77 insertions(+), 31 deletions(-) diff --git a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java index c846ec7601..d9741b22ce 100644 --- a/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/StmtResolver.java @@ -172,10 +172,6 @@ private static void resolveElim(@NotNull ExprResolver resolver, @NotNull M return; } - if (body.rawElims.isEmpty()) { - return; - } - var resolved = body.rawElims.map(elim -> { var result = resolver.resolve(new QualifiedID(elim.sourcePos(), elim.data())); if (!(result instanceof LocalVar localVar)) { diff --git a/base/src/test/java/org/aya/syntax/concrete/SyntaxTest.java b/base/src/test/java/org/aya/syntax/concrete/SyntaxTest.java index 8d04df5dc2..2a53e3768b 100644 --- a/base/src/test/java/org/aya/syntax/concrete/SyntaxTest.java +++ b/base/src/test/java/org/aya/syntax/concrete/SyntaxTest.java @@ -25,6 +25,9 @@ def bar (A : Type 0) : A -> A => fn x => {? x ?} open inductive Fin Nat | S n => FZ | S n => FS (Fin n) + open inductive Vec (A : Type) (n : Nat) elim n + | O => vnil + | S m => vcons A (Vec A m) def infixl + Nat Nat : Nat | 0, a => a | S a, b as b' => S (a + b') diff --git a/cli-impl/src/test/resources/negative/GoalAndMeta.txt b/cli-impl/src/test/resources/negative/GoalAndMeta.txt index 85c4828312..e1beb16a73 100644 --- a/cli-impl/src/test/resources/negative/GoalAndMeta.txt +++ b/cli-impl/src/test/resources/negative/GoalAndMeta.txt @@ -190,6 +190,15 @@ Error: Unable to solve the type of this literal: Let's learn from that. NonPattern: +In file C:\Users\hoshino\Documents\Projects\project-aya\aya-dev\cli-impl\src\test\resources\shared\src\data\vec\base.aya:5:6 -> + + 3 │ open inductive Vec (n : Nat) (A : Type) elim n + 4 │ | 0 => [] + 5 │ | suc n => infixr :> A (Vec n A) + │ ╰╯ + +Warning: The name `n` shadows a previous local definition from outer scope + In file $FILE:9:3 -> 6 │ def ++-assoc-type (xs : Vec n A) (ys : Vec m A) (zs : Vec o A) diff --git a/cli-impl/src/test/resources/negative/PatTyckError.txt b/cli-impl/src/test/resources/negative/PatTyckError.txt index 651f1151e8..e955433d45 100644 --- a/cli-impl/src/test/resources/negative/PatTyckError.txt +++ b/cli-impl/src/test/resources/negative/PatTyckError.txt @@ -13,6 +13,15 @@ Error: Unknown constructor Let's learn from that. SelectionFailed: +In file C:\Users\hoshino\Documents\Projects\project-aya\aya-dev\cli-impl\src\test\resources\shared\src\data\vec\base.aya:5:6 -> + + 3 │ open inductive Vec (n : Nat) (A : Type) elim n + 4 │ | 0 => [] + 5 │ | suc n => infixr :> A (Vec n A) + │ ╰╯ + +Warning: The name `n` shadows a previous local definition from outer scope + In file $FILE:4:2 -> 2 │ open import data::vec::base @@ -37,7 +46,7 @@ Error: I'm unsure if there should be a case for as index unification is blocked for type Vec ( + ) A -2 error(s), 0 warning(s). +2 error(s), 1 warning(s). Let's learn from that. SelectionBlocked: diff --git a/cli-impl/src/test/resources/shared/src/data/vec/base.aya b/cli-impl/src/test/resources/shared/src/data/vec/base.aya index 140730357a..50de0a1397 100644 --- a/cli-impl/src/test/resources/shared/src/data/vec/base.aya +++ b/cli-impl/src/test/resources/shared/src/data/vec/base.aya @@ -1,8 +1,8 @@ open import prelude hiding (++) -open inductive Vec Nat Type -| 0, A => [] -| suc n, A => infixr :> A (Vec n A) +open inductive Vec (n : Nat) (A : Type) elim n +| 0 => [] +| suc n => infixr :> A (Vec n A) variable A B : Type variable n m o : Nat diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java index 7562ba4902..25c730970b 100644 --- a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java +++ b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java @@ -41,6 +41,7 @@ public interface AyaPsiElementTypes { IElementType DO_BINDING = new AyaPsiElementType("DO_BINDING"); IElementType DO_BLOCK_CONTENT = new AyaPsiElementType("DO_BLOCK_CONTENT"); IElementType DO_EXPR = new AyaPsiElementType("DO_EXPR"); + IElementType ELIM_DATA_BODY = new AyaPsiElementType("ELIM_DATA_BODY"); IElementType EXPR = new AyaPsiElementType("EXPR"); IElementType FN_BODY = new AyaPsiElementType("FN_BODY"); IElementType FN_DECL = new AyaPsiElementType("FN_DECL"); diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java index 29fab8c069..b28c1d23d2 100644 --- a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java +++ b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java @@ -693,7 +693,7 @@ public static boolean dataConClause(PsiBuilder b, int l) { /* ********************************************************** */ // pragma* declModifier* // KW_DATA declNameOrInfix? - // tele* type? bindBlock? dataBody* + // tele* type? bindBlock? elimDataBody public static boolean dataDecl(PsiBuilder b, int l) { if (!recursion_guard_(b, l, "dataDecl")) return false; boolean r, p; @@ -706,7 +706,7 @@ public static boolean dataDecl(PsiBuilder b, int l) { r = p && report_error_(b, dataDecl_4(b, l + 1)) && r; r = p && report_error_(b, dataDecl_5(b, l + 1)) && r; r = p && report_error_(b, dataDecl_6(b, l + 1)) && r; - r = p && dataDecl_7(b, l + 1) && r; + r = p && elimDataBody(b, l + 1) && r; exit_section_(b, l, m, r, p, null); return r || p; } @@ -765,17 +765,6 @@ private static boolean dataDecl_6(PsiBuilder b, int l) { return true; } - // dataBody* - private static boolean dataDecl_7(PsiBuilder b, int l) { - if (!recursion_guard_(b, l, "dataDecl_7")) return false; - while (true) { - int c = current_position_(b); - if (!dataBody(b, l + 1)) break; - if (!empty_element_parsed_guard_(b, "dataDecl_7", c)) break; - } - return true; - } - /* ********************************************************** */ // fnDecl | primDecl | classDecl | dataDecl public static boolean decl(PsiBuilder b, int l) { @@ -862,6 +851,36 @@ public static boolean doBlockContent(PsiBuilder b, int l) { return r; } + /* ********************************************************** */ + // elims? dataBody* + public static boolean elimDataBody(PsiBuilder b, int l) { + if (!recursion_guard_(b, l, "elimDataBody")) return false; + boolean r; + Marker m = enter_section_(b, l, _NONE_, ELIM_DATA_BODY, ""); + r = elimDataBody_0(b, l + 1); + r = r && elimDataBody_1(b, l + 1); + exit_section_(b, l, m, r, false, null); + return r; + } + + // elims? + private static boolean elimDataBody_0(PsiBuilder b, int l) { + if (!recursion_guard_(b, l, "elimDataBody_0")) return false; + elims(b, l + 1); + return true; + } + + // dataBody* + private static boolean elimDataBody_1(PsiBuilder b, int l) { + if (!recursion_guard_(b, l, "elimDataBody_1")) return false; + while (true) { + int c = current_position_(b); + if (!dataBody(b, l + 1)) break; + if (!empty_element_parsed_guard_(b, "elimDataBody_1", c)) break; + } + return true; + } + /* ********************************************************** */ // KW_ELIM weakId+ static boolean elims(PsiBuilder b, int l) { diff --git a/parser/src/main/grammar/AyaPsiParser.bnf b/parser/src/main/grammar/AyaPsiParser.bnf index 7ebd42c282..b40be7b3e5 100644 --- a/parser/src/main/grammar/AyaPsiParser.bnf +++ b/parser/src/main/grammar/AyaPsiParser.bnf @@ -239,7 +239,9 @@ classMember dataDecl ::= pragma* declModifier* KW_DATA declNameOrInfix? - tele* type? bindBlock? dataBody* { pin=3 } + tele* type? bindBlock? elimDataBody { pin=3 } + +elimDataBody ::= elims? dataBody* dataBody ::= BAR (dataConClause | dataCon) { mixin="org.aya.intellij.psi.impl.AyaPsiGenericDeclImpl" diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java index e5c5dce8a0..f4663a6f78 100644 --- a/producer/src/main/java/org/aya/producer/AyaProducer.java +++ b/producer/src/main/java/org/aya/producer/AyaProducer.java @@ -353,20 +353,28 @@ private void giveMeOpen(@NotNull ModifierParser.Modifiers modiSet, @NotNull Decl } public @Nullable DataDecl dataDecl(GenericNode node, @NotNull MutableList additional) { - var body = node.childrenOfType(DATA_BODY).mapNotNull(this::dataBody).toImmutableSeq(); + var body = node.peekChild(ELIM_DATA_BODY); + if (body == null) return error(body, "Expect data body"); var tele = telescope(node.childrenOfType(TELE)); var info = declInfo(node, ModifierParser.DECL_FILTER); var name = info.checkName(this); if (name == null) return null; var ty = typeOrNull(node.peekChild(TYPE)); - // FIXME: parse elims - var decl = new DataDecl(info.info, name, tele, ty, ImmutableSeq.empty(), body); + var decl = new DataDecl(info.info, name, tele, ty, elimDataBody(body)); if (info.modifier.isExample()) decl.isExample = true; giveMeOpen(info.modifier, decl, additional); pragma(node, decl); return decl; } + public @NotNull MatchBody elimDataBody(@NotNull GenericNode node) { + var elims = node.childrenOfType(WEAK_ID) + .map(this::weakId) + .toImmutableSeq(); + var bodies = node.childrenOfType(DATA_BODY).mapNotNull(this::dataBody).toImmutableSeq(); + return new MatchBody<>(bodies, elims); + } + public @Nullable DataCon dataBody(@NotNull GenericNode node) { var dataConClause = node.peekChild(DATA_CON_CLAUSE); if (dataConClause != null) return dataCon( diff --git a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java index a719dd9b61..ad0158652a 100644 --- a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java +++ b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java @@ -434,11 +434,11 @@ else if (tighters.isEmpty()) return Doc.cat(Doc.line(), Doc.hang(2, Doc.sep( var elimList = elim == null ? body.rawElims.map(x -> Doc.plain(x.data())) : elim.map(BasePrettier::varDoc); - elimLine = Doc.sep(KW_ELIM, Doc.sep(elimList)); + elimLine = Doc.cat(Doc.spaced(KW_ELIM), Doc.sep(elimList)); } var clauses = Doc.emptyIf(body.clauses.isEmpty(), () -> prettier.apply(body.clauses)); - return Doc.vcatNonEmpty(elimLine, clauses); + return Doc.vcat(elimLine, clauses); } private @NotNull Doc visitLetBind(@NotNull Expr.LetBind letBind) { diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/DataDecl.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/DataDecl.java index 07ad01e726..770c84e169 100644 --- a/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/DataDecl.java +++ b/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/DataDecl.java @@ -27,11 +27,10 @@ public DataDecl( @NotNull String name, @NotNull ImmutableSeq telescope, @Nullable WithPos result, - @NotNull ImmutableSeq> elims, - @NotNull ImmutableSeq body + @NotNull MatchBody body ) { super(info, telescope, result); - this.body = new MatchBody<>(body, elims); + this.body = body; this.ref = DefVar.concrete(this, name); body.forEach(con -> con.dataRef = ref); } diff --git a/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/MatchBody.java b/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/MatchBody.java index 11312605b5..7c42da4266 100644 --- a/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/MatchBody.java +++ b/syntax/src/main/java/org/aya/syntax/concrete/stmt/decl/MatchBody.java @@ -41,7 +41,7 @@ public MatchBody(@NotNull ImmutableSeq clauses, @NotNull ImmutableSeq elims) { - assert this.elims != null; + assert this.elims == null; this.elims = elims; }