From 20266632d7c2a4ebd221fb456a8e7be5ce8e69b7 Mon Sep 17 00:00:00 2001
From: Peter Lozov <not_kill@gmail.ru>
Date: Sun, 31 Jul 2022 03:21:54 +0300
Subject: [PATCH] Added condo2.

---
 src/core/Core.ml  | 6 ++++++
 src/core/Core.mli | 2 ++
 2 files changed, 8 insertions(+)

diff --git a/src/core/Core.ml b/src/core/Core.ml
index bc001315b..954cbde3a 100644
--- a/src/core/Core.ml
+++ b/src/core/Core.ml
@@ -497,6 +497,12 @@ let (?|) gs st =
 
 let conde = (?|)
 
+let condo2 a b st =
+  let st = State.new_scope st in
+  match Stream.msplit @@ a st with
+  | Some (a, b) -> Stream.cons a b
+  | None -> b st
+
 let call_fresh f st =
   let x = State.fresh st in
   f x st
diff --git a/src/core/Core.mli b/src/core/Core.mli
index 7f2612b24..fff880bc9 100644
--- a/src/core/Core.mli
+++ b/src/core/Core.mli
@@ -82,6 +82,8 @@ val (|||) : goal -> goal -> goal
 *)
 val (?|) : goal list -> goal
 
+val condo2 : goal -> goal -> goal
+
 (** [conde] is a synonym for [?|] *)
 val conde : goal list -> goal