diff --git a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean index dec2078156..ff6cd8b4bc 100644 --- a/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean +++ b/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Lean.Util.HasConstCache -import Lean.Meta.CasesOn import Lean.Meta.Match.Match import Lean.Elab.RecAppSyntax import Lean.Elab.PreDefinition.Basic @@ -129,7 +128,7 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) return mkAppN f fArgs else return mkAppN (← loop below f) (← args.mapM (loop below)) - match (← matchMatcherApp? e) with + match (← matchMatcherApp? (alsoCasesOn := true) e) with | some matcherApp => if !recArgHasLooseBVarsAt recFnName recArgInfo.recArgPos e then processApp e @@ -162,21 +161,6 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo) pure { matcherApp with alts := altsNew }.toExpr else processApp e - | none => - match (← toCasesOnApp? e) with - | some casesOnApp => - if !recArgHasLooseBVarsAt recFnName recArgInfo.recArgPos e then - processApp e - else if let some casesOnApp ← casesOnApp.addArg? below then - let altsNew ← (Array.zip casesOnApp.alts casesOnApp.altNumParams).mapM fun (alt, numParams) => - lambdaTelescope alt fun xs altBody => do - unless xs.size >= numParams do - throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}" - let belowForAlt := xs[numParams]! - mkLambdaFVars xs (← loop belowForAlt altBody) - return { casesOnApp with alts := altsNew }.toExpr - else - processApp e | none => processApp e | e => ensureNoRecFn recFnName e loop below e |>.run' {} diff --git a/src/Lean/Elab/PreDefinition/WF/Fix.lean b/src/Lean/Elab/PreDefinition/WF/Fix.lean index 539aa6e428..658b731260 100644 --- a/src/Lean/Elab/PreDefinition/WF/Fix.lean +++ b/src/Lean/Elab/PreDefinition/WF/Fix.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ import Lean.Util.HasConstCache -import Lean.Meta.CasesOn import Lean.Meta.Match.Match import Lean.Meta.Tactic.Simp.Main import Lean.Meta.Tactic.Cleanup @@ -77,7 +76,7 @@ where | Expr.proj n i e => return mkProj n i (← loop F e) | Expr.const .. => if e.isConstOf recFnName then processRec F e else return e | Expr.app .. => - match (← matchMatcherApp? e) with + match (← matchMatcherApp? (alsoCasesOn := true) e) with | some matcherApp => if let some matcherApp ← matcherApp.addArg? F then let altsNew ← (Array.zip matcherApp.alts matcherApp.altNumParams).mapM fun (alt, numParams) => @@ -89,21 +88,6 @@ where return { matcherApp with alts := altsNew, discrs := (← matcherApp.discrs.mapM (loop F)) }.toExpr else processApp F e - | none => - match (← toCasesOnApp? e) with - | some casesOnApp => - if let some casesOnApp ← casesOnApp.addArg? F then - let altsNew ← (Array.zip casesOnApp.alts casesOnApp.altNumParams).mapM fun (alt, numParams) => - lambdaTelescope alt fun xs altBody => do - unless xs.size >= numParams do - throwError "unexpected `casesOn` application alternative{indentExpr alt}\nat application{indentExpr e}" - let FAlt := xs[numParams]! - mkLambdaFVars xs (← loop FAlt altBody) - return { casesOnApp with - alts := altsNew - remaining := (← casesOnApp.remaining.mapM (loop F)) }.toExpr - else - processApp F e | none => processApp F e | e => ensureNoRecFn recFnName e diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 517f8febf3..f4d7b50a4b 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -5,7 +5,6 @@ Authors: Joachim Breitner -/ import Lean.Util.HasConstCache -import Lean.Meta.CasesOn import Lean.Meta.Match.Match import Lean.Meta.Tactic.Cleanup import Lean.Meta.Tactic.Refl @@ -176,7 +175,7 @@ where | Expr.proj _n _i e => loop param e | Expr.const .. => if e.isConstOf recFnName then processRec param e | Expr.app .. => - match (← matchMatcherApp? e) with + match (← matchMatcherApp? (alsoCasesOn := true) e) with | some matcherApp => if let some altParams ← matcherApp.refineThrough? param then matcherApp.discrs.forM (loop param) @@ -191,23 +190,6 @@ where matcherApp.remaining.forM (loop param) else processApp param e - | none => - match (← toCasesOnApp? e) with - | some casesOnApp => - if let some altParams ← casesOnApp.refineThrough? param then - loop param casesOnApp.major - (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 altBody := alt.beta xs - loop altParam altBody - casesOnApp.remaining.forM (loop param) - else - trace[Elab.definition.wf] "withRecApps: casesOnApp.refineThrough? failed" - processApp param e | none => processApp param e | e => do let _ ← ensureNoRecFn recFnName e diff --git a/src/Lean/Meta.lean b/src/Lean/Meta.lean index 0a07f6bf5c..4aefcdb19a 100644 --- a/src/Lean/Meta.lean +++ b/src/Lean/Meta.lean @@ -39,7 +39,6 @@ import Lean.Meta.Structure import Lean.Meta.Constructions import Lean.Meta.CongrTheorems import Lean.Meta.Eqns -import Lean.Meta.CasesOn import Lean.Meta.ExprLens import Lean.Meta.ExprTraverse import Lean.Meta.Eval diff --git a/src/Lean/Meta/CasesOn.lean b/src/Lean/Meta/CasesOn.lean deleted file mode 100644 index 230008facf..0000000000 --- a/src/Lean/Meta/CasesOn.lean +++ /dev/null @@ -1,179 +0,0 @@ -/- -Copyright (c) 2022 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura --/ -import Lean.Meta.KAbstract -import Lean.Meta.Check -import Lean.Meta.AppBuilder - -namespace Lean.Meta - -structure CasesOnApp where - declName : Name - us : List Level - params : Array Expr - motive : Expr - indices : Array Expr - major : Expr - alts : Array Expr - altNumParams : Array Nat - remaining : Array Expr - /-- `true` if the `casesOn` can only eliminate into `Prop` -/ - propOnly : Bool - -/-- Return `some c` if `e` is a `casesOn` application. -/ -def toCasesOnApp? (e : Expr) : MetaM (Option CasesOnApp) := do - let f := e.getAppFn - let .const declName us := f | return none - unless isCasesOnRecursor (← getEnv) declName do return none - 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 indices := args[info.numParams + 1 : info.numParams + 1 + info.numIndices] - let major := args[info.numParams + 1 + info.numIndices]! - 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 propOnly := info.levelParams.length == us.length - let mut altNumParams := #[] - for ctor in info.ctors do - let .ctorInfo ctorInfo ← getConstInfo ctor | unreachable! - altNumParams := altNumParams.push ctorInfo.numFields - return some { declName, us, params, motive, indices, major, alts, remaining, propOnly, altNumParams } - -/-- Convert `c` back to `Expr` -/ -def CasesOnApp.toExpr (c : CasesOnApp) : Expr := - mkAppN (mkAppN (mkApp (mkAppN (mkApp (mkAppN (mkConst c.declName c.us) c.params) c.motive) c.indices) c.major) c.alts) c.remaining - -/-- - 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 `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 - ``` - 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) : MetaM CasesOnApp := do - lambdaTelescope c.motive fun motiveArgs motiveBody => do - unless motiveArgs.size == c.indices.size + 1 do - throwError "failed to add argument to `casesOn` application, motive must be lambda expression with #{c.indices.size + 1} binders" - let argType ← inferType arg - let discrs := c.indices ++ #[c.major] - let mut argTypeAbst := argType - for motiveArg in motiveArgs.reverse, discr in discrs.reverse do - argTypeAbst := (← kabstract argTypeAbst discr).instantiate1 motiveArg - let motiveBody ← mkArrow argTypeAbst motiveBody - let us ← if c.propOnly then pure c.us else pure ((← getLevel motiveBody) :: c.us.tail!) - let motive ← mkLambdaFVars motiveArgs motiveBody - let remaining := #[arg] ++ c.remaining - let aux := mkAppN (mkConst c.declName us) c.params - let aux := mkApp aux motive - let aux := mkAppN aux discrs - check aux - unless (← isTypeCorrect aux) do - throwError "failed to add argument to `casesOn` application, type error when constructing the new motive{indentExpr aux}" - let auxType ← inferType aux - let alts ← updateAlts argType auxType - return { c with us, motive, alts, remaining } -where - updateAlts (argType : Expr) (auxType : Expr) : MetaM (Array Expr) := do - let mut auxType := auxType - let mut altsNew := #[] - let mut refined := false - for alt in c.alts, numParams in c.altNumParams do - auxType ← whnfD auxType - match auxType with - | .forallE _ d b _ => - let (altNew, refinedAt) ← forallBoundedTelescope d (some numParams) fun xs d => do - forallBoundedTelescope d (some 1) fun x _ => do - let alt := alt.beta xs - let alt ← mkLambdaFVars x alt -- x is the new argument we are adding to the alternative - if refined then - return (← mkLambdaFVars xs alt, true) - else - return (← mkLambdaFVars xs alt, !(← isDefEq argType (← inferType x[0]!))) - refined := refinedAt - auxType := b.instantiate1 altNew - altsNew := altsNew.push altNew - | _ => throwError "unexpected type at `casesOnAddArg`" - unless refined do - throwError "failed to add argument to `casesOn` application, argument type was not refined by `casesOn`" - return altsNew - -/-- Similar to `CasesOnApp.addArg`, but returns `none` on failure. -/ -def CasesOnApp.addArg? (c : CasesOnApp) (arg : Expr) : MetaM (Option CasesOnApp) := - try - return some (← c.addArg arg) - 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 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. - - Unlike `addArg`, it does not bother recognizing if the type was actually refined in any branch. - - 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 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 - forallBoundedTelescope altAuxTy altNumParams fun fvs body => do - unless fvs.size = altNumParams do - 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 - mkLambdaFVars fvs body - -/-- 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/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean index 2aff1764fe..994b7ae572 100644 --- a/src/Lean/Meta/Match/MatcherInfo.lean +++ b/src/Lean/Meta/Match/MatcherInfo.lean @@ -131,6 +131,7 @@ structure MatcherApp where matcherName : Name matcherLevels : Array Level uElimPos? : Option Nat + discrInfos : Array Match.DiscrInfo params : Array Expr motive : Expr discrs : Array Expr @@ -138,28 +139,55 @@ structure MatcherApp where alts : Array Expr remaining : Array Expr -def matchMatcherApp? [Monad m] [MonadEnv m] (e : Expr) : m (Option MatcherApp) := do - match e.getAppFn with - | Expr.const declName declLevels => - match (← getMatcherInfo? declName) with - | none => return none - | some info => +/-- +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 - else - return some { - matcherName := declName - matcherLevels := declLevels.toArray - uElimPos? := info.uElimPos? - 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] - } - | _ => 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