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: unnecessary termination_by clauses cause warnings, not errors #4809

Merged
merged 1 commit into from
Jul 22, 2024
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
2 changes: 1 addition & 1 deletion src/Lean/Elab/PreDefinition/Main.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.")
Expand Down
10 changes: 5 additions & 5 deletions src/Lean/Elab/PreDefinition/TerminationHint.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down
28 changes: 14 additions & 14 deletions tests/lean/termination_by.lean.expected.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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`.
Expand Down
Loading