diff --git a/src/Lean/Elab/BindersUtil.lean b/src/Lean/Elab/BindersUtil.lean index 4aecae981c..eb022743f0 100644 --- a/src/Lean/Elab/BindersUtil.lean +++ b/src/Lean/Elab/BindersUtil.lean @@ -30,25 +30,25 @@ def getMatchAltsNumPatterns (matchAlts : Syntax) : Nat := /-- Expand a match alternative such as `| 0 | 1 => rhs` to an array containing `| 0 => rhs` and `| 1 => rhs`. -/ -def expandMatchAlt (stx : Syntax) : MacroM (Array Syntax) := - match stx with - | `(matchAltExpr| | $[$patss]|* => $rhs) => - if patss.size ≤ 1 then - return #[stx] - else - patss.mapM fun pats => let pats := #[pats]; `(matchAltExpr| | $[$pats]|* => $rhs) - | _ => return #[stx] +def expandMatchAlt (matchAlt : Syntax) : Array Syntax := + let patss := matchAlt[1] + let rhs := matchAlt[3] + if patss.getArgs.size ≤ 1 then + #[matchAlt] + else + patss.getSepArgs.map fun pats => + let patss := mkNullNode #[pats] + matchAlt.setArg 1 patss def shouldExpandMatchAlt (matchAlt : Syntax) : Bool := - match matchAlt with - | `(matchAltExpr| | $[$patss]|* => $rhs) => patss.size > 1 - | _ => false + let patss := matchAlt[1] + patss.getArgs.size > 1 def expandMatchAlts? (stx : Syntax) : MacroM (Option Syntax) := do match stx with | `(match $[$gen]? $[$motive]? $discrs,* with $alts:matchAlt*) => if alts.any shouldExpandMatchAlt then - let alts ← alts.foldlM (init := #[]) fun alts alt => return alts ++ (← expandMatchAlt alt) + let alts := alts.foldl (init := #[]) fun alts alt => alts ++ expandMatchAlt alt `(match $[$gen]? $[$motive]? $discrs,* with $alts:matchAlt*) else return none diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 30c4a06a60..f9553235d7 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -1460,7 +1460,7 @@ mutual let optMotive := doMatch[2] let discrs := doMatch[3] let matchAlts := doMatch[5][0].getArgs -- Array of `doMatchAlt` - let matchAlts ← matchAlts.foldlM (init := #[]) fun result matchAlt => return result ++ (← liftMacroM <| expandMatchAlt matchAlt) + let matchAlts := matchAlts.foldl (init := #[]) fun result matchAlt => result ++ expandMatchAlt matchAlt let alts ← matchAlts.mapM fun matchAlt => do let patterns := matchAlt[1][0] let vars ← getPatternsVarsEx patterns.getSepArgs diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index abeeccc7da..4311757942 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -1256,7 +1256,7 @@ enforce this. -/ where elabMatchDefault (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do match (← liftMacroM <| expandMatchAlts? stx) with - | some stxNew => withMacroExpansion stx stxNew <| elabTerm stxNew expectedType? + | some stxNew => trace[Meta.debug] "expanded alts"; withMacroExpansion stx stxNew <| elabTerm stxNew expectedType? | none => match (← expandNonAtomicDiscrs? stx) with | some stxNew => withMacroExpansion stx stxNew <| elabTerm stxNew expectedType? diff --git a/tests/lean/matchOrIssue.lean b/tests/lean/matchOrIssue.lean new file mode 100644 index 0000000000..fd39f7cdf0 --- /dev/null +++ b/tests/lean/matchOrIssue.lean @@ -0,0 +1,18 @@ +inductive A : Type +| ctor : A → A +| inh + +-- set_option trace.Elab true in +def f : A → A → Bool +| banana, a b | _, lol how => 1 + "test" + f1 -- Error +| _, _ => false + + +def g : A → A → Bool +| A.inh, _ | _, A.inh => true +| _, _ => false + +example : g .inh (.ctor a) = true := rfl +example : g .inh .inh = true := rfl +example : g (.ctor a) .inh = true := rfl +example : g (.ctor a) (.ctor b) = false := rfl diff --git a/tests/lean/matchOrIssue.lean.expected.out b/tests/lean/matchOrIssue.lean.expected.out new file mode 100644 index 0000000000..20bf424518 --- /dev/null +++ b/tests/lean/matchOrIssue.lean.expected.out @@ -0,0 +1 @@ +matchOrIssue.lean:7:10-7:13: error: invalid pattern, constructor or constant marked with '[matchPattern]' expected