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.