refactor: pass Measures around as Expr in GuessLex (#3665)
this refactor prepares GuessLex to be able to infer more complex termination arguments. As a side-effect it fixes an (obscure) bug where `sizeOf` would be applied to a term of the wrong type and thus a wrong `SizeOf` instance could be inferred.
This commit is contained in:
Joachim Breitner
GitHub
parent
0ec8862103
commit
f0ff01ae28
4 changed files with 163 additions and 189 deletions
|
|
@ -21,7 +21,7 @@ import Lean.Data.Array
|
|||
/-!
|
||||
This module finds lexicographic termination arguments for well-founded recursion.
|
||||
|
||||
Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`), it tries all combinations
|
||||
Starting with basic measures (`sizeOf xᵢ` for all parameters `xᵢ`) it tries all combinations
|
||||
until it finds one where all proof obligations go through with the given tactic (`decerasing_by`),
|
||||
if given, or the default `decreasing_tactic`.
|
||||
|
||||
|
|
@ -114,6 +114,77 @@ def naryVarNames (xs : Array Name) : MetaM (Array Name) := do
|
|||
else
|
||||
freshen ns (n.appendAfter "'")
|
||||
|
||||
/-- A termination measure with extra fields for use within GuessLex -/
|
||||
structure Measure extends TerminationArgument where
|
||||
/--
|
||||
Like `.fn`, but unconditionally with `sizeOf` at the right type.
|
||||
We use this one when in `evalRecCall`
|
||||
-/
|
||||
natFn : Expr
|
||||
deriving Inhabited
|
||||
|
||||
/-- String desription of this measure -/
|
||||
def Measure.toString (measure : Measure) : MetaM String := do
|
||||
lambdaTelescope measure.fn fun xs e => do
|
||||
let e ← mkLambdaFVars xs[measure.arity:] e -- undo overshooting
|
||||
return (← ppExpr e).pretty
|
||||
|
||||
/--
|
||||
Determine if the measure for parameter `x` should be `sizeOf x` or just `x`.
|
||||
|
||||
For non-mutual definitions, we omit `sizeOf` when the argument does not depend on
|
||||
the other varying parameters, and its `WellFoundedRelation` instance goes via `SizeOf`.
|
||||
|
||||
For mutual definitions, we omit `sizeOf` only when the argument is (at reducible transparency!) of
|
||||
type `Nat` (else we'd have to worry about differently-typed measures from different functions to
|
||||
line up).
|
||||
-/
|
||||
def mayOmitSizeOf (is_mutual : Bool) (args : Array Expr) (x : Expr) : MetaM Bool := do
|
||||
let t ← inferType x
|
||||
if is_mutual
|
||||
then
|
||||
withReducible (isDefEq t (.const `Nat []))
|
||||
else
|
||||
try
|
||||
if t.hasAnyFVar (fun fvar => args.contains (.fvar fvar)) then
|
||||
pure false
|
||||
else
|
||||
let u ← getLevel t
|
||||
let wfi ← synthInstance (.app (.const ``WellFoundedRelation [u]) t)
|
||||
let soi ← synthInstance (.app (.const ``SizeOf [u]) t)
|
||||
isDefEq wfi (mkApp2 (.const ``sizeOfWFRel [u]) t soi)
|
||||
catch _ =>
|
||||
pure false
|
||||
|
||||
/-- Sets the user names for the given freevars in `xs`. -/
|
||||
def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : MetaM α := do
|
||||
let mut lctx ← getLCtx
|
||||
for x in xs, n in ns do lctx := lctx.setUserName x.fvarId! n
|
||||
withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
|
||||
|
||||
/-- Create one measure for each (eligible) parameter of the given predefintion. -/
|
||||
def simpleMeasures (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
|
||||
(userVarNamess : Array (Array Name)) : MetaM (Array (Array Measure)) := do
|
||||
let is_mutual : Bool := preDefs.size > 1
|
||||
preDefs.mapIdxM fun funIdx preDef => do
|
||||
lambdaTelescope preDef.value fun xs _ => do
|
||||
withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
|
||||
let mut ret : Array Measure := #[]
|
||||
for x in xs[fixedPrefixSize:] do
|
||||
-- If the `SizeOf` instance produces a constant (e.g. because it's type is a `Prop` or
|
||||
-- `Type`), then ignore this parameter
|
||||
let sizeOf ← whnfD (← mkAppM ``sizeOf #[x])
|
||||
if sizeOf.isLit then continue
|
||||
|
||||
let natFn ← mkLambdaFVars xs (← mkAppM ``sizeOf #[x])
|
||||
-- Determine if we need to exclude `sizeOf` in the measure we show/pass on.
|
||||
let fn ←
|
||||
if ← mayOmitSizeOf is_mutual xs[fixedPrefixSize:] x
|
||||
then mkLambdaFVars xs x
|
||||
else pure natFn
|
||||
let extraParams := preDef.termination.extraParams
|
||||
ret := ret.push { ref := .missing, fn, natFn, arity := xs.size, extraParams }
|
||||
return ret
|
||||
|
||||
/-- Internal monad used by `withRecApps` -/
|
||||
abbrev M (recFnName : Name) (α β : Type) : Type :=
|
||||
|
|
@ -224,11 +295,11 @@ structure RecCallWithContext where
|
|||
ref : Syntax
|
||||
/-- Function index of caller -/
|
||||
caller : Nat
|
||||
/-- Parameters of caller -/
|
||||
/-- Parameters of caller (including fixed prefix) -/
|
||||
params : Array Expr
|
||||
/-- Function index of callee -/
|
||||
callee : Nat
|
||||
/-- Arguments to callee -/
|
||||
/-- Arguments to callee (including fixed prefix) -/
|
||||
args : Array Expr
|
||||
ctxt : SavedLocalContext
|
||||
|
||||
|
|
@ -260,7 +331,8 @@ def filterSubsumed (rcs : Array RecCallWithContext ) : Array RecCallWithContext
|
|||
return (false, true)
|
||||
return (true, true)
|
||||
|
||||
/-- Traverse a unary PreDefinition, and returns a `WithRecCall` closure for each recursive
|
||||
/--
|
||||
Traverse a unary `PreDefinition`, and returns a `WithRecCall` closure for each recursive
|
||||
call site.
|
||||
-/
|
||||
def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat)
|
||||
|
|
@ -270,6 +342,7 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat)
|
|||
unless xs.size == fixedPrefixSize + 1 do
|
||||
-- Maybe cleaner to have lambdaBoundedTelescope?
|
||||
throwError "Unexpected number of lambdas in unary pre-definition"
|
||||
let ys := xs[:fixedPrefixSize]
|
||||
let param := xs[fixedPrefixSize]!
|
||||
withRecApps unaryPreDef.declName fixedPrefixSize param body fun param args => do
|
||||
unless args.size ≥ fixedPrefixSize + 1 do
|
||||
|
|
@ -278,7 +351,7 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat)
|
|||
trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})"
|
||||
let (caller, params) ← argsPacker.unpack param
|
||||
let (callee, args) ← argsPacker.unpack arg
|
||||
RecCallWithContext.create (← getRef) caller params callee args
|
||||
RecCallWithContext.create (← getRef) caller (ys ++ params) callee (ys ++ args)
|
||||
|
||||
/-- A `GuessLexRel` described how a recursive call affects a measure; whether it
|
||||
decreases strictly, non-strictly, is equal, or else. -/
|
||||
|
|
@ -301,31 +374,18 @@ def GuessLexRel.toNatRel : GuessLexRel → Expr
|
|||
| le => mkAppN (mkConst ``LE.le [levelZero]) #[mkConst ``Nat, mkConst ``instLENat]
|
||||
| no_idea => unreachable!
|
||||
|
||||
/--
|
||||
Given an expression `e`, produce `sizeOf e` with a suitable instance.
|
||||
NB: We must use the instance of the type of the function parameter!
|
||||
The concrete argument at hand may have a different (still def-eq) typ.
|
||||
-/
|
||||
def mkSizeOf (e : Expr) : MetaM Expr := do
|
||||
let ty ← inferType e
|
||||
let lvl ← getLevel ty
|
||||
let inst ← synthInstance (mkAppN (mkConst ``SizeOf [lvl]) #[ty])
|
||||
let res := mkAppN (mkConst ``sizeOf [lvl]) #[ty, inst, e]
|
||||
check res
|
||||
return res
|
||||
|
||||
/--
|
||||
For a given recursive call, and a choice of parameter and argument index,
|
||||
try to prove equality, < or ≤.
|
||||
-/
|
||||
def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext)
|
||||
(paramIdx argIdx : Nat) : MetaM GuessLexRel := do
|
||||
def evalRecCall (decrTactic? : Option DecreasingBy) (callerMeasures calleeMeasures : Array Measure)
|
||||
(rcc : RecCallWithContext) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM GuessLexRel := do
|
||||
rcc.ctxt.run do
|
||||
let param := rcc.params[paramIdx]!
|
||||
let arg := rcc.args[argIdx]!
|
||||
let callerMeasure := callerMeasures[callerMeasureIdx]!
|
||||
let calleeMeasure := calleeMeasures[calleeMeasureIdx]!
|
||||
let param := callerMeasure.natFn.beta rcc.params
|
||||
let arg := calleeMeasure.natFn.beta rcc.args
|
||||
trace[Elab.definition.wf] "inspectRecCall: {rcc.caller} ({param}) → {rcc.callee} ({arg})"
|
||||
let arg ← mkSizeOf rcc.args[argIdx]!
|
||||
let param ← mkSizeOf rcc.params[paramIdx]!
|
||||
for rel in [GuessLexRel.eq, .lt, .le] do
|
||||
let goalExpr := mkAppN rel.toNatRel #[arg, param]
|
||||
trace[Elab.definition.wf] "Goal for {rel}: {goalExpr}"
|
||||
|
|
@ -358,32 +418,35 @@ def evalRecCall (decrTactic? : Option DecreasingBy) (rcc : RecCallWithContext)
|
|||
/- A cache for `evalRecCall` -/
|
||||
structure RecCallCache where mk'' ::
|
||||
decrTactic? : Option DecreasingBy
|
||||
callerMeasures : Array Measure
|
||||
calleeMeasures : Array Measure
|
||||
rcc : RecCallWithContext
|
||||
cache : IO.Ref (Array (Array (Option GuessLexRel)))
|
||||
|
||||
/-- Create a cache to memoize calls to `evalRecCall descTactic? rcc` -/
|
||||
def RecCallCache.mk (decrTactics : Array (Option DecreasingBy))
|
||||
def RecCallCache.mk (decrTactics : Array (Option DecreasingBy)) (measuress : Array (Array Measure))
|
||||
(rcc : RecCallWithContext) :
|
||||
BaseIO RecCallCache := do
|
||||
let decrTactic? := decrTactics[rcc.caller]!
|
||||
let cache ← IO.mkRef <| Array.mkArray rcc.params.size (Array.mkArray rcc.args.size Option.none)
|
||||
return { decrTactic?, rcc, cache }
|
||||
let callerMeasures := measuress[rcc.caller]!
|
||||
let calleeMeasures := measuress[rcc.callee]!
|
||||
let cache ← IO.mkRef <| Array.mkArray callerMeasures.size (Array.mkArray calleeMeasures.size Option.none)
|
||||
return { decrTactic?, callerMeasures, calleeMeasures, rcc, cache }
|
||||
|
||||
/-- Run `evalRecCall` and cache there result -/
|
||||
def RecCallCache.eval (rc: RecCallCache) (paramIdx argIdx : Nat) : MetaM GuessLexRel := do
|
||||
def RecCallCache.eval (rc: RecCallCache) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM GuessLexRel := do
|
||||
-- Check the cache first
|
||||
if let Option.some res := (← rc.cache.get)[paramIdx]![argIdx]! then
|
||||
if let Option.some res := (← rc.cache.get)[callerMeasureIdx]![calleeMeasureIdx]! then
|
||||
return res
|
||||
else
|
||||
let res ← evalRecCall rc.decrTactic? rc.rcc paramIdx argIdx
|
||||
rc.cache.modify (·.modify paramIdx (·.set! argIdx res))
|
||||
let res ← evalRecCall rc.decrTactic? rc.callerMeasures rc.calleeMeasures rc.rcc callerMeasureIdx calleeMeasureIdx
|
||||
rc.cache.modify (·.modify callerMeasureIdx (·.set! calleeMeasureIdx res))
|
||||
return res
|
||||
|
||||
|
||||
/-- Print a single cache entry as a string, without forcing it -/
|
||||
def RecCallCache.prettyEntry (rcc : RecCallCache) (paramIdx argIdx : Nat) : MetaM String := do
|
||||
def RecCallCache.prettyEntry (rcc : RecCallCache) (callerMeasureIdx calleeMeasureIdx : Nat) : MetaM String := do
|
||||
let cachedEntries ← rcc.cache.get
|
||||
return match cachedEntries[paramIdx]![argIdx]! with
|
||||
return match cachedEntries[callerMeasureIdx]![calleeMeasureIdx]! with
|
||||
| .some rel => toString rel
|
||||
| .none => "_"
|
||||
|
||||
|
|
@ -397,10 +460,10 @@ inductive MutualMeasure where
|
|||
|
||||
/-- Evaluate a recursive call at a given `MutualMeasure` -/
|
||||
def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel
|
||||
| .args argIdxs => do
|
||||
let paramIdx := argIdxs[rc.rcc.caller]!
|
||||
let argIdx := argIdxs[rc.rcc.callee]!
|
||||
rc.eval paramIdx argIdx
|
||||
| .args taIdxs => do
|
||||
let callerMeasureIdx := taIdxs[rc.rcc.caller]!
|
||||
let calleeMeasureIdx := taIdxs[rc.rcc.callee]!
|
||||
rc.eval callerMeasureIdx calleeMeasureIdx
|
||||
| .func funIdx => do
|
||||
if rc.rcc.caller == funIdx && rc.rcc.callee != funIdx then
|
||||
return .lt
|
||||
|
|
@ -409,97 +472,29 @@ def inspectCall (rc : RecCallCache) : MutualMeasure → MetaM GuessLexRel
|
|||
else
|
||||
return .eq
|
||||
|
||||
/--
|
||||
Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`,
|
||||
where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `sizeOf yᵢ` reduces to a literal.
|
||||
This is the case for types such as `Prop`, `Type u`, etc.
|
||||
These arguments should not be considered when guessing a well-founded relation.
|
||||
See `generateCombinations?`
|
||||
-/
|
||||
def getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
|
||||
lambdaTelescope preDef.value fun xs _ => do
|
||||
let mut result := #[]
|
||||
for x in xs[fixedPrefixSize:], i in [:xs.size] do
|
||||
try
|
||||
let sizeOf ← whnfD (← mkAppM ``sizeOf #[x])
|
||||
if sizeOf.isLit then
|
||||
result := result.push i
|
||||
catch _ =>
|
||||
result := result.push i
|
||||
return result
|
||||
|
||||
/--
|
||||
Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`,
|
||||
where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff the
|
||||
`WellFoundedRelation` of `aᵢ` goes via `SizeOf`, and `aᵢ` does not depend on `y₁`….
|
||||
Generate all combination of measures. Assumes we have numbered the measures of each function,
|
||||
and their counts is in `numMeasures`.
|
||||
|
||||
These are the parameters for which we omit an explicit call to `sizeOf` in the termination argument.
|
||||
|
||||
We only use this in the non-mutual case; in the mutual case we would have to additional check
|
||||
if the parameters that line up in the actual `TerminationWF` have the same type.
|
||||
-/
|
||||
def getSizeOfParams (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
|
||||
lambdaTelescope preDef.value fun xs _ => do
|
||||
let xs : Array Expr := xs[fixedPrefixSize:]
|
||||
let mut result := #[]
|
||||
for x in xs, i in [:xs.size] do
|
||||
try
|
||||
let t ← inferType x
|
||||
if t.hasAnyFVar (fun fvar => xs.contains (.fvar fvar)) then continue
|
||||
let u ← getLevel t
|
||||
let wfi ← synthInstance (.app (.const ``WellFoundedRelation [u]) t)
|
||||
let soi ← synthInstance (.app (.const ``SizeOf [u]) t)
|
||||
if ← isDefEq wfi (mkApp2 (.const ``sizeOfWFRel [u]) t soi) then
|
||||
result := result.push i
|
||||
catch _ =>
|
||||
pure ()
|
||||
return result
|
||||
|
||||
/--
|
||||
Given a predefinition with value `fun (x₁ ... xₙ) (y₁ : α₁)... (yₘ : αₘ) => ...`,
|
||||
where `n = fixedPrefixSize`, return an array `A` s.t. `i ∈ A` iff `aᵢ` is `Nat`.
|
||||
These are parameters where we can definitely omit the call to `sizeOf`.
|
||||
-/
|
||||
def getNatParams (fixedPrefixSize : Nat) (preDef : PreDefinition) : MetaM (Array Nat) :=
|
||||
lambdaTelescope preDef.value fun xs _ => do
|
||||
let xs : Array Expr := xs[fixedPrefixSize:]
|
||||
let mut result := #[]
|
||||
for x in xs, i in [:xs.size] do
|
||||
let t ← inferType x
|
||||
if ← withReducible (isDefEq t (.const `Nat [])) then
|
||||
result := result.push i
|
||||
return result
|
||||
|
||||
/--
|
||||
Generate all combination of arguments, skipping those that are forbidden.
|
||||
|
||||
Sorts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to
|
||||
This puts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to
|
||||
try first, when the mutually recursive functions have similar argument structures
|
||||
-/
|
||||
partial def generateCombinations? (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat)
|
||||
(threshold : Nat := 32) : Option (Array (Array Nat)) :=
|
||||
partial def generateCombinations? (numMeasures : Array Nat) (threshold : Nat := 32) :
|
||||
Option (Array (Array Nat)) :=
|
||||
(do goUniform 0; go 0 #[]) |>.run #[] |>.2
|
||||
where
|
||||
isForbidden (fidx : Nat) (argIdx : Nat) : Bool :=
|
||||
if h : fidx < forbiddenArgs.size then
|
||||
forbiddenArgs[fidx] |>.contains argIdx
|
||||
else
|
||||
false
|
||||
|
||||
-- Enumerate all permissible uniform combinations
|
||||
goUniform (argIdx : Nat) : OptionT (StateM (Array (Array Nat))) Unit := do
|
||||
if numArgs.all (argIdx < ·) then
|
||||
unless forbiddenArgs.any (·.contains argIdx) do
|
||||
modify (·.push (Array.mkArray numArgs.size argIdx))
|
||||
goUniform (argIdx + 1)
|
||||
goUniform (idx : Nat) : OptionT (StateM (Array (Array Nat))) Unit := do
|
||||
if numMeasures.all (idx < ·) then
|
||||
modify (·.push (Array.mkArray numMeasures.size idx))
|
||||
goUniform (idx + 1)
|
||||
|
||||
-- Enumerate all other permissible combinations
|
||||
go (fidx : Nat) : OptionT (ReaderT (Array Nat) (StateM (Array (Array Nat)))) Unit := do
|
||||
if h : fidx < numArgs.size then
|
||||
let n := numArgs[fidx]
|
||||
for argIdx in [:n] do
|
||||
unless isForbidden fidx argIdx do
|
||||
withReader (·.push argIdx) (go (fidx + 1))
|
||||
if h : fidx < numMeasures.size then
|
||||
let n := numMeasures[fidx]
|
||||
for idx in [:n] do withReader (·.push idx) (go (fidx + 1))
|
||||
else
|
||||
let comb ← read
|
||||
unless comb.all (· == comb[0]!) do
|
||||
|
|
@ -507,19 +502,19 @@ where
|
|||
if (← get).size > threshold then
|
||||
failure
|
||||
|
||||
|
||||
/--
|
||||
Enumerate all meausures we want to try: All arguments (resp. combinations thereof) and
|
||||
Enumerate all meausures we want to try.
|
||||
|
||||
All arguments (resp. combinations thereof) and
|
||||
possible orderings of functions (if more than one)
|
||||
-/
|
||||
def generateMeasures (forbiddenArgs : Array (Array Nat)) (arities : Array Nat) :
|
||||
MetaM (Array MutualMeasure) := do
|
||||
let some arg_measures := generateCombinations? forbiddenArgs arities
|
||||
def generateMeasures (numTermArgs : Array Nat) : MetaM (Array MutualMeasure) := do
|
||||
let some arg_measures := generateCombinations? numTermArgs
|
||||
| throwError "Too many combinations"
|
||||
|
||||
let func_measures :=
|
||||
if arities.size > 1 then
|
||||
(List.range arities.size).toArray
|
||||
if numTermArgs.size > 1 then
|
||||
(List.range numTermArgs.size).toArray
|
||||
else
|
||||
#[]
|
||||
|
||||
|
|
@ -609,19 +604,19 @@ def RecCallWithContext.posString (rcc : RecCallWithContext) : MetaM String := do
|
|||
|
||||
|
||||
/-- Explain what we found out about the recursive calls (non-mutual case) -/
|
||||
def explainNonMutualFailure (varNames : Array Name) (rcs : Array RecCallCache) : MetaM Format := do
|
||||
let header := varNames.map (·.eraseMacroScopes.toString)
|
||||
def explainNonMutualFailure (measures : Array Measure) (rcs : Array RecCallCache) : MetaM Format := do
|
||||
let header ← measures.mapM Measure.toString
|
||||
let mut table : Array (Array String) := #[#[""] ++ header]
|
||||
for i in [:rcs.size], rc in rcs do
|
||||
let mut row := #[s!"{i+1}) {← rc.rcc.posString}"]
|
||||
for argIdx in [:varNames.size] do
|
||||
for argIdx in [:measures.size] do
|
||||
row := row.push (← rc.prettyEntry argIdx argIdx)
|
||||
table := table.push row
|
||||
|
||||
return formatTable table
|
||||
|
||||
/-- Explain what we found out about the recursive calls (mutual case) -/
|
||||
def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name))
|
||||
def explainMutualFailure (declNames : Array Name) (measuress : Array (Array Measure))
|
||||
(rcs : Array RecCallCache) : MetaM Format := do
|
||||
let mut r := Format.nil
|
||||
|
||||
|
|
@ -631,33 +626,33 @@ def explainMutualFailure (declNames : Array Name) (varNamess : Array (Array Name
|
|||
r := r ++ f!"Call from {declNames[caller]!} to {declNames[callee]!} " ++
|
||||
f!"at {← rc.rcc.posString}:\n"
|
||||
|
||||
let header := varNamess[caller]!.map (·.eraseMacroScopes.toString)
|
||||
let header ← measuress[caller]!.mapM Measure.toString
|
||||
let mut table : Array (Array String) := #[#[""] ++ header]
|
||||
if caller = callee then
|
||||
-- For self-calls, only the diagonal is interesting, so put it into one row
|
||||
let mut row := #[""]
|
||||
for argIdx in [:varNamess[caller]!.size] do
|
||||
for argIdx in [:measuress[caller]!.size] do
|
||||
row := row.push (← rc.prettyEntry argIdx argIdx)
|
||||
table := table.push row
|
||||
else
|
||||
for argIdx in [:varNamess[callee]!.size] do
|
||||
for argIdx in [:measuress[callee]!.size] do
|
||||
let mut row := #[]
|
||||
row := row.push varNamess[callee]![argIdx]!.eraseMacroScopes.toString
|
||||
for paramIdx in [:varNamess[caller]!.size] do
|
||||
row := row.push (← measuress[callee]![argIdx]!.toString)
|
||||
for paramIdx in [:measuress[caller]!.size] do
|
||||
row := row.push (← rc.prettyEntry paramIdx argIdx)
|
||||
table := table.push row
|
||||
r := r ++ formatTable table ++ "\n"
|
||||
|
||||
return r
|
||||
|
||||
def explainFailure (declNames : Array Name) (varNamess : Array (Array Name))
|
||||
def explainFailure (declNames : Array Name) (measuress : Array (Array Measure))
|
||||
(rcs : Array RecCallCache) : MetaM Format := do
|
||||
let mut r : Format := "The arguments relate at each recursive call as follows:\n" ++
|
||||
"(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)\n"
|
||||
if declNames.size = 1 then
|
||||
r := r ++ (← explainNonMutualFailure varNamess[0]! rcs)
|
||||
r := r ++ (← explainNonMutualFailure measuress[0]! rcs)
|
||||
else
|
||||
r := r ++ (← explainMutualFailure declNames varNamess rcs)
|
||||
r := r ++ (← explainMutualFailure declNames measuress rcs)
|
||||
return r
|
||||
|
||||
/--
|
||||
|
|
@ -671,25 +666,16 @@ def mkProdElem (xs : Array Expr) : MetaM Expr := do
|
|||
let n := xs.size
|
||||
xs[0:n-1].foldrM (init:=xs[n-1]!) fun x p => mkAppM ``Prod.mk #[x,p]
|
||||
|
||||
def withUserNames {α} (xs : Array Expr) (ns : Array Name) (k : MetaM α) : MetaM α := do
|
||||
let mut lctx ← getLCtx
|
||||
for x in xs, n in ns do lctx := lctx.setUserName x.fvarId! n
|
||||
withTheReader Meta.Context (fun ctx => { ctx with lctx }) k
|
||||
|
||||
def toTerminationArguments (preDefs : Array PreDefinition) (fixedPrefixSize : Nat)
|
||||
(userVarNamess : Array (Array Name)) (needsNoSizeOf : Array (Array Nat))
|
||||
(userVarNamess : Array (Array Name)) (measuress : Array (Array Measure))
|
||||
(solution : Array MutualMeasure) : MetaM TerminationArguments := do
|
||||
preDefs.mapIdxM fun funIdx preDef => do
|
||||
let measures := measuress[funIdx]!
|
||||
lambdaTelescope preDef.value fun xs _ => do
|
||||
withUserNames xs[fixedPrefixSize:] userVarNamess[funIdx]! do
|
||||
let args ← solution.mapM fun
|
||||
| .args varIdxs =>
|
||||
let arg := varIdxs[funIdx]!
|
||||
if needsNoSizeOf[funIdx]!.contains arg then
|
||||
pure xs[fixedPrefixSize + arg]!
|
||||
else
|
||||
mkAppM ``sizeOf #[xs[fixedPrefixSize + arg]!]
|
||||
| .func funIdx' => pure <| mkNatLit <| if funIdx' == funIdx then 1 else 0
|
||||
let args := solution.map fun
|
||||
| .args taIdxs => measures[taIdxs[funIdx]!]!.fn.beta xs
|
||||
| .func funIdx' => mkNatLit <| if funIdx' == funIdx then 1 else 0
|
||||
let fn ← mkLambdaFVars xs (← mkProdElem args)
|
||||
let extraParams := preDef.termination.extraParams
|
||||
return { ref := .missing, arity := xs.size, extraParams, fn}
|
||||
|
|
@ -716,40 +702,36 @@ terminates. See the module doc string for a high-level overview.
|
|||
def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
|
||||
(fixedPrefixSize : Nat) (argsPacker : ArgsPacker) :
|
||||
MetaM TerminationArguments := do
|
||||
let arities := argsPacker.varNamess.map (·.size)
|
||||
let userVarNamess ← argsPacker.varNamess.mapM (naryVarNames ·)
|
||||
trace[Elab.definition.wf] "varNames is: {userVarNamess}"
|
||||
|
||||
let forbiddenArgs ← preDefs.mapM (getForbiddenByTrivialSizeOf fixedPrefixSize ·)
|
||||
let needsNoSizeOf ←
|
||||
if preDefs.size = 1 then
|
||||
preDefs.mapM (getSizeOfParams fixedPrefixSize ·)
|
||||
else
|
||||
preDefs.mapM (getNatParams fixedPrefixSize ·)
|
||||
-- For every function, the meaures we want to use
|
||||
-- (One for each non-forbiddend arg)
|
||||
let measuress ← simpleMeasures preDefs fixedPrefixSize userVarNamess
|
||||
|
||||
-- The list of measures, including the measures that order functions.
|
||||
-- The function ordering measures come last
|
||||
let measures ← generateMeasures forbiddenArgs arities
|
||||
let measures ← generateMeasures (measuress.map (·.size))
|
||||
|
||||
-- If there is only one plausible measure, use that
|
||||
if let #[solution] := measures then
|
||||
let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess needsNoSizeOf #[solution]
|
||||
let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess measuress #[solution]
|
||||
reportTermArgs preDefs termArgs
|
||||
return termArgs
|
||||
|
||||
-- Collect all recursive calls and extract their context
|
||||
let recCalls ← collectRecCalls unaryPreDef fixedPrefixSize argsPacker
|
||||
let recCalls := filterSubsumed recCalls
|
||||
let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) ·)
|
||||
let rcs ← recCalls.mapM (RecCallCache.mk (preDefs.map (·.termination.decreasingBy?)) measuress ·)
|
||||
let callMatrix := rcs.map (inspectCall ·)
|
||||
|
||||
match ← liftMetaM <| solve measures callMatrix with
|
||||
| .some solution => do
|
||||
let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess needsNoSizeOf solution
|
||||
let termArgs ← toTerminationArguments preDefs fixedPrefixSize userVarNamess measuress solution
|
||||
reportTermArgs preDefs termArgs
|
||||
return termArgs
|
||||
| .none =>
|
||||
let explanation ← explainFailure (preDefs.map (·.declName)) userVarNamess rcs
|
||||
let explanation ← explainFailure (preDefs.map (·.declName)) measuress rcs
|
||||
Lean.throwError <| "Could not find a decreasing measure.\n" ++
|
||||
explanation ++ "\n" ++
|
||||
"Please use `termination_by` to specify a decreasing measure."
|
||||
|
|
|
|||
|
|
@ -213,9 +213,9 @@ end MutualNotNat2
|
|||
|
||||
namespace MutualNotNat3
|
||||
-- A varant of the above, but where the type of the parameter refined to `Nat`.
|
||||
-- This tests if `GuessLex` is inferring the `SizeOf` instance based on the type of the
|
||||
-- concrete parameter/argument (wrong, but status quo), or based on the types in the function
|
||||
-- signature (correct, todo)
|
||||
-- Previously `GuessLex` was inferring the `SizeOf` instance based on the type of the
|
||||
-- *concrete* parameter or argument, which was wrong.
|
||||
-- The inference needs to be based on the parameter type in the function's signature.
|
||||
def OddNat3 := Nat
|
||||
instance : SizeOf OddNat3 := ⟨fun n => 42 - @id Nat n⟩
|
||||
@[simp] theorem OddNat3.sizeOf_eq (n : OddNat3) : sizeOf n = 42 - @id Nat n := rfl
|
||||
|
|
|
|||
|
|
@ -54,14 +54,7 @@ Inferred termination argument:
|
|||
termination_by x1 => x1
|
||||
Inferred termination argument:
|
||||
termination_by sizeOf o
|
||||
guessLex.lean:222:0-234:3: error: Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
||||
Call from MutualNotNat3.foo to MutualNotNat3.bar at 226:23-35:
|
||||
x1
|
||||
x1 <
|
||||
Call from MutualNotNat3.bar to MutualNotNat3.foo at 231:30-42:
|
||||
x1
|
||||
x1 ?
|
||||
|
||||
Please use `termination_by` to specify a decreasing measure.
|
||||
Inferred termination argument:
|
||||
termination_by x1 => x1
|
||||
Inferred termination argument:
|
||||
termination_by x1 => sizeOf x1
|
||||
|
|
|
|||
|
|
@ -46,10 +46,10 @@ Please use `termination_by` to specify a decreasing measure.
|
|||
guessLexFailures.lean:37:0-43:31: error: Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
|
||||
n m h x4
|
||||
1) 39:6-27 = = _ =
|
||||
2) 40:6-25 = < _ _
|
||||
3) 41:6-25 < _ _ _
|
||||
n m x4
|
||||
1) 39:6-27 = = =
|
||||
2) 40:6-25 = < _
|
||||
3) 41:6-25 < _ _
|
||||
Please use `termination_by` to specify a decreasing measure.
|
||||
guessLexFailures.lean:48:0-54:31: error: Could not find a decreasing measure.
|
||||
The arguments relate at each recursive call as follows:
|
||||
|
|
@ -79,18 +79,17 @@ Call from Mutual.f to Mutual.g at 63:8-39:
|
|||
n m l
|
||||
n < ? ?
|
||||
m ? = ?
|
||||
H _ _ _
|
||||
l ? ? <
|
||||
Call from Mutual.g to Mutual.g at 68:8-35:
|
||||
n m H l
|
||||
? ? _ =
|
||||
n m l
|
||||
? ? =
|
||||
Call from Mutual.g to Mutual.g at 69:8-33:
|
||||
n m H l
|
||||
_ _ _ <
|
||||
n m l
|
||||
_ _ <
|
||||
Call from Mutual.g to Mutual.h at 70:8-27:
|
||||
n m H l
|
||||
n _ _ _ ?
|
||||
m _ _ _ ?
|
||||
n m l
|
||||
n _ _ ?
|
||||
m _ _ ?
|
||||
Call from Mutual.h to Mutual.f at 75:8-33:
|
||||
n m
|
||||
n _ _
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue