diff --git a/base/src/main/java/org/aya/resolve/salt/Desalt.java b/base/src/main/java/org/aya/resolve/salt/Desalt.java index e91ed60229..af2f15729f 100644 --- a/base/src/main/java/org/aya/resolve/salt/Desalt.java +++ b/base/src/main/java/org/aya/resolve/salt/Desalt.java @@ -1,11 +1,13 @@ -// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang. +// Copyright (c) 2020-2025 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.resolve.salt; +import kala.collection.immutable.ImmutableSeq; import org.aya.generic.term.SortKind; import org.aya.resolve.ResolveInfo; import org.aya.syntax.concrete.Expr; import org.aya.syntax.concrete.Pattern; +import org.aya.syntax.ref.LocalVar; import org.aya.util.error.Panic; import org.aya.util.error.PosedUnaryOperator; import org.aya.util.error.SourcePos; @@ -70,6 +72,41 @@ public final class Desalt implements PosedUnaryOperator { case Expr.Idiom idiom -> throw new UnsupportedOperationException("TODO"); case Expr.RawSort(var kind) -> new Expr.Sort(kind, 0); case Expr.LetOpen letOpen -> apply(letOpen.body()); + case Expr.ClauseLam lam -> { + var isVanilla = lam.patterns().allMatch(x -> x.term().data() instanceof Pattern.BindLike); + + ImmutableSeq lamTele; + WithPos realBody; + + if (isVanilla) { + // fn a _ c => ... + lamTele = lam.patterns().map(x -> ((Pattern.BindLike) x.term().data()).toLocalVar(x.term().sourcePos())); + realBody = lam.body(); + } else { + lamTele = lam.patterns().mapIndexed((idx, pat) -> { + if (pat.term().data() instanceof Pattern.BindLike bindLike) { + var bind = bindLike.toLocalVar(pat.term().sourcePos()); + // we need fresh bind, since [bind] may be used in the body. + return LocalVar.generate(bind.name(), SourcePos.NONE); + } else { + return LocalVar.generate("IrrefutableLam" + idx, SourcePos.NONE); + } + }); + + // fn a' _ c' => match a', _, c' { a, _, (con c) => ... } + // the var with prime are renamed vars + + realBody = new WithPos<>(sourcePos, new Expr.Match( + lamTele.map(x -> new WithPos<>(x.definition(), new Expr.Ref(x))), + ImmutableSeq.of(lam.clause()), + ImmutableSeq.empty(), + true, + null + )); + } + + yield apply(Expr.buildLam(sourcePos, lamTele.view(), realBody)); + } }; } public @NotNull PosedUnaryOperator pattern = new Pat(); diff --git a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java index 7cb0f378ae..d304a16ad3 100644 --- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java @@ -1,4 +1,4 @@ -// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang. +// Copyright (c) 2020-2025 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.resolve.visitor; @@ -30,7 +30,6 @@ import org.aya.util.error.WithPos; import org.jetbrains.annotations.Contract; import org.jetbrains.annotations.NotNull; -import org.jetbrains.annotations.Nullable; /** * Resolves bindings. @@ -116,11 +115,7 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) { return switch (pre(expr)) { case Expr.Do doExpr -> doExpr.update(apply(SourcePos.NONE, doExpr.bindName()), bind(doExpr.binds(), MutableValue.create(ctx))); - case Expr.Lambda lam -> { - var mCtx = MutableValue.create(ctx); - mCtx.update(ctx -> ctx.bind(lam.ref())); - yield lam.update(lam.body().descent(enter(mCtx.get()))); - } + case Expr.ClauseLam lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause())); case Expr.DepType depType -> { var mCtx = MutableValue.create(ctx); var param = bind(depType.param(), mCtx); @@ -202,6 +197,8 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) { yield match.update(discriminant, clauses, returns); } + // Expr.Lambda is a desugar target, which is produced after resolving. + case Expr.Lambda _ -> Panic.unreachable(); case Expr newExpr -> newExpr.descent(this); }; } @@ -235,6 +232,9 @@ private void addReference(@NotNull DefVar defVar) { return clause.update(pats, body); } + /// Resolve a [Pattern] + /// + /// @param telescope the telescope of the clause which the {@param pattern} lives, can be [ImmutableSeq#empty()]. public @NotNull WithPos resolvePattern(@NotNull WithPos pattern, @NotNull ImmutableSeq telescope, MutableValue ctx) { var resolver = new PatternResolver(ctx.get(), telescope, this::addReference); var result = pattern.descent(resolver); diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java index 60b9fa2dc9..2e8cabbd38 100644 --- a/base/src/main/java/org/aya/tyck/ExprTycker.java +++ b/base/src/main/java/org/aya/tyck/ExprTycker.java @@ -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.tyck; +import kala.collection.AbstractSeqView; import kala.collection.immutable.ImmutableSeq; import kala.collection.immutable.ImmutableTreeSeq; import kala.collection.mutable.MutableList; diff --git a/cli-impl/src/test/resources/negative/ExprTyckError.txt b/cli-impl/src/test/resources/negative/ExprTyckError.txt index 44f3bb8299..66a7b99fcb 100644 --- a/cli-impl/src/test/resources/negative/ExprTyckError.txt +++ b/cli-impl/src/test/resources/negative/ExprTyckError.txt @@ -46,7 +46,7 @@ In file $FILE:2:19 -> │ ╰──────╯ Error: The following abstraction is not good: - \ x ⇒ x + fn x ⇒ x because the type being expected is not a Pi/Path type, but instead: Type 0 @@ -225,11 +225,11 @@ In file $FILE:3:4 -> Error: The following application is not good: match a { - | _ ⇒ \ x ⇒ x + | _ ⇒ fn x ⇒ x } 1 because the type of what you applied is not a Pi/Path type, but instead: 2 error(s), 0 warning(s). diff --git a/cli-impl/src/test/resources/negative/GoalAndMeta.txt b/cli-impl/src/test/resources/negative/GoalAndMeta.txt index 85c4828312..c2ded0f29a 100644 --- a/cli-impl/src/test/resources/negative/GoalAndMeta.txt +++ b/cli-impl/src/test/resources/negative/GoalAndMeta.txt @@ -281,7 +281,7 @@ In file $FILE:11:12 -> │ ╰───────────────────────────╯ Error: Cannot check the expression - pmap (\ _ ⇒ x :> _) (++-assoc' _ _ _) + pmap (fn _ ⇒ x :> _) (++-assoc' _ _ _) of type (=) {?B A x n m o _ ys zs} (x :> ?a A x n m o _ ys zs) (x :> ?b A x n m o _ ys zs) diff --git a/cli-impl/src/test/resources/success/src/Test.aya b/cli-impl/src/test/resources/success/src/Test.aya index 5549fa8e42..0972efe01f 100644 --- a/cli-impl/src/test/resources/success/src/Test.aya +++ b/cli-impl/src/test/resources/success/src/Test.aya @@ -105,3 +105,13 @@ module Issue1249 { variable A B : Type def transp (p : A = B) (a : A) : B => coe 0 1 p a } + +module Issue94 { + def absurd (A : Type) : Empty -> A => fn () + def obvious : Fn (a : Sig Nat ** Nat) -> Nat => fn { (a, b) => a + b } +} + +// relies on match elim +// open inductive IsZero Nat +// | zero => ack +// def irrefutable : Fn (a : Nat) -> IsZero a -> Nat => fn { zero, ack => 233 } diff --git a/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java b/parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java index 53a9265f2e..9902468ef3 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 7cf5155955..c54b58a31b 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 teleBinderUntyped (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 && teleBinderUntyped(b, l + 1); - r = r && lambdaExpr_2(b, l + 1); - exit_section_(b, m, LAMBDA_EXPR, r); + 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 c70ba53d5f..3cb307523b 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 teleBinderUntyped (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 d3d71de802..b4e05df3d6 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) { @@ -663,8 +664,22 @@ private record DeclNameOrInfix(@NotNull WithPos name, @Nullable OpDecl.O 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); + .map(LocalVar::from) + .map(v -> new WithPos(v.definition(), new Pattern.Bind(v))) + .map(Arg::ofExplicitly) + .toImmutableSeq(); + return new WithPos<>(pos, new Expr.ClauseLam(new Pattern.Clause(pos, tele, Option.some(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.ClauseLam(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.ClauseLam(new Pattern.Clause(pos, ImmutableSeq.of(tele), result))); } if (node.is(IDIOM_ATOM)) { var block = node.peekChild(IDIOM_BLOCK); diff --git a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java index 36dfd12e6e..cd17e8679b 100644 --- a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java +++ b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java @@ -2,12 +2,17 @@ // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file. package org.aya.prettier; +import java.util.Locale; +import java.util.Objects; +import java.util.function.Function; + +import static org.aya.prettier.Tokens.*; + import com.intellij.openapi.util.text.StringUtil; import kala.collection.Seq; import kala.collection.SeqLike; import kala.collection.SeqView; import kala.collection.immutable.ImmutableSeq; -import kala.collection.mutable.MutableEnumSet; import kala.collection.mutable.MutableList; import kala.range.primitive.IntRange; import org.aya.generic.Constants; @@ -25,19 +30,12 @@ import org.aya.syntax.ref.DefVar; import org.aya.syntax.ref.LocalVar; import org.aya.util.Arg; -import org.aya.util.IterableUtil; import org.aya.util.binop.Assoc; import org.aya.util.error.WithPos; import org.aya.util.prettier.PrettierOptions; import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; -import java.util.Locale; -import java.util.Objects; -import java.util.function.Function; - -import static org.aya.prettier.Tokens.*; - /** * @author ice1000, kiva */ @@ -118,6 +116,7 @@ yield visitConcreteCalls(assoc, } yield checkParen(outer, Doc.sep(prelude), Outer.BinOp); } + case Expr.ClauseLam(var cls) -> checkParen(outer, visitLambda(cls), Outer.BinOp); case Expr.Hole expr -> { if (!expr.explicit()) yield Doc.symbol(Constants.ANONYMOUS_PREFIX); var filling = expr.filling(); @@ -278,7 +277,7 @@ private Doc visitMaybeConPatterns(SeqLike>> patterns, Outer return Doc.join(delim, patterns.view().map(p -> pattern(p.map(WithPos::data), outer))); } - public Doc matchy(@NotNull Pattern.Clause match) { + public Doc clause(@NotNull Pattern.Clause match) { var doc = visitMaybeConPatterns(match.patterns, Outer.Free, Doc.plain(", ")); return match.expr.map(e -> Doc.sep(doc, FN_DEFINED_AS, term(Outer.Free, e))).getOrDefault(doc); } @@ -417,7 +416,7 @@ private Doc visitAccess(@NotNull Accessibility acc, @Nullable Accessibility theD private Doc visitClauses(@NotNull ImmutableSeq clauses) { if (clauses.isEmpty()) return Doc.empty(); return Doc.vcat(clauses.view() - .map(this::matchy) + .map(this::clause) .map(doc -> Doc.sep(BAR, doc))); } @@ -489,4 +488,11 @@ else if (tighters.isEmpty()) return Doc.cat(Doc.line(), Doc.hang(2, Doc.sep( ) { return visitCalls(assoc, fn, args.map(x -> new Arg<>(x.term().data(), x.explicit())), outer, showImplicits); } + + private @NotNull Doc visitLambda(@NotNull Pattern.Clause clause) { + var prelude = MutableList.of(LAMBDA); + var clauseDoc = clause(clause); + prelude.append(Doc.braced(clauseDoc)); + return Doc.sep(prelude); + } } diff --git a/syntax/src/main/java/org/aya/prettier/Tokens.java b/syntax/src/main/java/org/aya/prettier/Tokens.java index 0b65f50d70..ed765fccfc 100644 --- a/syntax/src/main/java/org/aya/prettier/Tokens.java +++ b/syntax/src/main/java/org/aya/prettier/Tokens.java @@ -12,7 +12,7 @@ public final class Tokens { private Tokens() { } - public static final Doc LAMBDA = Doc.styled(KEYWORD, Doc.symbol("\\")); + public static final Doc LAMBDA = Doc.styled(KEYWORD, Doc.symbol("fn")); public static final Doc ARROW = Doc.symbol("->"); public static final Doc LARROW = Doc.symbol("<-"); public static final Doc FN_DEFINED_AS = Doc.symbol("=>"); diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java index f4c1f26d6f..690dd52b35 100644 --- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java +++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java @@ -1,7 +1,11 @@ -// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang. +// Copyright (c) 2020-2025 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.syntax.concrete; +import java.util.function.BiFunction; +import java.util.function.Consumer; +import java.util.function.Function; + import kala.collection.SeqView; import kala.collection.immutable.ImmutableSeq; import kala.control.Either; @@ -18,6 +22,7 @@ import org.aya.syntax.core.term.Term; import org.aya.syntax.ref.AnyVar; import org.aya.syntax.ref.LocalVar; +import org.aya.util.Arg; import org.aya.util.BinOpElem; import org.aya.util.ForLSP; import org.aya.util.error.*; @@ -25,10 +30,6 @@ import org.jetbrains.annotations.NotNull; import org.jetbrains.annotations.Nullable; -import java.util.function.BiFunction; -import java.util.function.Consumer; -import java.util.function.Function; - public sealed interface Expr extends AyaDocile { @NotNull Expr descent(@NotNull PosedUnaryOperator<@NotNull Expr> f); void forEach(@NotNull PosedConsumer<@NotNull Expr> f); @@ -72,8 +73,7 @@ public Param(@NotNull SourcePos sourcePos, @NotNull LocalVar ref, @NotNull WithP } /// @param filling the inner expr of goal - /// @param explicit whether the hole is a type-directed programming goal or - /// a to-be-solved by tycking hole. + /// @param explicit whether the hole is a type-directed programming goal or a to-be-solved by tycking hole. record Hole( boolean explicit, @Nullable WithPos filling, @@ -134,6 +134,34 @@ public Ref(@NotNull AnyVar var) { @Override public void forEach(@NotNull PosedConsumer f) { } } + record ClauseLam(@NotNull Pattern.Clause clause) implements Expr, Sugar { + public static boolean canBeBind(@NotNull Arg> pat) { + var thePat = pat.term().data(); + return thePat instanceof Pattern.Bind || thePat == Pattern.CalmFace.INSTANCE; + } + + public ClauseLam { + assert clause.patterns.isNotEmpty(); + } + + public @NotNull Expr.ClauseLam update(@NotNull Pattern.Clause clause) { + return clause == this.clause ? this : new ClauseLam(clause); + } + + public @NotNull ImmutableSeq>> patterns() { return clause.patterns; } + public @NotNull WithPos body() { return clause.expr.get(); } + + @Override public @NotNull Expr.ClauseLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) { + return descent(f, PosedUnaryOperator.identity()); + } + + public @NotNull Expr.ClauseLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f, @NotNull PosedUnaryOperator<@NotNull Pattern> g) { + return update(clause.descent(f, g)); + } + + @Override public void forEach(@NotNull PosedConsumer f) { clause.forEach(f, (_, _) -> { }); } + } + record Lambda( @NotNull LocalVar ref, @Override @NotNull WithPos body diff --git a/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java b/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java index 13aeb69f95..1cde7028f6 100644 --- a/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java +++ b/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java @@ -1,4 +1,4 @@ -// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang. +// Copyright (c) 2020-2025 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.syntax.concrete; @@ -31,6 +31,15 @@ public sealed interface Pattern extends AyaDocile { void forEach(@NotNull PosedConsumer<@NotNull Pattern> f); interface Salt { } + /// Whether a [Pattern] can be a [Pattern.Bind], this is used by [Expr.ClauseLam] in desugarer. + /// + /// @see Pattern.Bind + /// @see Pattern.CalmFace + interface BindLike { + /// Returns the [LocalVar] this [Pattern] introduced, with [SourcePos] {@param pos} if it doesn't have one. + @NotNull LocalVar toLocalVar(@NotNull SourcePos pos); + } + @NotNull Pattern descent(@NotNull PosedUnaryOperator<@NotNull Pattern> f); @Override default @NotNull Doc toDoc(@NotNull PrettierOptions options) { @@ -63,11 +72,12 @@ enum Absurd implements Pattern { @Override public @NotNull Pattern descent(@NotNull PosedUnaryOperator<@NotNull Pattern> f) { return this; } } - enum CalmFace implements Pattern { + enum CalmFace implements Pattern, BindLike { INSTANCE; @Override public void forEach(@NotNull PosedConsumer<@NotNull Pattern> f) { } @Override public @NotNull Pattern descent(@NotNull PosedUnaryOperator<@NotNull Pattern> f) { return this; } + @Override public @NotNull LocalVar toLocalVar(@NotNull SourcePos pos) { return LocalVar.generate(pos); } } /** @@ -76,10 +86,11 @@ enum CalmFace implements Pattern { record Bind( @NotNull LocalVar bind, @ForLSP @NotNull MutableValue<@Nullable Term> type - ) implements Pattern { + ) implements Pattern, BindLike { public Bind(@NotNull LocalVar bind) { this(bind, MutableValue.create()); } @Override public void forEach(@NotNull PosedConsumer<@NotNull Pattern> f) { } @Override public @NotNull Bind descent(@NotNull PosedUnaryOperator<@NotNull Pattern> f) { return this; } + @Override public @NotNull LocalVar toLocalVar(@NotNull SourcePos pos) { return bind; } } record Con( diff --git a/syntax/src/main/java/org/aya/syntax/ref/LocalVar.java b/syntax/src/main/java/org/aya/syntax/ref/LocalVar.java index df4a029e24..d25ae0fca7 100644 --- a/syntax/src/main/java/org/aya/syntax/ref/LocalVar.java +++ b/syntax/src/main/java/org/aya/syntax/ref/LocalVar.java @@ -1,7 +1,8 @@ -// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang. +// Copyright (c) 2020-2025 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.syntax.ref; +import org.aya.generic.Constants; import org.aya.util.error.SourceNode; import org.aya.util.error.SourcePos; import org.aya.util.error.WithPos; @@ -21,6 +22,10 @@ public LocalVar(@NotNull String name, @NotNull SourcePos definition) { this(name, definition, GenerateKind.Basic.None); } + public static @NotNull LocalVar generate(@NotNull SourcePos sourcePos) { + return generate(Constants.ANONYMOUS_PREFIX, sourcePos); + } + public static @NotNull LocalVar generate(@NotNull String name, @NotNull SourcePos sourcePos) { return new LocalVar(name, sourcePos, GenerateKind.Basic.Tyck); } diff --git a/tools/src/main/java/org/aya/util/IterableUtil.java b/tools/src/main/java/org/aya/util/IterableUtil.java index 4d8346dd04..4c6c462d83 100644 --- a/tools/src/main/java/org/aya/util/IterableUtil.java +++ b/tools/src/main/java/org/aya/util/IterableUtil.java @@ -1,12 +1,12 @@ -// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang. +// Copyright (c) 2020-2025 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.util; -import org.jetbrains.annotations.NotNull; - import java.util.function.BiConsumer; import java.util.function.Consumer; +import org.jetbrains.annotations.NotNull; + public interface IterableUtil { static void forEach(@NotNull Iterable it, @NotNull BiConsumer separator, @NotNull Consumer run) { var iter = it.iterator(); diff --git a/tools/src/main/java/org/aya/util/error/PosedUnaryOperator.java b/tools/src/main/java/org/aya/util/error/PosedUnaryOperator.java index 46ecbb54ea..25a6542063 100644 --- a/tools/src/main/java/org/aya/util/error/PosedUnaryOperator.java +++ b/tools/src/main/java/org/aya/util/error/PosedUnaryOperator.java @@ -1,4 +1,4 @@ -// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang. +// Copyright (c) 2020-2025 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.util.error; @@ -8,6 +8,10 @@ @FunctionalInterface public interface PosedUnaryOperator extends BiFunction { + static PosedUnaryOperator identity() { + return (_, t) -> t; + } + default T apply(@NotNull WithPos a) { return apply(a.sourcePos(), a.data()); }