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.

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

Remove Callback.failed #1619

Merged
merged 1 commit into from
Dec 13, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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: 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