itp_server.mli 3.23 KB
Newer Older
1

Clément Fumex's avatar
Clément Fumex committed
2 3
open Call_provers

Sylvain Dailler's avatar
Sylvain Dailler committed
4 5 6
type prover = string
type transformation = string
type strategy = string
7 8

type node_ID = int
Clément Fumex's avatar
Clément Fumex committed
9 10
val root_node : node_ID

11
(* --------------------------- types to be expanded if needed --------------------------------- *)
Clément Fumex's avatar
Clément Fumex committed
12

13 14 15 16
(* Global information known when server process has started and that can be
   shared with the IDE through communication *)
type global_information =
    {
Clément Fumex's avatar
Clément Fumex committed
17 18 19
     provers         : prover list;
     transformations : transformation list;
     strategies      : strategy list;
20
     commands        : string list
21 22 23 24 25 26 27 28 29
     (* hidden_provers       : string list; *)
     (* session_time_limit   : int; *)
     (* session_mem_limit    : int; *)
     (* session_nb_processes : int; *)
     (* session_cntexample   : bool; *)
     (* main_dir             : string *)
    }

type message_notification =
30 31 32 33 34 35 36
  | Proof_error           of node_ID * string
  | Transf_error          of node_ID * string
  | Strat_error           of node_ID * string
  | Replay_Info           of string
  | Query_Info            of node_ID * string
  | Query_Error           of node_ID * string
  | Help                  of string
37
  (* General information *)
38 39 40
  | Information           of string
  (* Number               of task scheduled, running, etc *)
  | Task_Monitor          of int * int * int
41
  (* An error happened that could not be identified in server *)
42 43
  | Error                 of string
  | Open_File_Error       of string
Clément Fumex's avatar
Clément Fumex committed
44

45 46 47 48 49 50
type node_type =
  | NRoot
  | NFile
  | NTheory
  | NTransformation
  | NGoal
51
  | NProofAttempt
52 53 54 55 56 57 58 59

type update_info =
  | Proved of bool
  | Proof_status_change of
      Controller_itp.proof_attempt_status
      * bool   (* obsolete or not *)
      * Call_provers.resource_limit

Clément Fumex's avatar
Clément Fumex committed
60
type notification =
61
  | New_node     of node_ID * node_ID * node_type * string
62
  (* Notification of creation of new_node:
63 64 65
     New_node (new_node, parent_node, node_type, name). *)
  | Node_change  of node_ID * update_info
  (* inform that the data of the given node changed *)
Clément Fumex's avatar
Clément Fumex committed
66
  | Remove       of node_ID
67
  (* the given node was removed *)
Clément Fumex's avatar
Clément Fumex committed
68
  | Initialized  of global_information
69
  (* initial global data *)
Sylvain Dailler's avatar
Sylvain Dailler committed
70
  | Saved
71
  (* the session was saved on disk *)
Clément Fumex's avatar
Clément Fumex committed
72
  | Message      of message_notification
73
  (* an informative message, can be an error message *)
Clément Fumex's avatar
Clément Fumex committed
74
  | Dead         of string
75
  (* server exited *)
Clément Fumex's avatar
Clément Fumex committed
76
  | Task         of node_ID * string
77
  (* the node_ID's task *)
Clément Fumex's avatar
Clément Fumex committed
78

79 80 81 82 83 84 85
type ide_request =
  | Command_req       of node_ID * string
  | Prove_req         of node_ID * prover * resource_limit
  | Transform_req     of node_ID * transformation * string list
  | Strategy_req      of node_ID * strategy
  | Open_session_req  of string
  | Add_file_req      of string
Clément Fumex's avatar
Clément Fumex committed
86
  | Set_max_tasks_req of int
87
  | Get_task          of node_ID
88 89 90 91 92
  | Get_Session_Tree_req
  | Save_req
  | Reload_req
  | Replay_req
  | Exit_req
Clément Fumex's avatar
Clément Fumex committed
93

94
val print_request: Format.formatter -> ide_request -> unit
Sylvain Dailler's avatar
Sylvain Dailler committed
95 96
val print_msg: Format.formatter -> message_notification -> unit
val print_notify: Format.formatter -> notification -> unit
97

Sylvain Dailler's avatar
Sylvain Dailler committed
98
(* The server part of the protocol *)
Clément Fumex's avatar
Clément Fumex committed
99 100
module type Protocol = sig

Clément Fumex's avatar
Clément Fumex committed
101 102
  val get_requests : unit -> ide_request list
  val notify : notification -> unit
Clément Fumex's avatar
Clément Fumex committed
103 104 105

end

106
module Make (S:Controller_itp.Scheduler) (P:Protocol) : sig
Sylvain Dailler's avatar
Sylvain Dailler committed
107

108
(*
Clément Fumex's avatar
Clément Fumex committed
109
  val get_configs: unit -> Whyconf.config * Whyconf.config
110
 *)
111 112

  (* Nothing ! *)
Sylvain Dailler's avatar
Sylvain Dailler committed
113 114

end