Imandra (imandra-base.Imandra_interactive.Imandra)

Initialization

val set_lockdown : ?scope:Opentelemetry.Trace.scope -> int -> unit

set_lockdown uid enables lockdown mode. It will restrict what functions are in scope, and will Unix.setuid to the given user ID. NOTE: must be called before do_init or loop

val do_init : 
  ?scope:Opentelemetry.Trace.scope ->
  ?linenoise:bool ->
  ?syntax:Imandra_syntax.Syntax.t ->
  unit ->
  unit

Initialize the toplevel environment. Can be safely called several times but will only do something on the first call

Processing Statements

val on_eval_string : Imandra_surface.Code_fragment.t Imandra_util.Observable.t

Event triggered on every source code string evaluated. This may NOT include calls to #use and others.

val on_eval_top_phrase : Parsetree.toplevel_phrase Imandra_util.Observable.t

Event triggered for every top phrase evaluated, including program mode ones.

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

use_iml file loads the file in imandra, as #use "file" would do.

val eval_string : 
  ?scope:Opentelemetry.Trace.scope ->
  ?interrupted:Imandra_util.Switch.t ->
  ?syntax:Imandra_syntax.Syntax.t ->
  ?batch:bool ->
  ?out:Stdlib.Format.formatter ->
  ?quiet:bool ->
  ?filename:string ->
  string ->
  Imandra_surface.Top_result.t list

eval_string "1+1;;" will evaluate the given string as an Imandra statement.

parameter batch
if true, process all events in the string at once

parameter filename
used in the locations in error messages

returns
a list of toplevel results, to be printed somehow Precondition: do_init () was called.

val eval : 
  ?scope:Opentelemetry.Trace.scope ->
  ?interrupted:Imandra_util.Switch.t ->
  ?out:Stdlib.Format.formatter ->
  ?quiet:bool ->
  ?loc:Imandra_util.Iloc.t ->
  input:Imandra_util.Iloc.Input.t ->
  Parsetree.toplevel_phrase ->
  Imandra_surface.Top_result.t list

evaluate the given toplevel phrase.

returns
a list of toplevel results, to be printed somehow. Precondition: do_init () was called.

val eval_string_result : 
  ?scope:Opentelemetry.Trace.scope ->
  ?batch:bool ->
  ?out:Stdlib.Format.formatter ->
  ?quiet:bool ->
  ?filename:string ->
  string ->
  ( Imandra_surface.Top_result.t list, exn ) Stdlib.result

eval_string_result "1+1;;" will evaluate the given string as an Imandra statement.

parameter batch
if true, process all events in the string at once

returns
Ok l where l is a list of toplevel results, to be printed somehow, if evaluation succeeded; Error e if evaluation failed with exception e. Precondition: do_init () was called.

val eval_string_iter : 
  ?scope:Opentelemetry.Trace.scope ->
  ?out:Stdlib.Format.formatter ->
  ?quiet:bool ->
  ?interrupted:Imandra_util.Switch.t ->
  filename:string ->
  string ->
  ( (Imandra_util.Iloc.t list
     * Imandra_util.Console.Capture.t
     * ( Imandra_surface.Event.t list, string ) Stdlib.result) ->
    unit ) ->
  unit

eval_string_iter code f evaluates code into a list of events, processes these events one by one, calling f on the result of each event. Each result is: (locations, console, res) Precondition: do_init () was called.

type validate_result_async

Results of validating some events using logical reasoning, termination analysis, theorem proving, etc.

val process_events : 
  ?scope:Opentelemetry.Trace.scope ->
  ?console_cap:bool ->
  ?interrupted:Imandra_util.Switch.t ->
  ?batch:bool ->
  Imandra_surface.Event.t list ->
  validate_result_async list

Process events so as to validate them on the reasoning side. Returns a list of future results.

parameter batch
if true, validate all events at once

parameter console_cap
if true, capture console output on the reasoning side and into the validate result.

val wait_block_for_validate_res_async : 
  ?scope:Opentelemetry.Trace.scope ->
  ?quiet:bool ->
  validate_result_async ->
  ( Imandra_surface.Event.op list, exn ) Stdlib.result
  * Imandra_util.Console.Capture.t

Wait for a validation result

val wait_for_validate_res_async : 
  validate_result_async ->
  (( Imandra_surface.Event.op list, exn ) Stdlib.result
   * Imandra_util.Console.Capture.t)
    Imandra_thread_util.Fut.t

val eval_string_returning_string : 
  ?scope:Opentelemetry.Trace.scope ->
  string ->
  string

eval_string_returning_string s evaluates s, which must be a code fragment returning a string, and returns the resulting string value.

Example:

# Imandra.eval_string_returning_string {| "hello " ^ "world" |};;
- : string = "hello world"

             # Imandra.eval_string_returning_string {| Printf.sprintf "%B" true |};;
- : string = "true"

val parse_file : 
  ?syntax:Imandra_syntax.Syntax.t ->
  string ->
  ( Parsetree.toplevel_phrase list * Imandra_util.Iloc.Input.t, exn )
    Stdlib.result

Parse given file

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.Iloc.t Imandra_util.List1.t * exn )
    Stdlib.result

Parse given string.

returns
a result with phrases or an error, along with the last parse location

val port : 
  ?scope:Opentelemetry.Trace.scope ->
  ?quiet:bool ->
  var:string ->
  string ->
  unit

port ~var expr ports the content of expr, typically a variable (which must have a logic type) into logic mode, into the new variable var.

parameter var
the name of the variable that will receive the logic-mode value

parameter quiet
if true, won't print the binding

parameter expr
a string containing an OCaml expression whose type is defined in logic mode. In general this expression can be a simple variable, or a more complicated computation.
Example:
```
let a = print_endline "coucou"; 42 [@@program];;

Imandra.port ~var:"logic_a" "a";;

verify (logic_a=42);;

Imandra.port ~var:"logic_a_succ" "a+1";;

verify (logic_a_succ=43);;
```

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

val undo : int -> unit

undo n cancels the last n toplevel phrases entered by the user

module Gc_stat : sig ... end

val add_plugin : 
  ?scope:Opentelemetry.Trace.scope ->
  Imandra_surface.Plugin.t ->
  unit

Add the given plugin and apply it to history retroactively. From now on all events will be processed by this plugin. It blocks until all code fragments have been executed.

It is simpler to call this as early as possible if one wants to use #reset or #undo.

See Plugin for more information.

val collect_plugin : 
  Imandra_surface.Plugin.t ->
  Imandra_surface.Code_fragment.t list

Run the plugin on all events so far, but instead of executing its code fragments, just collect them

val add_plugin_pp : ?scope:Opentelemetry.Trace.scope -> unit -> unit

val add_plugin_yojson : ?scope:Opentelemetry.Trace.scope -> unit -> unit

val add_plugin_finite_type : ?scope:Opentelemetry.Trace.scope -> unit -> unit

val add_plugin_gen_json : 
  ?scope:Opentelemetry.Trace.scope ->
  ?logic_deser:bool ->
  mod_name:string ->
  unit ->
  unit

val add_plugin_rand : 
  ?scope:Opentelemetry.Trace.scope ->
  ?mod_name:string ->
  unit ->
  unit

Extension Points

module Custom_extension_point =
  Imandra_syntax.Rewrite_parsetree.Custom_extension

val add_custom_extension_expr : 
  string ->
  Custom_extension_point.expr_tr ->
  unit

Define a custom extension point

val add_custom_extension_value_binding : 
  string ->
  Custom_extension_point.value_binding_tr ->
  unit

val add_custom_extension_string_lit : 
  string ->
  Custom_extension_point.string_lit_tr ->
  unit

val with_local_custom_extensions : 
  (string * Custom_extension_point.tr) list ->
  ( unit -> 'a ) ->
  'a

Main Loop

val interactive_loop : 
  ?scope:Opentelemetry.Trace.scope ->
  ?init:bool ->
  ?syntax:Imandra_syntax.Syntax.t ->
  ?linenoise:bool ->
  unit ->
  unit

Main loop for a toplevel that reads on stdin and prints on stdout.

parameter init
if true, calls do_init first

parameter linenoise
if true, use linenoise for interactive input

parameter syntax
syntax to use

val process_file : 
  ?scope:Opentelemetry.Trace.scope ->
  ?init:bool ->
  ?syntax:Imandra_syntax.Syntax.t ->
  string ->
  Parsetree.toplevel_phrase list
  * Imandra_surface.Event.t list
  * Imandra_surface.Top_result.t list

process_file path parses the file and returns its content and a list of events. This is useful for batch compilation.

Render Documents

val display : Imandra_document.Document.t -> unit

Prints the document a way or another

String -> Term and Expr conversion

val term_of_string : 
  ?scope:Opentelemetry.Trace.scope ->
  string ->
  Imandra_surface.Term.t

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

Module System

val import_file : 
  ?scope:Opentelemetry.Trace.scope ->
  ?loc:Imandra_util.Iloc.t ->
  ?syntax:Imandra_syntax.Syntax.t ->
  ?quiet:bool ->
  string ->
  unit

Import given module (and its dependencies, recursively) by its file name

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

Require an ocamlfind library and its Imandra attachment, using either import or mod_use to load its content.

module Gist : sig ... end

exception Init_fail