diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index 3cb703f813..c5543df8d8 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -17,11 +17,6 @@ import Lean.Meta.Match.CaseValues namespace Lean.Meta.Match -structure DiscrInfo where - /-- `some h` if the discriminant is annotated with `h:` -/ - hName? : Option Name := none - deriving Inhabited - /-- The number of patterns in each AltLHS must be equal to the number of discriminants. -/ private def checkNumPatterns (numDiscrs : Nat) (lhss : List AltLHS) : MetaM Unit := do if lhss.any fun lhs => lhs.patterns.length != numDiscrs then @@ -784,6 +779,7 @@ where `v` is a universe parameter or 0 if `B[a_1, ..., a_n]` is a proposition. - def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := do let ⟨matcherName, matchType, discrInfos, lhss⟩ := input let numDiscrs := discrInfos.size + let numEqs := (discrInfos.filter fun info => info.hName?.isSome).size checkNumPatterns numDiscrs lhss forallBoundedTelescope matchType numDiscrs fun discrs matchTypeBody => do /- We generate an matcher that can eliminate using different motives with different universe levels. @@ -794,6 +790,7 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := do let uElimGen ← if uElim == levelZero then pure levelZero else mkFreshLevelMVar let mkMatcher (type val : Expr) (minors : Array (Expr × Nat)) (s : State) : MetaM MatcherResult := do trace[Meta.Match.debug] "matcher value: {val}\ntype: {type}" + trace[Meta.Match.debug] "minors num params: {minors.map (·.2)}" /- The option `bootstrap.gen_matcher_code` is a helper hack. It is useful, for example, for compiling `src/Init/Data/Int`. It is needed because the compiler uses `Int.decLt` for generating code for `Int.casesOn` applications, but `Int.casesOn` is used to @@ -812,12 +809,13 @@ def mkMatcher (input : MkMatcherInput) : MetaM MatcherResult := do discard <| isLevelDefEq uElimGen uElim let addMatcher := match addMatcher with - | some addMatcher => + | some addMatcher => addMatcher <| { numParams := matcher.getAppNumArgs - numDiscrs, - altNumParams := minors.map Prod.snd, - uElimPos? } - |> addMatcher + altNumParams := minors.map fun minor => minor.2 + numEqs + discrInfos + numDiscrs + uElimPos? + } | none => pure () trace[Meta.Match.debug] "matcher: {matcher}" diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean index c06a762635..da30ab3c0a 100644 --- a/src/Lean/Meta/Match/MatcherInfo.lean +++ b/src/Lean/Meta/Match/MatcherInfo.lean @@ -8,6 +8,11 @@ import Lean.Meta.Basic namespace Lean.Meta namespace Match +structure DiscrInfo where + /-- `some h` if the discriminant is annotated with `h:` -/ + hName? : Option Name := none + deriving Inhabited + /-- A "matcher" auxiliary declaration has the following structure: - `numParams` parameters @@ -18,10 +23,14 @@ A "matcher" auxiliary declaration has the following structure: `pos` is the position of the universe level parameter that specifies the elimination universe. It is `none` if the matcher only eliminates into `Prop`. -/ structure MatcherInfo where - numParams : Nat - numDiscrs : Nat + numParams : Nat + numDiscrs : Nat altNumParams : Array Nat - uElimPos? : Option Nat + uElimPos? : Option Nat + /-- + `discrInfos[i] = { hName? := some h }` if the i-th discriminant was annotated with `h :`. + -/ + discrInfos : Array DiscrInfo def MatcherInfo.numAlts (info : MatcherInfo) : Nat := info.altNumParams.size diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 254c7ffbab..1e3b9413a0 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -144,7 +144,7 @@ def matchAltExpr := matchAlt def matchAlts (rhsParser : Parser := termParser) : Parser := leading_parser withPosition $ many1Indent (ppLine >> matchAlt rhsParser) -def matchDiscr := leading_parser optional (atomic (ident >> ":")) >> termParser +def matchDiscr := leading_parser optional (atomic (ident >> " : ")) >> termParser def trueVal := leading_parser nonReservedSymbol "true" def falseVal := leading_parser nonReservedSymbol "false" diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 388264ca96..641d998556 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -383,27 +383,34 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat return { matcherTy := (← getConstInfo c).instantiateTypeLevelParams us, info := info : AppMatchState }) (fun st => do if st.params.size < st.info.numParams then - pure { st with params := st.params.push (← getExpr) } + return { st with params := st.params.push (← getExpr) } else if st.motive.isNone then - -- store motive argument separately - let lamMotive ← getExpr - let piMotive ← lambdaTelescope lamMotive fun xs body => mkForallFVars xs body - -- TODO: pp.analyze has not analyzed `piMotive`, only `lamMotive` - -- Thus the binder types won't have any annotations - let piStx ← withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab - let named ← getPPOption getPPAnalysisNamedArg - pure { st with motive := (piStx, lamMotive), motiveNamed := named } + -- store motive argument separately + let lamMotive ← getExpr + let piMotive ← lambdaTelescope lamMotive fun xs body => mkForallFVars xs body + -- TODO: pp.analyze has not analyzed `piMotive`, only `lamMotive` + -- Thus the binder types won't have any annotations + let piStx ← withTheReader SubExpr (fun cfg => { cfg with expr := piMotive }) delab + let named ← getPPOption getPPAnalysisNamedArg + return { st with motive := (piStx, lamMotive), motiveNamed := named } else if st.discrs.size < st.info.numDiscrs then - pure { st with discrs := st.discrs.push (← delab) } + let idx := st.discrs.size + let discr ← delab + if let some hName := st.info.discrInfos[idx].hName? then + -- TODO: we should check whether the corresponding binder name, matches `hName`. + -- If it does not we should pretty print this `match` as a regular application. + return { st with discrs := st.discrs.push (← `(matchDiscr| $(mkIdent hName):ident : $discr:term)) } + else + return { st with discrs := st.discrs.push (← `(matchDiscr| $discr:term)) } else if st.rhss.size < st.info.altNumParams.size then /- We save the variables names here to be able to implement safe_shadowing. The pattern delaboration must use the names saved here. -/ let (varNames, rhs) ← skippingBinders st.info.altNumParams[st.rhss.size] fun varNames => do let rhs ← delab return (varNames, rhs) - pure { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames } + return { st with rhss := st.rhss.push rhs, varNames := st.varNames.push varNames } else - pure { st with moreArgs := st.moreArgs.push (← delab) }) + return { st with moreArgs := st.moreArgs.push (← delab) }) if st.discrs.size < st.info.numDiscrs || st.rhss.size < st.info.altNumParams.size then -- underapplied @@ -421,9 +428,9 @@ def delabAppMatch : Delab := whenPPOption getPPNotation <| whenPPOption getPPMat let opts ← getOptions -- TODO: disable the match if other implicits are needed? if ← pure st.motiveNamed <||> shouldShowMotive lamMotive opts then - `(match (motive := $piStx) $[$st.discrs:term],* with $[| $pats,* => $st.rhss]*) + `(match (motive := $piStx) $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*) else - `(match $[$st.discrs:term],* with $[| $pats,* => $st.rhss]*) + `(match $[$st.discrs:matchDiscr],* with $[| $pats,* => $st.rhss]*) return Syntax.mkApp stx st.moreArgs /--