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 34e700cd9..cb0fa86c8 100644 --- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java +++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java @@ -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,6 +115,11 @@ 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.IrrefutableLam lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause())); case Expr.DepType depType -> { var mCtx = MutableValue.create(ctx); @@ -231,6 +235,11 @@ 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, + /// it is safe to supply an [ImmutableSeq#empty()] + /// if there is no telescope or the user cannot refer to it. 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 60b9fa2dc..2e8cabbd3 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/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java index 7cf515595..fb8643bec 100644 --- a/parser/src/main/gen/org/aya/parser/AyaPsiParser.java +++ b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java @@ -2425,14 +2425,14 @@ private static boolean sigmaExpr_0_1(PsiBuilder b, int l) { return r; } - // KW_LAMBDA teleBinderUntyped (IMPLIES expr)? + // KW_LAMBDA patterns (IMPLIES expr)? public static boolean lambdaExpr(PsiBuilder b, int l) { if (!recursion_guard_(b, l, "lambdaExpr")) 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 && patterns(b, l + 1); r = r && lambdaExpr_2(b, l + 1); exit_section_(b, m, LAMBDA_EXPR, r); return r; diff --git a/parser/src/main/grammar/AyaPsiParser.bnf b/parser/src/main/grammar/AyaPsiParser.bnf index c70ba53d5..b1d1b81c8 100644 --- a/parser/src/main/grammar/AyaPsiParser.bnf +++ b/parser/src/main/grammar/AyaPsiParser.bnf @@ -290,7 +290,7 @@ 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)? +lambdaExpr ::= KW_LAMBDA patterns (IMPLIES expr)? matchExpr ::= KW_MATCH KW_ELIM? exprList matchType? clauses doExpr ::= KW_DO LBRACE? <> RBRACE? selfExpr ::= KW_SELF (AT qualifiedId)? diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java index d3d71de80..165c1895b 100644 --- a/producer/src/main/java/org/aya/producer/AyaProducer.java +++ b/producer/src/main/java/org/aya/producer/AyaProducer.java @@ -662,9 +662,8 @@ 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); + 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(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 36dfd12e6..15b9d70de 100644 --- a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java +++ b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java @@ -7,8 +7,8 @@ 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.control.Option; import kala.range.primitive.IntRange; import org.aya.generic.Constants; import org.aya.generic.Modifier; @@ -25,8 +25,8 @@ 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.SourcePos; import org.aya.util.error.WithPos; import org.aya.util.prettier.PrettierOptions; import org.jetbrains.annotations.NotNull; @@ -105,19 +105,18 @@ yield visitConcreteCalls(assoc, optionImplicit()); } case Expr.Lambda expr -> { - var pair = Nested.destructNested(WithPos.dummy(expr)); - var telescope = pair.component1(); - var body = pair.component2().data(); - var prelude = MutableList.of(LAMBDA); - var docTele = telescope.map(BasePrettier::varDoc); - - prelude.appendAll(docTele); - if (!(body instanceof Expr.Hole hole && !hole.explicit())) { - prelude.append(FN_DEFINED_AS); - prelude.append(term(Outer.Free, body)); - } - yield checkParen(outer, Doc.sep(prelude), Outer.BinOp); + var unlam = Nested.destructNested(WithPos.dummy(expr)); + var dummyCls = new Pattern.Clause( + SourcePos.NONE, + unlam.component1().map(x -> + Arg.ofExplicitly(WithPos.dummy(new Pattern.Bind(x)))), + Option.some(unlam.component2()) + ); + + yield checkParen(outer, visitLambda(dummyCls), Outer.BinOp); } + // TODO + case Expr.IrrefutableLam(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,17 @@ 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); + prelude.append(clause(clause)); + var body = clause.expr.get().data(); + + if (!(body instanceof Expr.Hole hole && !hole.explicit())) { + prelude.append(FN_DEFINED_AS); + prelude.append(term(Outer.Free, body)); + } + + 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 0b65f50d7..ed765fccf 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("=>");