itp_server.mli 2.39 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

12
type node_type = NRoot | NFile | NTheory | NTransformation | NGoal | NProofAttempt of bool
Clément Fumex's avatar
Clément Fumex committed
13

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

17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
(* Global information known when server process has started and that can be
   shared with the IDE through communication *)
type global_information =
    {
     provers              : prover list;
     transformations      : transformation list;
     strategies           : strategy list;
     (* 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
33 34
  | Proof_error  of node_ID * string
  | Transf_error of node_ID * string
Clément Fumex's avatar
Clément Fumex committed
35
  | Strat_error  of node_ID * string
36 37 38 39 40
  | Replay_Info  of string
  | Query_Info   of node_ID * string
  | Query_Error  of node_ID * string
  | Help         of string
  | Information  of string
Clément Fumex's avatar
Clément Fumex committed
41 42 43

type notification =
  | Node_change    of node_ID * node_info
44
  (* inform that the data of the given node changed *)
45 46 47
  | New_node       of node_ID * node_ID * node_type * node_info
  (* 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
48
  | Remove         of node_ID
49
  (* the given node was removed *)
50
  | Initialized    of global_information
51
  (* initial global data *)
Sylvain Dailler's avatar
Sylvain Dailler committed
52
  | Saved
53
  (* the session was saved on disk *)
54 55
  | Message        of message_notification
  (* an informative message, can be an error message *)
Clément Fumex's avatar
Clément Fumex committed
56 57

type request_type =
58 59 60 61 62 63 64 65 66 67
  | Command_req   of string
  | Prove_req     of prover * resource_limit
  | Transform_req of transformation * string list
  | Strategy_req  of strategy
  | Open_req      of string
  | Get_Session_Tree_req
  | Save_req
  | Reload_req
  | Replay_req
  | Exit_req
Clément Fumex's avatar
Clément Fumex committed
68 69 70

type ide_request = request_type * node_ID

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

Clément Fumex's avatar
Clément Fumex committed
74 75
  val get_requests : unit -> ide_request list
  val notify : notification -> unit
Clément Fumex's avatar
Clément Fumex committed
76 77 78

end

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

81 82 83
  val get_config: unit -> Whyconf.config

  (* Nothing ! *)
Sylvain Dailler's avatar
Sylvain Dailler committed
84 85

end