max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Meta
History
Joachim Breitner d41f39fb10
perf: sparse case splitting in match compilation (#10823) 
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
```
2025-11-06 13:46:35 +00:00
..
ArgsPacker refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Constructions feat: sparse casesOn constructions (#11072) 2025-11-05 15:49:11 +00:00
Match perf: sparse case splitting in match compilation (#10823) 2025-11-06 13:46:35 +00:00
Tactic perf: sparse case splitting in match compilation (#10823) 2025-11-06 13:46:35 +00:00
AbstractMVars.lean fix: instantiate mvars in types of mvars in abstractMVars (#10612) 2025-09-29 16:33:10 +00:00
AbstractNestedProofs.lean chore: more module system fixes and improvements from Mathlib porting (#10655) 2025-10-08 11:30:09 +00:00
ACLt.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
AppBuilder.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
ArgsPacker.lean feat: Add List.zipWithM and Array.zipWithM (#9528) 2025-07-28 08:39:52 +00:00
Basic.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
BinderNameHint.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Canonicalizer.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
CasesInfo.lean feat: sparse casesOn constructions (#11072) 2025-11-05 15:49:11 +00:00
Check.lean fix: deep recursion type checking grind proof (#11061) 2025-11-02 19:43:48 +00:00
CheckTactic.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Closure.lean chore: add an assertion about mkValueTypeClosure (#10954) 2025-10-25 12:59:17 +00:00
Coe.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
CoeAttr.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
CollectFVars.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
CollectMVars.lean feat: split out Expr.getMVarDependencies from MVarId.getMVarDependencies (#9785) 2025-08-08 00:28:30 +00:00
CompletionName.lean refactor: move operations on String.Pos.Raw to the String.Pos.Raw namespace (#10735) 2025-10-18 12:12:55 +00:00
CongrTheorems.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Constructions.lean feat: sparse casesOn constructions (#11072) 2025-11-05 15:49:11 +00:00
CtorRecognizer.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
DecLevel.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Diagnostics.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
DiscrTree.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
DiscrTreeTypes.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Eqns.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Eval.lean fix: #guard should work with the module system (#10535) 2025-09-24 07:38:10 +00:00
ExprDefEq.lean chore: use String.ofList instead of String.mk in elaborator+kernel (#11048) 2025-11-01 14:44:16 +00:00
ExprLens.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
ExprTraverse.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
ForEachExpr.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
FunInfo.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
GeneralizeTelescope.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
GeneralizeVars.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
GetUnfoldableConst.lean feat: list definitions in defeq problems that could not be unfolded for lack of @[expose] (#10158) 2025-09-23 16:13:39 +00:00
GlobalInstances.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Hint.lean refactor: use String.ofList and String.toList for String <-> List Char conversion (#11017) 2025-10-31 14:41:23 +00:00
IndPredBelow.lean fix: complete overhaul of structural recursion on inductives predicates (#9995) 2025-09-01 08:17:58 +00:00
Inductive.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
InferType.lean feat: don't count symbols in instances and proofs 2025-10-26 10:29:47 +11:00
Injective.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Instances.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
IntInstTesters.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
Iterator.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
KAbstract.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
KExprMap.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
LazyDiscrTree.lean fix: check that compiler does not infer inconsistent types between modules (#10418) 2025-09-19 12:36:47 +00:00
LetToHave.lean chore: fix spelling errors (#10042) 2025-08-22 07:23:12 +00:00
LevelDefEq.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
LitValues.lean feat: support for Rat scientific literals (#10961) 2025-10-26 02:05:26 +00:00
Match.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
MatchUtil.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
MethodSpecs.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
MkIffOfInductiveProp.lean chore: minor optimizations on the critical path (#10900) 2025-10-22 19:32:26 +00:00
NatInstTesters.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
NatTable.lean chore: fix spelling errors (#10042) 2025-08-22 07:23:12 +00:00
Offset.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Order.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
PPGoal.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
PProdN.lean fix: complete overhaul of structural recursion on inductives predicates (#9995) 2025-09-01 08:17:58 +00:00
RecursorInfo.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Reduce.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
ReduceEval.lean feat: upstream ReduceEval instances from quote4 (#10563) 2025-09-26 04:02:55 +00:00
SameCtorUtils.lean refactor: introduce SameCtorUtils (#10316) 2025-09-10 14:32:58 +00:00
SizeOf.lean fix: run enableRealizationsForConst on sizeOf decls (#10944) 2025-10-24 16:15:38 +00:00
Sorry.lean feat: pretty print sorry in "declaration uses 'sorry'" (#10034) 2025-09-08 12:14:42 +00:00
Structure.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
SynthInstance.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Tactic.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Transform.lean fix: unfold more auxillary theorems in termination checking (#10733) 2025-10-10 11:09:28 +00:00
TransparencyMode.lean refactor: module-ize Lean (#9330) 2025-07-25 12:02:51 +00:00
TryThis.lean chore: rename String.Range to Lean.Syntax.Range (#10852) 2025-10-21 07:32:25 +00:00
UnificationHint.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
WHNF.lean feat: sparse casesOn constructions (#11072) 2025-11-05 15:49:11 +00:00