System (imandra-base.Imandra_interactive.System)

Reflected System Functions

Low level access to the functions used for #use "foo.ml", #directory "foo", etc. Use with care.

exception Ocaml_type_error

val home_ptr : ( unit -> string ) Stdlib.ref

val home : unit -> string

Get home directory

val version_ptr : ( unit -> string ) Stdlib.ref

val version : unit -> string

Get current version of Imandra

val use_ptr : 
  ( scope:Opentelemetry.Trace.scope option ->
    ?syntax:Imandra_syntax.Syntax.t ->
    ?batch:bool ->
    ?quiet:bool ->
    string ->
    unit )
    Stdlib.ref

val use : 
  ?scope:Opentelemetry.Trace.scope ->
  ?syntax:Imandra_syntax.Syntax.t ->
  ?batch:bool ->
  ?quiet:bool ->
  string ->
  unit

Load a file's statements directly into the environment. Same as #use "thefile.ml";;.

parameter batch
if true, load the whole file in batch

raises Ocaml_type_error
if the file is ill-typed

val mod_use_ptr : 
  ( scope:Opentelemetry.Trace.scope option ->
    ?syntax:Imandra_syntax.Syntax.t ->
    ?quiet:bool ->
    string ->
    unit )
    Stdlib.ref

val mod_use : 
  ?scope:Opentelemetry.Trace.scope ->
  ?syntax:Imandra_syntax.Syntax.t ->
  ?quiet:bool ->
  string ->
  unit

Load a file as a module. Same as #mod_use "thefile.ml";;.

raises Ocaml_type_error
if the file is ill-typed

val import_ptr : 
  ( scope:Opentelemetry.Trace.scope option ->
    ?quiet:bool ->
    ?syntax:Imandra_syntax.Syntax.t ->
    string ->
    unit )
    Stdlib.ref

val import : 
  ?scope:Opentelemetry.Trace.scope ->
  ?quiet:bool ->
  ?syntax:Imandra_syntax.Syntax.t ->
  string ->
  unit

Import a file as a module. Same as #import "thefile.iml";;.

raises Ocaml_type_error
if the file is ill-typed

val require_lib_ptr : 
  ( scope:Opentelemetry.Trace.scope option ->
    ?meth:[ `Mod_use | `Import | `Use ] ->
    ?syntax:Imandra_syntax.Syntax.t ->
    string ->
    unit )
    Stdlib.ref

val require_lib : 
  ?scope:Opentelemetry.Trace.scope ->
  ?meth:[ `Mod_use | `Import | `Use ] ->
  ?syntax:Imandra_syntax.Syntax.t ->
  string ->
  unit

Require an OCaml library, and possibly also load its imandra file using the given syntax and method of loading.

val add_path_ptr : 
  ( scope:Opentelemetry.Trace.scope option -> string -> unit ) Stdlib.ref

val add_path : ?scope:Opentelemetry.Trace.scope -> string -> unit

Add a path to OCaml's lookup mechanism. Same as #directory "thepath";;.

val reset_ptr : ( unit -> unit ) Stdlib.ref

val reset : unit -> unit

Reflection

An API for run-time reflection and meta-programming.

This is used to evaluate strings into the environment, at runtime, in a type-safe way.

val eval_ptr : 
  ( scope:Opentelemetry.Trace.scope option ->
    ?syntax:Imandra_syntax.Syntax.t ->
    ?batch:bool ->
    ?loc:string ->
    ?quiet:bool ->
    string ->
    unit )
    Stdlib.ref

val eval : 
  ?scope:Opentelemetry.Trace.scope ->
  ?syntax:Imandra_syntax.Syntax.t ->
  ?batch:bool ->
  ?loc:string ->
  ?quiet:bool ->
  string ->
  unit

eval code runs the given string code through Imandra's evaluator (and through OCaml toplevel evaluator).

val eval_code_fragment : 
  ?scope:Opentelemetry.Trace.scope ->
  ?loc:string ->
  ?quiet:bool ->
  Imandra_surface.Code_fragment.t ->
  unit

Same as eval but using a code fragment

module Prompt : sig ... end

module Util : sig ... end

module Mode : sig ... end