Reintroduce symbolic_choice.mli

Creates `symbolic_choice_intf.ml` to define the symbolic choice
monad's interface and `eval` type definition for easier reuse.

src/cmd/cmd_sym.ml

@@ -50,7 +50,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
   let res_queue = Wq.init () in
   let callback v =
     match v with
-    | Symbolic_choice_with_memory.EVal (Ok ()), _ -> ()
+    | Symbolic_choice_intf.EVal (Ok ()), _ -> ()
     | v -> Wq.push v res_queue
   in
   let join_handles =
@@ -75,7 +75,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
     | Seq.Nil -> Ok count_acc
     | Seq.Cons ((result, _thread), tl) ->
       let* model =
-        let open Symbolic_choice_with_memory in
+        let open Symbolic_choice_intf in
         match result with
         | EAssert (assertion, model) ->
           print_bug (`EAssert (assertion, model));

src/dune

@@ -61,6 +61,7 @@
   solver
   symbolic
   symbolic_choice
+  symbolic_choice_intf
   symbolic_choice_minimalist
   symbolic_choice_with_memory
   symbolic_choice_without_memory

src/intf/symbolic_choice_intf.ml

@@ -0,0 +1,81 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+type 'a eval =
+  | EVal of 'a
+  | ETrap of Trap.t * Smtml.Model.t
+  | EAssert of Smtml.Expr.t * Smtml.Model.t
+
+module type S = sig
+  module V : Func_intf.Value_types
+
+  type thread
+
+  type 'a t
+
+  val return : 'a -> 'a t
+
+  val bind : 'a t -> ('a -> 'b t) -> 'b t
+
+  val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+
+  val map : 'a t -> ('a -> 'b) -> 'b t
+
+  val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+
+  val trap : Trap.t -> 'a t
+
+  val select : V.vbool -> bool t
+
+  val select_i32 : V.int32 -> Int32.t t
+
+  val assertion : V.vbool -> unit t
+
+  val with_thread : (thread -> 'a) -> 'a t
+
+  val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
+
+  val solver : Solver.t t
+
+  val thread : thread t
+
+  val add_pc : V.vbool -> unit t
+
+  type 'a run_result = ('a eval * thread) Seq.t
+
+  val run :
+       workers:int
+    -> Smtml.Solver_dispatcher.solver_type
+    -> 'a t
+    -> thread
+    -> callback:('a eval * thread -> unit)
+    -> callback_init:(unit -> unit)
+    -> callback_end:(unit -> unit)
+    -> unit Domain.t array
+end
+
+module type Intf = sig
+  module type S = S
+
+  module CoreImpl : sig
+    (* The core implementation of the monad. It is isolated in a module to *)
+    (* restict its exposed interface and maintain its invariant. *)
+
+    module State : sig
+      type ('a, 's) t
+
+      val project_state :
+           ('st1 -> 'st2 * 'backup)
+        -> ('backup -> 'st2 -> 'st1)
+        -> ('a, 'st2) t
+        -> ('a, 'st1) t
+    end
+  end
+
+  module Make (Thread : Thread.S) :
+    S
+      with type 'a t = ('a eval, Thread.t) CoreImpl.State.t
+       and type thread := Thread.t
+       and module V := Symbolic_value
+end

src/symbolic/symbolic_choice.ml

@@ -2,68 +2,7 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
-module type S = sig
-  (*
-      The core implementation of the monad. It is isolated in a module to restict its exposed interface
-      and maintain its invariant. In particular, choose must guarantee that the Thread.t is cloned in each branch.
-      Using functions defined here should be foolproof.
-    *)
-
-  type thread
-
-  type 'a t
-
-  val return : 'a -> 'a t
-
-  val bind : 'a t -> ('a -> 'b t) -> 'b t
-
-  val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
-
-  val map : 'a t -> ('a -> 'b) -> 'b t
-
-  val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
-
-  val assertion_fail : Smtml.Expr.t -> Smtml.Model.t -> 'a t
-
-  val stop : 'a t
-
-  val trap : Trap.t -> 'a t
-
-  val thread : thread t
-
-  val yield : unit t
-
-  val solver : Solver.t t
-
-  val with_thread : (thread -> 'a) -> 'a t
-
-  val set_thread : thread -> unit t
-
-  val modify_thread : (thread -> thread) -> unit t
-
-  (*
-       Indicates a possible choice between two values. Thread duplication
-       is already handled by choose and should not be done before by the caller.
-    *)
-  val choose : 'a t -> 'a t -> 'a t
-
-  type 'a eval =
-    | EVal of 'a
-    | ETrap of Trap.t * Smtml.Model.t
-    | EAssert of Smtml.Expr.t * Smtml.Model.t
-
-  type 'a run_result = ('a eval * thread) Seq.t
-
-  val run :
-       workers:int
-    -> Smtml.Solver_dispatcher.solver_type
-    -> 'a t
-    -> thread
-    -> callback:('a eval * thread -> unit)
-    -> callback_init:(unit -> unit)
-    -> callback_end:(unit -> unit)
-    -> unit Domain.t array
-end
+include Symbolic_choice_intf
 
 (*
      Multicore is based on several layers of monad transformers defined here
@@ -238,11 +177,6 @@ module CoreImpl = struct
       *)
     module M = State
 
-    type 'a eval =
-      | EVal of 'a
-      | ETrap of Trap.t * Smtml.Model.t
-      | EAssert of Smtml.Expr.t * Smtml.Model.t
-
     type ('a, 's) t = ('a eval, 's) M.t
 
     let return x : _ t = M.return (EVal x)
@@ -273,10 +207,63 @@ module CoreImpl = struct
     let ( let+ ) = map
   end
 
-  (*  *)
-  module Make (Thread : Thread.S) :
-    S with type thread := Thread.t and type 'a t = ('a, Thread.t) Eval.t =
-  struct
+  module Make (Thread : Thread.S) : sig
+    (*
+      The core implementation of the monad. It is isolated in a module to restict its exposed interface
+      and maintain its invariant. In particular, choose must guarantee that the Thread.t is cloned in each branch.
+      Using functions defined here should be foolproof.
+    *)
+
+    type thread := Thread.t
+
+    type 'a t = ('a, Thread.t) Eval.t
+
+    val return : 'a -> 'a t
+
+    val bind : 'a t -> ('a -> 'b t) -> 'b t
+
+    val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
+
+    val map : 'a t -> ('a -> 'b) -> 'b t
+
+    val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
+
+    val assertion_fail : Smtml.Expr.t -> Smtml.Model.t -> 'a t
+
+    val stop : 'a t
+
+    val trap : Trap.t -> 'a t
+
+    val thread : thread t
+
+    val yield : unit t
+
+    val solver : Solver.t t
+
+    val with_thread : (thread -> 'a) -> 'a t
+
+    val set_thread : thread -> unit t
+
+    val modify_thread : (thread -> thread) -> unit t
+
+    (*
+       Indicates a possible choice between two values. Thread duplication
+       is already handled by choose and should not be done before by the caller.
+    *)
+    val choose : 'a t -> 'a t -> 'a t
+
+    type 'a run_result = ('a eval * thread) Seq.t
+
+    val run :
+         workers:int
+      -> Smtml.Solver_dispatcher.solver_type
+      -> 'a t
+      -> thread
+      -> callback:('a eval * thread -> unit)
+      -> callback_init:(unit -> unit)
+      -> callback_end:(unit -> unit)
+      -> unit Domain.t array
+  end = struct
     include Eval
 
     type 'a t = ('a, Thread.t) Eval.t
@@ -345,7 +332,6 @@ end
     We can now use CoreImpl only through its exposed signature which
     maintains all invariants.
   *)
-
 module Make (Thread : Thread.S) = struct
   include CoreImpl.Make (Thread)
 

src/symbolic/symbolic_choice.mli

@@ -0,0 +1,6 @@
+(* SPDX-License-Identifier: AGPL-3.0-or-later *)
+(* Copyright © 2021-2024 OCamlPro *)
+(* Written by the Owi programmers *)
+
+(** @inline *)
+include Symbolic_choice_intf.Intf

src/symbolic/symbolic_choice_with_memory.mli

@@ -2,24 +2,13 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
-type 'a eval = private
-  | EVal of 'a
-  | ETrap of Trap.t * Smtml.Model.t
-  | EAssert of Smtml.Expr.t * Smtml.Model.t
-
 include
-  Choice_intf.Complete
-    with type thread := Thread_with_memory.t
+  Symbolic_choice_intf.S
+    with type 'a t =
+      ( 'a Symbolic_choice_intf.eval
+      , Thread_with_memory.t )
+      Symbolic_choice.CoreImpl.State.t
+     and type thread := Thread_with_memory.t
      and module V := Symbolic_value
 
-val with_new_symbol : Smtml.Ty.t -> (Smtml.Symbol.t -> 'b) -> 'b t
-
-val run :
-     workers:int
-  -> Smtml.Solver_dispatcher.solver_type
-  -> 'a t
-  -> Thread_with_memory.t
-  -> callback:('a eval * Thread_with_memory.t -> unit)
-  -> callback_init:(unit -> unit)
-  -> callback_end:(unit -> unit)
-  -> unit Domain.t array
+val lift_mem : 'a Symbolic_choice_without_memory.t -> 'a t

src/symbolic/symbolic_choice_without_memory.mli

@@ -2,41 +2,11 @@
 (* Copyright © 2021-2024 OCamlPro *)
 (* Written by the Owi programmers *)
 
-type 'a eval = private
-  | EVal of 'a
-  | ETrap of Trap.t * Smtml.Model.t
-  | EAssert of Smtml.Expr.t * Smtml.Model.t
-
-type 'a t = ('a, Thread_without_memory.t) Symbolic_choice.CoreImpl.Eval.t
-
-type thread := Thread_without_memory.t
-
-module V := Symbolic_value
-
-type 'a run_result
-
-val return : 'a -> 'a t
-
-val bind : 'a t -> ('a -> 'b t) -> 'b t
-
-val map : 'a t -> ('a -> 'b) -> 'b t
-
-val select : V.vbool -> bool t
-
-val select_i32 : V.int32 -> Int32.t t
-
-val trap : Trap.t -> 'a t
-
-val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t
-
-val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t
-
-val assertion : V.vbool -> unit t
-
-val with_thread : (thread -> 'b) -> 'b t
-
-val solver : Solver.t t
-
-val thread : thread t
-
-val add_pc : V.vbool -> unit t
+include
+  Symbolic_choice_intf.S
+    with type 'a t =
+      ( 'a Symbolic_choice_intf.eval
+      , Thread_without_memory.t )
+      Symbolic_choice.CoreImpl.State.t
+     and type thread := Thread_without_memory.t
+     and module V := Symbolic_value