From 0ba21269e8f48f27633266bd67919f6517c1f50b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 31 Mar 2024 19:14:14 -0700 Subject: [PATCH] fix: matcher splitter is code (#3815) 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. --- src/Lean/Meta/Eqns.lean | 9 ++- src/Lean/Meta/Match/MatchEqs.lean | 116 ++++++++++++------------------ tests/lean/run/matchEqsBug.lean | 4 -- 3 files changed, 55 insertions(+), 74 deletions(-) diff --git a/src/Lean/Meta/Eqns.lean b/src/Lean/Meta/Eqns.lean index 7f65d689713c..c3ecc055c571 100644 --- a/src/Lean/Meta/Eqns.lean +++ b/src/Lean/Meta/Eqns.lean @@ -7,6 +7,7 @@ prelude import Lean.ReservedNameAction import Lean.Meta.Basic import Lean.Meta.AppBuilder +import Lean.Meta.Match.MatcherInfo namespace Lean.Meta /-- @@ -57,7 +58,13 @@ Ensures that `f.eq_def` and `f.eq_` are reserved names if `f` is a safe def -/ 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_.eq_` are private definitions and are not treated as reserved names + -- Reason: `f.match_.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 cf8f8a108c47..ac3ca09b3b33 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -649,13 +649,18 @@ where 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 @@ private partial def mkEquationsFor (matchDeclName : Name) : MetaM MatchEqns := 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 @@ def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do 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_.splitter` as a reserved name, but -we do not install a realizer. The `splitter` will be generated by the -`foo.match_.eq_` 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 7943c6e44210..4aa55ca9a6dc 100644 --- a/tests/lean/run/matchEqsBug.lean +++ b/tests/lean/run/matchEqsBug.lean @@ -26,10 +26,6 @@ set_option trace.Meta.Match.matchEqs true 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