Adding a primitive to the tactic monad to modify the exceptional content.

2 files changed, 15 insertions, 0 deletions

diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 79bf48acd..c88de133d 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -215,6 +215,14 @@ struct
   let modify f =
     { iolist = fun s nil cons -> cons () (f s) nil }
 
+  (** Exception manipulation *)
+
+  let interleave src dst m =
+    { iolist = fun s nil cons ->
+      m.iolist s (fun e1 -> nil (src e1))
+        (fun x s next -> cons x s (fun e2 -> next (dst e2)))
+    }
+
   (** List observation *)
 
   let once m =
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 42e49d5a7..1869f3263 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -115,6 +115,13 @@ module BackState : sig
   val get : ('s, 's, 's, 'e) t
   val modify : ('i -> 'o) -> (unit, 'i, 'o, 'e) t
 
+  val interleave : ('e1 -> 'e2) -> ('e2 -> 'e1) -> ('a, 'i, 'o, 'e1) t ->
+    ('a, 'i, 'o, 'e2) t
+  (** [interleave src dst m] adapts the exceptional content of the monad
+      according to the functions [src] and [dst]. To ensure a meaningful result,
+      those functions must form a retraction, i.e. [dst (src e1) = e1] for all
+      [e1]. This is typically the case when the type ['e1] is [unit]. *)
+
   val zero : 'e -> ('a, 'i, 'o, 'e) t
   val plus : ('a, 'i, 'o, 'e) t -> ('e -> ('a, 'i, 'o, 'e) t) -> ('a, 'i, 'o, 'e) t