itp_server.mli 1.92 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 6 7 8 9 10 11 12
type prover = string
type transformation = string
type strategy = string
type infos =
    {hidden_provers : string list;
     session_time_limit : int;
     session_mem_limit : int;
     session_nb_processes : int;
     session_cntexample : bool;
     main_dir : string}
Clément Fumex's avatar
Clément Fumex committed
13

Sylvain Dailler's avatar
Sylvain Dailler committed
14 15 16 17 18
(* TODO:
   Size of the name can be proportionnal to the size of the tree.
   Maybe, we should find an other solution *)
type node_ID = string
type pos_ID = string
Clément Fumex's avatar
Clément Fumex committed
19 20
val root_node : node_ID

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

Sylvain Dailler's avatar
Sylvain Dailler committed
23
type node_type = Root | File | Theory | Transformation | Goal | ProofAttempt of bool
Clément Fumex's avatar
Clément Fumex committed
24

Clément Fumex's avatar
Clément Fumex committed
25 26 27 28
type node_info = { proved : bool; (* TODO: add more *)
                   name   : string }

(* todo, separate what's updatable from the rest in types *)
Clément Fumex's avatar
Clément Fumex committed
29

Sylvain Dailler's avatar
Sylvain Dailler committed
30 31 32
(* pos_ID is the suffix of node_ID: its position in its brothers list *)
type session_tree =
  | Node of node_ID * pos_ID * node_type * node_info * session_tree list
Clément Fumex's avatar
Clément Fumex committed
33 34 35 36

type error_notification =
  | Proof_error  of node_ID * string
  | Transf_error of node_ID * string
Clément Fumex's avatar
Clément Fumex committed
37
  | Strat_error  of node_ID * string
Clément Fumex's avatar
Clément Fumex committed
38 39 40

type notification =
  | Node_change    of node_ID * node_info
Clément Fumex's avatar
Clément Fumex committed
41
  | New_subtree    of node_ID * session_tree
Clément Fumex's avatar
Clément Fumex committed
42
  | Remove         of node_ID
Sylvain Dailler's avatar
Sylvain Dailler committed
43 44
  | Initialized    of infos * prover list * transformation list * strategy list
  | Saved
Clément Fumex's avatar
Clément Fumex committed
45 46
  | Session_Tree   of session_tree
  | Error          of error_notification
Sylvain Dailler's avatar
Sylvain Dailler committed
47
  | Message        of string
Clément Fumex's avatar
Clément Fumex committed
48 49 50 51 52 53 54 55 56 57 58

type request_type =
  | Command   of string
  | Prove     of prover * resource_limit
  | Transform of transformation * string list
  | Strategy  of strategy
  | Open      of string
  | Get_Session_Tree
  | Save
  | Reload
  | Replay
Sylvain Dailler's avatar
Sylvain Dailler committed
59
  | Exit
Clément Fumex's avatar
Clément Fumex committed
60 61 62

type ide_request = request_type * node_ID

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

Clément Fumex's avatar
Clément Fumex committed
66 67
  val get_requests : unit -> ide_request list
  val notify : notification -> unit
Clément Fumex's avatar
Clément Fumex committed
68 69 70

end

Sylvain Dailler's avatar
Sylvain Dailler committed
71 72 73 74 75
module Make (P:Protocol) : sig

  val treat_requests: unit -> bool

end