Module Imandra_interactive.Imandra_eval

val on_eval_code : Imandra_surface.Code_fragment.t Imandra_util.Observable.t
val on_eval_code_tr_ : Imandra_surface.Code_fragment.t Imandra_util.Observable.send
val on_eval_top_phrase : Parsetree.toplevel_phrase Imandra_util.Observable.t
type validate_result_async = Define.Res.t Imandra_util_thread.Fut.t
val proc_phrase_l : scope:Imandra_interactive.Imandra_common_.Otel.Trace.scope option -> interrupted:Imandra_util.Switch.t -> out:Stdlib.Format.formatter option -> quiet:bool -> input:Imandra_util.Iloc.Input.t -> tr_evs:( Imandra_surface.Event.t list -> Imandra_surface.Event.t list ) -> side_loaded_phrases:Imandra_syntax.Logic_ast.Structure.t list -> Parsetree.toplevel_phrase list -> Imandra_surface.Event.t list Imandra_util.Error.result * Imandra_surface.Top_result.t list
val proc_phrase_l_log : scope:Imandra_interactive.Imandra_common_.Otel.Trace.scope option -> interrupted:Imandra_util.Switch.t -> out:Stdlib.Format.formatter option -> quiet:bool -> input:Imandra_util.Iloc.Input.t -> tr_evs:( Imandra_surface.Event.t list -> Imandra_surface.Event.t list ) -> side_loaded_phrases:Imandra_syntax.Logic_ast.Structure.t list -> Parsetree.toplevel_phrase list -> unit
val define_events_standalone : scope:Imandra_interactive.Imandra_common_.Otel.Trace.scope option -> interrupted:Imandra_util.Switch.t -> out:Stdlib.Format.formatter option -> Imandra_surface.Event.t list -> unit Imandra_util.Error.result * Imandra_util.Console.Capture.t * Imandra_surface.Top_result.t list

Standalone function to define events locally, validate them remotely. Does not evaluate OCaml code, code fragments, thus does not validate counter-examples.

val eval_real_list : scope:Imandra_interactive.Imandra_common_.Otel.Trace.scope option -> interrupted:Imandra_util.Switch.t -> out:Stdlib.Format.formatter option -> quiet:bool -> ?cb: ( Imandra_surface.Event.t list Imandra_util.Error.result -> Imandra_surface.Top_result.t list -> unit ) -> input:Imandra_util.Iloc.Input.t -> Parsetree.toplevel_phrase list -> unit Imandra_util.Error.result * Imandra_surface.Top_result.t list

Evaluate top phrases.

  • parameter cb

    if provided, called on intermediate results

val eval_string : scope:Imandra_interactive.Imandra_common_.Otel.Trace.scope option -> interrupted:Imandra_util.Switch.t -> syntax:Imandra_syntax.Syntax.t -> filename:string -> out:Stdlib.Format.formatter option -> quiet:bool -> ?input:Imandra_util.Iloc.Input.t -> string -> unit Imandra_util.Error.result * Imandra_surface.Top_result.t list
val eval_string_log : scope:Imandra_interactive.Imandra_common_.Otel.Trace.scope option -> interrupted:Imandra_util.Switch.t -> syntax:Imandra_syntax.Syntax.t -> filename:string -> out:Stdlib.Format.formatter option -> quiet:bool -> string -> unit
val eval_string_reraise : scope:Imandra_interactive.Imandra_common_.Otel.Trace.scope option -> interrupted:Imandra_util.Switch.t -> syntax:Imandra_syntax.Syntax.t -> filename:string -> out:Stdlib.Format.formatter option -> quiet:bool -> string -> unit

Like eval_string, but ignores results, and re-raises errors as exceptions

val import_file : scope:Imandra_interactive.Imandra_common_.Otel.Trace.scope option -> loc_of_import:Imandra_util.Iloc.t -> quiet:bool -> dir:string option -> string -> unit

import_iml filename imports the file (and its transitive dependencies).

  • parameter loc_of_import

    location of the import statement

type eval_iter_cb = (Imandra_util.Iloc.t list * Imandra_util.Console.Capture.t * Imandra_surface.Top_result.t list * ( Imandra_surface.Event.t list, Imandra_util.Error.t ) Stdlib.result) -> unit
val eval_string_iter_ : scope:Imandra_interactive.Imandra_common_.Otel.Trace.scope option -> interrupted:Imandra_util.Switch.t -> syntax:Imandra_syntax.Syntax.t -> filename:string -> out:Imandra_util.Fmt.t option -> quiet:bool -> string -> eval_iter_cb -> unit

eval_string_iter_ code f evaluates code, calling f multiple times with intermediate evaluation results

val use_iml : scope:Imandra_interactive.Imandra_common_.Otel.Trace.scope option -> interrupted:Imandra_util.Switch.t -> ?syntax:Imandra_syntax.Syntax.t -> out:Imandra_util.Fmt.t option -> quiet:bool -> string -> unit
val mod_use_iml : scope:Imandra_interactive.Imandra_common_.Otel.Trace.scope option -> interrupted:Imandra_util.Switch.t -> ?syntax:Imandra_syntax.Syntax.t -> quiet:bool -> string -> unit
val require_lib : scope:Imandra_interactive.Imandra_common_.Otel.Trace.scope option -> interrupted:Imandra_util.Switch.t -> loc_of_require:Imandra_util.Iloc.t -> meth:[< `Import | `Mod_use | `Use Import ] -> quiet:bool -> string -> unit
val parse_string_ : syntax:Imandra_syntax.Syntax.t -> filename:string -> string -> ( Parsetree.toplevel_phrase list * Imandra_util.Iloc.Input.t * Imandra_util.Iloc.t, Imandra_util.Error.t ) Stdlib.result
val get_toplevel_db : unit -> Imandra_surface.DB.t

Obtain global DB, or current transaction DB if called from within a nested transaction

module Internal_ : sig ... end