merge: Irrefutable Lambda (#1283)

This PR fixes #94 by:
* AyaProducer producing `Expr.IrrefutableLam`
* Desugar `Expr.IrrefutableLam` to `Expr.Lambda`

TODO:
+ [x] producer
+ [x] question: should we resolve `Expr.Lambda` even if it is a desugar
output?

base/src/main/java/org/aya/resolve/salt/Desalt.java

@@ -1,11 +1,13 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.resolve.salt;
 
+import kala.collection.immutable.ImmutableSeq;
 import org.aya.generic.term.SortKind;
 import org.aya.resolve.ResolveInfo;
 import org.aya.syntax.concrete.Expr;
 import org.aya.syntax.concrete.Pattern;
+import org.aya.syntax.ref.LocalVar;
 import org.aya.util.error.Panic;
 import org.aya.util.error.PosedUnaryOperator;
 import org.aya.util.error.SourcePos;
@@ -70,6 +72,41 @@ public final class Desalt implements PosedUnaryOperator<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.ClauseLam lam -> {
+        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.BindLike) x.term().data()).toLocalVar(x.term().sourcePos()));
+          realBody = lam.body();
+        } else {
+          lamTele = lam.patterns().mapIndexed((idx, pat) -> {
+            if (pat.term().data() instanceof Pattern.BindLike bindLike) {
+              var bind = bindLike.toLocalVar(pat.term().sourcePos());
+              // we need fresh bind, since [bind] may be used in the body.
+              return LocalVar.generate(bind.name(), SourcePos.NONE);
+            } else {
+              return LocalVar.generate("IrrefutableLam" + idx, SourcePos.NONE);
+            }
+          });
+
+          // fn a' _ c' => match a', _, c' { a, _, (con c) => ... }
+          // the var with prime are renamed vars
+
+          realBody = new WithPos<>(sourcePos, new Expr.Match(
+            lamTele.map(x -> new WithPos<>(x.definition(), new Expr.Ref(x))),
+            ImmutableSeq.of(lam.clause()),
+            ImmutableSeq.empty(),
+            true,
+            null
+          ));
+        }
+
+        yield apply(Expr.buildLam(sourcePos, lamTele.view(), realBody));
+      }
     };
   }
   public @NotNull PosedUnaryOperator<Pattern> pattern = new Pat();

base/src/main/java/org/aya/resolve/visitor/ExprResolver.java

@@ -1,4 +1,4 @@
-// Copyright (c) 2020-2024 Tesla (Yinsen) Zhang.
+// Copyright (c) 2020-2025 Tesla (Yinsen) Zhang.
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.resolve.visitor;
 
@@ -30,7 +30,6 @@
 import org.aya.util.error.WithPos;
 import org.jetbrains.annotations.Contract;
 import org.jetbrains.annotations.NotNull;
-import org.jetbrains.annotations.Nullable;
 
 /**
  * Resolves bindings.
@@ -116,11 +115,7 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) {
     return switch (pre(expr)) {
       case Expr.Do doExpr ->
         doExpr.update(apply(SourcePos.NONE, doExpr.bindName()), bind(doExpr.binds(), MutableValue.create(ctx)));
-      case Expr.Lambda lam -> {
-        var mCtx = MutableValue.create(ctx);
-        mCtx.update(ctx -> ctx.bind(lam.ref()));
-        yield lam.update(lam.body().descent(enter(mCtx.get())));
-      }
+      case Expr.ClauseLam lam -> lam.update(clause(ImmutableSeq.empty(), lam.clause()));
       case Expr.DepType depType -> {
         var mCtx = MutableValue.create(ctx);
         var param = bind(depType.param(), mCtx);
@@ -202,6 +197,8 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) {
         yield match.update(discriminant, clauses, returns);
       }
 
+      // Expr.Lambda is a desugar target, which is produced after resolving.
+      case Expr.Lambda _ -> Panic.unreachable();
       case Expr newExpr -> newExpr.descent(this);
     };
   }
@@ -235,6 +232,9 @@ private void addReference(@NotNull DefVar<?, ?> defVar) {
     return clause.update(pats, body);
   }
 
+  /// Resolve a [Pattern]
+  ///
+  /// @param telescope the telescope of the clause which the {@param pattern} lives, can be [ImmutableSeq#empty()].
   public @NotNull WithPos<Pattern> resolvePattern(@NotNull WithPos<Pattern> pattern, @NotNull ImmutableSeq<LocalVar> telescope, MutableValue<Context> ctx) {
     var resolver = new PatternResolver(ctx.get(), telescope, this::addReference);
     var result = pattern.descent(resolver);

base/src/main/java/org/aya/tyck/ExprTycker.java

@@ -2,6 +2,7 @@
 // Use of this source code is governed by the MIT license that can be found in the LICENSE.md file.
 package org.aya.tyck;
 
+import kala.collection.AbstractSeqView;
 import kala.collection.immutable.ImmutableSeq;
 import kala.collection.immutable.ImmutableTreeSeq;
 import kala.collection.mutable.MutableList;

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).

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)

cli-impl/src/test/resources/success/src/Test.aya

@@ -105,3 +105,13 @@ module Issue1249 {
   variable A B : Type
   def transp (p : A = B) (a : A) : B => coe 0 1 p a
 }
+
+module Issue94 {
+  def absurd (A : Type) : Empty -> A => fn ()
+  def obvious : Fn (a : Sig Nat ** Nat) -> Nat => fn { (a, b) => a + b }
+}
+
+// relies on match elim
+// open inductive IsZero Nat
+// | zero => ack
+// def irrefutable : Fn (a : Nat) -> IsZero a -> Nat => fn { zero, ack => 233 }

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

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 teleBinderUntyped (IMPLIES expr)?
-  public static boolean lambdaExpr(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "lambdaExpr")) return false;
+  // KW_LAMBDA teleBinderUntyped lambdaBody?
+  public static boolean lambda0Expr(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "lambda0Expr")) return false;
     if (!nextTokenIsSmart(b, KW_LAMBDA)) return false;
     boolean r;
     Marker m = enter_section_(b);
     r = consumeTokenSmart(b, KW_LAMBDA);
     r = r && teleBinderUntyped(b, l + 1);
-    r = r && lambdaExpr_2(b, l + 1);
-    exit_section_(b, m, LAMBDA_EXPR, r);
+    r = r && lambda0Expr_2(b, l + 1);
+    exit_section_(b, m, LAMBDA_0_EXPR, r);
     return r;
   }
 
-  // (IMPLIES expr)?
-  private static boolean lambdaExpr_2(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "lambdaExpr_2")) return false;
-    lambdaExpr_2_0(b, l + 1);
+  // lambdaBody?
+  private static boolean lambda0Expr_2(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "lambda0Expr_2")) return false;
+    lambdaBody(b, l + 1);
     return true;
   }
 
-  // IMPLIES expr
-  private static boolean lambdaExpr_2_0(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "lambdaExpr_2_0")) return false;
+  // KW_LAMBDA <<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;
   }