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.
This commit is contained in:
Joachim Breitner
GitHub
parent
47595540bb
commit
b27ab5e25d
9 changed files with 252 additions and 214 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
8
src/Lean/Meta/Match/MatcherApp.lean
Normal file
8
src/Lean/Meta/Match/MatcherApp.lean
Normal file
|
|
@ -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
|
||||
80
src/Lean/Meta/Match/MatcherApp/Basic.lean
Normal file
80
src/Lean/Meta/Match/MatcherApp/Basic.lean
Normal file
|
|
@ -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
|
||||
159
src/Lean/Meta/Match/MatcherApp/Transform.lean
Normal file
159
src/Lean/Meta/Match/MatcherApp/Transform.lean
Normal file
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue