Module Imandra_protocol.Query

Client query

type t = private {
view : view;
stamp : Stamp.t;
trace_id : Opentelemetry.Trace_id.t option;
parent_id : Opentelemetry.Span_id.t option;
}
and view =
| Q_init
| Q_user_input of string
| Q_update_config_nop of Imandra_util.Pconfig.op list
| Q_exec_builtin_op_nop of Imandra_surface.Builtin.State.op list
| Q_remote_show of Imandra_util.Remote_ref.remote_id
| Q_remote_get of Imandra_util.Remote_ref.remote_id
| Q_remote_forget_nop of Imandra_util.Remote_ref.remote_id
| Q_validate of Validate.Query.t
| Q_exec_ops_nop of Imandra_surface.Event.op list
| Q_verify of Verify.Query.t
| Q_simplify of Simplify.Query.t
| Q_modular_decomp of Modular_decomp.Query.t
| Q_abstractor of Abstractor.Query.t
| Q_snapshot of Snapshot.Query.t
| Q_extract_extend_nop of Imandra_surface.Type.def list
| Q_extract_get of {
signature : Imandra_surface.Uid.t option;
ext_sig : bool option;
accessors : bool option;
}
| Q_basis_nop of Basis.Query.t
| Q_debug_nop of {
color : bool;
names : string list;
lvl : int;
}
| Q_interrupt_nop of Stamp.t
| Q_list_ext_solvers
| Q_cache_nop of [ `On of string option | `Off | `Clear | `Sync ]
| Q_loading_prelude_begin_nop
| Q_loading_prelude_end
| Q_cache_upload of Cache_upload.query
| Q_load_plugin of string
| Q_get_gc_stat
| Q_custom of {
plugin : string;
f : string;
payload : string;
}
| Q_sync(*

do nothing, but client will wait. this synchronizes client and server

*)
| Q_quit(*

exit

*)
val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val pp_view : Ppx_deriving_runtime.Format.formatter -> view -> Ppx_deriving_runtime.unit
val show_view : view -> Ppx_deriving_runtime.string
val make : ?trace_id:Opentelemetry.Trace_id.t -> ?parent_id:Opentelemetry.Span_id.t -> ?stamp:Stamp.t -> view -> t
val set_scope : ?trace_id:Opentelemetry.Trace_id.t -> ?parent_id:Opentelemetry.Span_id.t -> t -> t
val get_scope : t -> Opentelemetry.Trace.scope option
val interrupt : t -> t
val kind : t -> string * ( unit -> string )

Short description of the variant and the argument

val should_trace : t -> bool