Console

This section covers the use of the reasoner through the console command interface running at the OCaml/HOL Light toplevel. This includes the available commands and responses.

The JSON API mode can be loaded using the following command:

1loads (!hol_dir ^ "/workflowfm/make.console.ml");;

The entire interface is structured as the following module type:

 1module type Composer_console_type =
 2    sig
 3      module Composer : Composer_type
 4
 5      val responses : unit -> Composer.Response.t list
 6
 7      val add_process : Composer.Process.t -> Composer.Process.t
 8      val get_process : string -> Composer.Process.t
 9      val exists_process : string -> bool
10      val del_process : string -> unit
11      val reset_processes : unit -> unit
12      val list : unit -> string list
13
14      val add_intermediate : Composer.Process.t -> Composer.Process.t
15      val get_intermediate : string -> Composer.Process.t
16      val exists_intermediate : string -> bool
17      val del_intermediate : string -> unit
18      val reset_intermediates : unit -> unit
19      val ilist : unit -> string list
20
21      val get : string -> Composer.Process.t
22
23      val resetstep : unit -> unit
24      val reset : unit -> unit
25      val full_reset : unit -> unit
26
27      val create : string -> term list -> term -> Composer.Response.t
28      val compose1 : Action.t -> Composer.Response.t
29      val tensor : string -> string -> Composer.Response.t
30      val cwith : string -> string -> string -> string -> Composer.Response.t
31      val join : string -> string -> string -> string -> Composer.Response.t
32
33      val store : string -> string -> Composer.Response.t
34      val load : string -> unit
35    end ;;

Each of these functions/commands is explained in more detail in the next sections.