max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: unnecessary termination_by clauses cause warnings, not errors (#4809)

Browse source 
fixes #4804
This commit is contained in:
Joachim Breitner 2024-07-22 22:52:14 +02:00 • committed by GitHub
parent 9f1eb479b0
commit 20c857147c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 20 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Elab/PreDefinition/Main.lean
View file

@ -114,7 +114,7 @@ def checkTerminationByHints (preDefs : Array PreDefinition) : CoreM Unit := do
if !structural && !preDefsWithout.isEmpty then
let m := MessageData.andList (preDefsWithout.toList.map (m!"{·.declName}"))
let doOrDoes := if preDefsWithout.size = 1 then "does" else "do"
logErrorAt termBy.ref (m!"Incomplete set of `termination_by` annotations:\n"++
logErrorAt termBy.ref (m!"incomplete set of `termination_by` annotations:\n"++
m!"This function is mutually with {m}, which {doOrDoes} not have " ++
m!"a `termination_by` clause.\n" ++
m!"The present clause is ignored.")

10
src/Lean/Elab/PreDefinition/TerminationHint.lean
View file

@ -57,18 +57,18 @@ structure TerminationHints where
def TerminationHints.none : TerminationHints := ⟨.missing, .none, .none, .none, 0⟩
/-- Logs warnings when the `TerminationHints` are present. -/
/-- Logs warnings when the `TerminationHints` are unexpectedly present. -/
def TerminationHints.ensureNone (hints : TerminationHints) (reason : String) : CoreM Unit := do
match hints.terminationBy??, hints.terminationBy?, hints.decreasingBy? with
| .none, .none, .none => pure ()
| .none, .none, .some dec_by =>
logErrorAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
logWarningAt dec_by.ref m!"unused `decreasing_by`, function is {reason}"
| .some term_by?, .none, .none =>
logErrorAt term_by? m!"unused `termination_by?`, function is {reason}"
logWarningAt term_by? m!"unused `termination_by?`, function is {reason}"
| .none, .some term_by, .none =>
logErrorAt term_by.ref m!"unused `termination_by`, function is {reason}"
logWarningAt term_by.ref m!"unused `termination_by`, function is {reason}"
| _, _, _ =>
logErrorAt hints.ref m!"unused termination hints, function is {reason}"
logWarningAt hints.ref m!"unused termination hints, function is {reason}"
/-- True if any form of termination hint is present. -/
def TerminationHints.isNotNone (hints : TerminationHints) : Bool :=

28
tests/lean/termination_by.lean.expected.out
View file

@ -1,20 +1,20 @@
termination_by.lean:9:2-9:18: error: unused `termination_by`, function is not recursive
termination_by.lean:12:2-12:21: error: unused `decreasing_by`, function is not recursive
termination_by.lean:15:2-16:21: error: unused termination hints, function is not recursive
termination_by.lean:19:2-19:18: error: unused `termination_by`, function is partial
termination_by.lean:22:2-22:21: error: unused `decreasing_by`, function is partial
termination_by.lean:25:2-26:21: error: unused termination hints, function is partial
termination_by.lean:29:0-29:16: error: unused `termination_by`, function is unsafe
termination_by.lean:32:2-32:21: error: unused `decreasing_by`, function is unsafe
termination_by.lean:35:2-36:21: error: unused termination hints, function is unsafe
termination_by.lean:40:4-40:20: error: unused `termination_by`, function is not recursive
termination_by.lean:44:4-44:20: error: unused `termination_by`, function is not recursive
termination_by.lean:54:2-54:18: error: unused `termination_by`, function is not recursive
termination_by.lean:62:2-62:23: error: Incomplete set of `termination_by` annotations:
termination_by.lean:9:2-9:18: warning: unused `termination_by`, function is not recursive
termination_by.lean:12:2-12:21: warning: unused `decreasing_by`, function is not recursive
termination_by.lean:15:2-16:21: warning: unused termination hints, function is not recursive
termination_by.lean:19:2-19:18: warning: unused `termination_by`, function is partial
termination_by.lean:22:2-22:21: warning: unused `decreasing_by`, function is partial
termination_by.lean:25:2-26:21: warning: unused termination hints, function is partial
termination_by.lean:29:0-29:16: warning: unused `termination_by`, function is unsafe
termination_by.lean:32:2-32:21: warning: unused `decreasing_by`, function is unsafe
termination_by.lean:35:2-36:21: warning: unused termination hints, function is unsafe
termination_by.lean:40:4-40:20: warning: unused `termination_by`, function is not recursive
termination_by.lean:44:4-44:20: warning: unused `termination_by`, function is not recursive
termination_by.lean:54:2-54:18: warning: unused `termination_by`, function is not recursive
termination_by.lean:62:2-62:23: error: incomplete set of `termination_by` annotations:
This function is mutually with isOdd, which does not have a `termination_by` clause.
The present clause is ignored.
Try this: termination_by x1 => x1
termination_by.lean:79:2-79:27: error: Incomplete set of `termination_by` annotations:
termination_by.lean:79:2-79:27: error: incomplete set of `termination_by` annotations:
This function is mutually with Test.f, Test.h and Test.i, which do not have a `termination_by` clause.
The present clause is ignored.
termination_by.lean:101:2-101:27: error: Invalid `termination_by`; this function is mutually recursive with Test2.f, which is marked as `termination_by structural` so this one also needs to be marked `structural`.