perf: match_expr join points

We use `let_delayed` to elaborate `match_expr` join points, which elaborate the body of the `let` before its value. Thus, there is a difference between: - `let_delayed f (x : Expr) := <val>; <body>` - `let_delayed f := fun (x : Expr) => <val>; <body>` In the latter, when `<body>` is elaborated, the elaborator does not know that `f` takes an argument of type `Expr`, and that `f` is a function. Before this commit ensures the former representation is used.
2026-03-19 19:34:13 +00:00 · 2024-03-03 09:52:57 -08:00
2 changed files with 69 additions and 6 deletions
--- a/src/Lean/Elab/MatchExpr.lean
+++ b/src/Lean/Elab/MatchExpr.lean
@@ -122,15 +122,15 @@ def initK (alt : Alt) : MacroM Alt := withFreshMacroScope do
 Generates parameters for the continuation function used to execute
 the RHS of the given alternative.
 -/
-def getParams (alt : Alt) : MacroM (Array Term) := do
+def getParams (alt : Alt) : MacroM (Array (TSyntax ``bracketedBinder)) := do
  let mut params := #[]
  if let some var := alt.var? then
-    params := params.push (← `(($var : Expr)))
+    params := params.push (← `(bracketedBinderF| ($var : Expr)))
  params := params ++ (← alt.pvars.toArray.reverse.filterMapM fun
    | none => return none
-    | some arg => return some (← `(($arg : Expr))))
+    | some arg => return some (← `(bracketedBinderF| ($arg : Expr))))
  if params.isEmpty then
-    return #[(← `(_))]
+    return #[(← `(bracketedBinderF| (_ : Unit)))]
  return params

 /--
@@ -182,10 +182,10 @@ partial def generate (discr : Term) (alts : List Alt) (elseAlt : ElseAlt) : Macr
        result ← `(if ($discr).isConstOf $(toDoubleQuotedName funName) then $alt.k $actuals* else $result)
    return result
  let body ← loop discr' alts
-  let mut result ← `(let_delayed __do_jp := fun (_ : Unit) => $(⟨elseAlt.rhs⟩):term; let __discr := Expr.cleanupAnnotations $discr:term; $body:term)
+  let mut result ← `(let_delayed __do_jp (_ : Unit) := $(⟨elseAlt.rhs⟩):term; let __discr := Expr.cleanupAnnotations $discr:term; $body:term)
  for alt in alts do
    let params ← getParams alt
-    result ← `(let_delayed $alt.k:ident := fun $params:term* => $(⟨alt.rhs⟩):term; $result:term)
+    result ← `(let_delayed $alt.k:ident $params:bracketedBinder* := $(⟨alt.rhs⟩):term; $result:term)
  return result

 def main (discr : Term) (alts : Array Syntax) (elseAlt : Syntax) : MacroM Syntax := do
--- a/tests/lean/run/match_expr_perf.lean
+++ b/tests/lean/run/match_expr_perf.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+prelude
+import Lean.Elab.Tactic.Omega.Core
+import Lean.Elab.Tactic.FalseOrByContra
+import Lean.Meta.Tactic.Cases
+import Lean.Elab.Tactic.Config
+
+open Lean Meta Omega
+
+set_option maxHeartbeats 5000
+def pushNot (h P : Expr) : MetaM (Option Expr) := do
+  let P ← whnfR P
+  trace[omega] "pushing negation: {P}"
+  match P with
+  | .forallE _ t b _ =>
+    if (← isProp t) && (← isProp b) then
+     return some (mkApp4 (.const ``Decidable.and_not_of_not_imp []) t b
+      (.app (.const ``Classical.propDecidable []) t) h)
+    else
+      return none
+  | .app _ _ =>
+    match_expr P with
+    | LT.lt α _ x y => match_expr α with
+      | Nat => return some (mkApp3 (.const ``Nat.le_of_not_lt []) x y h)
+      | Int => return some (mkApp3 (.const ``Int.le_of_not_lt []) x y h)
+      | Fin n => return some (mkApp4 (.const ``Fin.le_of_not_lt []) n x y h)
+      | _ => return none
+    | LE.le α _ x y => match_expr α with
+      | Nat => return some (mkApp3 (.const ``Nat.lt_of_not_le []) x y h)
+      | Int => return some (mkApp3 (.const ``Int.lt_of_not_le []) x y h)
+      | Fin n => return some (mkApp4 (.const ``Fin.lt_of_not_le []) n x y h)
+      | _ => return none
+    | Eq α x y => match_expr α with
+      | Nat => return some (mkApp3 (.const ``Nat.lt_or_gt_of_ne []) x y h)
+      | Int => return some (mkApp3 (.const ``Int.lt_or_gt_of_ne []) x y h)
+      | Fin n => return some (mkApp4 (.const ``Fin.lt_or_gt_of_ne []) n x y h)
+      | _ => return none
+    | Dvd.dvd α _ k x => match_expr α with
+      | Nat => return some (mkApp3 (.const ``Nat.emod_pos_of_not_dvd []) k x h)
+      | Int =>
+        -- This introduces a disjunction that could be avoided by checking `k ≠ 0`.
+        return some (mkApp3 (.const ``Int.emod_pos_of_not_dvd []) k x h)
+      | _ => return none
+    | Prod.Lex _ _ _ _ _ _ => return some (← mkAppM ``Prod.of_not_lex #[h])
+    | Not P =>
+      return some (mkApp3 (.const ``Decidable.of_not_not []) P
+        (.app (.const ``Classical.propDecidable []) P) h)
+    | And P Q =>
+      return some (mkApp5 (.const ``Decidable.or_not_not_of_not_and []) P Q
+        (.app (.const ``Classical.propDecidable []) P)
+        (.app (.const ``Classical.propDecidable []) Q) h)
+    | Or P Q =>
+      return some (mkApp3 (.const ``and_not_not_of_not_or []) P Q h)
+    | Iff P Q =>
+      return some (mkApp5 (.const ``Decidable.and_not_or_not_and_of_not_iff []) P Q
+        (.app (.const ``Classical.propDecidable []) P)
+        (.app (.const ``Classical.propDecidable []) Q) h)
+    | _ => return none
+  | _ => return none