itp_server.mli 1.34 KB
Newer Older
Clément Fumex's avatar
Clément Fumex committed
1 2 3 4 5 6 7 8 9 10 11
open Call_provers

type prover
type transformation
type strategy

type node_ID
val root_node : node_ID

(* --------------------------- types to be expanded on call by need --------------------------------- *)

Clément Fumex's avatar
Clément Fumex committed
12
type node_type = File | Theory | Transformation | Goal | ProofAttempt of bool
Clément Fumex's avatar
Clément Fumex committed
13

Clément Fumex's avatar
Clément Fumex committed
14 15 16 17
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
18 19 20 21 22 23

type session_tree = Node of node_ID * node_type * node_info * session_tree list

type error_notification =
  | Proof_error  of node_ID * string
  | Transf_error of node_ID * string
Clément Fumex's avatar
Clément Fumex committed
24
  | Strat_error  of node_ID * string
Clément Fumex's avatar
Clément Fumex committed
25 26 27

type notification =
  | Node_change    of node_ID * node_info
Clément Fumex's avatar
Clément Fumex committed
28
  | New_subtree    of node_ID * session_tree
Clément Fumex's avatar
Clément Fumex committed
29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
  | Remove         of node_ID
  | Initialized    of prover list * transformation list * strategy list
  | Session_Tree   of session_tree
  | Error          of error_notification

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

type ide_request = request_type * node_ID

module type Protocol = sig

Clément Fumex's avatar
Clément Fumex committed
49 50
  val get_requests : unit -> ide_request list
  val notify : notification -> unit
Clément Fumex's avatar
Clément Fumex committed
51 52 53 54

end

module Make (P:Protocol) : sig end