Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: GuessLex: print inferred termination argument #3012

Merged
merged 6 commits into from
Dec 5, 2023
Merged

feat: GuessLex: print inferred termination argument #3012

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
e902a82
feat: GuessLex: Print inferred termination argument
nomeata Dec 2, 2023
7f8e78f
Add predefs to environment so that `unresolveNameGlobal` works
nomeata Dec 2, 2023
d7a67e7
Move to WF.TerminationHint
nomeata Dec 4, 2023
781f642
Merge branch 'nightly-with-mathlib' of github.com:leanprover/lean4 in…
nomeata Dec 4, 2023
0f95ca4
No need for a space here
nomeata Dec 4, 2023
e1bf2f2
Merge branch 'master' of github.com:leanprover/lean4 into joachim/gue…
nomeata Dec 5, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Move to WF.TerminationHint
  • Loading branch information
@nomeata
nomeata committed Dec 4, 2023
commit d7a67e7c3cec9da4ee6e42f9cc22908efe76a05d
19 changes: 5 additions & 14 deletions src/Lean/Elab/PreDefinition/WF/GuessLex.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -566,19 +566,6 @@ def buildTermWF (declNames : Array Name) (varNamess : Array (Array Name))
}
return .ext termByElements

open Parser.Command in
def delabTermWF (preDefs : Array PreDefinition) : TerminationWF → MetaM Syntax
| .ext elements => do
withoutModifyingState do
preDefs.forM (addAsAxiom ·)
let elementStxs ← elements.mapM fun element => do
let fn : Ident := mkIdent (← unresolveNameGlobal element.declName)
let body : Term := ⟨element.body⟩
let vars : Array Ident := element.vars.map TSyntax.mk
`(terminationByElement|$fn $vars* => $body)
`(terminationBy|termination_by $elementStxs*)
| .core _ => unreachable! -- we don't synthetize termination_by' syntax

end Lean.Elab.WF.GuessLex

namespace Lean.Elab.WF
Expand Down Expand Up @@ -619,8 +606,12 @@ def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
| .some solution => do
let wf ← buildTermWF (preDefs.map (·.declName)) varNamess solution

let wfStx ← withoutModifyingState do
preDefs.forM (addAsAxiom ·)
wf.unexpand

if showInferredTerminationBy.get (← getOptions) then
logInfo m!"Inferred termination argument:{← delabTermWF preDefs wf}"
logInfo m!"Inferred termination argument: {wfStx}"

return wf
| .none => throwError "Cannot find a decreasing lexicographic order"
Expand Down
11 changes: 11 additions & 0 deletions src/Lean/Elab/PreDefinition/WF/TerminationHint.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,6 +152,17 @@ def expandTerminationBy (hint? : Option Syntax) (cliques : Array (Array Name)) :
else
return TerminationBy.core TerminationHint.none

open Parser.Command in
def TerminationWF.unexpand : TerminationWF → MetaM Syntax
| .ext elements => do
let elementStxs ← elements.mapM fun element => do
let fn : Ident := mkIdent (← unresolveNameGlobal element.declName)
let body : Term := ⟨element.body⟩
let vars : Array Ident := element.vars.map TSyntax.mk
`(terminationByElement|$fn $vars* => $body)
`(terminationBy|termination_by $elementStxs*)
| .core _ => unreachable! -- we don't synthetize termination_by' syntax

def TerminationBy.markAsUsed (t : TerminationBy) (cliqueNames : Array Name) : TerminationBy :=
match t with
| core hint => core (hint.markAsUsed cliqueNames)
Expand Down