refactor: CasesOnApp.refineThrough can return a lambda, not an open term (#2974)
which also removes an error condition at the use site. While I am at it, I rename a parameter in `GuessLex` that I forgot to rename earlier. The effect will be user-visible (in obscure corner cases) with #2960, so I’ll have the test there. A few places would benefit from a `lambdaTelescopeBounded` that garantees the result has the right length (eta-expanding when necessary). I’ll look into that separately, and left TODOs here.
This commit is contained in:
Joachim Breitner
GitHub
parent
e4f2c39ab2
commit
18459cb537
3 changed files with 52 additions and 58 deletions
|
|
@ -92,90 +92,92 @@ abbrev M (recFnName : Name) (α β : Type) : Type :=
|
|||
Traverses the given expression `e`, and invokes the continuation `k`
|
||||
at every saturated call to `recFnName`.
|
||||
|
||||
The expression `scrut` is passed along, and refined when going under a matcher
|
||||
The expression `param` is passed along, and refined when going under a matcher
|
||||
or `casesOn` application.
|
||||
-/
|
||||
partial def withRecApps {α} (recFnName : Name) (fixedPrefixSize : Nat) (scrut : Expr) (e : Expr)
|
||||
partial def withRecApps {α} (recFnName : Name) (fixedPrefixSize : Nat) (param : Expr) (e : Expr)
|
||||
(k : Expr → Array Expr → MetaM α) : MetaM (Array α) := do
|
||||
trace[Elab.definition.wf] "withRecApps: {indentExpr e}"
|
||||
let (_, as) ← loop scrut e |>.run #[] |>.run' {}
|
||||
let (_, as) ← loop param e |>.run #[] |>.run' {}
|
||||
return as
|
||||
where
|
||||
processRec (scrut : Expr) (e : Expr) : M recFnName α Unit := do
|
||||
processRec (param : Expr) (e : Expr) : M recFnName α Unit := do
|
||||
if e.getAppNumArgs < fixedPrefixSize + 1 then
|
||||
loop scrut (← etaExpand e)
|
||||
loop param (← etaExpand e)
|
||||
else
|
||||
let a ← k scrut e.getAppArgs
|
||||
let a ← k param e.getAppArgs
|
||||
modifyThe (Array α) (·.push a)
|
||||
|
||||
processApp (scrut : Expr) (e : Expr) : M recFnName α Unit := do
|
||||
processApp (param : Expr) (e : Expr) : M recFnName α Unit := do
|
||||
e.withApp fun f args => do
|
||||
args.forM (loop scrut)
|
||||
args.forM (loop param)
|
||||
if f.isConstOf recFnName then
|
||||
processRec scrut e
|
||||
processRec param e
|
||||
else
|
||||
loop scrut f
|
||||
loop param f
|
||||
|
||||
containsRecFn (e : Expr) : M recFnName α Bool := do
|
||||
modifyGetThe (HasConstCache recFnName) (·.contains e)
|
||||
|
||||
loop (scrut : Expr) (e : Expr) : M recFnName α Unit := do
|
||||
loop (param : Expr) (e : Expr) : M recFnName α Unit := do
|
||||
if !(← containsRecFn e) then
|
||||
return
|
||||
match e with
|
||||
| Expr.lam n d b c =>
|
||||
loop scrut d
|
||||
loop param d
|
||||
withLocalDecl n c d fun x => do
|
||||
loop scrut (b.instantiate1 x)
|
||||
loop param (b.instantiate1 x)
|
||||
| Expr.forallE n d b c =>
|
||||
loop scrut d
|
||||
loop param d
|
||||
withLocalDecl n c d fun x => do
|
||||
loop scrut (b.instantiate1 x)
|
||||
loop param (b.instantiate1 x)
|
||||
| Expr.letE n type val body _ =>
|
||||
loop scrut type
|
||||
loop scrut val
|
||||
loop param type
|
||||
loop param val
|
||||
withLetDecl n type val fun x => do
|
||||
loop scrut (body.instantiate1 x)
|
||||
loop param (body.instantiate1 x)
|
||||
| Expr.mdata _d b =>
|
||||
if let some stx := getRecAppSyntax? e then
|
||||
withRef stx <| loop scrut b
|
||||
withRef stx <| loop param b
|
||||
else
|
||||
loop scrut b
|
||||
| Expr.proj _n _i e => loop scrut e
|
||||
| Expr.const .. => if e.isConstOf recFnName then processRec scrut e
|
||||
loop param b
|
||||
| Expr.proj _n _i e => loop param e
|
||||
| Expr.const .. => if e.isConstOf recFnName then processRec param e
|
||||
| Expr.app .. =>
|
||||
match (← matchMatcherApp? e) with
|
||||
| some matcherApp =>
|
||||
if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
|
||||
processApp scrut e
|
||||
processApp param e
|
||||
else
|
||||
if let some altScruts ← matcherApp.refineThrough? scrut then
|
||||
(Array.zip matcherApp.alts (Array.zip matcherApp.altNumParams altScruts)).forM
|
||||
fun (alt, altNumParam, altScrut) =>
|
||||
lambdaTelescope alt fun xs altBody => do
|
||||
unless altNumParam ≤ xs.size do
|
||||
throwError "unexpected matcher application alternative{indentExpr alt}\nat application{indentExpr e}"
|
||||
let altScrut := altScrut.instantiateRev xs[:altNumParam]
|
||||
loop altScrut altBody
|
||||
if let some altParams ← matcherApp.refineThrough? param then
|
||||
(Array.zip matcherApp.alts (Array.zip matcherApp.altNumParams altParams)).forM
|
||||
fun (alt, altNumParam, altParam) =>
|
||||
lambdaTelescope altParam fun xs altParam => do
|
||||
-- TODO: Use boundedLambdaTelescope
|
||||
unless altNumParam = xs.size do
|
||||
throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}"
|
||||
let altBody := alt.beta xs
|
||||
loop altParam altBody
|
||||
else
|
||||
processApp scrut e
|
||||
processApp param e
|
||||
| none =>
|
||||
match (← toCasesOnApp? e) with
|
||||
| some casesOnApp =>
|
||||
if !Structural.recArgHasLooseBVarsAt recFnName fixedPrefixSize e then
|
||||
processApp scrut e
|
||||
processApp param e
|
||||
else
|
||||
if let some altScruts ← casesOnApp.refineThrough? scrut then
|
||||
(Array.zip casesOnApp.alts (Array.zip casesOnApp.altNumParams altScruts)).forM
|
||||
fun (alt, altNumParam, altScrut) =>
|
||||
lambdaTelescope alt fun xs altBody => do
|
||||
unless altNumParam ≤ xs.size do
|
||||
if let some altParams ← casesOnApp.refineThrough? param then
|
||||
(Array.zip casesOnApp.alts (Array.zip casesOnApp.altNumParams altParams)).forM
|
||||
fun (alt, altNumParam, altParam) =>
|
||||
lambdaTelescope altParam fun xs altParam => do
|
||||
-- TODO: Use boundedLambdaTelescope
|
||||
unless altNumParam = xs.size do
|
||||
throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}"
|
||||
let altScrut := altScrut.instantiateRev xs[:altNumParam]
|
||||
loop altScrut altBody
|
||||
let altBody := alt.beta xs
|
||||
loop altParam altBody
|
||||
else
|
||||
processApp scrut e
|
||||
| none => processApp scrut e
|
||||
processApp param e
|
||||
| none => processApp param e
|
||||
| e => do
|
||||
let _ ← ensureNoRecFn recFnName e
|
||||
|
||||
|
|
|
|||
|
|
@ -124,8 +124,7 @@ def CasesOnApp.addArg? (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := f
|
|||
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`.
|
||||
for every alternative `i`, construct the expression `fun ys_i => B[_, C_i[ys_i]]`
|
||||
|
||||
This is similar to `CasesOnApp.addArg` when you only have an expression to
|
||||
refined, and not a type with a value.
|
||||
|
|
@ -133,9 +132,6 @@ def CasesOnApp.addArg? (c : CasesOnApp) (arg : Expr) (checkIfRefined : Bool := f
|
|||
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
|
||||
|
|
@ -163,13 +159,13 @@ def CasesOnApp.refineThrough (c : CasesOnApp) (e : Expr) : MetaM (Array Expr) :=
|
|||
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
|
||||
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"
|
||||
throwError "failed to transfer argument through `casesOn` 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
|
||||
mkLambdaFVars fvs body
|
||||
|
||||
/-- A non-failing version of `CasesOnApp.refineThrough` -/
|
||||
def CasesOnApp.refineThrough? (c : CasesOnApp) (e : Expr) :
|
||||
|
|
|
|||
|
|
@ -967,9 +967,8 @@ def MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option Matc
|
|||
|
||||
/-- 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`.
|
||||
- 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`
|
||||
|
|
@ -981,9 +980,6 @@ def MatcherApp.addArg? (matcherApp : MatcherApp) (e : Expr) : MetaM (Option Matc
|
|||
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
|
||||
|
|
@ -1015,13 +1011,13 @@ def MatcherApp.refineThrough (matcherApp : MatcherApp) (e : Expr) : MetaM (Array
|
|||
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
|
||||
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
|
||||
Expr.abstractM body fvs
|
||||
mkLambdaFVars fvs body
|
||||
|
||||
/-- A non-failing version of `MatcherApp.refineThrough` -/
|
||||
def MatcherApp.refineThrough? (matcherApp : MatcherApp) (e : Expr) :
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue