From cae7d5290320f6e5f1dc1094ea8235b0ede686b5 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Tue, 14 Jan 2025 01:29:11 +0800
Subject: [PATCH 01/17] pat-lam: intro

---
 .../org/aya/resolve/visitor/ExprResolver.java |   8 +-
 .../main/java/org/aya/tyck/ExprTycker.java    | 125 ++++++++++++++----
 .../java/org/aya/syntax/concrete/Expr.java    |  69 ++++++++--
 .../java/org/aya/syntax/ref/LocalVar.java     |   7 +-
 .../aya/util/error/PosedUnaryOperator.java    |   6 +-
 5 files changed, 172 insertions(+), 43 deletions(-)

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..ea1c3b1b20 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;
 
@@ -116,11 +116,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.Lambda lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause()));
       case Expr.DepType depType -> {
         var mCtx = MutableValue.create(ctx);
         var param = bind(depType.param(), mCtx);
diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index 60b9fa2dc9..d7857179ec 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -6,6 +6,7 @@
 import kala.collection.immutable.ImmutableTreeSeq;
 import kala.collection.mutable.MutableList;
 import kala.collection.mutable.MutableTreeSet;
+import kala.control.Option;
 import org.aya.generic.Constants;
 import org.aya.generic.term.DTKind;
 import org.aya.pretty.doc.Doc;
@@ -51,6 +52,7 @@
 import org.jetbrains.annotations.Nullable;
 
 import java.util.Comparator;
+import java.util.Objects;
 import java.util.function.BiFunction;
 import java.util.function.Function;
 
@@ -90,34 +92,49 @@ public void solveMetas() {
    */
   public @NotNull Jdg inherit(@NotNull WithPos<Expr> expr, @NotNull Term type) {
     return switch (expr.data()) {
-      case Expr.Lambda(var ref, var body) -> switch (whnf(type)) {
-        case DepTypeTerm(var kind, var dom, var cod) when kind == DTKind.Pi -> {
-          // unifyTyReported(param, dom, expr);
-          try (var _ = subscope(ref, dom)) {
-            var core = inherit(body, cod.apply(new FreeTerm(ref))).wellTyped().bind(ref);
-            yield new Jdg.Default(new LamTerm(core), type);
+      case Expr.Lambda lam -> {
+        var pats = lam.patterns();
+        var body = lam.body();
+
+        switch (whnf(type)) {
+          case EqTerm eq -> {
+            var unlam = lam.unlam();
+
+            if (unlam == null) {
+              // first pattern is not bind or meta
+              throw new UnsupportedOperationException("TODO");
+            }
+
+            var ref = unlam.ref();
+            body = unlam.body();
+
+            Closure.Locns core;
+            try (var _ = subscope(ref, DimTyTerm.INSTANCE)) {
+              core = inherit(body, eq.appA(new FreeTerm(ref))).wellTyped().bind(ref);
+            }
+            checkBoundaries(eq, core, body.sourcePos(), msg ->
+              new CubicalError.BoundaryDisagree(expr, msg, new UnifyInfo(state)));
+            yield new Jdg.Default(new LamTerm(core), eq);
           }
-        }
-        case EqTerm eq -> {
-          Closure.Locns core;
-          try (var _ = subscope(ref, DimTyTerm.INSTANCE)) {
-            core = inherit(body, eq.appA(new FreeTerm(ref))).wellTyped().bind(ref);
+          case DepTypeTerm(var kind, var dom, var cod) when kind == DTKind.Pi -> {
+            // unifyTyReported(param, dom, expr);
+            try (var _ = subscope(ref, dom)) {
+              var core = inherit(body, cod.apply(new FreeTerm(ref))).wellTyped().bind(ref);
+              yield new Jdg.Default(new LamTerm(core), type);
+            }
           }
-          checkBoundaries(eq, core, body.sourcePos(), msg ->
-            new CubicalError.BoundaryDisagree(expr, msg, new UnifyInfo(state)));
-          yield new Jdg.Default(new LamTerm(core), eq);
-        }
-        case MetaCall metaCall -> {
-          var pi = metaCall.asDt(this::whnf, "_dom", "_cod", DTKind.Pi);
-          if (pi == null) yield fail(expr.data(), type, BadTypeError.absOnNonPi(state, expr, type));
-          unifier(metaCall.ref().pos(), Ordering.Eq).compare(metaCall, pi, null);
-          try (var _ = subscope(ref, pi.param())) {
-            var core = inherit(body, pi.body().apply(new FreeTerm(ref))).wellTyped().bind(ref);
-            yield new Jdg.Default(new LamTerm(core), pi);
+          case MetaCall metaCall -> {
+            var pi = metaCall.asDt(this::whnf, "_dom", "_cod", DTKind.Pi);
+            if (pi == null) yield fail(expr.data(), type, BadTypeError.absOnNonPi(state, expr, type));
+            unifier(metaCall.ref().pos(), Ordering.Eq).compare(metaCall, pi, null);
+            try (var _ = subscope(ref, pi.param())) {
+              var core = inherit(body, pi.body().apply(new FreeTerm(ref))).wellTyped().bind(ref);
+              yield new Jdg.Default(new LamTerm(core), pi);
+            }
           }
+          default -> fail(expr.data(), type, BadTypeError.absOnNonPi(state, expr, type));
         }
-        default -> fail(expr.data(), type, BadTypeError.absOnNonPi(state, expr, type));
-      };
+      }
       case Expr.Hole hole -> {
         var freshHole = freshMeta(Constants.randomName(hole), expr.sourcePos(),
           new MetaVar.OfType(type), hole.explicit());
@@ -511,6 +528,66 @@ private Jdg computeArgs(
     return new ArgsComputer(this, pos, args, params).boot(k);
   }
 
+  /// Tyck a [Expr.Lambda] against to {@param type}
+  ///
+  /// @param unpier provides the telescope of PiTerm, can be shorter than required
+  private @NotNull Term checkLam(
+    @NotNull SourcePos pos,
+    @NotNull Expr.Lambda lam,
+    @NotNull Function<ImmutableSeq<LocalVar>, DepTypeTerm.Unpi> unpier
+  ) {
+    // FIXME: unify with Expr.Lambda#unlam
+    var binds = lam.patterns().map(pat -> switch (pat.term().data()) {
+      case Pattern.Bind bindPat -> bindPat.bind();
+      case Pattern.CalmFace _ -> LocalVar.generate(Constants.ANONYMOUS_PREFIX, pat.term().sourcePos());
+      default -> null;
+    });
+
+    // is the lambda a vanilla version?
+    var isVanilla = binds.allMatch(Objects::nonNull);
+
+    if (isVanilla) {
+      var unpi = unpier.apply(binds);
+
+      try (var _ = subscope()) {
+        // load all binds
+        binds.forEachWith(unpi.params(), (ref, param) ->
+          localCtx().put(ref, param.type()));
+
+        var paramSize = unpi.params().size();
+
+        // check body
+        WithPos<Expr> realBody = paramSize == lam.patterns().size()
+          ? lam.body()
+          // trigger a error report
+          : new WithPos<>(pos, new Expr.Lambda(lam.clause().update(lam.clause().patterns.drop(paramSize), lam.clause().expr)));
+
+        return inherit(realBody, unpi.body()).wellTyped();
+      }
+    } else {
+      var teleVars = ImmutableSeq.fill(lam.patterns().size(), i -> LocalVar.generate("LambdaMatch" + i));
+      var unpi = unpier.apply(teleVars);
+
+      var worker = new ClauseTycker.Worker(
+        new ClauseTycker(this),
+        unpi.params(),
+        new DepTypeTerm.Unpi(unpi.body()),
+        teleVars,
+        ImmutableSeq.empty(),
+        ImmutableSeq.of(lam.clause())
+      );
+
+      var clsResult = worker.check(pos);
+      if (clsResult.hasLhsError()) {
+        return new ErrorTerm(lam);
+      }
+
+      // TODO: optimize leading bindings
+      // TODO: make match call
+      throw new UnsupportedOperationException("TODO");
+    }
+  }
+
   /**
    * tyck a let expr with the given checker
    *
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..9aeb05461d 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -1,12 +1,14 @@
-// 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 kala.collection.SeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.control.Either;
+import kala.control.Option;
 import kala.value.MutableValue;
 import org.aya.generic.AyaDocile;
+import org.aya.generic.Constants;
 import org.aya.generic.Nested;
 import org.aya.generic.term.DTKind;
 import org.aya.generic.term.ParamLike;
@@ -18,6 +20,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.*;
@@ -134,19 +137,61 @@ public Ref(@NotNull AnyVar var) {
     @Override public void forEach(@NotNull PosedConsumer<Expr> f) { }
   }
 
-  record Lambda(
-    @NotNull LocalVar ref,
-    @Override @NotNull WithPos<Expr> body
-  ) implements Expr, Nested<LocalVar, Expr, Lambda> {
-    @Override public @NotNull LocalVar param() { return ref; }
-    public @NotNull Lambda update(@NotNull WithPos<Expr> body) {
-      return body == body() ? this : new Lambda(ref, body);
+  record Lambda(@NotNull Pattern.Clause clause) implements Expr {
+    public Lambda {
+      assert clause.patterns.isNotEmpty();
+    }
+
+    public Lambda(@NotNull SeqView<WithPos<Pattern>> patterns, @NotNull WithPos<Expr> body) {
+      this(new Pattern.Clause(SourcePos.NONE, patterns.map(Arg::ofExplicitly).toImmutableSeq(), Option.some(body)));
+    }
+
+    public Lambda(@NotNull LocalVar ref, @NotNull WithPos<Expr> body) {
+      this(SeqView.of(new WithPos<>(ref.definition(), new Pattern.Bind(ref))), body);
+    }
+
+    public @NotNull Lambda update(@NotNull Pattern.Clause clause) {
+      return clause == this.clause ? this : new Lambda(clause);
+    }
+
+    public @NotNull ImmutableSeq<Arg<WithPos<Pattern>>> patterns() {
+      return clause.patterns;
+    }
+
+    public @NotNull WithPos<Expr> body() {
+      return clause.expr.get();
+    }
+
+    public record Unlam(@NotNull LocalVar ref, @NotNull WithPos<Expr> body) { }
+
+    /// Transform this lambda to vanilla lambda, if the first pattern is a bind or meta.
+    public @Nullable Unlam unlam() {
+      var fst = patterns().getFirst().term();
+      var ref = switch (fst.data()) {
+        case Pattern.Bind bind -> bind.bind();
+        case Pattern.CalmFace _ -> LocalVar.generate(fst.sourcePos());
+        default -> null;
+      };
+
+      if (ref == null) return null;
+
+      var remainPats = patterns().drop(1);
+      WithPos<Expr> body = remainPats.isEmpty()
+        ? body()
+        : body().replace(new Lambda(clause.update(remainPats, clause.expr)));
+
+      return new Unlam(ref, body);
     }
 
     @Override public @NotNull Lambda descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
-      return update(body.descent(f));
+      return descent(f, PosedUnaryOperator.identity());
     }
-    @Override public void forEach(@NotNull PosedConsumer<Expr> f) { f.accept(body); }
+
+    public @NotNull Lambda descent(@NotNull PosedUnaryOperator<@NotNull Expr> f, @NotNull PosedUnaryOperator<@NotNull Pattern> g) {
+      return update(clause.descent(f, g));
+    }
+
+    @Override public void forEach(@NotNull PosedConsumer<Expr> f) { clause.forEach(f, (_, _) -> { }); }
   }
 
   record BinTuple(@NotNull WithPos<Expr> lhs, @NotNull WithPos<Expr> rhs) implements Expr {
@@ -597,7 +642,9 @@ record Match(
   }
 
   static @NotNull WithPos<Expr> buildLam(@NotNull SourcePos sourcePos, @NotNull SeqView<LocalVar> params, @NotNull WithPos<Expr> body) {
-    return buildNested(sourcePos, params, body, Lambda::new);
+    return new WithPos<>(sourcePos, new Lambda(
+      params.map(x -> new WithPos<Pattern>(x.definition(), new Pattern.Bind(x))),
+      body));
   }
 
   static @NotNull WithPos<Expr> buildLet(@NotNull SourcePos sourcePos, @NotNull SeqView<LetBind> binds, @NotNull WithPos<Expr> body) {
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/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<T> extends BiFunction<SourcePos, T, T> {
+  static <T> PosedUnaryOperator<T> identity() {
+    return (_, t) -> t;
+  }
+
   default T apply(@NotNull WithPos<T> a) {
     return apply(a.sourcePos(), a.data());
   }

From 06bb52dcee6ca9d001e3573c30584e58e1c0446c Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Tue, 14 Jan 2025 13:25:06 +0800
Subject: [PATCH 02/17] pat-lam: how about this?

---
 .../main/java/org/aya/tyck/ExprTycker.java    | 41 +++++++------------
 .../java/org/aya/syntax/concrete/Expr.java    | 29 ++++++-------
 .../main/java/org/aya/util/IterableUtil.java  |  3 +-
 3 files changed, 31 insertions(+), 42 deletions(-)

diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index d7857179ec..9b0903a793 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -6,7 +6,6 @@
 import kala.collection.immutable.ImmutableTreeSeq;
 import kala.collection.mutable.MutableList;
 import kala.collection.mutable.MutableTreeSet;
-import kala.control.Option;
 import org.aya.generic.Constants;
 import org.aya.generic.term.DTKind;
 import org.aya.pretty.doc.Doc;
@@ -93,19 +92,18 @@ public void solveMetas() {
   public @NotNull Jdg inherit(@NotNull WithPos<Expr> expr, @NotNull Term type) {
     return switch (expr.data()) {
       case Expr.Lambda lam -> {
-        var pats = lam.patterns();
         var body = lam.body();
 
         switch (whnf(type)) {
           case EqTerm eq -> {
-            var unlam = lam.unlam();
+            var unlam = lam.unlam(1);
 
             if (unlam == null) {
               // first pattern is not bind or meta
               throw new UnsupportedOperationException("TODO");
             }
 
-            var ref = unlam.ref();
+            var ref = unlam.binds().getFirst();
             body = unlam.body();
 
             Closure.Locns core;
@@ -116,12 +114,9 @@ public void solveMetas() {
               new CubicalError.BoundaryDisagree(expr, msg, new UnifyInfo(state)));
             yield new Jdg.Default(new LamTerm(core), eq);
           }
-          case DepTypeTerm(var kind, var dom, var cod) when kind == DTKind.Pi -> {
-            // unifyTyReported(param, dom, expr);
-            try (var _ = subscope(ref, dom)) {
-              var core = inherit(body, cod.apply(new FreeTerm(ref))).wellTyped().bind(ref);
-              yield new Jdg.Default(new LamTerm(core), type);
-            }
+          case DepTypeTerm dtTerm when dtTerm.kind() == DTKind.Pi -> {
+            var wellTyped = checkLam(expr.sourcePos(), lam, DepTypeTerm.unpiDBI(dtTerm, this::whnf, lam.clause().patterns.size()));
+            yield new Jdg.Default(wellTyped, dtTerm);
           }
           case MetaCall metaCall -> {
             var pi = metaCall.asDt(this::whnf, "_dom", "_cod", DTKind.Pi);
@@ -529,44 +524,36 @@ private Jdg computeArgs(
   }
 
   /// Tyck a [Expr.Lambda] against to {@param type}
-  ///
-  /// @param unpier provides the telescope of PiTerm, can be shorter than required
   private @NotNull Term checkLam(
     @NotNull SourcePos pos,
     @NotNull Expr.Lambda lam,
-    @NotNull Function<ImmutableSeq<LocalVar>, DepTypeTerm.Unpi> unpier
+    @NotNull DepTypeTerm.Unpi unpi
   ) {
-    // FIXME: unify with Expr.Lambda#unlam
-    var binds = lam.patterns().map(pat -> switch (pat.term().data()) {
-      case Pattern.Bind bindPat -> bindPat.bind();
-      case Pattern.CalmFace _ -> LocalVar.generate(Constants.ANONYMOUS_PREFIX, pat.term().sourcePos());
-      default -> null;
-    });
+    var unlam = lam.unlam(lam.clause().patterns.size());
 
     // is the lambda a vanilla version?
-    var isVanilla = binds.allMatch(Objects::nonNull);
-
-    if (isVanilla) {
-      var unpi = unpier.apply(binds);
-
+    if (unlam != null) {
+      var binds = unlam.binds();
       try (var _ = subscope()) {
         // load all binds
         binds.forEachWith(unpi.params(), (ref, param) ->
           localCtx().put(ref, param.type()));
 
         var paramSize = unpi.params().size();
+        var lamSize = lam.patterns().size();
 
         // check body
-        WithPos<Expr> realBody = paramSize == lam.patterns().size()
+        WithPos<Expr> realBody = paramSize == lamSize
           ? lam.body()
           // trigger a error report
           : new WithPos<>(pos, new Expr.Lambda(lam.clause().update(lam.clause().patterns.drop(paramSize), lam.clause().expr)));
+        // in case [paramSize] is lower than [lamSize]
+        var realResult = unpi.body().instTeleVar(binds.view().take(paramSize));
 
-        return inherit(realBody, unpi.body()).wellTyped();
+        return inherit(realBody, realResult).wellTyped();
       }
     } else {
       var teleVars = ImmutableSeq.fill(lam.patterns().size(), i -> LocalVar.generate("LambdaMatch" + i));
-      var unpi = unpier.apply(teleVars);
 
       var worker = new ClauseTycker.Worker(
         new ClauseTycker(this),
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 9aeb05461d..91e75a6e41 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -8,7 +8,6 @@
 import kala.control.Option;
 import kala.value.MutableValue;
 import org.aya.generic.AyaDocile;
-import org.aya.generic.Constants;
 import org.aya.generic.Nested;
 import org.aya.generic.term.DTKind;
 import org.aya.generic.term.ParamLike;
@@ -28,6 +27,7 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
+import java.util.Objects;
 import java.util.function.BiFunction;
 import java.util.function.Consumer;
 import java.util.function.Function;
@@ -162,25 +162,26 @@ public Lambda(@NotNull LocalVar ref, @NotNull WithPos<Expr> body) {
       return clause.expr.get();
     }
 
-    public record Unlam(@NotNull LocalVar ref, @NotNull WithPos<Expr> body) { }
+    public record Unlam(@NotNull ImmutableSeq<LocalVar> binds, @NotNull WithPos<Expr> body) { }
 
-    /// Transform this lambda to vanilla lambda, if the first pattern is a bind or meta.
-    public @Nullable Unlam unlam() {
-      var fst = patterns().getFirst().term();
-      var ref = switch (fst.data()) {
+    public @Nullable Unlam unlam(int size) {
+      assert 0 < size && size <= patterns().size();
+
+      var pats = patterns().view().take(size).map(Arg::term);
+      var binds = pats.map(p -> switch (p.data()) {
         case Pattern.Bind bind -> bind.bind();
-        case Pattern.CalmFace _ -> LocalVar.generate(fst.sourcePos());
+        case Pattern.CalmFace _ -> LocalVar.generate(p.sourcePos());
         default -> null;
-      };
-
-      if (ref == null) return null;
+      }).toImmutableSeq();
+      if (binds.anyMatch(Objects::isNull)) return null;
 
-      var remainPats = patterns().drop(1);
-      WithPos<Expr> body = remainPats.isEmpty()
+      var remains = patterns().drop(size);
+      // make body
+      WithPos<Expr> body = remains.isEmpty()
         ? body()
-        : body().replace(new Lambda(clause.update(remainPats, clause.expr)));
+        : body().replace(new Lambda(clause.update(remains, clause.expr)));
 
-      return new Unlam(ref, body);
+      return new Unlam(binds, body);
     }
 
     @Override public @NotNull Lambda descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
diff --git a/tools/src/main/java/org/aya/util/IterableUtil.java b/tools/src/main/java/org/aya/util/IterableUtil.java
index 4d8346dd04..a9259d104f 100644
--- a/tools/src/main/java/org/aya/util/IterableUtil.java
+++ b/tools/src/main/java/org/aya/util/IterableUtil.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.util;
 
+import kala.collection.SeqView;
 import org.jetbrains.annotations.NotNull;
 
 import java.util.function.BiConsumer;

From 71a9d4b85aa849820cf64f3f97938cea0a904a34 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Tue, 14 Jan 2025 14:40:05 +0800
Subject: [PATCH 03/17] pat-lam: impl in desugar

---
 .../java/org/aya/resolve/salt/Desalt.java     |  37 +++++-
 .../org/aya/resolve/visitor/ExprResolver.java |   2 +-
 .../main/java/org/aya/tyck/ExprTycker.java    | 112 ++++--------------
 .../java/org/aya/syntax/concrete/Expr.java    |  64 ++++------
 .../main/java/org/aya/util/IterableUtil.java  |   1 -
 5 files changed, 87 insertions(+), 129 deletions(-)

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..ed6c52f936 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,15 @@
-// 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 kala.value.primitive.MutableBooleanValue;
+import org.aya.generic.Constants;
 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 +74,37 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
       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.IrrefutableLam lam -> {
+        MutableBooleanValue isVanilla = MutableBooleanValue.create(true);
+        var lamTele = lam.patterns().mapIndexed((idx, pat) -> {
+          var name = switch (pat.term().data()) {
+            case Pattern.Bind(var bind, var _) -> bind.name();
+            case Pattern.CalmFace _ -> Constants.ANONYMOUS_PREFIX;
+            default -> {
+              isVanilla.set(false);
+              yield "IrrefutableLam" + idx;
+            }
+          };
+
+          return LocalVar.generate(name, pat.term().sourcePos());
+        });
+
+        WithPos<Expr> realBody;
+
+        if (isVanilla.get()) {
+          realBody = lam.body();
+        } else {
+          realBody = new WithPos<>(sourcePos, new Expr.Match(
+            lamTele.map(x -> new WithPos<>(x.definition(), new Expr.Ref(x))),
+            ImmutableSeq.of(lam.clause()),
+            ImmutableSeq.empty(),
+            false,
+            null
+          ));
+        }
+
+        yield apply(Expr.buildLam(sourcePos, lamTele.view(), realBody));
+      }
     };
   }
   public @NotNull PosedUnaryOperator<Pattern> 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 ea1c3b1b20..34e700cd9f 100644
--- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
+++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
@@ -116,7 +116,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 -> lam.update(clause(ImmutableSeq.empty(), lam.clause()));
+      case Expr.IrrefutableLam lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause()));
       case Expr.DepType depType -> {
         var mCtx = MutableValue.create(ctx);
         var param = bind(depType.param(), mCtx);
diff --git a/base/src/main/java/org/aya/tyck/ExprTycker.java b/base/src/main/java/org/aya/tyck/ExprTycker.java
index 9b0903a793..60b9fa2dc9 100644
--- a/base/src/main/java/org/aya/tyck/ExprTycker.java
+++ b/base/src/main/java/org/aya/tyck/ExprTycker.java
@@ -51,7 +51,6 @@
 import org.jetbrains.annotations.Nullable;
 
 import java.util.Comparator;
-import java.util.Objects;
 import java.util.function.BiFunction;
 import java.util.function.Function;
 
@@ -91,45 +90,34 @@ public void solveMetas() {
    */
   public @NotNull Jdg inherit(@NotNull WithPos<Expr> expr, @NotNull Term type) {
     return switch (expr.data()) {
-      case Expr.Lambda lam -> {
-        var body = lam.body();
-
-        switch (whnf(type)) {
-          case EqTerm eq -> {
-            var unlam = lam.unlam(1);
-
-            if (unlam == null) {
-              // first pattern is not bind or meta
-              throw new UnsupportedOperationException("TODO");
-            }
-
-            var ref = unlam.binds().getFirst();
-            body = unlam.body();
-
-            Closure.Locns core;
-            try (var _ = subscope(ref, DimTyTerm.INSTANCE)) {
-              core = inherit(body, eq.appA(new FreeTerm(ref))).wellTyped().bind(ref);
-            }
-            checkBoundaries(eq, core, body.sourcePos(), msg ->
-              new CubicalError.BoundaryDisagree(expr, msg, new UnifyInfo(state)));
-            yield new Jdg.Default(new LamTerm(core), eq);
+      case Expr.Lambda(var ref, var body) -> switch (whnf(type)) {
+        case DepTypeTerm(var kind, var dom, var cod) when kind == DTKind.Pi -> {
+          // unifyTyReported(param, dom, expr);
+          try (var _ = subscope(ref, dom)) {
+            var core = inherit(body, cod.apply(new FreeTerm(ref))).wellTyped().bind(ref);
+            yield new Jdg.Default(new LamTerm(core), type);
           }
-          case DepTypeTerm dtTerm when dtTerm.kind() == DTKind.Pi -> {
-            var wellTyped = checkLam(expr.sourcePos(), lam, DepTypeTerm.unpiDBI(dtTerm, this::whnf, lam.clause().patterns.size()));
-            yield new Jdg.Default(wellTyped, dtTerm);
+        }
+        case EqTerm eq -> {
+          Closure.Locns core;
+          try (var _ = subscope(ref, DimTyTerm.INSTANCE)) {
+            core = inherit(body, eq.appA(new FreeTerm(ref))).wellTyped().bind(ref);
           }
-          case MetaCall metaCall -> {
-            var pi = metaCall.asDt(this::whnf, "_dom", "_cod", DTKind.Pi);
-            if (pi == null) yield fail(expr.data(), type, BadTypeError.absOnNonPi(state, expr, type));
-            unifier(metaCall.ref().pos(), Ordering.Eq).compare(metaCall, pi, null);
-            try (var _ = subscope(ref, pi.param())) {
-              var core = inherit(body, pi.body().apply(new FreeTerm(ref))).wellTyped().bind(ref);
-              yield new Jdg.Default(new LamTerm(core), pi);
-            }
+          checkBoundaries(eq, core, body.sourcePos(), msg ->
+            new CubicalError.BoundaryDisagree(expr, msg, new UnifyInfo(state)));
+          yield new Jdg.Default(new LamTerm(core), eq);
+        }
+        case MetaCall metaCall -> {
+          var pi = metaCall.asDt(this::whnf, "_dom", "_cod", DTKind.Pi);
+          if (pi == null) yield fail(expr.data(), type, BadTypeError.absOnNonPi(state, expr, type));
+          unifier(metaCall.ref().pos(), Ordering.Eq).compare(metaCall, pi, null);
+          try (var _ = subscope(ref, pi.param())) {
+            var core = inherit(body, pi.body().apply(new FreeTerm(ref))).wellTyped().bind(ref);
+            yield new Jdg.Default(new LamTerm(core), pi);
           }
-          default -> fail(expr.data(), type, BadTypeError.absOnNonPi(state, expr, type));
         }
-      }
+        default -> fail(expr.data(), type, BadTypeError.absOnNonPi(state, expr, type));
+      };
       case Expr.Hole hole -> {
         var freshHole = freshMeta(Constants.randomName(hole), expr.sourcePos(),
           new MetaVar.OfType(type), hole.explicit());
@@ -523,58 +511,6 @@ private Jdg computeArgs(
     return new ArgsComputer(this, pos, args, params).boot(k);
   }
 
-  /// Tyck a [Expr.Lambda] against to {@param type}
-  private @NotNull Term checkLam(
-    @NotNull SourcePos pos,
-    @NotNull Expr.Lambda lam,
-    @NotNull DepTypeTerm.Unpi unpi
-  ) {
-    var unlam = lam.unlam(lam.clause().patterns.size());
-
-    // is the lambda a vanilla version?
-    if (unlam != null) {
-      var binds = unlam.binds();
-      try (var _ = subscope()) {
-        // load all binds
-        binds.forEachWith(unpi.params(), (ref, param) ->
-          localCtx().put(ref, param.type()));
-
-        var paramSize = unpi.params().size();
-        var lamSize = lam.patterns().size();
-
-        // check body
-        WithPos<Expr> realBody = paramSize == lamSize
-          ? lam.body()
-          // trigger a error report
-          : new WithPos<>(pos, new Expr.Lambda(lam.clause().update(lam.clause().patterns.drop(paramSize), lam.clause().expr)));
-        // in case [paramSize] is lower than [lamSize]
-        var realResult = unpi.body().instTeleVar(binds.view().take(paramSize));
-
-        return inherit(realBody, realResult).wellTyped();
-      }
-    } else {
-      var teleVars = ImmutableSeq.fill(lam.patterns().size(), i -> LocalVar.generate("LambdaMatch" + i));
-
-      var worker = new ClauseTycker.Worker(
-        new ClauseTycker(this),
-        unpi.params(),
-        new DepTypeTerm.Unpi(unpi.body()),
-        teleVars,
-        ImmutableSeq.empty(),
-        ImmutableSeq.of(lam.clause())
-      );
-
-      var clsResult = worker.check(pos);
-      if (clsResult.hasLhsError()) {
-        return new ErrorTerm(lam);
-      }
-
-      // TODO: optimize leading bindings
-      // TODO: make match call
-      throw new UnsupportedOperationException("TODO");
-    }
-  }
-
   /**
    * tyck a let expr with the given checker
    *
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 91e75a6e41..8e88a6beaa 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -137,21 +137,18 @@ public Ref(@NotNull AnyVar var) {
     @Override public void forEach(@NotNull PosedConsumer<Expr> f) { }
   }
 
-  record Lambda(@NotNull Pattern.Clause clause) implements Expr {
-    public Lambda {
-      assert clause.patterns.isNotEmpty();
-    }
-
-    public Lambda(@NotNull SeqView<WithPos<Pattern>> patterns, @NotNull WithPos<Expr> body) {
-      this(new Pattern.Clause(SourcePos.NONE, patterns.map(Arg::ofExplicitly).toImmutableSeq(), Option.some(body)));
+  record IrrefutableLam(@NotNull Pattern.Clause clause) implements Expr, Sugar {
+    public static boolean canBeBind(@NotNull Arg<WithPos<Pattern>> pat) {
+      var thePat = pat.term().data();
+      return thePat instanceof Pattern.Bind || thePat == Pattern.CalmFace.INSTANCE;
     }
 
-    public Lambda(@NotNull LocalVar ref, @NotNull WithPos<Expr> body) {
-      this(SeqView.of(new WithPos<>(ref.definition(), new Pattern.Bind(ref))), body);
+    public IrrefutableLam {
+      assert clause.patterns.isNotEmpty();
     }
 
-    public @NotNull Lambda update(@NotNull Pattern.Clause clause) {
-      return clause == this.clause ? this : new Lambda(clause);
+    public @NotNull IrrefutableLam update(@NotNull Pattern.Clause clause) {
+      return clause == this.clause ? this : new IrrefutableLam(clause);
     }
 
     public @NotNull ImmutableSeq<Arg<WithPos<Pattern>>> patterns() {
@@ -162,39 +159,32 @@ public Lambda(@NotNull LocalVar ref, @NotNull WithPos<Expr> body) {
       return clause.expr.get();
     }
 
-    public record Unlam(@NotNull ImmutableSeq<LocalVar> binds, @NotNull WithPos<Expr> body) { }
-
-    public @Nullable Unlam unlam(int size) {
-      assert 0 < size && size <= patterns().size();
-
-      var pats = patterns().view().take(size).map(Arg::term);
-      var binds = pats.map(p -> switch (p.data()) {
-        case Pattern.Bind bind -> bind.bind();
-        case Pattern.CalmFace _ -> LocalVar.generate(p.sourcePos());
-        default -> null;
-      }).toImmutableSeq();
-      if (binds.anyMatch(Objects::isNull)) return null;
-
-      var remains = patterns().drop(size);
-      // make body
-      WithPos<Expr> body = remains.isEmpty()
-        ? body()
-        : body().replace(new Lambda(clause.update(remains, clause.expr)));
-
-      return new Unlam(binds, body);
-    }
-
-    @Override public @NotNull Lambda descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
+    @Override public @NotNull IrrefutableLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
       return descent(f, PosedUnaryOperator.identity());
     }
 
-    public @NotNull Lambda descent(@NotNull PosedUnaryOperator<@NotNull Expr> f, @NotNull PosedUnaryOperator<@NotNull Pattern> g) {
+    public @NotNull IrrefutableLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f, @NotNull PosedUnaryOperator<@NotNull Pattern> g) {
       return update(clause.descent(f, g));
     }
 
     @Override public void forEach(@NotNull PosedConsumer<Expr> f) { clause.forEach(f, (_, _) -> { }); }
   }
 
+  record Lambda(
+    @NotNull LocalVar ref,
+    @Override @NotNull WithPos<Expr> body
+  ) implements Expr, Nested<LocalVar, Expr, Lambda> {
+    @Override public @NotNull LocalVar param() { return ref; }
+    public @NotNull Lambda update(@NotNull WithPos<Expr> body) {
+      return body == body() ? this : new Lambda(ref, body);
+    }
+
+    @Override public @NotNull Lambda descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
+      return update(body.descent(f));
+    }
+    @Override public void forEach(@NotNull PosedConsumer<Expr> f) { f.accept(body); }
+  }
+
   record BinTuple(@NotNull WithPos<Expr> lhs, @NotNull WithPos<Expr> rhs) implements Expr {
     public @NotNull Expr.BinTuple update(@NotNull WithPos<Expr> newLhs, @NotNull WithPos<Expr> newRhs) {
       return lhs == newLhs && rhs == newRhs ? this : new BinTuple(newLhs, newRhs);
@@ -643,9 +633,7 @@ record Match(
   }
 
   static @NotNull WithPos<Expr> buildLam(@NotNull SourcePos sourcePos, @NotNull SeqView<LocalVar> params, @NotNull WithPos<Expr> body) {
-    return new WithPos<>(sourcePos, new Lambda(
-      params.map(x -> new WithPos<Pattern>(x.definition(), new Pattern.Bind(x))),
-      body));
+    return buildNested(sourcePos, params, body, Lambda::new);
   }
 
   static @NotNull WithPos<Expr> buildLet(@NotNull SourcePos sourcePos, @NotNull SeqView<LetBind> binds, @NotNull WithPos<Expr> body) {
diff --git a/tools/src/main/java/org/aya/util/IterableUtil.java b/tools/src/main/java/org/aya/util/IterableUtil.java
index a9259d104f..8a695fb28f 100644
--- a/tools/src/main/java/org/aya/util/IterableUtil.java
+++ b/tools/src/main/java/org/aya/util/IterableUtil.java
@@ -2,7 +2,6 @@
 // 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 kala.collection.SeqView;
 import org.jetbrains.annotations.NotNull;
 
 import java.util.function.BiConsumer;

From 7e18116dfae93f45d11d583e9566492a1f942fac Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Wed, 15 Jan 2025 08:45:15 +0800
Subject: [PATCH 04/17] pat-lam: fix potential bug

---
 .../java/org/aya/resolve/salt/Desalt.java     | 35 +++++++++++--------
 .../java/org/aya/syntax/concrete/Pattern.java | 15 ++++++--
 2 files changed, 33 insertions(+), 17 deletions(-)

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 ed6c52f936..cdb65717c7 100644
--- a/base/src/main/java/org/aya/resolve/salt/Desalt.java
+++ b/base/src/main/java/org/aya/resolve/salt/Desalt.java
@@ -10,6 +10,7 @@
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.concrete.Pattern;
 import org.aya.syntax.ref.LocalVar;
+import org.aya.util.Arg;
 import org.aya.util.error.Panic;
 import org.aya.util.error.PosedUnaryOperator;
 import org.aya.util.error.SourcePos;
@@ -17,6 +18,8 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
+import java.util.Objects;
+
 /** Desugar, but the sugars are not sweet enough, therefore called salt. */
 public final class Desalt implements PosedUnaryOperator<Expr> {
   private final @NotNull ResolveInfo info;
@@ -75,25 +78,29 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
       case Expr.RawSort(var kind) -> new Expr.Sort(kind, 0);
       case Expr.LetOpen letOpen -> apply(letOpen.body());
       case Expr.IrrefutableLam lam -> {
-        MutableBooleanValue isVanilla = MutableBooleanValue.create(true);
-        var lamTele = lam.patterns().mapIndexed((idx, pat) -> {
-          var name = switch (pat.term().data()) {
-            case Pattern.Bind(var bind, var _) -> bind.name();
-            case Pattern.CalmFace _ -> Constants.ANONYMOUS_PREFIX;
-            default -> {
-              isVanilla.set(false);
-              yield "IrrefutableLam" + idx;
-            }
-          };
-
-          return LocalVar.generate(name, pat.term().sourcePos());
-        });
+        var isVanilla = lam.patterns().allMatch(x -> x.term().data() instanceof Pattern.Refutable);
 
+        ImmutableSeq<LocalVar> lamTele;
         WithPos<Expr> realBody;
 
-        if (isVanilla.get()) {
+        if (isVanilla) {
+          // fn a _ c => ...
+          lamTele = lam.patterns().map(x -> ((Pattern.Refutable) x.term().data()).toLocalVar(x.term().sourcePos()));
           realBody = lam.body();
         } else {
+          lamTele = lam.patterns().mapIndexed((idx, pat) -> {
+            if (pat.term().data() instanceof Pattern.Refutable refutable) {
+              var bind = refutable.toLocalVar(pat.term().sourcePos());
+              // we need fresh bind, since [bind] may be used in the body.
+              return LocalVar.generate(bind.name(), bind.definition());
+            } else {
+              return LocalVar.generate("IrrefutableLam" + idx, pat.term().sourcePos());
+            }
+          });
+
+          // 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()),
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..2e9c4f0948 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;
 
@@ -30,6 +30,9 @@
 public sealed interface Pattern extends AyaDocile {
   void forEach(@NotNull PosedConsumer<@NotNull Pattern> f);
   interface Salt { }
+  interface Refutable {
+    @NotNull LocalVar toLocalVar(@NotNull SourcePos pos);
+  }
 
   @NotNull Pattern descent(@NotNull PosedUnaryOperator<@NotNull Pattern> f);
 
@@ -63,11 +66,14 @@ enum Absurd implements Pattern {
     @Override public @NotNull Pattern descent(@NotNull PosedUnaryOperator<@NotNull Pattern> f) { return this; }
   }
 
-  enum CalmFace implements Pattern {
+  enum CalmFace implements Pattern, Refutable {
     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 +82,13 @@ enum CalmFace implements Pattern {
   record Bind(
     @NotNull LocalVar bind,
     @ForLSP @NotNull MutableValue<@Nullable Term> type
-  ) implements Pattern {
+  ) implements Pattern, Refutable {
     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(

From 495e937d2d25096c8b32b13476f68be8ddaed46f Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Fri, 17 Jan 2025 08:00:20 +0800
Subject: [PATCH 05/17] pat-lam: impl producer and prettier

---
 .../org/aya/resolve/visitor/ExprResolver.java | 11 ++++-
 .../main/java/org/aya/tyck/ExprTycker.java    |  1 +
 .../main/gen/org/aya/parser/AyaPsiParser.java |  4 +-
 parser/src/main/grammar/AyaPsiParser.bnf      |  2 +-
 .../java/org/aya/producer/AyaProducer.java    |  5 +--
 .../org/aya/prettier/ConcretePrettier.java    | 44 ++++++++++++-------
 .../main/java/org/aya/prettier/Tokens.java    |  2 +-
 7 files changed, 45 insertions(+), 24 deletions(-)

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 34e700cd9f..cb0fa86c84 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<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);
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/parser/src/main/gen/org/aya/parser/AyaPsiParser.java b/parser/src/main/gen/org/aya/parser/AyaPsiParser.java
index 7cf5155955..fb8643becf 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 c70ba53d5f..b1d1b81c8a 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? <<commaSep doBlockContent>> 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 d3d71de802..165c1895bf 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<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);
diff --git a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
index 36dfd12e6e..15b9d70de9 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<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);
+  }
 }
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("=>");

From f784e8b02f1362858ec6208e1c69424e2c6bea09 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Fri, 17 Jan 2025 16:31:23 +0800
Subject: [PATCH 06/17] pat-lam: fix test

---
 cli-impl/src/test/resources/negative/ExprTyckError.txt    | 6 +++---
 cli-impl/src/test/resources/negative/GoalAndMeta.txt      | 2 +-
 cli-impl/src/test/resources/shared/src/data/sum/base.aya  | 2 +-
 .../test/resources/shared/src/relation/binary/path.aya    | 2 +-
 cli-impl/src/test/resources/success/src/PLFA.aya          | 8 ++++----
 cli-impl/src/test/resources/success/src/Pattern.aya       | 2 +-
 .../src/main/java/org/aya/prettier/ConcretePrettier.java  | 8 --------
 syntax/src/main/java/org/aya/syntax/concrete/Pattern.java | 6 ++++++
 8 files changed, 17 insertions(+), 19 deletions(-)

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:
          <type of `match a {
-          | _ ⇒ \ x ⇒ x
+          | _ ⇒ fn x ⇒ x
         }`>
 
 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/shared/src/data/sum/base.aya b/cli-impl/src/test/resources/shared/src/data/sum/base.aya
index 79e2b1e74f..1da8af224c 100644
--- a/cli-impl/src/test/resources/shared/src/data/sum/base.aya
+++ b/cli-impl/src/test/resources/shared/src/data/sum/base.aya
@@ -11,7 +11,7 @@ def Sum-rec
   (P : Type)
   (lrec : A -> P)
   (rrec : B -> P)
-  : P => Sum-ind e (fn _e => P) (fn a _p => lrec a) (fn b _p => rrec b)
+  : P => Sum-ind e (fn _ => P) (fn a, _ => lrec a) (fn b, _ => rrec b)
 
 def Sum-ind
   (e : Sum A B)
diff --git a/cli-impl/src/test/resources/shared/src/relation/binary/path.aya b/cli-impl/src/test/resources/shared/src/relation/binary/path.aya
index d5f6007a33..a826e4e9ef 100644
--- a/cli-impl/src/test/resources/shared/src/relation/binary/path.aya
+++ b/cli-impl/src/test/resources/shared/src/relation/binary/path.aya
@@ -8,7 +8,7 @@ def refl {a : A} : a = a => \i => a
 def pmap (f : A -> B) {a b : A} (p : a = b) : f a = f b => \i => f (p i)
 def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
 
-def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
+def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i, a => p a i
 
 def pmapd {A : I -> Type} (B : ∀ i -> A i -> Type)
     (f : ∀ i -> ∀ (a : A i) -> B i a) {a b : _} (p : Path A a b)
diff --git a/cli-impl/src/test/resources/success/src/PLFA.aya b/cli-impl/src/test/resources/success/src/PLFA.aya
index f258bc4341..e2b38d301b 100644
--- a/cli-impl/src/test/resources/success/src/PLFA.aya
+++ b/cli-impl/src/test/resources/success/src/PLFA.aya
@@ -12,7 +12,7 @@ def deMorgan-law => Fn (A B : Type) -> (neg (Sig (neg A) ** (neg B))) -> Sum A B
 
 @suppress(MostGeneralSolution)
 def LEM=>deMorgan-law (lem : LEM) : deMorgan-law =>
-  fn tyA tyB np =>
+  fn tyA, tyB, np =>
     Sum-rec (lem tyA)
     _
     (fn A => A)
@@ -23,7 +23,7 @@ def LEM=>deMorgan-law (lem : LEM) : deMorgan-law =>
       (fn ¬B => exfalso (np (¬A, ¬B))))
 
 def deMorgan-law=>imply-as-lor (dml : deMorgan-law) : imply-as-lor =>
-  fn tyA tyB f =>
+  fn tyA, tyB, f =>
     dml (neg tyA) tyB (fn p => p.1 (fn A => exfalso (p.2 (f A))))
 
 def imply-as-lor=>LEM (ial : imply-as-lor) : LEM =>
@@ -32,7 +32,7 @@ def imply-as-lor=>LEM (ial : imply-as-lor) : LEM =>
 @suppress(MostGeneralSolution)
 def imply-as-lor=>peirce-law (ial : imply-as-lor) : peirce-law =>
   // f : ((A -> B) -> A)
-  fn tyA tyB f => Sum-rec
+  fn tyA, tyB, f => Sum-rec
     (imply-as-lor=>LEM ial tyA)
     _
     (fn A => A)
@@ -40,7 +40,7 @@ def imply-as-lor=>peirce-law (ial : imply-as-lor) : peirce-law =>
 
 @suppress(MostGeneralSolution)
 def peirce-law=>double-neg-elim (pl : peirce-law) : double-neg-elim =>
-  fn tyA ¬¬A =>
+  fn tyA, ¬¬A =>
     pl tyA Empty (fn ¬A => exfalso (¬¬A ¬A))
 
 @suppress(MostGeneralSolution)
diff --git a/cli-impl/src/test/resources/success/src/Pattern.aya b/cli-impl/src/test/resources/success/src/Pattern.aya
index 35a0beb245..6980139943 100644
--- a/cli-impl/src/test/resources/success/src/Pattern.aya
+++ b/cli-impl/src/test/resources/success/src/Pattern.aya
@@ -53,5 +53,5 @@ module PullRequest1268 {
   // unpi: D d0 -> d1
   @suppress(LocalShadow)
   def elims {A : Type} (a : A) (B : Type) (b : B) {C : Type} : Fn (D : Type) D -> D elim a, b
-  | a => fn b D => id D
+  | a => fn b, D => id D
 }
diff --git a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
index 15b9d70de9..b5bad20143 100644
--- a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
@@ -115,7 +115,6 @@ yield visitConcreteCalls(assoc,
 
         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);
@@ -492,13 +491,6 @@ else if (tighters.isEmpty()) return Doc.cat(Doc.line(), Doc.hang(2, Doc.sep(
   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/syntax/concrete/Pattern.java b/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java
index 2e9c4f0948..94f9bfad4a 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java
@@ -30,7 +30,13 @@
 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.IrrefutableLam] in desugarer.
+  ///
+  /// @see Pattern.Bind
+  /// @see Pattern.CalmFace
   interface Refutable {
+    /// Returns the [LocalVar] this [Pattern] introduced, with [SourcePos] {@param pos} if it doesn't have one.
     @NotNull LocalVar toLocalVar(@NotNull SourcePos pos);
   }
 

From a734bb6f85ea24c5535d2e169317174de5b8c12e Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Fri, 17 Jan 2025 20:45:35 +0800
Subject: [PATCH 07/17] pat-lam: something

---
 .../main/java/org/aya/resolve/visitor/ExprResolver.java    | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

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 cb0fa86c84..8807ae1ea8 100644
--- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
+++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
@@ -115,11 +115,6 @@ 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);
@@ -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);
     };
   }

From 47ba19a13b713a5d59ece031964e4718be2c5d17 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Mon, 20 Jan 2025 02:48:42 -0500
Subject: [PATCH 08/17] 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 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 fb8643becf..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 | <<licit lambdaTeleBinder>>
   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, "<expr>");
@@ -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 <<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;
@@ -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 b1d1b81c8a..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 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"
@@ -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 <<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
@@ -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*)>>
 
@@ -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
diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java
index 165c1895bf..24cadbfb4e 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:
  * <ul>
@@ -654,7 +655,7 @@ 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) {
@@ -662,9 +663,21 @@ 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);
+    }
+    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(

From 7c126eceab75e8fa2738808fbb6f2a4fdb093938 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Mon, 20 Jan 2025 02:57:16 -0500
Subject: [PATCH 09/17] revert: syntax changes in stdlib (sorry)

---
 cli-impl/src/test/resources/shared/src/data/sum/base.aya  | 2 +-
 .../test/resources/shared/src/relation/binary/path.aya    | 2 +-
 cli-impl/src/test/resources/success/src/PLFA.aya          | 8 ++++----
 cli-impl/src/test/resources/success/src/Pattern.aya       | 2 +-
 4 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/cli-impl/src/test/resources/shared/src/data/sum/base.aya b/cli-impl/src/test/resources/shared/src/data/sum/base.aya
index 1da8af224c..79e2b1e74f 100644
--- a/cli-impl/src/test/resources/shared/src/data/sum/base.aya
+++ b/cli-impl/src/test/resources/shared/src/data/sum/base.aya
@@ -11,7 +11,7 @@ def Sum-rec
   (P : Type)
   (lrec : A -> P)
   (rrec : B -> P)
-  : P => Sum-ind e (fn _ => P) (fn a, _ => lrec a) (fn b, _ => rrec b)
+  : P => Sum-ind e (fn _e => P) (fn a _p => lrec a) (fn b _p => rrec b)
 
 def Sum-ind
   (e : Sum A B)
diff --git a/cli-impl/src/test/resources/shared/src/relation/binary/path.aya b/cli-impl/src/test/resources/shared/src/relation/binary/path.aya
index a826e4e9ef..d5f6007a33 100644
--- a/cli-impl/src/test/resources/shared/src/relation/binary/path.aya
+++ b/cli-impl/src/test/resources/shared/src/relation/binary/path.aya
@@ -8,7 +8,7 @@ def refl {a : A} : a = a => \i => a
 def pmap (f : A -> B) {a b : A} (p : a = b) : f a = f b => \i => f (p i)
 def pinv {a b : A} (p : a = b) : b = a => coe 0 1 (\i => p i = a) refl
 
-def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i, a => p a i
+def funExt (f g : A -> B) (p : ∀ a -> f a = g a) : f = g => \i a => p a i
 
 def pmapd {A : I -> Type} (B : ∀ i -> A i -> Type)
     (f : ∀ i -> ∀ (a : A i) -> B i a) {a b : _} (p : Path A a b)
diff --git a/cli-impl/src/test/resources/success/src/PLFA.aya b/cli-impl/src/test/resources/success/src/PLFA.aya
index e2b38d301b..f258bc4341 100644
--- a/cli-impl/src/test/resources/success/src/PLFA.aya
+++ b/cli-impl/src/test/resources/success/src/PLFA.aya
@@ -12,7 +12,7 @@ def deMorgan-law => Fn (A B : Type) -> (neg (Sig (neg A) ** (neg B))) -> Sum A B
 
 @suppress(MostGeneralSolution)
 def LEM=>deMorgan-law (lem : LEM) : deMorgan-law =>
-  fn tyA, tyB, np =>
+  fn tyA tyB np =>
     Sum-rec (lem tyA)
     _
     (fn A => A)
@@ -23,7 +23,7 @@ def LEM=>deMorgan-law (lem : LEM) : deMorgan-law =>
       (fn ¬B => exfalso (np (¬A, ¬B))))
 
 def deMorgan-law=>imply-as-lor (dml : deMorgan-law) : imply-as-lor =>
-  fn tyA, tyB, f =>
+  fn tyA tyB f =>
     dml (neg tyA) tyB (fn p => p.1 (fn A => exfalso (p.2 (f A))))
 
 def imply-as-lor=>LEM (ial : imply-as-lor) : LEM =>
@@ -32,7 +32,7 @@ def imply-as-lor=>LEM (ial : imply-as-lor) : LEM =>
 @suppress(MostGeneralSolution)
 def imply-as-lor=>peirce-law (ial : imply-as-lor) : peirce-law =>
   // f : ((A -> B) -> A)
-  fn tyA, tyB, f => Sum-rec
+  fn tyA tyB f => Sum-rec
     (imply-as-lor=>LEM ial tyA)
     _
     (fn A => A)
@@ -40,7 +40,7 @@ def imply-as-lor=>peirce-law (ial : imply-as-lor) : peirce-law =>
 
 @suppress(MostGeneralSolution)
 def peirce-law=>double-neg-elim (pl : peirce-law) : double-neg-elim =>
-  fn tyA, ¬¬A =>
+  fn tyA ¬¬A =>
     pl tyA Empty (fn ¬A => exfalso (¬¬A ¬A))
 
 @suppress(MostGeneralSolution)
diff --git a/cli-impl/src/test/resources/success/src/Pattern.aya b/cli-impl/src/test/resources/success/src/Pattern.aya
index 6980139943..35a0beb245 100644
--- a/cli-impl/src/test/resources/success/src/Pattern.aya
+++ b/cli-impl/src/test/resources/success/src/Pattern.aya
@@ -53,5 +53,5 @@ module PullRequest1268 {
   // unpi: D d0 -> d1
   @suppress(LocalShadow)
   def elims {A : Type} (a : A) (B : Type) (b : B) {C : Type} : Fn (D : Type) D -> D elim a, b
-  | a => fn b, D => id D
+  | a => fn b D => id D
 }

From 7ad19659f98ecbd2881cc5b2dcdbae5e8e3b2fc1 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Mon, 20 Jan 2025 02:59:25 -0500
Subject: [PATCH 10/17] revert: prettier, with some changes

---
 .../org/aya/prettier/ConcretePrettier.java    | 38 ++++++++++---------
 1 file changed, 20 insertions(+), 18 deletions(-)

diff --git a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
index b5bad20143..ac24bfe0cf 100644
--- a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
@@ -2,13 +2,18 @@
 // 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.MutableList;
-import kala.control.Option;
 import kala.range.primitive.IntRange;
 import org.aya.generic.Constants;
 import org.aya.generic.Modifier;
@@ -26,18 +31,11 @@
 import org.aya.syntax.ref.LocalVar;
 import org.aya.util.Arg;
 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;
 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
  */
@@ -105,15 +103,18 @@ yield visitConcreteCalls(assoc,
           optionImplicit());
       }
       case Expr.Lambda expr -> {
-        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);
+        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);
       }
       case Expr.IrrefutableLam(var cls) -> checkParen(outer, visitLambda(cls), Outer.BinOp);
       case Expr.Hole expr -> {
@@ -490,7 +491,8 @@ else if (tighters.isEmpty()) return Doc.cat(Doc.line(), Doc.hang(2, Doc.sep(
 
   private @NotNull Doc visitLambda(@NotNull Pattern.Clause clause) {
     var prelude = MutableList.of(LAMBDA);
-    prelude.append(clause(clause));
+    var clauseDoc = clause(clause);
+    prelude.append(Doc.braced(clauseDoc));
     return Doc.sep(prelude);
   }
 }

From 17f69e1822ff5413b1e43f127289f236e52ff4a7 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Mon, 20 Jan 2025 03:09:44 -0500
Subject: [PATCH 11/17] producer: reimplement og lambda

---
 .../java/org/aya/resolve/salt/Desalt.java     |  7 +-----
 .../org/aya/resolve/visitor/ExprResolver.java |  2 +-
 .../java/org/aya/producer/AyaProducer.java    | 11 ++++++----
 .../org/aya/prettier/ConcretePrettier.java    |  2 +-
 .../java/org/aya/syntax/concrete/Expr.java    | 22 +++++++++----------
 .../java/org/aya/syntax/concrete/Pattern.java |  2 +-
 .../main/java/org/aya/util/IterableUtil.java  |  4 ++--
 7 files changed, 23 insertions(+), 27 deletions(-)

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 cdb65717c7..38e5002cbd 100644
--- a/base/src/main/java/org/aya/resolve/salt/Desalt.java
+++ b/base/src/main/java/org/aya/resolve/salt/Desalt.java
@@ -3,14 +3,11 @@
 package org.aya.resolve.salt;
 
 import kala.collection.immutable.ImmutableSeq;
-import kala.value.primitive.MutableBooleanValue;
-import org.aya.generic.Constants;
 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.Arg;
 import org.aya.util.error.Panic;
 import org.aya.util.error.PosedUnaryOperator;
 import org.aya.util.error.SourcePos;
@@ -18,8 +15,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.Objects;
-
 /** Desugar, but the sugars are not sweet enough, therefore called salt. */
 public final class Desalt implements PosedUnaryOperator<Expr> {
   private final @NotNull ResolveInfo info;
@@ -77,7 +72,7 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
       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.IrrefutableLam lam -> {
+      case Expr.RawLam lam -> {
         var isVanilla = lam.patterns().allMatch(x -> x.term().data() instanceof Pattern.Refutable);
 
         ImmutableSeq<LocalVar> lamTele;
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 8807ae1ea8..70ef946af0 100644
--- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
+++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
@@ -115,7 +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.IrrefutableLam lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause()));
+      case Expr.RawLam lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause()));
       case Expr.DepType depType -> {
         var mCtx = MutableValue.create(ctx);
         var param = bind(depType.param(), mCtx);
diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java
index 24cadbfb4e..97725bda8f 100644
--- a/producer/src/main/java/org/aya/producer/AyaProducer.java
+++ b/producer/src/main/java/org/aya/producer/AyaProducer.java
@@ -664,19 +664,22 @@ private record DeclNameOrInfix(@NotNull WithPos<String> 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<Pattern>(v.definition(), new Pattern.Bind(v)))
+        .map(Arg::ofExplicitly)
+        .toImmutableSeq();
+      return new WithPos<>(pos, new Expr.RawLam(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.IrrefutableLam(new Pattern.Clause(pos, tele, Option.some(result))));
+      return new WithPos<>(pos, new Expr.RawLam(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)));
+      return new WithPos<>(pos, new Expr.RawLam(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 ac24bfe0cf..c4ac09de1c 100644
--- a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
@@ -116,7 +116,7 @@ yield visitConcreteCalls(assoc,
         }
         yield checkParen(outer, Doc.sep(prelude), Outer.BinOp);
       }
-      case Expr.IrrefutableLam(var cls) -> checkParen(outer, visitLambda(cls), Outer.BinOp);
+      case Expr.RawLam(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();
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 8e88a6beaa..dfc8088f15 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -2,10 +2,13 @@
 // 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;
-import kala.control.Option;
 import kala.value.MutableValue;
 import org.aya.generic.AyaDocile;
 import org.aya.generic.Nested;
@@ -27,11 +30,6 @@
 import org.jetbrains.annotations.NotNull;
 import org.jetbrains.annotations.Nullable;
 
-import java.util.Objects;
-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);
@@ -137,18 +135,18 @@ public Ref(@NotNull AnyVar var) {
     @Override public void forEach(@NotNull PosedConsumer<Expr> f) { }
   }
 
-  record IrrefutableLam(@NotNull Pattern.Clause clause) implements Expr, Sugar {
+  record RawLam(@NotNull Pattern.Clause clause) implements Expr, Sugar {
     public static boolean canBeBind(@NotNull Arg<WithPos<Pattern>> pat) {
       var thePat = pat.term().data();
       return thePat instanceof Pattern.Bind || thePat == Pattern.CalmFace.INSTANCE;
     }
 
-    public IrrefutableLam {
+    public RawLam {
       assert clause.patterns.isNotEmpty();
     }
 
-    public @NotNull IrrefutableLam update(@NotNull Pattern.Clause clause) {
-      return clause == this.clause ? this : new IrrefutableLam(clause);
+    public @NotNull Expr.RawLam update(@NotNull Pattern.Clause clause) {
+      return clause == this.clause ? this : new RawLam(clause);
     }
 
     public @NotNull ImmutableSeq<Arg<WithPos<Pattern>>> patterns() {
@@ -159,11 +157,11 @@ public static boolean canBeBind(@NotNull Arg<WithPos<Pattern>> pat) {
       return clause.expr.get();
     }
 
-    @Override public @NotNull IrrefutableLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
+    @Override public @NotNull Expr.RawLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
       return descent(f, PosedUnaryOperator.identity());
     }
 
-    public @NotNull IrrefutableLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f, @NotNull PosedUnaryOperator<@NotNull Pattern> g) {
+    public @NotNull Expr.RawLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f, @NotNull PosedUnaryOperator<@NotNull Pattern> g) {
       return update(clause.descent(f, g));
     }
 
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 94f9bfad4a..67f6e5c841 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java
@@ -31,7 +31,7 @@ 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.IrrefutableLam] in desugarer.
+  /// Whether a [Pattern] can be a [Pattern.Bind], this is used by [Expr.RawLam] in desugarer.
   ///
   /// @see Pattern.Bind
   /// @see Pattern.CalmFace
diff --git a/tools/src/main/java/org/aya/util/IterableUtil.java b/tools/src/main/java/org/aya/util/IterableUtil.java
index 8a695fb28f..4c6c462d83 100644
--- a/tools/src/main/java/org/aya/util/IterableUtil.java
+++ b/tools/src/main/java/org/aya/util/IterableUtil.java
@@ -2,11 +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.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 <T> void forEach(@NotNull Iterable<T> it, @NotNull BiConsumer<T, T> separator, @NotNull Consumer<T> run) {
     var iter = it.iterator();

From 0b48848f72480cf9594606186e452089bb31552c Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Mon, 20 Jan 2025 03:10:30 -0500
Subject: [PATCH 12/17] concrete: rename

---
 .../java/org/aya/resolve/salt/Desalt.java     |  2 +-
 .../org/aya/resolve/visitor/ExprResolver.java |  2 +-
 .../java/org/aya/producer/AyaProducer.java    |  6 ++---
 .../org/aya/prettier/ConcretePrettier.java    |  2 +-
 .../java/org/aya/syntax/concrete/Expr.java    | 25 ++++++++-----------
 .../java/org/aya/syntax/concrete/Pattern.java |  2 +-
 6 files changed, 17 insertions(+), 22 deletions(-)

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 38e5002cbd..16c87250c6 100644
--- a/base/src/main/java/org/aya/resolve/salt/Desalt.java
+++ b/base/src/main/java/org/aya/resolve/salt/Desalt.java
@@ -72,7 +72,7 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
       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.RawLam lam -> {
+      case Expr.ClauseLam lam -> {
         var isVanilla = lam.patterns().allMatch(x -> x.term().data() instanceof Pattern.Refutable);
 
         ImmutableSeq<LocalVar> lamTele;
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 70ef946af0..56b42350d2 100644
--- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
+++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
@@ -115,7 +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.RawLam lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause()));
+      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);
diff --git a/producer/src/main/java/org/aya/producer/AyaProducer.java b/producer/src/main/java/org/aya/producer/AyaProducer.java
index 97725bda8f..b4e05df3d6 100644
--- a/producer/src/main/java/org/aya/producer/AyaProducer.java
+++ b/producer/src/main/java/org/aya/producer/AyaProducer.java
@@ -668,18 +668,18 @@ private record DeclNameOrInfix(@NotNull WithPos<String> name, @Nullable OpDecl.O
         .map(v -> new WithPos<Pattern>(v.definition(), new Pattern.Bind(v)))
         .map(Arg::ofExplicitly)
         .toImmutableSeq();
-      return new WithPos<>(pos, new Expr.RawLam(new Pattern.Clause(pos, tele, Option.some(result))));
+      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.RawLam(new Pattern.Clause(pos, tele, Option.some(result))));
+      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<WithPos<Expr>> result = bodyExpr == null ? Option.none() : Option.some(expr(bodyExpr));
       var tele = unitPattern(node.child(UNIT_PATTERN));
-      return new WithPos<>(pos, new Expr.RawLam(new Pattern.Clause(pos, ImmutableSeq.of(tele), result)));
+      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 c4ac09de1c..cd17e8679b 100644
--- a/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
+++ b/syntax/src/main/java/org/aya/prettier/ConcretePrettier.java
@@ -116,7 +116,7 @@ yield visitConcreteCalls(assoc,
         }
         yield checkParen(outer, Doc.sep(prelude), Outer.BinOp);
       }
-      case Expr.RawLam(var cls) -> checkParen(outer, visitLambda(cls), 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();
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 dfc8088f15..663f4e6206 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -74,7 +74,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.
+  ///                                 a to-be-solved by tycking hole.
   record Hole(
     boolean explicit,
     @Nullable WithPos<Expr> filling,
@@ -135,33 +135,28 @@ public Ref(@NotNull AnyVar var) {
     @Override public void forEach(@NotNull PosedConsumer<Expr> f) { }
   }
 
-  record RawLam(@NotNull Pattern.Clause clause) implements Expr, Sugar {
+  record ClauseLam(@NotNull Pattern.Clause clause) implements Expr, Sugar {
     public static boolean canBeBind(@NotNull Arg<WithPos<Pattern>> pat) {
       var thePat = pat.term().data();
       return thePat instanceof Pattern.Bind || thePat == Pattern.CalmFace.INSTANCE;
     }
 
-    public RawLam {
+    public ClauseLam {
       assert clause.patterns.isNotEmpty();
     }
 
-    public @NotNull Expr.RawLam update(@NotNull Pattern.Clause clause) {
-      return clause == this.clause ? this : new RawLam(clause);
+    public @NotNull Expr.ClauseLam update(@NotNull Pattern.Clause clause) {
+      return clause == this.clause ? this : new ClauseLam(clause);
     }
 
-    public @NotNull ImmutableSeq<Arg<WithPos<Pattern>>> patterns() {
-      return clause.patterns;
-    }
-
-    public @NotNull WithPos<Expr> body() {
-      return clause.expr.get();
-    }
+    public @NotNull ImmutableSeq<Arg<WithPos<Pattern>>> patterns() { return clause.patterns; }
+    public @NotNull WithPos<Expr> body() { return clause.expr.get(); }
 
-    @Override public @NotNull Expr.RawLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
+    @Override public @NotNull Expr.ClauseLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f) {
       return descent(f, PosedUnaryOperator.identity());
     }
 
-    public @NotNull Expr.RawLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f, @NotNull PosedUnaryOperator<@NotNull Pattern> g) {
+    public @NotNull Expr.ClauseLam descent(@NotNull PosedUnaryOperator<@NotNull Expr> f, @NotNull PosedUnaryOperator<@NotNull Pattern> g) {
       return update(clause.descent(f, g));
     }
 
@@ -456,7 +451,7 @@ public void forEach(@NotNull Consumer<Expr> f) {
     /// @param generator `x * y` part above
     /// @param binds     `x <- [1, 2, 3], y <- [4, 5, 6]` part above
     /// @param names     the bind (`>>=`) function, it is [#monadBind] in default,
-    ///                  the pure (`return`) function, it is [#functorPure] in default
+    ///                                   the pure (`return`) function, it is [#functorPure] in default
     /// @apiNote a ArrayCompBlock will be desugar to a do-block. For the example above,
     /// it will be desugared to `do x <- [1, 2, 3], y <- [4, 5, 6], return x * y`
     public record CompBlock(
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 67f6e5c841..09fe397125 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java
@@ -31,7 +31,7 @@ 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.RawLam] in desugarer.
+  /// Whether a [Pattern] can be a [Pattern.Bind], this is used by [Expr.ClauseLam] in desugarer.
   ///
   /// @see Pattern.Bind
   /// @see Pattern.CalmFace

From bac54409c9066b774e4ace5b9f52791abfaaf44c Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Mon, 20 Jan 2025 03:12:47 -0500
Subject: [PATCH 13/17] fmt: IntelliJ has a bug

---
 base/src/main/java/org/aya/resolve/visitor/ExprResolver.java | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

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 56b42350d2..d304a16ad3 100644
--- a/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
+++ b/base/src/main/java/org/aya/resolve/visitor/ExprResolver.java
@@ -234,9 +234,7 @@ private void addReference(@NotNull DefVar<?, ?> defVar) {
 
   /// 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.
+  /// @param telescope the telescope of the clause which the {@param pattern} lives, can be [ImmutableSeq#empty()].
   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);

From db281fb7ddb89fec9e3bbb2b71ca434a0a9b6651 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Mon, 20 Jan 2025 03:15:50 -0500
Subject: [PATCH 14/17] fmt: more workarounds to intellij bug, rename
 `Refutable` to `BindLike`

---
 .../src/main/java/org/aya/resolve/salt/Desalt.java |  8 ++++----
 .../main/java/org/aya/syntax/concrete/Expr.java    |  5 ++---
 .../main/java/org/aya/syntax/concrete/Pattern.java | 14 +++++---------
 3 files changed, 11 insertions(+), 16 deletions(-)

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 16c87250c6..820e42a10a 100644
--- a/base/src/main/java/org/aya/resolve/salt/Desalt.java
+++ b/base/src/main/java/org/aya/resolve/salt/Desalt.java
@@ -73,19 +73,19 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
       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.Refutable);
+        var isVanilla = lam.patterns().allMatch(x -> x.term().data() instanceof Pattern.BindLike);
 
         ImmutableSeq<LocalVar> lamTele;
         WithPos<Expr> realBody;
 
         if (isVanilla) {
           // fn a _ c => ...
-          lamTele = lam.patterns().map(x -> ((Pattern.Refutable) x.term().data()).toLocalVar(x.term().sourcePos()));
+          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.Refutable refutable) {
-              var bind = refutable.toLocalVar(pat.term().sourcePos());
+            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(), bind.definition());
             } else {
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 663f4e6206..690dd52b35 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Expr.java
@@ -73,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<Expr> filling,
@@ -451,7 +450,7 @@ public void forEach(@NotNull Consumer<Expr> f) {
     /// @param generator `x * y` part above
     /// @param binds     `x <- [1, 2, 3], y <- [4, 5, 6]` part above
     /// @param names     the bind (`>>=`) function, it is [#monadBind] in default,
-    ///                                   the pure (`return`) function, it is [#functorPure] in default
+    ///                  the pure (`return`) function, it is [#functorPure] in default
     /// @apiNote a ArrayCompBlock will be desugar to a do-block. For the example above,
     /// it will be desugared to `do x <- [1, 2, 3], y <- [4, 5, 6], return x * y`
     public record CompBlock(
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 09fe397125..1cde7028f6 100644
--- a/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java
+++ b/syntax/src/main/java/org/aya/syntax/concrete/Pattern.java
@@ -35,7 +35,7 @@ interface Salt { }
   ///
   /// @see Pattern.Bind
   /// @see Pattern.CalmFace
-  interface Refutable {
+  interface BindLike {
     /// Returns the [LocalVar] this [Pattern] introduced, with [SourcePos] {@param pos} if it doesn't have one.
     @NotNull LocalVar toLocalVar(@NotNull SourcePos pos);
   }
@@ -72,14 +72,12 @@ enum Absurd implements Pattern {
     @Override public @NotNull Pattern descent(@NotNull PosedUnaryOperator<@NotNull Pattern> f) { return this; }
   }
 
-  enum CalmFace implements Pattern, Refutable {
+  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);
-    }
+    @Override public @NotNull LocalVar toLocalVar(@NotNull SourcePos pos) { return LocalVar.generate(pos); }
   }
 
   /**
@@ -88,13 +86,11 @@ enum CalmFace implements Pattern, Refutable {
   record Bind(
     @NotNull LocalVar bind,
     @ForLSP @NotNull MutableValue<@Nullable Term> type
-  ) implements Pattern, Refutable {
+  ) 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;
-    }
+    @Override public @NotNull LocalVar toLocalVar(@NotNull SourcePos pos) { return bind; }
   }
 
   record Con(

From 79c8c442d26688eef92e5a17931c8344ce0dc9e6 Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Mon, 20 Jan 2025 03:30:13 -0500
Subject: [PATCH 15/17] test: for #94

---
 cli-impl/src/test/resources/success/src/Test.aya | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/cli-impl/src/test/resources/success/src/Test.aya b/cli-impl/src/test/resources/success/src/Test.aya
index 5549fa8e42..309da5bd8a 100644
--- a/cli-impl/src/test/resources/success/src/Test.aya
+++ b/cli-impl/src/test/resources/success/src/Test.aya
@@ -105,3 +105,10 @@ module Issue1249 {
   variable A B : Type
   def transp (p : A = B) (a : A) : B => coe 0 1 p a
 }
+
+module Issue94 {
+  open inductive IsZero Nat
+  | zero => ack
+  def absurd (A : Type) : Empty -> A => fn ()
+  def irrefutable : Fn (a : Nat) -> IsZero a -> Nat => fn { zero, ack => 233 }
+}

From 330ff1721c442f6f8060916d5afaa1c87a5362fd Mon Sep 17 00:00:00 2001
From: ice1000 <ice1000kotlin@foxmail.com>
Date: Mon, 20 Jan 2025 03:53:50 -0500
Subject: [PATCH 16/17] test: do not test too complicated case yet

---
 base/src/main/java/org/aya/resolve/salt/Desalt.java | 2 +-
 cli-impl/src/test/resources/success/src/Test.aya    | 9 ++++++---
 2 files changed, 7 insertions(+), 4 deletions(-)

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 820e42a10a..ac26e76c89 100644
--- a/base/src/main/java/org/aya/resolve/salt/Desalt.java
+++ b/base/src/main/java/org/aya/resolve/salt/Desalt.java
@@ -100,7 +100,7 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
             lamTele.map(x -> new WithPos<>(x.definition(), new Expr.Ref(x))),
             ImmutableSeq.of(lam.clause()),
             ImmutableSeq.empty(),
-            false,
+            true,
             null
           ));
         }
diff --git a/cli-impl/src/test/resources/success/src/Test.aya b/cli-impl/src/test/resources/success/src/Test.aya
index 309da5bd8a..0972efe01f 100644
--- a/cli-impl/src/test/resources/success/src/Test.aya
+++ b/cli-impl/src/test/resources/success/src/Test.aya
@@ -107,8 +107,11 @@ module Issue1249 {
 }
 
 module Issue94 {
-  open inductive IsZero Nat
-  | zero => ack
   def absurd (A : Type) : Empty -> A => fn ()
-  def irrefutable : Fn (a : Nat) -> IsZero a -> Nat => fn { zero, ack => 233 }
+  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 }

From bbf708696499ad2a0cd09ec19fd145be40de4576 Mon Sep 17 00:00:00 2001
From: HoshinoTented <hoshinotented@qq.com>
Date: Mon, 20 Jan 2025 17:48:07 +0800
Subject: [PATCH 17/17] fix: test

---
 base/src/main/java/org/aya/resolve/salt/Desalt.java | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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 ac26e76c89..af2f15729f 100644
--- a/base/src/main/java/org/aya/resolve/salt/Desalt.java
+++ b/base/src/main/java/org/aya/resolve/salt/Desalt.java
@@ -87,9 +87,9 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
             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(), bind.definition());
+              return LocalVar.generate(bind.name(), SourcePos.NONE);
             } else {
-              return LocalVar.generate("IrrefutableLam" + idx, pat.term().sourcePos());
+              return LocalVar.generate("IrrefutableLam" + idx, SourcePos.NONE);
             }
           });