d41f39fb10
This PR lets the match compilation procedure use sparse case analysis when the patterns only match on some but not all constructors of an inductive type. This way, less code is produce. Before, code handling each of the other cases was then optimized and commoned-up by later compilation pipeline, but that is wasteful to do. In some cases this will prevent Lean from noticing that a match statement is complete because it performs less case-splitting for the unreachable case. In this case, give explicit patterns to perform the deeper split with `by contradiction` as the right-hand side. At least temporarily, there is also the option to disable this behaviour with ``` set_option backwards.match.sparseCases false ```
83 lines
3.2 KiB
Text
83 lines
3.2 KiB
Text
import Lean
|
|
open Lean Expr Level -- just for shorter outpt
|
|
|
|
-- set_option trace.Meta.Match.match true
|
|
-- set_option trace.Meta.Match.debug true
|
|
-- set_option trace.Meta.Tactic.induction true
|
|
|
|
def simple : Lean.Expr → Bool
|
|
| .sort _ => true
|
|
| _ => false
|
|
|
|
def expensive : Lean.Expr → Lean.Expr → Bool
|
|
| .app (.app (.sort 1) (.sort 1)) (.sort 1), .app (.app (.sort 1) (.sort 1)) (.sort 1) => false
|
|
| _, _ => true
|
|
|
|
/-- info: false -/
|
|
#guard_msgs in
|
|
#eval expensive (.app (.app (.sort 1) (.sort 1)) (.sort 1)) (.app (.app (.sort 1) (.sort 1)) (.sort 1))
|
|
|
|
/-- info: true -/
|
|
#guard_msgs in
|
|
#eval expensive (.app (.app (.sort 2) (.sort 1)) (.sort 1)) (.app (.app (.sort 1) (.sort 1)) (.sort 1))
|
|
|
|
example : expensive (.app (.app (.sort 1) (.sort 1)) (.sort 1)) (.app (.app (.sort 1) (.sort 1)) (.sort 1)) = false := rfl
|
|
example : expensive (.app (.app (.sort 2) (.sort 1)) (.sort 1)) (.app (.app (.sort 1) (.sort 1)) (.sort 1)) = true := rfl
|
|
|
|
/--
|
|
info: expensive.match_1.{u_1} (motive : Expr → Expr → Sort u_1) (x✝ x✝¹ : Expr)
|
|
(h_1 :
|
|
Unit →
|
|
motive (((sort zero.succ).app (sort zero.succ)).app (sort zero.succ))
|
|
(((sort zero.succ).app (sort zero.succ)).app (sort zero.succ)))
|
|
(h_2 : (x x_1 : Expr) → motive x x_1) : motive x✝ x✝¹
|
|
-/
|
|
#guard_msgs in
|
|
#check expensive.match_1
|
|
/--
|
|
info: expensive.match_1.splitter.{u_1} (motive : Expr → Expr → Sort u_1) (x✝ x✝¹ : Expr)
|
|
(h_1 :
|
|
motive (((sort zero.succ).app (sort zero.succ)).app (sort zero.succ))
|
|
(((sort zero.succ).app (sort zero.succ)).app (sort zero.succ)))
|
|
(h_2 :
|
|
(x x_1 : Expr) →
|
|
(x = ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) →
|
|
x_1 = ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) → False) →
|
|
motive x x_1) :
|
|
motive x✝ x✝¹
|
|
-/
|
|
#guard_msgs in
|
|
#check expensive.match_1.splitter
|
|
/--
|
|
info: expensive.match_1.eq_1.{u_1} (motive : Expr → Expr → Sort u_1)
|
|
(h_1 :
|
|
Unit →
|
|
motive (((sort zero.succ).app (sort zero.succ)).app (sort zero.succ))
|
|
(((sort zero.succ).app (sort zero.succ)).app (sort zero.succ)))
|
|
(h_2 : (x x_1 : Expr) → motive x x_1) :
|
|
(match ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ),
|
|
((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) with
|
|
| ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ),
|
|
((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) => h_1 ()
|
|
| x, x_1 => h_2 x x_1) =
|
|
h_1 ()
|
|
-/
|
|
#guard_msgs in
|
|
#check expensive.match_1.eq_1
|
|
/--
|
|
info: expensive.match_1.eq_2.{u_1} (motive : Expr → Expr → Sort u_1) (x✝ x✝¹ : Expr)
|
|
(h_1 :
|
|
Unit →
|
|
motive (((sort zero.succ).app (sort zero.succ)).app (sort zero.succ))
|
|
(((sort zero.succ).app (sort zero.succ)).app (sort zero.succ)))
|
|
(h_2 : (x x_1 : Expr) → motive x x_1) :
|
|
(x✝ = ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) →
|
|
x✝¹ = ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) → False) →
|
|
(match x✝, x✝¹ with
|
|
| ((sort zero.succ).app (sort zero.succ)).app (sort zero.succ),
|
|
((sort zero.succ).app (sort zero.succ)).app (sort zero.succ) => h_1 ()
|
|
| x, x_1 => h_2 x x_1) =
|
|
h_2 x✝ x✝¹
|
|
-/
|
|
#guard_msgs in
|
|
#check expensive.match_1.eq_2
|