ParserMonad (soteria-rust.Soteria_rust_lib.Value

type query = Charon.Types.ty * Soteria_rust_lib.Typed.T.sint Typed.t

type 'a res = ('a, Error.t, State_tys.fix) State_tys.SM.Result.t

type get_all_query =
  Soteria_rust_lib.Typed.T.nonzero Typed.t
  * Soteria_rust_lib.Typed.T.sint Typed.t

type handler = query -> rust_val res

type get_all_handler =
  get_all_query ->
  (rust_val * Soteria_rust_lib.Typed.T.sint Typed.t) list res

type 'a t = handler -> get_all_handler -> 'a res

val parse : 
  handler:handler ->
  get_all:get_all_handler ->
  (handler -> get_all_handler -> 'a res) ->
  'a res

val ok : 'a -> 'a t

val error : Error.t -> 'a t

val bind2 : 'a t -> ('a -> 'b t) -> (Error.t -> 'b t) -> 'b t

val bind : 'a t -> ('a -> 'b t) -> 'b t

val map : 'a t -> ('a -> 'b) -> 'b t

val query : query -> rust_val t

val get_all : 
  get_all_query ->
  (rust_val * Soteria_rust_lib.Typed.T.sint Typed.t) list t

val lift : 'a DecayMapMonad.t -> 'a t

val lift_rsymex : ('a, Error.t, State_tys.fix) Rustsymex.Result.t -> 'a t

val not_impl : string -> 'a t

val of_opt_not_impl : string -> 'a option -> 'a t

val layout_of : Charon.Types.ty -> Layout.t t

val normalise : Charon.Types.ty -> Charon.Types.ty t

val assert_or_error : 
  DecayMapMonad.Value.sbool DecayMapMonad.Value.t ->
  'a ->
  'b ->
  'c ->
  'd ->
  (unit * 'd, 'a, 'e) DecayMapMonad.Result.t

val fold_iter : 
  'a Soteria.Soteria_std.Foldable.Iter.t ->
  init:'b ->
  f:('b -> 'a -> 'b t) ->
  'b t

module Syntax : sig ... end