From cf030a16348481c18f6c09fcd77c851bf7dff443 Mon Sep 17 00:00:00 2001
From: Daniel Fabian <daniel.fabian@integral-it.ch>
Date: Tue, 18 May 2021 03:23:31 +0000
Subject: [PATCH] refactor: Add `MkMatcherInput`.

Since we are going to make `mkMatcher` reversible, it's quite useful to have the input be a `structure`. This way we make sure, that the inverse function always returns the same type as `mkMatcher` needs as input.
---
 src/Lean/Elab/Match.lean       |  6 +++---
 src/Lean/Meta/Match/Match.lean | 10 +++++++++-
 tests/lean/run/depElim1.lean   |  2 +-
 3 files changed, 13 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index 9596f7727f..9a0c6bb3d7 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -941,8 +941,8 @@ where
     let wildcards := mkArray num hole
     return altViews.map fun altView => { altView with patterns := wildcards ++ altView.patterns }
 
-def mkMatcher (elimName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss : List AltLHS) : TermElabM MatcherResult :=
-  Meta.Match.mkMatcher elimName matchType numDiscrs lhss
+def mkMatcher (input : Meta.Match.MkMatcherInput) : TermElabM MatcherResult :=
+  Meta.Match.mkMatcher input
 
 register_builtin_option match.ignoreUnusedAlts : Bool := {
   defValue := false
@@ -1044,7 +1044,7 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax
   else
     let numDiscrs := discrs.size
     let matcherName ← mkAuxName `match
-    let matcherResult ← mkMatcher matcherName matchType numDiscrs altLHSS
+    let matcherResult ← mkMatcher { matcherName, matchType, numDiscrs, lhss := altLHSS }
     let motive ← forallBoundedTelescope matchType numDiscrs fun xs matchType => mkLambdaFVars xs matchType
     reportMatcherResultErrors altLHSS matcherResult
     let r := mkApp matcherResult.matcher motive
diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean
index 7963a4ac37..8de65a6c62 100644
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -700,6 +700,13 @@ def mkMatcherAuxDefinition (name : Name) (type : Expr) (value : Expr) : MetaM (B
     modifyEnv fun env => matcherExt.modifyState env fun s => s.insert (result.value, compile) name
     return (true, mkAppN (mkConst name result.levelArgs.toList) result.exprArgs)
 
+
+structure MkMatcherInput where
+  matcherName : Name 
+  matchType : Expr
+  numDiscrs : Nat
+  lhss : List Match.AltLHS
+
 /-
 Create a dependent matcher for `matchType` where `matchType` is of the form
 `(a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> B[a_1, ..., a_n]`
@@ -709,7 +716,8 @@ The number of patterns must be the same in each `AltLHS`.
 The generated matcher has the structure described at `MatcherInfo`. The motive argument is of the form
 `(motive : (a_1 : A_1) -> (a_2 : A_2[a_1]) -> ... -> (a_n : A_n[a_1, a_2, ... a_{n-1}]) -> Sort v)`
 where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition. -/
-def mkMatcher (matcherName : Name) (matchType : Expr) (numDiscrs : Nat) (lhss : List AltLHS) : MetaM MatcherResult :=
+def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult :=
+  let ⟨matcherName, matchType, numDiscrs, lhss⟩ := input
   forallBoundedTelescope matchType numDiscrs fun majors matchTypeBody => do
   checkNumPatterns majors lhss
   /- We generate an matcher that can eliminate using different motives with different universe levels.
diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean
index 27127e3ded..017b370f62 100644
--- a/tests/lean/run/depElim1.lean
+++ b/tests/lean/run/depElim1.lean
@@ -160,7 +160,7 @@ def mkTester (elimName : Name) (majors : List Expr) (lhss : List AltLHS) (inProp
 generalizeTelescope majors.toArray fun majors => do
   let resultType := if inProp then mkConst `True /- some proposition -/ else mkConst `Nat
   let matchType ← mkForallFVars majors resultType
-  Match.mkMatcher elimName matchType majors.size lhss
+  Match.mkMatcher { matcherName := elimName, matchType, numDiscrs := majors.size, lhss }
 
 def test (ex : Name) (numPats : Nat) (elimName : Name) (inProp : Bool := false) : MetaM Unit :=
 withDepElimFrom ex numPats fun majors alts => do