itp_server.mli 3.04 KB
Newer Older
Clément Fumex's avatar
Clément Fumex committed
1 2
open Call_provers

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

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

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

Clément Fumex's avatar
Clément Fumex committed
12 13 14 15 16 17 18
type node_type =
  | NRoot
  | NFile
  | NTheory
  | NTransformation
  | NGoal
  | NProofAttempt of Call_provers.prover_answer option * bool
Clément Fumex's avatar
Clément Fumex committed
19

Clément Fumex's avatar
Clément Fumex committed
20 21 22
type node_info = { proved : bool; (* TODO: add more *)
                   name   : string }

23 24 25 26
(* 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
27 28 29 30
     provers         : prover list;
     transformations : transformation list;
     strategies      : strategy list;
     commands        : string list;
31 32 33 34 35 36 37 38 39
     (* 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 =
Clément Fumex's avatar
Clément Fumex committed
40 41
  | Proof_error  of node_ID * string
  | Transf_error of node_ID * string
Clément Fumex's avatar
Clément Fumex committed
42
  | Strat_error  of node_ID * string
43 44 45 46
  | Replay_Info  of string
  | Query_Info   of node_ID * string
  | Query_Error  of node_ID * string
  | Help         of string
47
  (* General information *)
48
  | Information  of string
49
  (* Number of task scheduled, running, etc *)
Clément Fumex's avatar
Clément Fumex committed
50
  | Task_Monitor of int * int * int
51 52
  (* An error happened that could not be identified in server *)
  | Error        of string
Clément Fumex's avatar
Clément Fumex committed
53 54

type notification =
Clément Fumex's avatar
Clément Fumex committed
55
  | Node_change  of node_ID * node_info
56
  (* inform that the data of the given node changed *)
Clément Fumex's avatar
Clément Fumex committed
57
  | New_node     of node_ID * node_ID * node_type * node_info
58 59
  (* Notification of creation of new_node:
     New_node (new_node, parent_node, new_node_type, new_node_content). *)
Clément Fumex's avatar
Clément Fumex committed
60
  | Remove       of node_ID
61
  (* the given node was removed *)
Clément Fumex's avatar
Clément Fumex committed
62
  | Initialized  of global_information
63
  (* initial global data *)
Sylvain Dailler's avatar
Sylvain Dailler committed
64
  | Saved
65
  (* the session was saved on disk *)
Clément Fumex's avatar
Clément Fumex committed
66
  | Message      of message_notification
67
  (* an informative message, can be an error message *)
Clément Fumex's avatar
Clément Fumex committed
68
  | Dead         of string
69
  (* server exited *)
Clément Fumex's avatar
Clément Fumex committed
70 71 72 73
  | Proof_update of node_ID * Controller_itp.proof_attempt_status
  (* update proof attempt *)
  | Task         of node_ID * string
  (* te node_ID's task *)
Clément Fumex's avatar
Clément Fumex committed
74 75

type request_type =
Clément Fumex's avatar
Clément Fumex committed
76 77 78 79 80 81 82
  | Command_req       of string
  | Prove_req         of prover * resource_limit
  | Transform_req     of transformation * string list
  | Strategy_req      of strategy
  | Open_req          of string
  | Set_max_tasks_req of int
  | Get_task
83 84 85 86 87
  | Get_Session_Tree_req
  | Save_req
  | Reload_req
  | Replay_req
  | Exit_req
Clément Fumex's avatar
Clément Fumex committed
88

89 90
val print_request: Format.formatter -> request_type -> unit

Clément Fumex's avatar
Clément Fumex committed
91
(* TODO: change to request_type * node_ID list ? *)
Clément Fumex's avatar
Clément Fumex committed
92 93
type ide_request = request_type * node_ID

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

Clément Fumex's avatar
Clément Fumex committed
97 98
  val get_requests : unit -> ide_request list
  val notify : notification -> unit
Clément Fumex's avatar
Clément Fumex committed
99 100 101

end

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

Clément Fumex's avatar
Clément Fumex committed
104
  val get_configs: unit -> Whyconf.config * Whyconf.config
105 106

  (* Nothing ! *)
Sylvain Dailler's avatar
Sylvain Dailler committed
107 108

end