From 7fb91acdcd047c526aa17e7ecc6ea769775d3c20 Mon Sep 17 00:00:00 2001
From: Matt Bovel <matthieu@bovel.net>
Date: Tue, 10 Dec 2024 21:00:50 +0000
Subject: [PATCH] Remove Callback.failed

---
 .../scala/stainless/frontend/BatchedCallBack.scala |  2 --
 .../main/scala/stainless/frontend/CallBack.scala   | 14 +++++++-------
 .../scala/stainless/frontend/SplitCallBack.scala   |  2 --
 .../src/test/scala/stainless/InputUtils.scala      |  1 -
 4 files changed, 7 insertions(+), 12 deletions(-)

diff --git a/core/src/main/scala/stainless/frontend/BatchedCallBack.scala b/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
index 98165ad0d..8b58c072f 100644
--- a/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
+++ b/core/src/main/scala/stainless/frontend/BatchedCallBack.scala
@@ -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))
diff --git a/core/src/main/scala/stainless/frontend/CallBack.scala b/core/src/main/scala/stainless/frontend/CallBack.scala
index 4b9c41cd5..ea1f1a220 100644
--- a/core/src/main/scala/stainless/frontend/CallBack.scala
+++ b/core/src/main/scala/stainless/frontend/CallBack.scala
@@ -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.
@@ -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".
diff --git a/core/src/main/scala/stainless/frontend/SplitCallBack.scala b/core/src/main/scala/stainless/frontend/SplitCallBack.scala
index 8c149ab5b..ac4edeed6 100644
--- a/core/src/main/scala/stainless/frontend/SplitCallBack.scala
+++ b/core/src/main/scala/stainless/frontend/SplitCallBack.scala
@@ -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()
diff --git a/frontends/common/src/test/scala/stainless/InputUtils.scala b/frontends/common/src/test/scala/stainless/InputUtils.scala
index 41b5bdffa..cbb8b7950 100644
--- a/frontends/common/src/test/scala/stainless/InputUtils.scala
+++ b/frontends/common/src/test/scala/stainless/InputUtils.scala
@@ -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 = ()