refactor: simplify structural recursion elaboration (#13008)
This PR removes the custom `M`/`State` monad from structural recursion elaboration, replacing it with plain `MetaM`. This simplifies the code and makes the control flow more explicit, in preparation for #12987 which introduces named `_f` auxiliary definitions for structural recursion. Key changes: - Remove `State`/`M` types from `Structural.Basic`, use `MetaM` throughout - Extract `withRecFunsAsAxioms` helper for adding recursive functions as temporary axioms - Split `tryAllArgs` into `findRecArgCandidates` (analysis) and `tryCandidates` (backtracking execution) - Move `withoutModifyingEnv` into each phase that needs it - For inductive predicates, return matchers from `mkIndPredBRecOnF` instead of accumulating in state - Pass `fnTypes` explicitly to `mkBRecOnMotive` instead of re-inferring This is a pure refactoring with no behavior changes (except matcher numbering in `inductive_pred` test due to changed `saveState`/`restoreState` boundaries). 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Joachim Breitner
GitHub
parent
4d6accd55d
commit
1362cc6041
6 changed files with 150 additions and 114 deletions
|
|
@ -123,11 +123,11 @@ partial def toBelow (below : Expr) (numIndParams : Nat) (positions : Positions)
|
|||
toBelowAux Cs[fnIndex]! belowDict recArg below
|
||||
|
||||
private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions : Positions)
|
||||
(below : Expr) (e : Expr) : M Expr :=
|
||||
(below : Expr) (e : Expr) : MetaM Expr :=
|
||||
let recFnNames := recArgInfos.map (·.fnName)
|
||||
let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnNames) M Bool :=
|
||||
let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnNames) MetaM Bool :=
|
||||
modifyGet (HasConstCache.contains e |>.run ·)
|
||||
let rec loop (below : Expr) (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr := do
|
||||
let rec loop (below : Expr) (e : Expr) : StateRefT (HasConstCache recFnNames) MetaM Expr := do
|
||||
if !(← containsRecFn e) then
|
||||
return e
|
||||
match e with
|
||||
|
|
@ -147,7 +147,7 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions :
|
|||
return mkMData d (← loop below b)
|
||||
| Expr.proj n i e => return mkProj n i (← loop below e)
|
||||
| Expr.app _ _ =>
|
||||
let processApp (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr :=
|
||||
let processApp (e : Expr) : StateRefT (HasConstCache recFnNames) MetaM Expr :=
|
||||
e.withApp fun f args => do
|
||||
if let .some fnIdx := recArgInfos.findFinIdx? (f.isConstOf ·.fnName) then
|
||||
let recArgInfo := recArgInfos[fnIdx]
|
||||
|
|
@ -208,10 +208,11 @@ private partial def replaceRecApps (recArgInfos : Array RecArgInfo) (positions :
|
|||
/--
|
||||
Calculates the `.brecOn` motive corresponding to one structural recursive function.
|
||||
The `value` is the function with (only) the fixed parameters moved into the context.
|
||||
The `type` is the corresponding function type with (only) the fixed parameters instantiated.
|
||||
-/
|
||||
def mkBRecOnMotive (recArgInfo : RecArgInfo) (value : Expr) : M Expr := do
|
||||
lambdaTelescope value fun xs value => do
|
||||
let type := (← inferType value).headBeta
|
||||
def mkBRecOnMotive (recArgInfo : RecArgInfo) (value : Expr) (type : Expr) : MetaM Expr := do
|
||||
lambdaTelescope value fun xs _value => do
|
||||
let type ← instantiateForall type xs
|
||||
let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
|
||||
let motive ← mkForallFVars otherArgs type
|
||||
mkLambdaFVars indexMajorArgs motive
|
||||
|
|
@ -224,7 +225,7 @@ The `recArgInfos` is used to transform the body of the function to replace recur
|
|||
uses of the `below` induction hypothesis.
|
||||
-/
|
||||
def mkBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions)
|
||||
(recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) : M Expr := do
|
||||
(recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) : MetaM Expr := do
|
||||
lambdaTelescope value fun xs value => do
|
||||
let (indicesMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
|
||||
let FType ← instantiateForall FType indicesMajorArgs
|
||||
|
|
|
|||
|
|
@ -12,22 +12,6 @@ public section
|
|||
|
||||
namespace Lean.Elab.Structural
|
||||
|
||||
structure State where
|
||||
/-- As part of the inductive predicates case, we keep adding more and more discriminants from the
|
||||
local context and build up a bigger matcher application until we reach a fixed point.
|
||||
As a side-effect, this creates matchers. Here we capture all these side-effects, because
|
||||
the construction rolls back any changes done to the environment and the side-effects
|
||||
need to be replayed. -/
|
||||
addMatchers : Array (MetaM Unit) := #[]
|
||||
|
||||
abbrev M := StateRefT State MetaM
|
||||
|
||||
instance : Inhabited (M α) where
|
||||
default := throwError "failed"
|
||||
|
||||
def run (x : M α) (s : State := {}) : MetaM (α × State) :=
|
||||
StateRefT'.run x s
|
||||
|
||||
/--
|
||||
Return true iff `e` contains an application `recFnName .. t ..` where the term `t` is
|
||||
the argument we are trying to recurse on, and it contains loose bound variables.
|
||||
|
|
|
|||
|
|
@ -235,9 +235,27 @@ def allCombinations (xss : Array (Array α)) : Option (Array (Array α)) :=
|
|||
some (go 0 #[])
|
||||
|
||||
|
||||
def tryAllArgs (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs : Array Expr)
|
||||
(values : Array Expr) (termMeasure?s : Array (Option TerminationMeasure)) (k : Array RecArgInfo → M α) : M α := do
|
||||
/-- A candidate argument combination to try for structural recursion. -/
|
||||
structure RecArgCandidate where
|
||||
group : IndGroupInst
|
||||
comb : Array RecArgInfo
|
||||
|
||||
/-- Result of `findRecArgCandidates`: candidate combinations and a diagnostic report. -/
|
||||
structure RecArgCandidates where
|
||||
candidates : Array RecArgCandidate
|
||||
report : MessageData
|
||||
|
||||
/--
|
||||
Precompute all candidate argument combinations for structural recursion.
|
||||
This performs the analysis that may need function axioms in the environment
|
||||
(via `isDefEq`, `inferType`, etc.) but does not run the callback that
|
||||
attempts to eliminate mutual recursion.
|
||||
-/
|
||||
def findRecArgCandidates (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs : Array Expr)
|
||||
(values : Array Expr) (termMeasure?s : Array (Option TerminationMeasure)) :
|
||||
MetaM RecArgCandidates := do
|
||||
let mut report := m!""
|
||||
let mut candidates := #[]
|
||||
-- Gather information on all possible recursive arguments
|
||||
let mut recArgInfoss := #[]
|
||||
for fnName in fnNames, value in values, termMeasure? in termMeasure?s, fixedParamPerm in fixedParamPerms.perms do
|
||||
|
|
@ -263,23 +281,30 @@ def tryAllArgs (fnNames : Array Name) (fixedParamPerms : FixedParamPerms) (xs :
|
|||
continue
|
||||
if let some combs := allCombinations recArgInfoss' then
|
||||
for comb in combs do
|
||||
try
|
||||
-- Check that the group actually has a brecOn (we used to check this in getRecArgInfo,
|
||||
-- but in the first phase we do not want to rule-out non-recursive types like `Array`, which
|
||||
-- are ok in a nested group. This logic can maybe simplified)
|
||||
unless (← hasConst (group.brecOnName 0)) do
|
||||
throwError "the type {group} does not have a `.brecOn` recursor"
|
||||
let r ← k comb
|
||||
trace[Elab.definition.structural] "tryAllArgs report:\n{report}"
|
||||
return r
|
||||
catch e =>
|
||||
let m ← prettyParameterSet fnNames xs values comb
|
||||
report := report ++ m!"Cannot use {m}:{indentD e.toMessageData}\n"
|
||||
candidates := candidates.push { group, comb }
|
||||
else
|
||||
report := report ++ m!"Too many possible combinations of parameters of type {group} (or " ++
|
||||
m!"please indicate the recursive argument explicitly using `termination_by structural`).\n"
|
||||
report := report ++ m!"Too many possible combinations of parameters of type {group} (or " ++
|
||||
m!"please indicate the recursive argument explicitly using `termination_by structural`).\n"
|
||||
return { candidates, report }
|
||||
|
||||
/--
|
||||
Try each candidate argument combination for structural recursion.
|
||||
Uses `commitIfNoEx` to backtrack on failure.
|
||||
-/
|
||||
def tryCandidates (fnNames : Array Name) (xs : Array Expr) (values : Array Expr)
|
||||
(candidates : RecArgCandidates) (k : Array RecArgInfo → MetaM α) : MetaM α := do
|
||||
let mut report := candidates.report
|
||||
for candidate in candidates.candidates do
|
||||
try
|
||||
return ← commitIfNoEx do
|
||||
unless (← hasConst (candidate.group.brecOnName 0)) do
|
||||
throwError "the type {candidate.group} does not have a `.brecOn` recursor"
|
||||
k candidate.comb
|
||||
catch e =>
|
||||
let m ← prettyParameterSet fnNames xs values candidate.comb
|
||||
report := report ++ m!"Cannot use {m}:{indentD e.toMessageData}\n"
|
||||
report := m!"failed to infer structural recursion:\n" ++ report
|
||||
trace[Elab.definition.structural] "tryAllArgs:\n{report}"
|
||||
trace[Elab.definition.structural] "tryCandidates:\n{report}"
|
||||
throwError report
|
||||
|
||||
end Lean.Elab.Structural
|
||||
|
|
|
|||
|
|
@ -43,12 +43,15 @@ def replaceIndPredRecApp (recArgInfo : RecArgInfo) (ctx : RecursionContext) (fid
|
|||
let recApp := andProj pos positions[motiveIdx]!.size recApp
|
||||
return mkAppN recApp ys
|
||||
|
||||
/-- Monad for inductive predicate recursion that accumulates matcher creation side-effects. -/
|
||||
private abbrev IndPredM := StateRefT (Array (MetaM Unit)) MetaM
|
||||
|
||||
partial def replaceIndPredRecApps (recArgInfos : Array RecArgInfo) (positions : Positions)
|
||||
(params : Array Expr) (ctx : RecursionContext) (e : Expr) : M Expr := do
|
||||
(params : Array Expr) (ctx : RecursionContext) (e : Expr) : IndPredM Expr := do
|
||||
let recFnNames := recArgInfos.map (·.fnName)
|
||||
let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnNames) M Bool :=
|
||||
let containsRecFn (e : Expr) : StateRefT (HasConstCache recFnNames) IndPredM Bool :=
|
||||
modifyGet (·.contains e)
|
||||
let rec loop (ctx : RecursionContext) (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr := do
|
||||
let rec loop (ctx : RecursionContext) (e : Expr) : StateRefT (HasConstCache recFnNames) IndPredM Expr := do
|
||||
unless ← containsRecFn e do
|
||||
return e
|
||||
match e with
|
||||
|
|
@ -68,7 +71,7 @@ partial def replaceIndPredRecApps (recArgInfos : Array RecArgInfo) (positions :
|
|||
return e.updateMData! (← loop ctx b)
|
||||
| .proj _ _ e' => return e.updateProj! (← loop ctx e')
|
||||
| .app _ _ =>
|
||||
let processApp (e : Expr) : StateRefT (HasConstCache recFnNames) M Expr := do
|
||||
let processApp (e : Expr) : StateRefT (HasConstCache recFnNames) IndPredM Expr := do
|
||||
e.withApp fun f args => do
|
||||
let args ← args.mapM (loop ctx)
|
||||
if let .const c _ := f then
|
||||
|
|
@ -84,7 +87,7 @@ partial def replaceIndPredRecApps (recArgInfos : Array RecArgInfo) (positions :
|
|||
IndPredBelow.mkBelowMatcher matcherApp params nrealParams ctx fun ctx e =>
|
||||
g (loop ctx e)
|
||||
if let some (newApp, addMatcher) := matcherResult then
|
||||
modifyThe State fun s => { s with addMatchers := s.addMatchers.push addMatcher }
|
||||
modifyThe (Array (MetaM Unit)) (·.push addMatcher)
|
||||
processApp newApp -- recursive applications may still be hidden in e.g. the discriminants
|
||||
else
|
||||
-- Note: `recArgHasLooseBVarsAt` has false positives, so sometimes everything might stay
|
||||
|
|
@ -99,10 +102,10 @@ partial def replaceIndPredRecApps (recArgInfos : Array RecArgInfo) (positions :
|
|||
Turns `fun a b => x` into `let funType := fun a b => α` (where `x : α`).
|
||||
The continuation is the called with all `funType`s corresponding to the values.
|
||||
-/
|
||||
public def withFunTypes (values : Array Expr) (k : Array Expr → M α) : M α := do
|
||||
public def withFunTypes (values : Array Expr) (k : Array Expr → MetaM α) : MetaM α := do
|
||||
go 0 #[]
|
||||
where
|
||||
go (i : Nat) (res : Array Expr) : M α :=
|
||||
go (i : Nat) (res : Array Expr) : MetaM α :=
|
||||
if h : i < values.size then
|
||||
lambdaTelescope values[i] fun xs value => do
|
||||
let type := (← inferType value).headBeta
|
||||
|
|
@ -117,7 +120,7 @@ where
|
|||
Calculates the `.brecOn` motive corresponding to one structural recursive function.
|
||||
The `value` is the function with (only) the fixed parameters moved into the context.
|
||||
-/
|
||||
public def mkIndPredBRecOnMotive (recArgInfo : RecArgInfo) (value funType : Expr) : M Expr := do
|
||||
public def mkIndPredBRecOnMotive (recArgInfo : RecArgInfo) (value funType : Expr) : MetaM Expr := do
|
||||
lambdaTelescope value fun xs _ => do
|
||||
let type := mkAppN funType xs
|
||||
let (indexMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
|
||||
|
|
@ -130,9 +133,12 @@ The `value` is the function with (only) the fixed parameters moved into the cont
|
|||
The `FType` is the expected type of the argument.
|
||||
The `recArgInfos` is used to transform the body of the function to replace recursive calls with
|
||||
uses of the `below` induction hypothesis.
|
||||
Returns the functional argument and any matchers that were created as side effects.
|
||||
The matchers are created inside `withoutModifyingEnv` and need to be replayed afterwards.
|
||||
-/
|
||||
public def mkIndPredBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positions)
|
||||
(recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) (params : Array Expr) : M Expr := do
|
||||
(recArgInfo : RecArgInfo) (value : Expr) (FType : Expr) (params : Array Expr) :
|
||||
MetaM (Expr × Array (MetaM Unit)) := do
|
||||
lambdaTelescope value fun xs value => do
|
||||
let (indicesMajorArgs, otherArgs) := recArgInfo.pickIndicesMajor xs
|
||||
let FType ← instantiateForall FType indicesMajorArgs
|
||||
|
|
@ -143,8 +149,9 @@ public def mkIndPredBRecOnF (recArgInfos : Array RecArgInfo) (positions : Positi
|
|||
belows := .insert {} indicesMajorArgs.back!.fvarId! (belowName, below)
|
||||
motives := {}
|
||||
}
|
||||
let valueNew ← withDeclNameForAuxNaming recArgInfo.fnName <|
|
||||
replaceIndPredRecApps recArgInfos positions params ctx value
|
||||
mkLambdaFVars (indicesMajorArgs ++ #[below] ++ otherArgs) valueNew
|
||||
let (valueNew, matchers) ← (withDeclNameForAuxNaming recArgInfo.fnName <|
|
||||
replaceIndPredRecApps recArgInfos positions params ctx value).run #[]
|
||||
let expr ← mkLambdaFVars (indicesMajorArgs ++ #[below] ++ otherArgs) valueNew
|
||||
return (expr, matchers)
|
||||
|
||||
end Lean.Elab.Structural
|
||||
|
|
|
|||
|
|
@ -21,9 +21,25 @@ namespace Lean.Elab
|
|||
namespace Structural
|
||||
open Meta
|
||||
|
||||
/--
|
||||
Temporarily adds the recursive functions as axioms to the environment and runs the given action.
|
||||
The environment is restored afterwards, so no persistent changes (e.g. auxiliary definitions) can
|
||||
be made inside the action.
|
||||
|
||||
This is needed around any `MetaM` code that may try to infer the type of, or unfold, expressions
|
||||
that still mention the recursive function constants (e.g. `isDefEq`, `inferType`, `whnf` on
|
||||
arguments of recursive calls). Without these axioms, the kernel would reject the unknown constants.
|
||||
-/
|
||||
private def withRecFunsAsAxioms [Monad n] [MonadLiftT MetaM n] [MonadEnv n] [MonadFinally n]
|
||||
(preDefs : Array PreDefinition) (k : n α) : n α :=
|
||||
withoutModifyingEnv do
|
||||
preDefs.forM (liftM <| addAsAxiom ·)
|
||||
k
|
||||
|
||||
private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms : FixedParamPerms)
|
||||
(xs : Array Expr) (recArgInfos : Array RecArgInfo) : M (Array PreDefinition) := do
|
||||
(xs : Array Expr) (recArgInfos : Array RecArgInfo) : MetaM (Array PreDefinition) := do
|
||||
let values ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda ·.value xs)
|
||||
let fnTypes ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateForall ·.type xs)
|
||||
let indInfo ← getConstInfoInduct recArgInfos[0]!.indGroupInst.all[0]!
|
||||
|
||||
-- Groups the (indices of the) definitions by their position in indInfo.all
|
||||
|
|
@ -32,15 +48,16 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms
|
|||
|
||||
let isIndPred ← isInductivePredicate indInfo.name
|
||||
|
||||
let withFunTypesAndMotives (k : Array Expr → Array Expr → M (Array PreDefinition)) :
|
||||
M (Array PreDefinition) := do
|
||||
let withFunTypesAndMotives (k : Array Expr → Array Expr → MetaM (Array PreDefinition)) :
|
||||
MetaM (Array PreDefinition) := do
|
||||
if isIndPred then
|
||||
withFunTypes values fun funTypes => do
|
||||
let motives ← recArgInfos.mapIdxM fun idx r =>
|
||||
mkIndPredBRecOnMotive r values[idx]! funTypes[idx]!
|
||||
k funTypes motives
|
||||
else
|
||||
let motives ← recArgInfos.zipWithM (bs := values) fun r v => mkBRecOnMotive r v
|
||||
let motives ← recArgInfos.mapIdxM fun idx r =>
|
||||
mkBRecOnMotive r values[idx]! fnTypes[idx]!
|
||||
k #[] motives
|
||||
withFunTypesAndMotives fun funTypes motives => do
|
||||
trace[Elab.definition.structural] "funTypes: {funTypes}, motives: {motives}"
|
||||
|
|
@ -49,13 +66,19 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms
|
|||
let FTypes ← inferBRecOnFTypes recArgInfos positions brecOnConst
|
||||
trace[Elab.definition.structural] "FTypes: {FTypes}"
|
||||
|
||||
-- `withRecFunsAsAxioms` is needed for `replaceRecApps`/`replaceIndPredRecApps` which transform
|
||||
-- recursive calls in the function body.
|
||||
-- For inductive predicates, `mkIndPredBRecOnF` additionally creates matchers as side effects
|
||||
-- (inside `withoutModifyingEnv`); these are replayed immediately after.
|
||||
let FArgs ← recArgInfos.mapIdxM fun idx r =>
|
||||
let v := values[idx]!
|
||||
let t := FTypes[idx]!
|
||||
if isIndPred then
|
||||
mkIndPredBRecOnF recArgInfos positions r v t (brecOnConst 0).getAppArgs
|
||||
if isIndPred then do
|
||||
let (fArg, matchers) ← withRecFunsAsAxioms preDefs do
|
||||
mkIndPredBRecOnF recArgInfos positions r values[idx]! FTypes[idx]! (brecOnConst 0).getAppArgs
|
||||
matchers.forM (·)
|
||||
return fArg
|
||||
else
|
||||
mkBRecOnF recArgInfos positions r v t
|
||||
withRecFunsAsAxioms preDefs do
|
||||
mkBRecOnF recArgInfos positions r values[idx]! FTypes[idx]!
|
||||
trace[Elab.definition.structural] "FArgs: {FArgs}"
|
||||
let brecOn := brecOnConst 0
|
||||
-- the indices and the major premise are not mentioned in the minor premises
|
||||
|
|
@ -74,50 +97,54 @@ private def elimMutualRecursion (preDefs : Array PreDefinition) (fixedParamPerms
|
|||
-- NB: Do not eta-contract here, other code (e.g. FunInd) expects this to have the
|
||||
-- same number of head lambdas as the original definition
|
||||
mkLambdaFVars (fixedParamPerms.perms[i]!.buildArgs xs ys) (valueNew.beta ys)
|
||||
return preDefs.zipWith (bs := valuesNew) fun preDef valueNew => { preDef with value := valueNew }
|
||||
return preDefs.zipWith (bs := valuesNew) fun preDef valueNew =>
|
||||
{ preDef with value := valueNew }
|
||||
|
||||
private def inferRecArgPos (preDefs : Array PreDefinition) (termMeasure?s : Array (Option TerminationMeasure)) :
|
||||
M (Array Nat × Array PreDefinition × FixedParamPerms) := do
|
||||
withoutModifyingEnv do
|
||||
preDefs.forM (addAsAxiom ·)
|
||||
let fnNames := preDefs.map (·.declName)
|
||||
let numSectionVars := preDefs[0]!.numSectionVars
|
||||
let preDefs ← preDefs.mapM fun preDef =>
|
||||
MetaM (Array Nat × Array PreDefinition × FixedParamPerms) := do
|
||||
let fnNames := preDefs.map (·.declName)
|
||||
let numSectionVars := preDefs[0]!.numSectionVars
|
||||
let preDefs ← withRecFunsAsAxioms preDefs do
|
||||
preDefs.mapM fun preDef =>
|
||||
return { preDef with value := (← preprocess preDef.value fnNames numSectionVars) }
|
||||
-- The syntactically fixed arguments
|
||||
let fixedParamPerms ← getFixedParamPerms preDefs
|
||||
let fixedParamPerms ← withRecFunsAsAxioms preDefs do
|
||||
getFixedParamPerms preDefs
|
||||
|
||||
fixedParamPerms.perms[0]!.forallTelescope preDefs[0]!.type fun xs => do
|
||||
let values ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda ·.value xs)
|
||||
fixedParamPerms.perms[0]!.forallTelescope preDefs[0]!.type fun xs => do
|
||||
let values ← preDefs.mapIdxM (fixedParamPerms.perms[·]!.instantiateLambda ·.value xs)
|
||||
|
||||
tryAllArgs fnNames fixedParamPerms xs values termMeasure?s fun recArgInfos => do
|
||||
let recArgPoss := recArgInfos.map (·.recArgPos)
|
||||
trace[Elab.definition.structural] "Trying argument set {recArgPoss}"
|
||||
let (fixedParamPerms', xs', toErase) := fixedParamPerms.erase xs (recArgInfos.map (·.indicesAndRecArgPos))
|
||||
-- We may have to turn some fixed parameters into varying parameters
|
||||
let recArgInfos := recArgInfos.mapIdx fun i recArgInfo =>
|
||||
{recArgInfo with fixedParamPerm := fixedParamPerms'.perms[i]!}
|
||||
if xs'.size != xs.size then
|
||||
trace[Elab.definition.structural] "Reduced fixed params from {xs} to {xs'}, erasing {toErase.map mkFVar}"
|
||||
trace[Elab.definition.structural] "New recArgInfos {repr recArgInfos}"
|
||||
-- Check that the parameters of the IndGroupInsts are still fine
|
||||
for recArgInfo in recArgInfos do
|
||||
for indParam in recArgInfo.indGroupInst.params do
|
||||
for y in toErase do
|
||||
if (← dependsOn indParam y) then
|
||||
if indParam.isFVarOf y then
|
||||
throwError "its type is an inductive datatype and the datatype parameter\
|
||||
{indentExpr indParam}\n\
|
||||
which cannot be fixed as it is an index or depends on an index, and indices \
|
||||
cannot be fixed parameters when using structural recursion."
|
||||
else
|
||||
throwError "its type is an inductive datatype and the datatype parameter\
|
||||
{indentExpr indParam}\ndepends on the function parameter{indentExpr (mkFVar y)}\n\
|
||||
which cannot be fixed as it is an index or depends on an index, and indices \
|
||||
cannot be fixed parameters when using structural recursion."
|
||||
withErasedFVars toErase do
|
||||
let preDefs' ← elimMutualRecursion preDefs fixedParamPerms' xs' recArgInfos
|
||||
return (recArgPoss, preDefs', fixedParamPerms')
|
||||
let candidates ← withRecFunsAsAxioms preDefs do
|
||||
findRecArgCandidates fnNames fixedParamPerms xs values termMeasure?s
|
||||
|
||||
-- `tryCandidates` uses `saveState`/`restoreState` to properly backtrack on failure.
|
||||
tryCandidates fnNames xs values candidates fun recArgInfos => do
|
||||
let recArgPoss := recArgInfos.map (·.recArgPos)
|
||||
trace[Elab.definition.structural] "Trying argument set {recArgPoss}"
|
||||
let (fixedParamPerms', xs', toErase) := fixedParamPerms.erase xs (recArgInfos.map (·.indicesAndRecArgPos))
|
||||
-- We may have to turn some fixed parameters into varying parameters
|
||||
let recArgInfos := recArgInfos.mapIdx fun i recArgInfo =>
|
||||
{recArgInfo with fixedParamPerm := fixedParamPerms'.perms[i]!}
|
||||
if xs'.size != xs.size then
|
||||
trace[Elab.definition.structural] "Reduced fixed params from {xs} to {xs'}, erasing {toErase.map mkFVar}"
|
||||
trace[Elab.definition.structural] "New recArgInfos {repr recArgInfos}"
|
||||
-- Check that the parameters of the IndGroupInsts are still fine
|
||||
for recArgInfo in recArgInfos do
|
||||
for indParam in recArgInfo.indGroupInst.params do
|
||||
for y in toErase do
|
||||
if (← dependsOn indParam y) then
|
||||
if indParam.isFVarOf y then
|
||||
throwError "its type is an inductive datatype and the datatype parameter\
|
||||
{indentExpr indParam}\n\
|
||||
which cannot be fixed as it is an index or depends on an index, and indices \
|
||||
cannot be fixed parameters when using structural recursion."
|
||||
else
|
||||
throwError "its type is an inductive datatype and the datatype parameter\
|
||||
{indentExpr indParam}\ndepends on the function parameter{indentExpr (mkFVar y)}\n\
|
||||
which cannot be fixed as it is an index or depends on an index, and indices \
|
||||
cannot be fixed parameters when using structural recursion."
|
||||
withErasedFVars toErase do
|
||||
let preDefsNonRec ← elimMutualRecursion preDefs fixedParamPerms' xs' recArgInfos
|
||||
return (recArgPoss, preDefsNonRec, fixedParamPerms')
|
||||
|
||||
def reportTermMeasure (preDef : PreDefinition) (recArgPos : Nat) : MetaM Unit := do
|
||||
if let some ref := preDef.termination.terminationBy?? then
|
||||
|
|
@ -132,10 +159,9 @@ def structuralRecursion
|
|||
(termMeasure?s : Array (Option TerminationMeasure)) :
|
||||
TermElabM Unit := do
|
||||
let names := preDefs.map (·.declName)
|
||||
let ((recArgPoss, preDefsNonRec, fixedParamPerms), state) ← run <| inferRecArgPos preDefs termMeasure?s
|
||||
let (recArgPoss, preDefsNonRec, fixedParamPerms) ← inferRecArgPos preDefs termMeasure?s
|
||||
for recArgPos in recArgPoss, preDef in preDefs do
|
||||
reportTermMeasure preDef recArgPos
|
||||
state.addMatchers.forM liftM
|
||||
preDefsNonRec.forM fun preDefNonRec => do
|
||||
let preDefNonRec ← eraseRecAppSyntax preDefNonRec
|
||||
prependError m!"structural recursion failed, produced type incorrect term" do
|
||||
|
|
|
|||
|
|
@ -255,8 +255,8 @@
|
|||
n_1))
|
||||
(mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n n_1)
|
||||
[Elab.definition.structural] FArgs: [fun {m} x x_1 x_2 =>
|
||||
@mul'.match_1_6 n funType_1 (fun m x x_3 below => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m))
|
||||
m x_2 x x_1
|
||||
@mul'.match_1_10 n funType_1
|
||||
(fun m x x_3 below => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m)) m x_2 x x_1
|
||||
(fun h1 =>
|
||||
@of_eq_true
|
||||
(Power2
|
||||
|
|
@ -282,8 +282,8 @@
|
|||
(@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n_1))
|
||||
(mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n n_1)]
|
||||
[Elab.definition.structural] packedFArgs: [fun {m} x x_1 x_2 =>
|
||||
@mul'.match_1_6 n funType_1 (fun m x x_3 below => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m))
|
||||
m x_2 x x_1
|
||||
@mul'.match_1_10 n funType_1
|
||||
(fun m x x_3 below => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m)) m x_2 x x_1
|
||||
(fun h1 =>
|
||||
@of_eq_true
|
||||
(Power2
|
||||
|
|
@ -308,10 +308,3 @@
|
|||
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat)
|
||||
(@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n_1))
|
||||
(mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n n_1)]
|
||||
[Elab.definition.structural] tryAllArgs report:
|
||||
Not considering parameter n of Ex.Power2.mul':
|
||||
it is unchanged in the recursive calls
|
||||
Cannot use parameter #3:
|
||||
failed to eliminate recursive application
|
||||
@mul' n n✝ h1 h2
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue