Tlcontext (imandra-base.Imandra_interactive.Tlcontext)

Toplevel globals and low-level contextual book-keeping

module Sync_queue = Imandra_thread_util.Sync_queue

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 : 
  scope:Opentelemetry.Trace.scope option ->
  string ->
  Imandra_surface.Term.t

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

val syn_term_of_string : 
  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

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.

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

Parse and evaluate a string containing Imandra code.

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 code_to_exec : Imandra_surface.Code_fragment.t Sync_queue.t

Queue of code fragments to execute

val side_loaded_events : Imandra_surface.Event.t Sync_queue.t

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

val pp_timer : unit -> unit

Print last timer on stdout

val pp_directives : unit -> unit

Print available toplevel directives on stdout