From 47ba19a13b713a5d59ece031964e4718be2c5d17 Mon Sep 17 00:00:00 2001 From: ice1000 Date: Mon, 20 Jan 2025 02:48:42 -0500 Subject: [PATCH] syntax: update irrefutable lambda syntax --- .../org/aya/parser/AyaPsiElementTypes.java | 4 +- .../main/gen/org/aya/parser/AyaPsiParser.java | 119 ++++++++++++------ parser/src/main/grammar/AyaPsiParser.bnf | 21 ++-- .../java/org/aya/producer/AyaProducer.java | 29 +++-- 4 files changed, 122 insertions(+), 51 deletions(-) diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java index 53a9265f2..9902468ef 100644 --- a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java +++ b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java @@ -55,7 +55,9 @@ public interface AyaPsiElementTypes { IElementType IDIOM_ATOM = new AyaPsiElementType("IDIOM_ATOM"); IElementType IDIOM_BLOCK = new AyaPsiElementType("IDIOM_BLOCK"); IElementType IMPORT_CMD = new AyaPsiElementType("IMPORT_CMD"); - IElementType LAMBDA_EXPR = new AyaPsiElementType("LAMBDA_EXPR"); + IElementType LAMBDA_0_EXPR = new AyaPsiElementType("LAMBDA_0_EXPR"); + IElementType LAMBDA_1_EXPR = new AyaPsiElementType("LAMBDA_1_EXPR"); + IElementType LAMBDA_2_EXPR = new AyaPsiElementType("LAMBDA_2_EXPR"); IElementType LAMBDA_TELE = new AyaPsiElementType("LAMBDA_TELE"); IElementType LAMBDA_TELE_BINDER = new AyaPsiElementType("LAMBDA_TELE_BINDER"); IElementType LET_BIND = new AyaPsiElementType("LET_BIND"); diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java index fb8643bec..c54b58a31 100644 --- a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java +++ b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java @@ -47,11 +47,11 @@ static boolean parse_root_(IElementType t, PsiBuilder b, int l) { PRIM_DECL, STMT), create_token_set_(APP_EXPR, ARRAY_ATOM, ARROW_EXPR, ATOM_EXPR, CALM_FACE_EXPR, DO_EXPR, EXPR, FORALL_EXPR, - GOAL_EXPR, HOLE_EXPR, IDIOM_ATOM, LAMBDA_EXPR, - LET_EXPR, LITERAL, LIT_INT_EXPR, LIT_STRING_EXPR, - MATCH_EXPR, NEW_EXPR, PI_EXPR, PROJ_EXPR, - REF_EXPR, SELF_EXPR, SIGMA_EXPR, TUPLE_ATOM, - ULIFT_ATOM, UNIV_EXPR), + GOAL_EXPR, HOLE_EXPR, IDIOM_ATOM, LAMBDA_0_EXPR, + LAMBDA_1_EXPR, LAMBDA_2_EXPR, LET_EXPR, LITERAL, + LIT_INT_EXPR, LIT_STRING_EXPR, MATCH_EXPR, NEW_EXPR, + PI_EXPR, PROJ_EXPR, REF_EXPR, SELF_EXPR, + SIGMA_EXPR, TUPLE_ATOM, ULIFT_ATOM, UNIV_EXPR), }; /* ********************************************************** */ @@ -1192,6 +1192,19 @@ private static boolean importCmd_3_0(PsiBuilder b, int l) { return r; } + /* ********************************************************** */ + // IMPLIES expr + static boolean lambdaBody(PsiBuilder b, int l) { + if (!recursion_guard_(b, l, "lambdaBody")) return false; + if (!nextTokenIs(b, IMPLIES)) 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; + } + /* ********************************************************** */ // teleParamName | <> public static boolean lambdaTele(PsiBuilder b, int l) { @@ -2241,15 +2254,17 @@ public static boolean weakId(PsiBuilder b, int l) { // 1: PREFIX(piExpr) // 2: PREFIX(forallExpr) // 3: PREFIX(sigmaExpr) - // 4: ATOM(lambdaExpr) - // 5: ATOM(matchExpr) - // 6: PREFIX(letExpr) - // 7: ATOM(doExpr) - // 8: ATOM(selfExpr) - // 9: ATOM(atomExpr) - // 10: BINARY(arrowExpr) - // 11: POSTFIX(appExpr) - // 12: POSTFIX(projExpr) + // 4: ATOM(lambda0Expr) + // 5: ATOM(lambda1Expr) + // 6: ATOM(lambda2Expr) + // 7: ATOM(matchExpr) + // 8: PREFIX(letExpr) + // 9: ATOM(doExpr) + // 10: ATOM(selfExpr) + // 11: ATOM(atomExpr) + // 12: BINARY(arrowExpr) + // 13: POSTFIX(appExpr) + // 14: POSTFIX(projExpr) public static boolean expr(PsiBuilder b, int l, int g) { if (!recursion_guard_(b, l, "expr")) return false; addVariant(b, ""); @@ -2259,7 +2274,9 @@ public static boolean expr(PsiBuilder b, int l, int g) { if (!r) r = piExpr(b, l + 1); if (!r) r = forallExpr(b, l + 1); if (!r) r = sigmaExpr(b, l + 1); - if (!r) r = lambdaExpr(b, l + 1); + if (!r) r = lambda0Expr(b, l + 1); + if (!r) r = lambda1Expr(b, l + 1); + if (!r) r = lambda2Expr(b, l + 1); if (!r) r = matchExpr(b, l + 1); if (!r) r = letExpr(b, l + 1); if (!r) r = doExpr(b, l + 1); @@ -2276,15 +2293,15 @@ public static boolean expr_0(PsiBuilder b, int l, int g) { boolean r = true; while (true) { Marker m = enter_section_(b, l, _LEFT_, null); - if (g < 10 && consumeTokenSmart(b, TO)) { - r = expr(b, l, 9); + if (g < 12 && consumeTokenSmart(b, TO)) { + r = expr(b, l, 11); exit_section_(b, l, m, ARROW_EXPR, r, true, null); } - else if (g < 11 && appExpr_0(b, l + 1)) { + else if (g < 13 && appExpr_0(b, l + 1)) { r = true; exit_section_(b, l, m, APP_EXPR, r, true, null); } - else if (g < 12 && projFix(b, l + 1)) { + else if (g < 14 && projFix(b, l + 1)) { r = true; exit_section_(b, l, m, PROJ_EXPR, r, true, null); } @@ -2425,37 +2442,69 @@ private static boolean sigmaExpr_0_1(PsiBuilder b, int l) { return r; } - // KW_LAMBDA patterns (IMPLIES expr)? - public static boolean lambdaExpr(PsiBuilder b, int l) { - if (!recursion_guard_(b, l, "lambdaExpr")) return false; + // KW_LAMBDA teleBinderUntyped lambdaBody? + public static boolean lambda0Expr(PsiBuilder b, int l) { + if (!recursion_guard_(b, l, "lambda0Expr")) return false; if (!nextTokenIsSmart(b, KW_LAMBDA)) return false; boolean r; Marker m = enter_section_(b); r = consumeTokenSmart(b, KW_LAMBDA); - r = r && patterns(b, l + 1); - r = r && lambdaExpr_2(b, l + 1); - exit_section_(b, m, LAMBDA_EXPR, r); + r = r && teleBinderUntyped(b, l + 1); + r = r && lambda0Expr_2(b, l + 1); + exit_section_(b, m, LAMBDA_0_EXPR, r); return r; } - // (IMPLIES expr)? - private static boolean lambdaExpr_2(PsiBuilder b, int l) { - if (!recursion_guard_(b, l, "lambdaExpr_2")) return false; - lambdaExpr_2_0(b, l + 1); + // lambdaBody? + private static boolean lambda0Expr_2(PsiBuilder b, int l) { + if (!recursion_guard_(b, l, "lambda0Expr_2")) return false; + lambdaBody(b, l + 1); return true; } - // IMPLIES expr - private static boolean lambdaExpr_2_0(PsiBuilder b, int l) { - if (!recursion_guard_(b, l, "lambdaExpr_2_0")) return false; + // KW_LAMBDA <> + public static boolean lambda1Expr(PsiBuilder b, int l) { + if (!recursion_guard_(b, l, "lambda1Expr")) return false; + if (!nextTokenIsSmart(b, KW_LAMBDA)) return false; boolean r; Marker m = enter_section_(b); - r = consumeTokenSmart(b, IMPLIES); - r = r && expr(b, l + 1, -1); + r = consumeTokenSmart(b, KW_LAMBDA); + r = r && braced(b, l + 1, AyaPsiParser::lambda1Expr_1_0); + exit_section_(b, m, LAMBDA_1_EXPR, r); + return r; + } + + // patterns lambdaBody + private static boolean lambda1Expr_1_0(PsiBuilder b, int l) { + if (!recursion_guard_(b, l, "lambda1Expr_1_0")) return false; + boolean r; + Marker m = enter_section_(b); + r = patterns(b, l + 1); + r = r && lambdaBody(b, l + 1); exit_section_(b, m, null, r); return r; } + // KW_LAMBDA unitPattern lambdaBody? + public static boolean lambda2Expr(PsiBuilder b, int l) { + if (!recursion_guard_(b, l, "lambda2Expr")) return false; + if (!nextTokenIsSmart(b, KW_LAMBDA)) return false; + boolean r; + Marker m = enter_section_(b); + r = consumeTokenSmart(b, KW_LAMBDA); + r = r && unitPattern(b, l + 1); + r = r && lambda2Expr_2(b, l + 1); + exit_section_(b, m, LAMBDA_2_EXPR, r); + return r; + } + + // lambdaBody? + private static boolean lambda2Expr_2(PsiBuilder b, int l) { + if (!recursion_guard_(b, l, "lambda2Expr_2")) return false; + lambdaBody(b, l + 1); + return true; + } + // KW_MATCH KW_ELIM? exprList matchType? clauses public static boolean matchExpr(PsiBuilder b, int l) { if (!recursion_guard_(b, l, "matchExpr")) return false; @@ -2492,7 +2541,7 @@ public static boolean letExpr(PsiBuilder b, int l) { Marker m = enter_section_(b, l, _NONE_, null); r = letExpr_0(b, l + 1); p = r; - r = p && expr(b, l, 6); + r = p && expr(b, l, 8); exit_section_(b, l, m, LET_EXPR, r, p, null); return r || p; } diff --git a/parser/src/main/grammar/AyaPsiParser.bnf b/parser/src/main/grammar/AyaPsiParser.bnf index b1d1b81c8..3cb307523 100644 --- a/parser/src/main/grammar/AyaPsiParser.bnf +++ b/parser/src/main/grammar/AyaPsiParser.bnf @@ -136,7 +136,7 @@ ] // IMPORTANT: when editing extends(..), please also modify `AyaGKProducer` accordingly! - extends("newExpr|piExpr|forallExpr|sigmaExpr|lambdaExpr|matchExpr|letExpr|doExpr|idiomExpr|arrayExpr|atomExpr|appExpr|arrowExpr|projExpr|selfExpr|partialExpr|pathExpr") = expr + extends("(new|pi|forall|sigma|lambda.|match|let|do|idiom|array|atom|app|arrow|proj|self|partial)Expr") = expr extends("literal") = expr extends("refExpr|holeExpr|lit.+Expr|univExpr") = literal extends("goalExpr|calmFaceExpr") = holeExpr @@ -258,7 +258,9 @@ expr ::= newExpr | piExpr | forallExpr | sigmaExpr - | lambdaExpr + | lambda0Expr + | lambda1Expr + | lambda2Expr | matchExpr | letExpr | doExpr @@ -286,14 +288,11 @@ idiomBlock ::= barred* expr newExpr ::= KW_NEW expr // newBody? appExpr ::= expr argument+ arrowExpr ::= expr TO expr { rightAssociative = true } -projExpr ::= expr projFix piExpr ::= KW_PI tele+ TO expr forallExpr ::= KW_FORALL lambdaTele+ TO expr sigmaExpr ::= KW_SIGMA tele+ SUCHTHAT expr -lambdaExpr ::= KW_LAMBDA patterns (IMPLIES expr)? -matchExpr ::= KW_MATCH KW_ELIM? exprList matchType? clauses -doExpr ::= KW_DO LBRACE? <> RBRACE? selfExpr ::= KW_SELF (AT qualifiedId)? + letBind ::= weakId lambdaTele* type? DEFINE_AS expr { mixin="org.aya.intellij.psi.impl.AyaPsiNamedWeakIdImpl" implements="org.aya.intellij.psi.AyaPsiNamedWeakId" @@ -301,9 +300,16 @@ letBind ::= weakId lambdaTele* type? DEFINE_AS expr { letBindBlock ::= letBind | (BAR letBind)+ letExpr ::= KW_LET (KW_OPEN qualifiedId useHide? | letBindBlock) KW_IN expr +private lambdaBody ::= IMPLIES expr +lambda0Expr ::= KW_LAMBDA teleBinderUntyped lambdaBody? +lambda1Expr ::= KW_LAMBDA <> +lambda2Expr ::= KW_LAMBDA unitPattern lambdaBody? + doBlockContent ::= doBinding | expr +doExpr ::= KW_DO LBRACE? <> RBRACE? matchType ::= (KW_AS <>)? KW_RETURNS expr +matchExpr ::= KW_MATCH KW_ELIM? exprList matchType? clauses argument ::= atomExArgument | tupleImArgument @@ -315,6 +321,7 @@ namedImArgument ::= <> projFix ::= DOT (NUMBER | projFixId) // kiva: Used in IntelliJ IDEA projFixId ::= qualifiedId +projExpr ::= expr projFix clauses ::= <> @@ -375,7 +382,7 @@ teleParamName ::= weakId { implements="org.aya.intellij.psi.AyaPsiNamedWeakId" } -// lambda tele is always named +// named tele lambdaTele ::= teleParamName | <> lambdaTeleBinder ::= teleBinderTyped diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java index 165c1895b..24cadbfb4 100644 --- a/producer/src/main/java/org/aya/producer/AyaProducer.java +++ b/producer/src/main/java/org/aya/producer/AyaProducer.java @@ -2,6 +2,11 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.producer; +import java.util.Arrays; +import java.util.stream.Collectors; + +import static org.aya.parser.AyaPsiElementTypes.*; + import com.intellij.lexer.FlexLexer; import com.intellij.openapi.util.TextRange; import com.intellij.openapi.util.text.StringUtil; @@ -9,7 +14,9 @@ import com.intellij.psi.tree.TokenSet; import kala.collection.SeqView; import kala.collection.immutable.ImmutableSeq; -import kala.collection.mutable.*; +import kala.collection.mutable.FreezableMutableList; +import kala.collection.mutable.MutableList; +import kala.collection.mutable.MutableSinglyLinkedList; import kala.control.Either; import kala.control.Option; import kala.function.BooleanObjBiFunction; @@ -45,12 +52,6 @@ import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; -import java.util.Arrays; -import java.util.Objects; -import java.util.stream.Collectors; - -import static org.aya.parser.AyaPsiElementTypes.*; - /** * Working with GK parser: *
    @@ -654,7 +655,7 @@ private record DeclNameOrInfix(@NotNull WithPos name, @Nullable OpDecl.O if (node.is(SIGMA_EXPR)) return Expr.buildSigma(pos, telescope(node.childrenOfType(TELE)).view(), expr(node.child(EXPR))); - if (node.is(LAMBDA_EXPR)) { + if (node.is(LAMBDA_0_EXPR)) { WithPos result; var bodyExpr = node.peekChild(EXPR); if (bodyExpr == null) { @@ -662,9 +663,21 @@ private record DeclNameOrInfix(@NotNull WithPos name, @Nullable OpDecl.O var bodyHolePos = impliesToken == null ? pos : sourcePosOf(impliesToken); result = new WithPos<>(bodyHolePos, new Expr.Hole(false, null)); } else result = expr(bodyExpr); + var tele = teleBinderUntyped(node.child(TELE_BINDER_UNTYPED)).view() + .map(LocalVar::from); + return Expr.buildLam(pos, tele, result); + } + if (node.is(LAMBDA_1_EXPR)) { + var result = expr(node.child(EXPR)); var tele = patterns(node.child(PATTERNS).child(COMMA_SEP)); return new WithPos<>(pos, new Expr.IrrefutableLam(new Pattern.Clause(pos, tele, Option.some(result)))); } + if (node.is(LAMBDA_2_EXPR)) { + var bodyExpr = node.peekChild(EXPR); + Option> result = bodyExpr == null ? Option.none() : Option.some(expr(bodyExpr)); + var tele = unitPattern(node.child(UNIT_PATTERN)); + return new WithPos<>(pos, new Expr.IrrefutableLam(new Pattern.Clause(pos, ImmutableSeq.of(tele), result))); + } if (node.is(IDIOM_ATOM)) { var block = node.peekChild(IDIOM_BLOCK); var names = new Expr.IdiomNames(