From b27ab5e25d994cfa3dc761907b5b3e56ca413ef2 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Thu, 22 Feb 2024 17:16:26 +0100 Subject: [PATCH] refactor: module MatcherApp.Transform (#3439) PR #3432 will introduce more operations on `MatcherApp`, including somet that have more dependencies. This change prepares by introducing `Lean.Meta.Match.MatcherApp.Basic` for the basic definition, and `Lean.Meta.MatcherApp.Transform` for the transformations, currently `addArg` and `refineThrough`, but more to come. --- .../Elab/PreDefinition/Structural/BRecOn.lean | 2 +- .../Structural/SmartUnfolding.lean | 1 + src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 2 +- src/Lean/Meta/Match/Match.lean | 144 +--------------- src/Lean/Meta/Match/MatcherApp.lean | 8 + src/Lean/Meta/Match/MatcherApp/Basic.lean | 80 +++++++++ src/Lean/Meta/Match/MatcherApp/Transform.lean | 159 ++++++++++++++++++ src/Lean/Meta/Match/MatcherInfo.lean | 69 -------- src/Lean/Meta/Tactic/Split.lean | 1 + 9 files changed, 252 insertions(+), 214 deletions(-) create mode 100644 src/Lean/Meta/Match/MatcherApp.lean create mode 100644 src/Lean/Meta/Match/MatcherApp/Basic.lean create mode 100644 src/Lean/Meta/Match/MatcherApp/Transform.lean diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index 6146af3670..122e0a4db0 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura -/ prelude import Lean.Util.HasConstCache -import Lean.Meta.Match.Match +import Lean.Meta.Match.MatcherApp.Transform import Lean.Elab.RecAppSyntax import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.Structural.Basic diff --git a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean index 05269edb42..9c322f7215 100644 --- a/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean +++ b/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura prelude import Lean.Elab.PreDefinition.Basic import Lean.Elab.PreDefinition.Structural.Basic +import Lean.Meta.Match.MatcherApp.Basic namespace Lean.Elab.Structural open Meta diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index e06f0ab626..523ba0db00 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -5,7 +5,7 @@ Authors: Joachim Breitner -/ prelude import Lean.Util.HasConstCache -import Lean.Meta.Match.Match +import Lean.Meta.Match.MatcherApp.Transform import Lean.Meta.Tactic.Cleanup import Lean.Meta.Tactic.Refl import Lean.Elab.Quotation diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index e3cdc9259c..99f73f2deb 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -10,6 +10,7 @@ import Lean.Meta.Tactic.Cases import Lean.Meta.Tactic.Contradiction import Lean.Meta.GeneralizeTelescope import Lean.Meta.Match.Basic +import Lean.Meta.Match.MatcherApp.Basic namespace Lean.Meta.Match @@ -889,149 +890,6 @@ def withMkMatcherInput (matcherName : Name) (k : MkMatcherInput → MetaM α) : end Match -/-- Auxiliary function for MatcherApp.addArg -/ -private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNumParams : Array Nat) (alts : Array Expr) (refined : Bool) (i : Nat) : MetaM (Array Nat × Array Expr) := do - if h : i < alts.size then - let alt := alts.get ⟨i, h⟩ - let numParams := altNumParams[i]! - let typeNew ← whnfD typeNew - match typeNew with - | Expr.forallE _ d b _ => - let (alt, refined) ← forallBoundedTelescope d (some numParams) fun xs d => do - let alt ← try instantiateLambda alt xs catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative" - forallBoundedTelescope d (some 1) fun x _ => do - let alt ← mkLambdaFVars x alt -- x is the new argument we are adding to the alternative - let refined := if refined then refined else - !(← isDefEq unrefinedArgType (← inferType x[0]!)) - return (← mkLambdaFVars xs alt, refined) - updateAlts unrefinedArgType (b.instantiate1 alt) (altNumParams.set! i (numParams+1)) (alts.set ⟨i, h⟩ alt) refined (i+1) - | _ => throwError "unexpected type at MatcherApp.addArg" - else - if refined then - return (altNumParams, alts) - else - throwError "failed to add argument to matcher application, argument type was not refined by `casesOn`" - -/-- Given - - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and - - expression `e : B[discrs]`, - Construct the term - `match_i As (fun xs => B[xs] -> motive[xs]) discrs (fun ys_1 (y : B[C_1[ys_1]]) => alt_1) ... (fun ys_n (y : B[C_n[ys_n]]) => alt_n) e remaining`. - - We use `kabstract` to abstract the discriminants from `B[discrs]`. - - This method assumes - - the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size` - - each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]` - - This is used in in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to - the argument provided by `fix` to refine the termination argument, which may mention `major`. - See there for how to use this function. --/ -def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp := - lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do - unless motiveArgs.size == matcherApp.discrs.size do - -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`. - throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" - let eType ← inferType e - let eTypeAbst ← matcherApp.discrs.size.foldRevM (init := eType) fun i eTypeAbst => do - let motiveArg := motiveArgs[i]! - let discr := matcherApp.discrs[i]! - let eTypeAbst ← kabstract eTypeAbst discr - return eTypeAbst.instantiate1 motiveArg - let motiveBody ← mkArrow eTypeAbst motiveBody - let matcherLevels ← match matcherApp.uElimPos? with - | none => pure matcherApp.matcherLevels - | some pos => - let uElim ← getLevel motiveBody - pure <| matcherApp.matcherLevels.set! pos uElim - let motive ← mkLambdaFVars motiveArgs motiveBody - -- Construct `aux` `match_i As (fun xs => B[xs] → motive[xs]) discrs`, and infer its type `auxType`. - -- We use `auxType` to infer the type `B[C_i[ys_i]]` of the new argument in each alternative. - let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params - let aux := mkApp aux motive - let aux := mkAppN aux matcherApp.discrs - unless (← isTypeCorrect aux) do - throwError "failed to add argument to matcher application, type error when constructing the new motive" - let auxType ← inferType aux - let (altNumParams, alts) ← updateAlts eType auxType matcherApp.altNumParams matcherApp.alts false 0 - return { matcherApp with - matcherLevels := matcherLevels, - motive := motive, - alts := alts, - altNumParams := altNumParams, - remaining := #[e] ++ matcherApp.remaining - } - -/-- Similar to `MatcherApp.addArg`, but returns `none` on failure. -/ -def MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option MatcherApp) := - try - return some (← matcherApp.addArg e) - catch _ => - return none - - -/-- Given - - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and - - a expression `B[discrs]` (which may not be a type, e.g. `n : Nat`), - returns the expressions `fun ys_1 ... ys_i => B[C_1[ys_1]] ... B[C_n[ys_n]]`, - - This method assumes - - the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size` - - each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]` - - This is similar to `MatcherApp.addArg` when you only have an expression to - refined, and not a type with a value. - - This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive - calls to refine the functions' paramter, which may mention `major`. - See there for how to use this function. --/ -def MatcherApp.refineThrough (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) := - lambdaTelescope matcherApp.motive fun motiveArgs _motiveBody => do - unless motiveArgs.size == matcherApp.discrs.size do - -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`. - throwError "failed to transfer argument through matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" - - let eAbst ← matcherApp.discrs.size.foldRevM (init := e) fun i eAbst => do - let motiveArg := motiveArgs[i]! - let discr := matcherApp.discrs[i]! - let eTypeAbst ← kabstract eAbst discr - return eTypeAbst.instantiate1 motiveArg - -- Let's create something that’s a `Sort` and mentions `e` - -- (recall that `e` itself possibly isn't a type), - -- by writing `e = e`, so that we can use it as a motive - let eEq ← mkEq eAbst eAbst - - let matcherLevels ← match matcherApp.uElimPos? with - | none => pure matcherApp.matcherLevels - | some pos => - pure <| matcherApp.matcherLevels.set! pos levelZero - let motive ← mkLambdaFVars motiveArgs eEq - let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params - let aux := mkApp aux motive - let aux := mkAppN aux matcherApp.discrs - unless (← isTypeCorrect aux) do - throwError "failed to transfer argument through matcher application, type error when constructing the new motive" - let auxType ← inferType aux - forallTelescope auxType fun altAuxs _ => do - let altAuxTys ← altAuxs.mapM (inferType ·) - (Array.zip matcherApp.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do - forallBoundedTelescope altAuxTy altNumParams fun fvs body => do - unless fvs.size = altNumParams do - throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" - -- extract type from our synthetic equality - let body := body.getArg! 2 - -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out - mkLambdaFVars fvs body - -/-- A non-failing version of `MatcherApp.refineThrough` -/ -def MatcherApp.refineThrough? (matcherApp : MatcherApp) (e : Expr) : - MetaM (Option (Array Expr)) := - try - return some (← matcherApp.refineThrough e) - catch _ => - return none builtin_initialize registerTraceClass `Meta.Match.match diff --git a/src/Lean/Meta/Match/MatcherApp.lean b/src/Lean/Meta/Match/MatcherApp.lean new file mode 100644 index 0000000000..035c2ec292 --- /dev/null +++ b/src/Lean/Meta/Match/MatcherApp.lean @@ -0,0 +1,8 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura, Joachim Breitner +-/ +prelude +import Lean.Meta.Match.MatcherApp.Basic +import Lean.Meta.Match.MatcherApp.Transform diff --git a/src/Lean/Meta/Match/MatcherApp/Basic.lean b/src/Lean/Meta/Match/MatcherApp/Basic.lean new file mode 100644 index 0000000000..946dc7e1c4 --- /dev/null +++ b/src/Lean/Meta/Match/MatcherApp/Basic.lean @@ -0,0 +1,80 @@ +/- +Copyright (c) 2020 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import Lean.Meta.Match.MatcherInfo + +namespace Lean.Meta + +structure MatcherApp where + matcherName : Name + matcherLevels : Array Level + uElimPos? : Option Nat + discrInfos : Array Match.DiscrInfo + params : Array Expr + motive : Expr + discrs : Array Expr + altNumParams : Array Nat + alts : Array Expr + remaining : Array Expr + +/-- +Recognizes if `e` is a matcher application, and destructs it into the `MatcherApp` data structure. + +This can optionally also treat `casesOn` recursor applications as a special case +of matcher applications. +-/ +def matchMatcherApp? [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (alsoCasesOn := false) : + m (Option MatcherApp) := do + if let .const declName declLevels := e.getAppFn then + if let some info ← getMatcherInfo? declName then + let args := e.getAppArgs + if args.size < info.arity then + return none + return some { + matcherName := declName + matcherLevels := declLevels.toArray + uElimPos? := info.uElimPos? + discrInfos := info.discrInfos + params := args.extract 0 info.numParams + motive := args[info.getMotivePos]! + discrs := args[info.numParams + 1 : info.numParams + 1 + info.numDiscrs] + altNumParams := info.altNumParams + alts := args[info.numParams + 1 + info.numDiscrs : info.numParams + 1 + info.numDiscrs + info.numAlts] + remaining := args[info.numParams + 1 + info.numDiscrs + info.numAlts : args.size] + } + + if alsoCasesOn && isCasesOnRecursor (← getEnv) declName then + let indName := declName.getPrefix + let .inductInfo info ← getConstInfo indName | return none + let args := e.getAppArgs + unless args.size >= info.numParams + 1 /- motive -/ + info.numIndices + 1 /- major -/ + info.numCtors do return none + let params := args[:info.numParams] + let motive := args[info.numParams]! + let discrs := args[info.numParams + 1 : info.numParams + 1 + info.numIndices + 1] + let discrInfos := Array.mkArray (info.numIndices + 1) {} + let alts := args[info.numParams + 1 + info.numIndices + 1 : info.numParams + 1 + info.numIndices + 1 + info.numCtors] + let remaining := args[info.numParams + 1 + info.numIndices + 1 + info.numCtors :] + let uElimPos? := if info.levelParams.length == declLevels.length then none else some 0 + let mut altNumParams := #[] + for ctor in info.ctors do + let .ctorInfo ctorInfo ← getConstInfo ctor | unreachable! + altNumParams := altNumParams.push ctorInfo.numFields + return some { + matcherName := declName + matcherLevels := declLevels.toArray + uElimPos?, discrInfos, params, motive, discrs, alts, remaining, altNumParams + } + + return none + +def MatcherApp.toExpr (matcherApp : MatcherApp) : Expr := + let result := mkAppN (mkConst matcherApp.matcherName matcherApp.matcherLevels.toList) matcherApp.params + let result := mkApp result matcherApp.motive + let result := mkAppN result matcherApp.discrs + let result := mkAppN result matcherApp.alts + mkAppN result matcherApp.remaining + +end Lean.Meta diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean new file mode 100644 index 0000000000..f44a588264 --- /dev/null +++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean @@ -0,0 +1,159 @@ +/- +Copyright (c) 2024 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura, Joachim Breitner +-/ + +prelude +import Lean.Meta.Match +import Lean.Meta.InferType +import Lean.Meta.Check +import Lean.Meta.Tactic.Split + +namespace Lean.Meta.MatcherApp + +/-- Auxiliary function for MatcherApp.addArg -/ +private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNumParams : Array Nat) (alts : Array Expr) (refined : Bool) (i : Nat) : MetaM (Array Nat × Array Expr) := do + if h : i < alts.size then + let alt := alts.get ⟨i, h⟩ + let numParams := altNumParams[i]! + let typeNew ← whnfD typeNew + match typeNew with + | Expr.forallE _ d b _ => + let (alt, refined) ← forallBoundedTelescope d (some numParams) fun xs d => do + let alt ← try instantiateLambda alt xs catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative" + forallBoundedTelescope d (some 1) fun x _ => do + let alt ← mkLambdaFVars x alt -- x is the new argument we are adding to the alternative + let refined := if refined then refined else + !(← isDefEq unrefinedArgType (← inferType x[0]!)) + return (← mkLambdaFVars xs alt, refined) + updateAlts unrefinedArgType (b.instantiate1 alt) (altNumParams.set! i (numParams+1)) (alts.set ⟨i, h⟩ alt) refined (i+1) + | _ => throwError "unexpected type at MatcherApp.addArg" + else + if refined then + return (altNumParams, alts) + else + throwError "failed to add argument to matcher application, argument type was not refined by `casesOn`" + +/-- Given + - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and + - expression `e : B[discrs]`, + Construct the term + `match_i As (fun xs => B[xs] -> motive[xs]) discrs (fun ys_1 (y : B[C_1[ys_1]]) => alt_1) ... (fun ys_n (y : B[C_n[ys_n]]) => alt_n) e remaining`. + + We use `kabstract` to abstract the discriminants from `B[discrs]`. + + This method assumes + - the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size` + - each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]` + + This is used in in `Lean.Elab.PreDefinition.WF.Fix` when replacing recursive calls with calls to + the argument provided by `fix` to refine the termination argument, which may mention `major`. + See there for how to use this function. +-/ +def addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp := + lambdaTelescope matcherApp.motive fun motiveArgs motiveBody => do + unless motiveArgs.size == matcherApp.discrs.size do + -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`. + throwError "unexpected matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" + let eType ← inferType e + let eTypeAbst ← matcherApp.discrs.size.foldRevM (init := eType) fun i eTypeAbst => do + let motiveArg := motiveArgs[i]! + let discr := matcherApp.discrs[i]! + let eTypeAbst ← kabstract eTypeAbst discr + return eTypeAbst.instantiate1 motiveArg + let motiveBody ← mkArrow eTypeAbst motiveBody + let matcherLevels ← match matcherApp.uElimPos? with + | none => pure matcherApp.matcherLevels + | some pos => + let uElim ← getLevel motiveBody + pure <| matcherApp.matcherLevels.set! pos uElim + let motive ← mkLambdaFVars motiveArgs motiveBody + -- Construct `aux` `match_i As (fun xs => B[xs] → motive[xs]) discrs`, and infer its type `auxType`. + -- We use `auxType` to infer the type `B[C_i[ys_i]]` of the new argument in each alternative. + let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params + let aux := mkApp aux motive + let aux := mkAppN aux matcherApp.discrs + unless (← isTypeCorrect aux) do + throwError "failed to add argument to matcher application, type error when constructing the new motive" + let auxType ← inferType aux + let (altNumParams, alts) ← updateAlts eType auxType matcherApp.altNumParams matcherApp.alts false 0 + return { matcherApp with + matcherLevels := matcherLevels, + motive := motive, + alts := alts, + altNumParams := altNumParams, + remaining := #[e] ++ matcherApp.remaining + } + +/-- Similar to `MatcherApp.addArg`, but returns `none` on failure. -/ +def addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option MatcherApp) := + try + return some (← matcherApp.addArg e) + catch _ => + return none + + +/-- Given + - matcherApp `match_i As (fun xs => motive[xs]) discrs (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining`, and + - a expression `B[discrs]` (which may not be a type, e.g. `n : Nat`), + returns the expressions `fun ys_1 ... ys_i => B[C_1[ys_1]] ... B[C_n[ys_n]]`, + + This method assumes + - the `matcherApp.motive` is a lambda abstraction where `xs.size == discrs.size` + - each alternative is a lambda abstraction where `ys_i.size == matcherApp.altNumParams[i]` + + This is similar to `MatcherApp.addArg` when you only have an expression to + refined, and not a type with a value. + + This is used in in `Lean.Elab.PreDefinition.WF.GuessFix` when constructing the context of recursive + calls to refine the functions' paramter, which may mention `major`. + See there for how to use this function. +-/ +def refineThrough (matcherApp : MatcherApp) (e : Expr) : MetaM (Array Expr) := + lambdaTelescope matcherApp.motive fun motiveArgs _motiveBody => do + unless motiveArgs.size == matcherApp.discrs.size do + -- This error can only happen if someone implemented a transformation that rewrites the motive created by `mkMatcher`. + throwError "failed to transfer argument through matcher application, motive must be lambda expression with #{matcherApp.discrs.size} arguments" + + let eAbst ← matcherApp.discrs.size.foldRevM (init := e) fun i eAbst => do + let motiveArg := motiveArgs[i]! + let discr := matcherApp.discrs[i]! + let eTypeAbst ← kabstract eAbst discr + return eTypeAbst.instantiate1 motiveArg + -- Let's create something that’s a `Sort` and mentions `e` + -- (recall that `e` itself possibly isn't a type), + -- by writing `e = e`, so that we can use it as a motive + let eEq ← mkEq eAbst eAbst + + let matcherLevels ← match matcherApp.uElimPos? with + | none => pure matcherApp.matcherLevels + | some pos => + pure <| matcherApp.matcherLevels.set! pos levelZero + let motive ← mkLambdaFVars motiveArgs eEq + let aux := mkAppN (mkConst matcherApp.matcherName matcherLevels.toList) matcherApp.params + let aux := mkApp aux motive + let aux := mkAppN aux matcherApp.discrs + unless (← isTypeCorrect aux) do + throwError "failed to transfer argument through matcher application, type error when constructing the new motive" + let auxType ← inferType aux + forallTelescope auxType fun altAuxs _ => do + let altAuxTys ← altAuxs.mapM (inferType ·) + (Array.zip matcherApp.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do + forallBoundedTelescope altAuxTy altNumParams fun fvs body => do + unless fvs.size = altNumParams do + throwError "failed to transfer argument through matcher application, alt type must be telescope with #{altNumParams} arguments" + -- extract type from our synthetic equality + let body := body.getArg! 2 + -- and abstract over the parameters of the alternatives, so that we can safely pass the Expr out + mkLambdaFVars fvs body + +/-- A non-failing version of `MatcherApp.refineThrough` -/ +def refineThrough? (matcherApp : MatcherApp) (e : Expr) : + MetaM (Option (Array Expr)) := + try + return some (← matcherApp.refineThrough e) + catch _ => + return none + +end Lean.Meta.MatcherApp diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean index d30a6b6d48..d21e1ae66d 100644 --- a/src/Lean/Meta/Match/MatcherInfo.lean +++ b/src/Lean/Meta/Match/MatcherInfo.lean @@ -128,73 +128,4 @@ def isMatcherAppCore (env : Environment) (e : Expr) : Bool := def isMatcherApp [Monad m] [MonadEnv m] (e : Expr) : m Bool := return isMatcherAppCore (← getEnv) e -structure MatcherApp where - matcherName : Name - matcherLevels : Array Level - uElimPos? : Option Nat - discrInfos : Array Match.DiscrInfo - params : Array Expr - motive : Expr - discrs : Array Expr - altNumParams : Array Nat - alts : Array Expr - remaining : Array Expr - -/-- -Recognizes if `e` is a matcher application, and destructs it into the `MatcherApp` data structure. - -This can optionally also treat `casesOn` recursor applications as a special case -of matcher applications. --/ -def matchMatcherApp? [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (alsoCasesOn := false) : - m (Option MatcherApp) := do - if let .const declName declLevels := e.getAppFn then - if let some info ← getMatcherInfo? declName then - let args := e.getAppArgs - if args.size < info.arity then - return none - return some { - matcherName := declName - matcherLevels := declLevels.toArray - uElimPos? := info.uElimPos? - discrInfos := info.discrInfos - params := args.extract 0 info.numParams - motive := args[info.getMotivePos]! - discrs := args[info.numParams + 1 : info.numParams + 1 + info.numDiscrs] - altNumParams := info.altNumParams - alts := args[info.numParams + 1 + info.numDiscrs : info.numParams + 1 + info.numDiscrs + info.numAlts] - remaining := args[info.numParams + 1 + info.numDiscrs + info.numAlts : args.size] - } - - if alsoCasesOn && isCasesOnRecursor (← getEnv) declName then - let indName := declName.getPrefix - let .inductInfo info ← getConstInfo indName | return none - let args := e.getAppArgs - unless args.size >= info.numParams + 1 /- motive -/ + info.numIndices + 1 /- major -/ + info.numCtors do return none - let params := args[:info.numParams] - let motive := args[info.numParams]! - let discrs := args[info.numParams + 1 : info.numParams + 1 + info.numIndices + 1] - let discrInfos := Array.mkArray (info.numIndices + 1) {} - let alts := args[info.numParams + 1 + info.numIndices + 1 : info.numParams + 1 + info.numIndices + 1 + info.numCtors] - let remaining := args[info.numParams + 1 + info.numIndices + 1 + info.numCtors :] - let uElimPos? := if info.levelParams.length == declLevels.length then none else some 0 - let mut altNumParams := #[] - for ctor in info.ctors do - let .ctorInfo ctorInfo ← getConstInfo ctor | unreachable! - altNumParams := altNumParams.push ctorInfo.numFields - return some { - matcherName := declName - matcherLevels := declLevels.toArray - uElimPos?, discrInfos, params, motive, discrs, alts, remaining, altNumParams - } - - return none - -def MatcherApp.toExpr (matcherApp : MatcherApp) : Expr := - let result := mkAppN (mkConst matcherApp.matcherName matcherApp.matcherLevels.toList) matcherApp.params - let result := mkApp result matcherApp.motive - let result := mkAppN result matcherApp.discrs - let result := mkAppN result matcherApp.alts - mkAppN result matcherApp.remaining - end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index 6a48b1d2d8..9e68455dc0 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude +import Lean.Meta.Match.MatcherApp.Basic import Lean.Meta.Tactic.Simp.Main import Lean.Meta.Tactic.SplitIf import Lean.Meta.Tactic.Apply