fix: matcher splitter is code It have to keep it as a private definition for now. We currently only support duplicate theorems in different modules. Splitters are generated on demand, and are also used to write code.
diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean index 7f65d68..c3ecc05 100644 --- a/src/Lean/Meta/Eqns.lean +++ b/src/Lean/Meta/Eqns.lean
@@ -7,6 +7,7 @@ import Lean.ReservedNameAction import Lean.Meta.Basic import Lean.Meta.AppBuilder +import Lean.Meta.Match.MatcherInfo namespace Lean.Meta /-- @@ -57,7 +58,13 @@ -/ builtin_initialize registerReservedNamePredicate fun env n => match n with - | .str p s => (isEqnReservedNameSuffix s || isUnfoldReservedNameSuffix s) && env.isSafeDefinition p + | .str p s => + (isEqnReservedNameSuffix s || isUnfoldReservedNameSuffix s) + && env.isSafeDefinition p + -- Remark: `f.match_<idx>.eq_<idx>` are private definitions and are not treated as reserved names + -- Reason: `f.match_<idx>.splitter is generated at the same time, and can eliminate into type. + -- Thus, it cannot be defined in different modules since it is not a theorem, and is used to generate code. + && !isMatcherCore env p | _ => false def GetEqnsFn := Name → MetaM (Option (Array Name))
diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index cf8f8a1..ac3ca09 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean
@@ -649,13 +649,18 @@ private partial def mkEquationsFor (matchDeclName : Name) : MetaM MatchEqns := withLCtx {} {} do trace[Meta.Match.matchEqs] "mkEquationsFor '{matchDeclName}'" withConfig (fun c => { c with etaStruct := .none }) do - let baseName := matchDeclName + /- + Remark: user have requested the `split` tactic to be available for writing code. + Thus, the `splitter` declaration must be a definition instead of a theorem. + Moreover, the `splitter` is generated on demand, and we currently + can't import the same definition from different modules. Thus, we must + keep `splitter` as a private declaration to prevent import failures. + -/ + let baseName := mkPrivateName (← getEnv) matchDeclName let splitterName := baseName ++ `splitter let constInfo ← getConstInfo matchDeclName let us := constInfo.levelParams.map mkLevelParam let some matchInfo ← getMatcherInfo? matchDeclName | throwError "'{matchDeclName}' is not a matcher function" - -- `alreadyDeclared` is `true` if matcher equations were defined in an imported module - let alreadyDeclared := (← getEnv).contains splitterName let numDiscrEqs := getNumEqsFromDiscrInfos matchInfo.discrInfos forallTelescopeReducing constInfo.type fun xs matchResultType => do let mut eqnNames := #[] @@ -690,59 +695,51 @@ for discr in discrs.toArray.reverse, pattern in patterns.reverse do notAlt ← mkArrow (← mkEqHEq discr pattern) notAlt notAlt ← mkForallFVars (discrs ++ ys) notAlt - if alreadyDeclared then - -- If the matcher equations and splitter have already been declared, the only - -- values we are `notAlt` and `splitterAltNumParam`. This code is a bit hackish. - return (notAlt, default, splitterAltNumParam, default) - else - /- Recall that when we use the `h : discr`, the alternative type depends on the discriminant. - Thus, we need to create new `alts`. -/ - withNewAlts numDiscrEqs discrs patterns alts fun alts => do - let alt := alts[i]! - let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts) - let rhs := mkAppN alt rhsArgs - let thmType ← mkEq lhs rhs - let thmType ← hs.foldrM (init := thmType) (mkArrow · ·) - let thmType ← mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType - let thmType ← unfoldNamedPattern thmType - let thmVal ← proveCondEqThm matchDeclName thmType - addDecl <| Declaration.thmDecl { - name := thmName - levelParams := constInfo.levelParams - type := thmType - value := thmVal - } - return (notAlt, splitterAltType, splitterAltNumParam, argMask) + /- Recall that when we use the `h : discr`, the alternative type depends on the discriminant. + Thus, we need to create new `alts`. -/ + withNewAlts numDiscrEqs discrs patterns alts fun alts => do + let alt := alts[i]! + let lhs := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ patterns ++ alts) + let rhs := mkAppN alt rhsArgs + let thmType ← mkEq lhs rhs + let thmType ← hs.foldrM (init := thmType) (mkArrow · ·) + let thmType ← mkForallFVars (params ++ #[motive] ++ ys ++ alts) thmType + let thmType ← unfoldNamedPattern thmType + let thmVal ← proveCondEqThm matchDeclName thmType + addDecl <| Declaration.thmDecl { + name := thmName + levelParams := constInfo.levelParams + type := thmType + value := thmVal + } + return (notAlt, splitterAltType, splitterAltNumParam, argMask) notAlts := notAlts.push notAlt splitterAltTypes := splitterAltTypes.push splitterAltType splitterAltNumParams := splitterAltNumParams.push splitterAltNumParam altArgMasks := altArgMasks.push argMask trace[Meta.Match.matchEqs] "splitterAltType: {splitterAltType}" idx := idx + 1 - if alreadyDeclared then - return { eqnNames, splitterName, splitterAltNumParams } - else - -- Define splitter with conditional/refined alternatives - withSplitterAlts splitterAltTypes fun altsNew => do - let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew - let splitterType ← mkForallFVars splitterParams matchResultType - trace[Meta.Match.matchEqs] "splitterType: {splitterType}" - let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts) - let template ← deltaExpand template (· == constInfo.name) - let template := template.headBeta - let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltNumParams altArgMasks) - addAndCompile <| Declaration.defnDecl { - name := splitterName - levelParams := constInfo.levelParams - type := splitterType - value := splitterVal - hints := .abbrev - safety := .safe - } - setInlineAttribute splitterName - let result := { eqnNames, splitterName, splitterAltNumParams } - registerMatchEqns matchDeclName result - return result + -- Define splitter with conditional/refined alternatives + withSplitterAlts splitterAltTypes fun altsNew => do + let splitterParams := params.toArray ++ #[motive] ++ discrs.toArray ++ altsNew + let splitterType ← mkForallFVars splitterParams matchResultType + trace[Meta.Match.matchEqs] "splitterType: {splitterType}" + let template := mkAppN (mkConst constInfo.name us) (params ++ #[motive] ++ discrs ++ alts) + let template ← deltaExpand template (· == constInfo.name) + let template := template.headBeta + let splitterVal ← mkLambdaFVars splitterParams (← mkSplitterProof matchDeclName template alts altsNew splitterAltNumParams altArgMasks) + addAndCompile <| Declaration.defnDecl { + name := splitterName + levelParams := constInfo.levelParams + type := splitterType + value := splitterVal + hints := .abbrev + safety := .safe + } + setInlineAttribute splitterName + let result := { eqnNames, splitterName, splitterAltNumParams } + registerMatchEqns matchDeclName result + return result /- See header at `MatchEqsExt.lean` -/ @[export lean_get_match_equations_for] @@ -753,23 +750,4 @@ builtin_initialize registerTraceClass `Meta.Match.matchEqs -private def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do - unless (← isMatcher declName) do - return none - let result ← getEquationsForImpl declName - return some result.eqnNames - -builtin_initialize - registerGetEqnsFn getEqnsFor? - -/- -We register `foo.match_<idx>.splitter` as a reserved name, but -we do not install a realizer. The `splitter` will be generated by the -`foo.match_<idx>.eq_<idx>` realizer. --/ -builtin_initialize registerReservedNamePredicate fun env n => - match n with - | .str p "splitter" => isMatcherCore env p - | _ => false - end Lean.Meta.Match
diff --git a/tests/lean/run/matchEqsBug.lean b/tests/lean/run/matchEqsBug.lean index 7943c6e..4aa55ca 100644 --- a/tests/lean/run/matchEqsBug.lean +++ b/tests/lean/run/matchEqsBug.lean
@@ -26,10 +26,6 @@ test% f.match_1 #check f.match_1.splitter -/-- -error: 'g.match_1.splitter' is a reserved name --/ -#guard_msgs (error) in def g.match_1.splitter := 4 test% g.match_1