itp_communication.ml 3.07 KB
Newer Older
Sylvain Dailler's avatar
Sylvain Dailler committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34
(* Information that the IDE may want to have *)
type prover = string
type transformation = string
type strategy = string


type node_ID = int
let root_node : node_ID = 0


type global_information =
    {
     provers         : prover list;
     transformations : transformation list;
     strategies      : strategy list;
     commands        : string 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 =
  | 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
  | Information           of string
  | Task_Monitor          of int * int * int
35
  | Parse_Or_Type_Error   of string
36
  | File_Saved            of string
Sylvain Dailler's avatar
Sylvain Dailler committed
37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62
  | Error                 of string
  | Open_File_Error       of string

type node_type =
  | NRoot
  | NFile
  | NTheory
  | NTransformation
  | NGoal
  | NProofAttempt

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

type notification =
  | New_node     of node_ID * node_ID * node_type * string * bool
  (* Notification of creation of new_node:
     New_node (new_node, parent_node, node_type, name, detached). *)
  | Node_change  of node_ID * update_info
  (* inform that the data of the given node changed *)
  | Remove       of node_ID
  (* the given node was removed *)
63 64 65
  | Next_Unproven_Node_Id of node_ID * node_ID
  (* Next_Unproven_Node_Id (asked_id, next_unproved_id). Returns a node and the
     next unproven node from this node *)
Sylvain Dailler's avatar
Sylvain Dailler committed
66 67 68 69 70 71 72 73 74 75
  | Initialized  of global_information
  (* initial global data *)
  | Saved
  (* the session was saved on disk *)
  | Message      of message_notification
  (* an informative message, can be an error message *)
  | Dead         of string
  (* server exited *)
  | Task         of node_ID * string
  (* the node_ID's task *)
76
  | File_contents of string * string
77
  (* File_contents (filename, contents) *)
Sylvain Dailler's avatar
Sylvain Dailler committed
78 79

type ide_request =
80 81 82 83 84 85 86 87 88 89 90 91
  | Command_req             of node_ID * string
  | Prove_req               of node_ID * prover * Call_provers.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
  | Set_max_tasks_req       of int
  | Get_file_contents       of string
  | Get_task                of node_ID
  | Remove_subtree          of node_ID
  | Copy_paste              of node_ID * node_ID
  | Copy_detached           of node_ID
92
  | Save_file_req           of string * string
93
  | Get_first_unproven_node of node_ID
Sylvain Dailler's avatar
Sylvain Dailler committed
94 95 96 97 98
  | Get_Session_Tree_req
  | Save_req
  | Reload_req
  | Replay_req
  | Exit_req
99
  | Interrupt_req