Module InterpM.StateM

type st = State.t option
module Symex : sig ... end
type 'a t = st -> ('a * st) Symex.t
val get_state : unit -> st t
val set_state : st -> unit t
val map_state : (st -> st) -> unit t
val run_with_state : state:st -> 'a t -> ('a * st) Symex.t
val with_state : state:st -> 'a t -> 'a t
val lift : 'a Symex.t -> 'a t
module Value : sig ... end
val return : 'a -> 'a t
val bind : 'a t -> ('a -> 'b t) -> 'b t
val map : 'a t -> ('a -> 'b) -> 'b t
type lfail = [
  1. | `Lfail of Value.sbool Value.t
]
val pp_lfail : Ppx_deriving_runtime.Format.formatter -> lfail -> Ppx_deriving_runtime.unit
val show_lfail : lfail -> Ppx_deriving_runtime.string
type cons_fail = [
  1. | `Lfail of Value.sbool Value.t
  2. | `Missing_subst of Soteria.Symex.Var.t
]
val pp_cons_fail : Ppx_deriving_runtime.Format.formatter -> cons_fail -> Ppx_deriving_runtime.unit
val show_cons_fail : cons_fail -> Ppx_deriving_runtime.string
val assume : Value.sbool Value.t list -> unit t
val vanish : unit -> 'a t
val assert_ : Value.sbool Value.t -> bool t
val nondet_UNSAFE : 'a Value.ty -> 'a Value.t
val nondet : 'a Value.ty -> 'a Value.t t
val simplify : 'a Value.t -> 'a Value.t t
val fresh_var : 'a Value.ty -> Soteria.Symex.Var.t t
val branch_on : ?left_branch_name:string -> ?right_branch_name:string -> Value.sbool Value.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t
val if_sure : ?left_branch_name:string -> ?right_branch_name:string -> Value.sbool Value.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t
val branch_on_take_one : ?left_branch_name:string -> ?right_branch_name:string -> Value.sbool Value.t -> then_:(unit -> 'a t) -> else_:(unit -> 'a t) -> 'a t
val give_up : string -> 'a t
val branches : (unit -> 'a t) list -> 'a t
val consume_fuel_steps : int -> unit t
val assert_or_error : Value.sbool Value.t -> 'err -> (unit, 'err, 'f) Soteria.Symex.Compo_res.t t
val some_or_give_up : string -> 'a option -> 'a t
val all : ('a -> 'b t) -> 'a list -> 'b list t
val fold_list : 'a list -> init:'b -> f:('b -> 'a -> 'b t) -> 'b t
val fold_iter : 'a Soteria.Soteria_std.Iter.t -> init:'b -> f:('b -> 'a -> 'b t) -> 'b t
val fold_seq : 'a Soteria.Soteria_std.Seq.t -> init:'b -> f:('b -> 'a -> 'b t) -> 'b t
val iter_list : 'a list -> f:('a -> unit t) -> unit t
val iter_iter : 'a Soteria.Soteria_std.Iter.t -> f:('a -> unit t) -> unit t
val map_list : 'a list -> f:('a -> 'b t) -> 'b list t
module Producer : sig ... end
module Consumer : sig ... end
module Result : sig ... end
module Syntax : sig ... end