Match elim

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

@@ -46,7 +46,7 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
       }
       case Expr.Match match -> {
         return match.update(
-          match.discriminant().map(e -> e.descent(this)),
+          match.discriminant().map(d -> d.descent(this)),
           match.clauses().map(clause -> clause.descent(this, pattern)),
           match.returns() != null ? match.returns().descent(this) : null
         );
@@ -97,10 +97,12 @@ public final class Desalt implements PosedUnaryOperator<Expr> {
           // 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))),
+            lamTele.map(x -> new Expr.Match.Discriminant(
+              new WithPos<>(x.definition(), new Expr.Ref(x)),
+              null,
+              true
+            )),
             ImmutableSeq.of(lam.clause()),
-            ImmutableSeq.empty(),
-            true,
             null
           ));
         }

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

@@ -184,9 +184,13 @@ public ExprResolver(@NotNull Context ctx, boolean allowGeneralizing) {
         yield letOpen.update(letOpen.body().descent(enter(context)));
       }
       case Expr.Match match -> {
-        var discriminant = match.discriminant().map(x -> x.descent(this));
+        var discriminant = match.discriminant().map(d -> d.descent(this));
         var returnsCtx = ctx;
-        for (var binding : match.asBindings()) returnsCtx = returnsCtx.bind(binding);
+        for (var discr : match.discriminant()) {
+          if (discr.asBinding() != null) {
+            returnsCtx = returnsCtx.bind(discr.asBinding());
+          }
+        }
         var returns = match.returns() != null ? match.returns().descent(enter(returnsCtx)) : null;
 
         // Requires exhaustiveness check, therefore must need the full data body

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;
@@ -152,20 +153,13 @@
           element -> inherit(element, elementTy).wellTyped()));
         yield new Jdg.Default(new ListTerm(results, recog, dataCall), type);
       }
-      case Expr.Match(var discriminant, var clauses, var asBindings, var isElim, var returns) -> {
-        var wellArgs = discriminant.map(this::synthesize);
+      case Expr.Match(var discriminant, var clauses, var returns) -> {
+        var wellArgs = discriminant.map(d -> synthesize(d.discr()));
         Term storedTy;
         // Type check the type annotation
         if (returns != null) {
-          if (asBindings.isEmpty()) {
-            unifyTyReported(type, storedTy = ty(returns), returns);
-          } else {
-            try (var _ = subscope()) {
-              asBindings.forEachWith(wellArgs, (as, discr) -> localCtx().put(as, discr.type()));
-              storedTy = ty(returns).bindTele(asBindings.view());
-            }
-            unifyTyReported(type, storedTy.instTele(wellArgs.view().map(Jdg::wellTyped)), returns);
-          }
+          storedTy = matchReturnTy(discriminant, wellArgs, returns);
+          unifyTyReported(type, storedTy.instTele(wellArgs.view().map(Jdg::wellTyped)), returns);
         } else {
           storedTy = type;
         }
@@ -182,17 +176,50 @@
     };
   }
 
+  private @NotNull Term matchReturnTy(
+    ImmutableSeq<Expr.Match.Discriminant> discriminant,
+    ImmutableSeq<Jdg> wellArgs, WithPos<Expr> returns
+  ) {
+    try (var _ = subscope()) {
+      var tele = MutableList.<LocalVar>create();
+      wellArgs.forEachWith(discriminant, (arg, discr) -> {
+        if (discr.asBinding() != null) {
+          localCtx().put(discr.asBinding(), arg.type());
+          tele.append(discr.asBinding());
+        } else if (discr.isElim() && arg.wellTyped() instanceof FreeTerm(LocalVar name)) {
+          tele.append(name);
+        } else {
+          tele.append(LocalVar.generate(discr.discr().sourcePos()));
+        }
+      });
+
+      return ty(returns).bindTele(tele.view());
+    }
+  }
+
   private @NotNull MatchCall match(
-    ImmutableSeq<WithPos<Expr>> discriminant, @NotNull SourcePos exprPos,
+    ImmutableSeq<Expr.Match.Discriminant> discriminant, @NotNull SourcePos exprPos,
     ImmutableSeq<Pattern.Clause> clauses, ImmutableSeq<Jdg> wellArgs, Term type
   ) {
-    var telescope = wellArgs.map(x -> new Param(Constants.ANONYMOUS_PREFIX, x.type(), true));
+    var elimVarTele = MutableList.<LocalVar>create();
+    var paramTele = MutableList.<Param>create();
+    wellArgs.forEachWith(discriminant, (arg, discr) -> {
+      var paramTy = arg.type().bindTele(elimVarTele.view());
+
+      if (discr.isElim() && arg.wellTyped() instanceof FreeTerm(LocalVar name)) {
+        elimVarTele.append(name);
+      } else {
+        elimVarTele.append(LocalVar.generate(discr.discr().sourcePos()));
+      }
+
+      paramTele.append(new Param(Constants.ANONYMOUS_PREFIX, paramTy, true));
+    });
+
     var clauseTycker = new ClauseTycker.Worker(
       new ClauseTycker(this),
-      telescope,
+      paramTele.toSeq(),
       new DepTypeTerm.Unpi(ImmutableSeq.empty(), type),
-      ImmutableSeq.fill(discriminant.size(), i ->
-        new LocalVar("match" + i, discriminant.get(i).sourcePos(), GenerateKind.Basic.Tyck)),
+      elimVarTele.toSeq(),
       ImmutableSeq.empty(), clauses);
     var wellClauses = clauseTycker.check(exprPos).wellTyped().matchingsView();
 
@@ -458,16 +485,11 @@
 
         yield new Jdg.Default(new NewTerm(call), call);
       }
-      case Expr.Match(var discriminant, var clauses, var asBindings, var isElim, var returns) -> {
-        var wellArgs = discriminant.map(this::synthesize);
+      case Expr.Match(var discriminant, var clauses, var returns) -> {
+        var wellArgs = discriminant.map(d -> synthesize(d.discr()));
         if (returns == null) yield fail(expr.data(), new MatchMissingReturnsError(expr));
         // Type check the type annotation
-        Term type;
-        if (asBindings.isEmpty()) type = ty(returns);
-        else try (var _ = subscope()) {
-          asBindings.forEachWith(wellArgs, (as, discr) -> localCtx().put(as, discr.type()));
-          type = ty(returns).bindTele(asBindings.view());
-        }
+        Term type = matchReturnTy(discriminant, wellArgs, returns);
         yield new Jdg.Default(match(discriminant, expr.sourcePos(), clauses, wellArgs, type), type);
       }
       case Expr.Unresolved _ -> Panic.unreachable();

cli-impl/src/test/java/org/aya/test/fixtures/ParseError.java

@@ -21,8 +21,8 @@ public interface ParseError {
     @suppress(thisWillNeverBeARealWarning)
     def id {A : Type} (a : A) => a
     """;
-  @Language("Aya") String testMatchElim = "def test => match elim Type {}";
-  @Language("Aya") String testMatchNumMismatch = "def test => match e as a, b returns Type {}";
+  @Language("Aya") String testMatchElim = "def test => match elim Type, elim Type {}";
+  @Language("Aya") String testMatchElimAs = "def test => match elim e as a, elim f as b {}";
   @Language("Aya") String testImplicitTuplePat = """
     def test (Sig Type ** Type) : Type
     | ({a}, b) => a

cli-impl/src/test/resources/negative/ParseError.txt

@@ -64,27 +64,43 @@ Warning: Unrecognized warning `thisWillNeverBeARealWarning` will be ignored.
 That looks right!
 
 MatchElim:
-In file $FILE:1:12 ->
+In file $FILE:1:23 ->
 
-  1 │   def test => match elim Type {}
-    │               ╰────────────────╯
+  1 │   def test => match elim Type, elim Type {}
+    │                          ╰──╯
 
-Error: Elimination match must be on variables
+Error: Expect variable in match elim
+
+In file $FILE:1:34 ->
+
+  1 │   def test => match elim Type, elim Type {}
+    │                                     ╰──╯
+
+Error: Expect variable in match elim
 
 Parsing interrupted due to:
-1 error(s), 0 warning(s).
+2 error(s), 0 warning(s).
 Let's learn from that.
 
-MatchNumMismatch:
-In file $FILE:1:12 ->
+MatchElimAs:
+In file $FILE:1:18 ->
 
-  1 │   def test => match e as a, b returns Type {}
-    │               ╰─────────────────────────────╯
+  1 │   def test => match elim e as a, elim f as b {}
+    │                     ╰─────────╯
 
-Error: I see 2 as-binding(s) but 1 discriminant(s)
+Error: Don't use as-binding together with elim. Just use the elim-variable 
+       directly
+
+In file $FILE:1:31 ->
+
+  1 │   def test => match elim e as a, elim f as b {}
+    │                                  ╰─────────╯
+
+Error: Don't use as-binding together with elim. Just use the elim-variable 
+       directly
 
 Parsing interrupted due to:
-1 error(s), 0 warning(s).
+2 error(s), 0 warning(s).
 Let's learn from that.
 
 ImplicitTuplePat:

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

@@ -119,10 +119,15 @@ module Issue94 {
   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 }
+
+module Issue1212 {
+  open inductive IsZero Nat
+  | zero => ack
+  def matchElim : Fn (a : Nat) (b : Nat) -> IsZero a -> Nat => fn a b p => match elim a, b, p {
+  | zero, _, ack => 233
+  }
+  def irrefutable : Fn (a : Nat) -> IsZero a -> Nat => fn { zero, ack => 233 }
+}
 
 module Issue243 {
   open import data::vec using (Vec, [], :>)

parser/src/main/gen/org/aya/parser/AyaPsiElementTypes.java

@@ -1,3 +1,6 @@
+// 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.
+
 // This is a generated file. Not intended for manual editing.
 package org.aya.parser;
 
@@ -65,6 +68,7 @@ public interface AyaPsiElementTypes {
   IElementType LIT_INT_EXPR = new AyaPsiElementType("LIT_INT_EXPR");
   IElementType LIT_STRING_EXPR = new AyaPsiElementType("LIT_STRING_EXPR");
   IElementType LOOSERS = new AyaPsiElementType("LOOSERS");
+  IElementType MATCH_DISCR = new AyaPsiElementType("MATCH_DISCR");
   IElementType MATCH_EXPR = new AyaPsiElementType("MATCH_EXPR");
   IElementType MATCH_TYPE = new AyaPsiElementType("MATCH_TYPE");
   IElementType MEMBER_MODIFIER = new AyaPsiElementType("MEMBER_MODIFIER");

parser/src/main/gen/org/aya/parser/AyaPsiParser.java

@@ -1,3 +1,6 @@
+// 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.
+
 // This is a generated file. Not intended for manual editing.
 package org.aya.parser;
 
@@ -1399,37 +1402,56 @@ private static boolean loosers_1(PsiBuilder b, int l) {
   }
 
   /* ********************************************************** */
-  // (KW_AS <<commaSep weakId>>)? KW_RETURNS expr
-  public static boolean matchType(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "matchType")) return false;
-    if (!nextTokenIs(b, "<match type>", KW_AS, KW_RETURNS)) return false;
+  // KW_ELIM? expr (KW_AS weakId)?
+  public static boolean matchDiscr(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "matchDiscr")) return false;
     boolean r;
-    Marker m = enter_section_(b, l, _NONE_, MATCH_TYPE, "<match type>");
-    r = matchType_0(b, l + 1);
-    r = r && consumeToken(b, KW_RETURNS);
+    Marker m = enter_section_(b, l, _NONE_, MATCH_DISCR, "<match discr>");
+    r = matchDiscr_0(b, l + 1);
     r = r && expr(b, l + 1, -1);
+    r = r && matchDiscr_2(b, l + 1);
     exit_section_(b, l, m, r, false, null);
     return r;
   }
 
-  // (KW_AS <<commaSep weakId>>)?
-  private static boolean matchType_0(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "matchType_0")) return false;
-    matchType_0_0(b, l + 1);
+  // KW_ELIM?
+  private static boolean matchDiscr_0(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "matchDiscr_0")) return false;
+    consumeToken(b, KW_ELIM);
     return true;
   }
 
-  // KW_AS <<commaSep weakId>>
-  private static boolean matchType_0_0(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "matchType_0_0")) return false;
+  // (KW_AS weakId)?
+  private static boolean matchDiscr_2(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "matchDiscr_2")) return false;
+    matchDiscr_2_0(b, l + 1);
+    return true;
+  }
+
+  // KW_AS weakId
+  private static boolean matchDiscr_2_0(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "matchDiscr_2_0")) return false;
     boolean r;
     Marker m = enter_section_(b);
     r = consumeToken(b, KW_AS);
-    r = r && commaSep(b, l + 1, AyaPsiParser::weakId);
+    r = r && weakId(b, l + 1);
     exit_section_(b, m, null, r);
     return r;
   }
 
+  /* ********************************************************** */
+  // KW_RETURNS expr
+  public static boolean matchType(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "matchType")) return false;
+    if (!nextTokenIs(b, KW_RETURNS)) return false;
+    boolean r;
+    Marker m = enter_section_(b);
+    r = consumeToken(b, KW_RETURNS);
+    r = r && expr(b, l + 1, -1);
+    exit_section_(b, m, MATCH_TYPE, r);
+    return r;
+  }
+
   /* ********************************************************** */
   // KW_CLASSIFIYING | KW_OVERRIDE | KW_COERCE
   public static boolean memberModifier(PsiBuilder b, int l) {
@@ -2505,31 +2527,23 @@ private static boolean lambda2Expr_2(PsiBuilder b, int l) {
     return true;
   }
 
-  // KW_MATCH KW_ELIM? exprList matchType? clauses
+  // KW_MATCH <<commaSep matchDiscr>> matchType? clauses
   public static boolean matchExpr(PsiBuilder b, int l) {
     if (!recursion_guard_(b, l, "matchExpr")) return false;
     if (!nextTokenIsSmart(b, KW_MATCH)) return false;
     boolean r;
     Marker m = enter_section_(b);
     r = consumeTokenSmart(b, KW_MATCH);
-    r = r && matchExpr_1(b, l + 1);
-    r = r && exprList(b, l + 1);
-    r = r && matchExpr_3(b, l + 1);
+    r = r && commaSep(b, l + 1, AyaPsiParser::matchDiscr);
+    r = r && matchExpr_2(b, l + 1);
     r = r && clauses(b, l + 1);
     exit_section_(b, m, MATCH_EXPR, r);
     return r;
   }
 
-  // KW_ELIM?
-  private static boolean matchExpr_1(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "matchExpr_1")) return false;
-    consumeTokenSmart(b, KW_ELIM);
-    return true;
-  }
-
   // matchType?
-  private static boolean matchExpr_3(PsiBuilder b, int l) {
-    if (!recursion_guard_(b, l, "matchExpr_3")) return false;
+  private static boolean matchExpr_2(PsiBuilder b, int l) {
+    if (!recursion_guard_(b, l, "matchExpr_2")) return false;
     matchType(b, l + 1);
     return true;
   }

parser/src/main/grammar/AyaPsiParser.bnf

@@ -309,8 +309,9 @@ 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
+matchType ::= KW_RETURNS expr
+matchDiscr ::= KW_ELIM? expr (KW_AS weakId)?
+matchExpr ::= KW_MATCH <<commaSep matchDiscr>> matchType? clauses
 
 argument ::= atomExArgument
            | tupleImArgument