package soteria

  1. Overview
  2. Docs
package soteria
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module SM.Consumer

type ('a, 'fix) t
include Soteria.Soteria_std.Monad.Extension2 with type ('a, 'fix) t := ('a, 'fix) t
val fold : (module M : Soteria_std.Sigs.Foldable) -> 'elem M.t -> init:'a -> f:('a -> 'elem -> ('a, 'b) t) -> ('a, 'b) t
val fold_list : 'elem list -> init:'a -> f:('a -> 'elem -> ('a, 'b) t) -> ('a, 'b) t
val fold_iter : 'elem Iter.t -> init:'a -> f:('a -> 'elem -> ('a, 'b) t) -> ('a, 'b) t
val iter : (module M : Soteria_std.Sigs.Foldable) -> 'elem M.t -> f:('elem -> (unit, 'b) t) -> (unit, 'b) t
val iter_list : 'elem list -> f:('elem -> (unit, 'b) t) -> (unit, 'b) t
val iter_iter : 'elem Iter.t -> f:('elem -> (unit, 'b) t) -> (unit, 'b) t
val map_m : (module M : Soteria_std.Sigs.Foldable) -> 'elem M.t -> f:('elem -> ('a, 'b) t) -> ('a list, 'b) t
val map_list : 'elem list -> f:('elem -> ('a, 'b) t) -> ('a list, 'b) t
val map_iter : 'elem Iter.t -> f:('elem -> ('a, 'b) t) -> ('a list, 'b) t
val apply_subst : ((Value.Expr.t -> 'a Value.t) -> 'syn -> 'sem) -> 'syn -> ('sem, 'fix) t
val assert_pure : Value.sbool Value.t -> (unit, 'fix) t
val consume_pure : Value.Expr.t -> (unit, 'fix) t
val learn_eq : Value.Expr.t -> 'a Value.t -> (unit, 'fix) t
val expose_subst : unit -> (Value.Expr.Subst.t, 'fix) t
val lift_res : ('a, cons_fail, 'fix) Soteria.Soteria_std.Compo_res.t t -> ('a, 'fix) t
val lift : 'a t -> ('a, 'fix) t
val branches : (unit -> ('a, 'fix) t) list -> ('a, 'fix) t
val ok : 'a -> ('a, 'fix) t
val lfail : Value.sbool Value.t -> ('a, 'fix) t
val miss : 'fix list -> ('a, 'fix) t
val miss_no_fix : reason:string -> unit -> ('a, 'fix) t
val map : ('a -> 'b) -> ('a, 'fix) t -> ('b, 'fix) t
val map_missing : ('fix -> 'g) -> ('a, 'fix) t -> ('a, 'g) t
val bind : ('a -> ('b, 'fix) t) -> ('a, 'fix) t -> ('b, 'fix) t
val bind_res : (('a, cons_fail, 'fix) Soteria.Soteria_std.Compo_res.t -> ('b, 'fix2) t) -> ('a, 'fix) t -> ('b, 'fix2) t
val run : subst:Value.Expr.Subst.t -> ('a, 'fix) t -> ('a * Value.Expr.Subst.t, cons_fail, 'fix) Soteria.Soteria_std.Compo_res.t t
val from_raw_UNSAFE : (Value.Expr.Subst.t -> ('a * Value.Expr.Subst.t, cons_fail, 'fix) Soteria.Soteria_std.Compo_res.t t) -> ('a, 'fix) t

This is unsafe and shouldn't be used in clients, it is only available to enable the implementation of the state monad transformer.

module Syntax : sig ... end
val run_with_state : state:st -> ('a, 'f) t -> ('a * st, 'f) Symex.Consumer.t