From 6592df52ccb73da9f99dd1a983765b767cafa359 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 27 Nov 2023 16:52:32 +0100 Subject: [PATCH] feat: Add MatcherApp. and CasesOnApp.refineThrough (#2882) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- src/Lean/Meta/CasesOn.lean | 72 +++++++++++++++++++++++++++++-- src/Lean/Meta/Match/Match.lean | 77 +++++++++++++++++++++++++++++++++- 2 files changed, 144 insertions(+), 5 deletions(-) diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean index 7646455f9e..86371632a4 100644 --- a/src/Lean/Meta/CasesOn.lean +++ b/src/Lean/Meta/CasesOn.lean @@ -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 diff --git a/src/Lean/Meta/Match/Match.lean b/src/Lean/Meta/Match/Match.lean index b4ce227904..00295e4cc1 100644 --- a/src/Lean/Meta/Match/Match.lean +++ b/src/Lean/Meta/Match/Match.lean @@ -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