Module Imandra_interactive.Tlcontext

Toplevel globals and low-level contextual book-keeping

type exec_level =
| INTERACT(*

toplevel / interactive interpreter

*)
| NO_INTERP(*

no interpreter, e.g., for -d(ependency)

*)

Mode of execution (interactive or not)

val toplevel_env : Env.t Stdlib.ref

Environment for top phrase evaluation

val logic_env : Env.t Stdlib.ref

Environment for logical statement extraction. Isomorphic to, but disjoint from, toplevel_env

val tick : unit -> int

number of phrases interpreted

val exec_level : exec_level Stdlib.ref
val update_exec_level : exec_level -> unit
val pp_type : Types.type_expr CCFormat.printer

Pretty print a type

val string_of_ml_type : Types.type_expr -> string

Pretty print a type into a string

val term_of_string : ?db:Imandra_surface.DB.t -> string -> Imandra_surface.Term.t

Parse, type, and scope a string into an Imandra term

val syn_term_of_string : ?db:Imandra_surface.DB.t -> scope:Opentelemetry.Trace.scope option -> string -> Imandra_surface.Term.Syn.t

Parse, type, and scope a string into an Imandra syntactic term

val quit : unit -> 'a

Quit execution

Execution

val execute_phrase : ?quiet:bool -> ?out:Stdlib.Format.formatter -> input:Imandra_util.Iloc.Input.t -> Parsetree.toplevel_phrase -> bool

execute_phrase p executes the given parsetree phrase (directive or OCaml structure) and returns true upon success, false upon failure.

  • parameter quiet

    if true, execution is silent; if false, results are printed

val eval_str : ?filename:string -> ?syntax:Imandra_syntax.Syntax.t -> ?quiet:bool -> string -> unit

Parse and evaluate a string containing Imandra code.

  • parameter syntax

    syntax to use

  • parameter filename

    for locations

  • parameter quiet

    if true, execution is silent; if false, results are printed

module Gist : sig ... end
val cur_prompt : unit -> string

Current prompt

val install_doc : string -> unit

Install given function as a document printer

val remove_doc : string -> unit

Removes given function as a document printer

val side_loaded_events : Imandra_surface.Event.t Imandra_util_thread.Sync_queue.t

Events that are produced as a side effect of program-mode execution

Printing

val pp_timer : unit -> unit

Print last timer on stdout

val pp_directives : unit -> unit

Print available toplevel directives on stdout