Skip to content

Commit

Permalink
syntax: update irrefutable lambda syntax
Browse files Browse the repository at this point in the history
  • Loading branch information
@ice1000
ice1000 committed Jan 20, 2025
1 parent a734bb6 commit 47ba19a
Show file tree
Hide file tree
Showing 4 changed files with 122 additions and 51 deletions.
4 changes: 3 additions & 1 deletion parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand Down
119 changes: 84 additions & 35 deletions parser/src/main/gen/org/aya/parser/AyaPsiParser.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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),
};

/* ********************************************************** */
Expand Down Expand Up @@ -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 | <<licit lambdaTeleBinder>>
public static boolean lambdaTele(PsiBuilder b, int l) {
Expand Down Expand Up @@ -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, "<expr>");
Expand All @@ -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);
Expand All @@ -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);
}
Expand Down Expand Up @@ -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 <<braced (patterns lambdaBody)>>
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;
Expand Down Expand Up @@ -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;
}
Expand Down
21 changes: 14 additions & 7 deletions parser/src/main/grammar/AyaPsiParser.bnf
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -258,7 +258,9 @@ expr ::= newExpr
| piExpr
| forallExpr
| sigmaExpr
| lambdaExpr
| lambda0Expr
| lambda1Expr
| lambda2Expr
| matchExpr
| letExpr
| doExpr
Expand Down Expand Up @@ -286,24 +288,28 @@ 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? <<commaSep doBlockContent>> 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"
}
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 <<braced (patterns lambdaBody)>>
lambda2Expr ::= KW_LAMBDA unitPattern lambdaBody?

doBlockContent ::= doBinding | expr
doExpr ::= KW_DO LBRACE? <<commaSep doBlockContent>> RBRACE?

matchType ::= (KW_AS <<commaSep weakId>>)? KW_RETURNS expr
matchExpr ::= KW_MATCH KW_ELIM? exprList matchType? clauses

argument ::= atomExArgument
| tupleImArgument
Expand All @@ -315,6 +321,7 @@ namedImArgument ::= <<braced (weakId DEFINE_AS expr)>>
projFix ::= DOT (NUMBER | projFixId)
// kiva: Used in IntelliJ IDEA
projFixId ::= qualifiedId
projExpr ::= expr projFix

clauses ::= <<braced (bareClause? barredClause*)>>

Expand Down Expand Up @@ -375,7 +382,7 @@ teleParamName ::= weakId {
implements="org.aya.intellij.psi.AyaPsiNamedWeakId"
}

// lambda tele is always named
// named tele
lambdaTele ::= teleParamName | <<licit lambdaTeleBinder>>

lambdaTeleBinder ::= teleBinderTyped
Expand Down
29 changes: 21 additions & 8 deletions producer/src/main/java/org/aya/producer/AyaProducer.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,21 @@
// 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;
import com.intellij.psi.tree.IElementType;
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;
Expand Down Expand Up @@ -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:
* <ul>
Expand Down Expand Up @@ -654,17 +655,29 @@ private record DeclNameOrInfix(@NotNull WithPos<String> 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<Expr> result;
var bodyExpr = node.peekChild(EXPR);
if (bodyExpr == null) {
var impliesToken = node.peekChild(IMPLIES);
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<WithPos<Expr>> 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(
Expand Down

0 comments on commit 47ba19a

Please sign in to comment.