From e80dfb384af65009e9ce6b7a549092c5955e29de Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 28 Nov 2023 11:44:54 +0100 Subject: [PATCH] refactor: CasesOnApp.refineThrough can return a lambda, not an open term MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 86 ++++++++++---------- src/Lean/Meta/CasesOn.lean | 12 +-- src/Lean/Meta/Match/Match.lean | 12 +-- 3 files changed, 52 insertions(+), 58 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index e74aaa3394fc..a74030a72417 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -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 diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean index 86371632a4cc..ca9a5504d53a 100644 --- a/src/Lean/Meta/CasesOn.lean +++ b/src/Lean/Meta/CasesOn.lean @@ -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) : diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index 00295e4cc1dc..d60f82f14f00 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -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) :