pat-lam: impl producer and prettier

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<Pattern> resolvePattern(@NotNull WithPos<Pattern> pattern, @NotNull ImmutableSeq<LocalVar> telescope, MutableValue<Context> ctx) {
     var resolver = new PatternResolver(ctx.get(), telescope, this::addReference);
     var result = pattern.descent(resolver);

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;

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;

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? <<commaSep doBlockContent>> RBRACE?
 selfExpr ::= KW_SELF (AT qualifiedId)?

producer/src/main/java/org/aya/producer/AyaProducer.java

@@ -662,9 +662,8 @@ private record DeclNameOrInfix(@NotNull WithPos<String> 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);

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<Arg<WithPos<Pattern>>> 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<Pattern.Clause> 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);
+  }
 }

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("=>");