Skip to content

Commit

Permalink
Remove Callback.failed (#1619)
Browse files Browse the repository at this point in the history
`Callback.failed` is always a no-op, and is not called from anywhere.
This PR removes it.
  • Loading branch information
mbovel authored Dec 13, 2024
1 parent f341bcf commit d1e4909
Show file tree
Hide file tree
Showing 4 changed files with 7 additions and 12 deletions.
2 changes: 0 additions & 2 deletions core/src/main/scala/stainless/frontend/BatchedCallBack.scala
Original file line number Diff line number Diff line change
Expand Up @@ -67,8 +67,6 @@ class BatchedCallBack(components: Seq[Component])(using val context: inox.Contex
}
}

def failed(): Unit = {}

def endExtractions(): Unit = {
def reportProgress(msg: String) =
context.reporter.emit(context.reporter.ProgressMessage(context.reporter.INFO, PreprocessingTag, msg))
Expand Down
14 changes: 7 additions & 7 deletions core/src/main/scala/stainless/frontend/CallBack.scala
Original file line number Diff line number Diff line change
Expand Up @@ -16,12 +16,13 @@ object optKeep extends inox.OptionDef[Seq[String]] {
/**
* Process the extracted units.
*
* Frontends are required to follow this workflow (== one cycle):
* - when starting extracting compilation unit, [[beginExtractions]] should be called once;
* - the [[CallBack.apply]] method after extracting each compilation unit (i.e. a Scala file);
* - the [[CallBack.failed]] method if the compilation unit extraction failed (or it contained errors);
* - finally, the frontend calls [[endExtractions]] to let the CallBack know all the data
* should be available by now.
* During a cycle, a [[Frontend]] should call:
* - [[CallBack.beginExtractions]] once before starting any extraction,
* - [[CallBack.apply]] for each compilation unit that is extracted succeffuly,
* - [[CallBack.endExtractions]] once after all extractions are done, whereas
* there has been errors or not during the extractions.
*
* A compilation unit usually corresponds to one Scala file.
*
* When a compilation unit is recompiled, the callback deals with any potential invalidation of
* existing data without blocking the callee's thread.
Expand All @@ -36,7 +37,6 @@ object optKeep extends inox.OptionDef[Seq[String]] {
trait CallBack {
def beginExtractions(): Unit
def apply(file: String, unit: xt.UnitDef, classes: Seq[xt.ClassDef], functions: Seq[xt.FunDef], typeDefs: Seq[xt.TypeDef]): Unit
def failed(): Unit
def endExtractions(): Unit

def stop(): Unit // Blocking "stop".
Expand Down
2 changes: 0 additions & 2 deletions core/src/main/scala/stainless/frontend/SplitCallBack.scala
Original file line number Diff line number Diff line change
Expand Up @@ -71,8 +71,6 @@ class SplitCallBack(components: Seq[Component])(using override val context: inox
}
}

final override def failed(): Unit = ()

final override def endExtractions(): Unit = {
if (reporter.errorCount != 0) {
reporter.reset()
Expand Down
1 change: 0 additions & 1 deletion frontends/common/src/test/scala/stainless/InputUtils.scala
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,6 @@ trait InputUtils {
val callback = new CallBack {
override def join(): Unit = ()
override def stop(): Unit = ()
override def failed(): Unit = ()
override def getReport = None

override def beginExtractions(): Unit = ()
Expand Down

0 comments on commit d1e4909

Please sign in to comment.