Module Imandra_interactive.History

type iml =
| Iml_ty of Imandra_surface.Type.def list
| Iml_term of Imandra_surface.Term.t
| Iml_alias of Imandra_surface.Uid.t
| Iml_struct of Imandra_surface.Event.t list
| Iml_import of string * iml list
| Iml_list of iml list
| Iml_msg of string
| Iml_none
val pp_iml : Ppx_deriving_runtime.Format.formatter -> iml -> Ppx_deriving_runtime.unit
val show_iml : iml -> Ppx_deriving_runtime.string
type event = Imandra_surface.Event.t
type error = {
err_loc : Imandra_util.Iloc.t;
err_msg : string;
}
val pp_error : Ppx_deriving_runtime.Format.formatter -> error -> Ppx_deriving_runtime.unit
val show_error : error -> Ppx_deriving_runtime.string
type internal_state
type t = private {
events : event list;
len : int;
db : Imandra_surface.Event.DB.t;
errors : error list;
internal_state : internal_state;
prev : t option;
}
val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val iter_from_oldest : t -> rec_:bool -> ?ignore_prelude:bool -> ( int -> event -> unit ) -> unit
val iter_from_most_recent : t -> rec_:bool -> ?ignore_prelude:bool -> ( int -> event -> unit ) -> unit
val last_env : t -> Env.t
val set_last_env : Env.t -> t -> t
val len : t -> int
val record_event : event -> t -> t
val record_event_l : event list -> t -> t
val record_error : ?loc:Imandra_util.Iloc.t -> string -> t -> t
val record_exn_seen : t -> t
val db : t -> Imandra_surface.Event.DB.t
val set_db : Imandra_surface.Event.DB.t -> t -> t
val exn_seen : t -> bool
val n_exn_seen : t -> int
val error_seen : t -> bool
val n_error_seen : t -> int
module State : sig ... end
val show_history : ?ignore_prelude:bool -> ?key:string option -> unit -> unit

Show history on stdout.

  • parameter key

    the particular event to display if Pconfig.State.state.top_results is true, it pushes a top result instead of printing

val show_history_to_doc : ?ignore_prelude:bool -> ?key:string option -> unit -> Imandra_document.Document.t
val show_all_thms : unit -> unit
val pp_dot : ?ignore_prelude:bool -> unit CCFormat.printer

Print the history as a dependency graph

val to_string_dot : ?ignore_prelude:bool -> unit -> string
val event_to_doc : ?proofs:bool -> ?txt:bool -> event -> Imandra_document.Document.t
val to_list : ?ignore_prelude:bool -> unit -> event list
val zero_landmark_ev : unit Imandra_util.Observable.t
val set_zero_landmark : unit -> unit
val has_seen_zero_landmark : unit -> bool
val num_to_ubt_for_name : string -> int
val iter_plugins : t -> ?ignore_prelude:bool -> acts:Imandra_surface.Plugin.actions -> Imandra_surface.Plugin.set -> unit

Apply the plugins to each even in hist with actions acts.

module Print : sig ... end