feat: Add MatcherApp. and CasesOnApp.refineThrough (#2882)
these are compagnions to `MatcherApp.addArg` and `CasesOnApp.addArg` when one only has an expression (which may not be a type) to transform, but not a concret values. This is a prerequisite for guessing lexicographic order (#2874). Keeping this on a separate PR because it’s sizable, and has a clear independent specification.
This commit is contained in:
Joachim Breitner
GitHub
parent
9769ad6572
commit
6592df52cc
2 changed files with 144 additions and 5 deletions
|
|
@ -5,6 +5,7 @@ Authors: Leonardo de Moura
|
|||
-/
|
||||
import Lean.Meta.KAbstract
|
||||
import Lean.Meta.Check
|
||||
import Lean.Meta.AppBuilder
|
||||
|
||||
namespace Lean.Meta
|
||||
|
||||
|
|
@ -50,13 +51,17 @@ def CasesOnApp.toExpr (c : CasesOnApp) : Expr :=
|
|||
/--
|
||||
Given a `casesOn` application `c` of the form
|
||||
```
|
||||
casesOn As (fun is x => motive[i, xs]) is major (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining
|
||||
casesOn As (fun is x => motive[is, xs]) is major (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining
|
||||
```
|
||||
and an expression `e : B[is, major]`, construct the term
|
||||
```
|
||||
casesOn As (fun is x => B[is, x] → motive[i, xs]) is major (fun ys_1 (y : B[C_1[ys_1]]) => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n (y : B[C_n[ys_n]]) => (alt_n : motive (C_n[ys_n]) e remaining
|
||||
casesOn As (fun is x => B[is, x] → motive[i, xs]) is major (fun ys_1 (y : B[_, C_1[ys_1]]) => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n (y : B[_, C_n[ys_n]]) => (alt_n : motive (C_n[ys_n]) e remaining
|
||||
```
|
||||
We use `kabstract` to abstract the `is` and `major` from `B[is, major]`.
|
||||
|
||||
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 CasesOnApp.addArg (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := false) : MetaM CasesOnApp := do
|
||||
lambdaTelescope c.motive fun motiveArgs motiveBody => do
|
||||
|
|
@ -106,11 +111,72 @@ where
|
|||
throwError "failed to add argument to `casesOn` application, argument type was not refined by `casesOn`"
|
||||
return altsNew
|
||||
|
||||
/-- Similar `CasesOnApp.addArg`, but returns `none` on failure. -/
|
||||
/-- Similar to `CasesOnApp.addArg`, but returns `none` on failure. -/
|
||||
def CasesOnApp.addArg? (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := false) : MetaM (Option CasesOnApp) :=
|
||||
try
|
||||
return some (← c.addArg arg checkIfRefined)
|
||||
catch _ =>
|
||||
return none
|
||||
|
||||
/--
|
||||
Given a `casesOn` application `c` of the form
|
||||
```
|
||||
casesOn As (fun is x => motive[is, xs]) is major (fun ys_1 => (alt_1 : motive (C_1[ys_1])) ... (fun ys_n => (alt_n : motive (C_n[ys_n]) remaining
|
||||
```
|
||||
and an expression `B[is, major]` (which may not be a type, e.g. `n : Nat`)
|
||||
for every alternative `i`, construct the type `B[_, C_i[ys_i]]`
|
||||
with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `CasesOnApp.altNumParams`.
|
||||
|
||||
This is similar to `CasesOnApp.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.
|
||||
|
||||
It returns an open term, rather than following the idiom of applying a continuation,
|
||||
so that `CasesOn.refineThrough?` can reliably recognize failure from within this function.
|
||||
-/
|
||||
def CasesOnApp.refineThrough (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) :=
|
||||
lambdaTelescope c.motive fun motiveArgs _motiveBody => do
|
||||
unless motiveArgs.size == c.indices.size + 1 do
|
||||
throwError "failed to transfer argument through `casesOn` application, motive must be lambda expression with #{c.indices.size + 1} binders"
|
||||
let discrs := c.indices ++ #[c.major]
|
||||
let mut eAbst := e
|
||||
for motiveArg in motiveArgs.reverse, discr in discrs.reverse do
|
||||
eAbst ← kabstract eAbst discr
|
||||
eAbst := eAbst.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 motive ← mkLambdaFVars motiveArgs eEq
|
||||
let us := if c.propOnly then c.us else levelZero :: c.us.tail!
|
||||
-- Now instantiate the casesOn wth this synthetic motive
|
||||
let aux := mkAppN (mkConst c.declName us) c.params
|
||||
let aux := mkApp aux motive
|
||||
let aux := mkAppN aux discrs
|
||||
check aux
|
||||
let auxType ← inferType aux
|
||||
-- The type of the remaining arguments will mention `e` instantiated for each arg
|
||||
-- so extract them
|
||||
forallTelescope auxType fun altAuxs _ => do
|
||||
let altAuxTys ← altAuxs.mapM (inferType ·)
|
||||
(Array.zip c.altNumParams altAuxTys).mapM fun (altNumParams, altAuxTy) => do
|
||||
forallTelescope altAuxTy 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
|
||||
Expr.abstractM body fvs
|
||||
|
||||
/-- A non-failing version of `CasesOnApp.refineThrough` -/
|
||||
def CasesOnApp.refineThrough? (c : CasesOnApp) (e : Expr) :
|
||||
MetaM (Option (Array Expr)) :=
|
||||
try
|
||||
return some (← c.refineThrough e)
|
||||
catch _ =>
|
||||
return none
|
||||
|
||||
end Lean.Meta
|
||||
|
|
|
|||
|
|
@ -910,11 +910,17 @@ private partial def updateAlts (typeNew : Expr) (altNumParams : Array Nat) (alts
|
|||
- 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`, and
|
||||
`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
|
||||
|
|
@ -951,13 +957,80 @@ def MatcherApp.addArg (matcherApp : MatcherApp) (e : Expr) : MetaM MatcherApp :=
|
|||
remaining := #[e] ++ matcherApp.remaining
|
||||
}
|
||||
|
||||
/-- Similar `MatcherApp.addArg?`, but returns `none` on failure. -/
|
||||
/-- 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 type `B[discrs]` (which may not be a type, e.g. `n : Nat`),
|
||||
returns the types `B[C_1[ys_1]] ... B[C_n[ys_n]]`,
|
||||
with `ys_i` as loose bound variables, ready to be `.instantiateRev`d; arity according to `matcherApp.altNumParams`.
|
||||
|
||||
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.
|
||||
|
||||
It returns an open term, rather than following the idiom of applying a continuation,
|
||||
so that `MatcherApp.refineThrough?` can reliably recognize failure from within 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
|
||||
forallTelescope altAuxTy 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
|
||||
Expr.abstractM body fvs
|
||||
|
||||
/-- 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
|
||||
registerTraceClass `Meta.Match.debug
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue