itp_communication.ml 5.06 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2017   --   INRIA - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

Sylvain Dailler's avatar
Sylvain Dailler committed
12 13 14 15 16 17 18 19 20 21 22 23
(* 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 =
    {
MARCHE Claude's avatar
MARCHE Claude committed
24
     provers         : (string * prover) list;
Sylvain Dailler's avatar
Sylvain Dailler committed
25 26 27 28 29 30 31 32 33 34 35 36 37
     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
38 39
  | Transf_error          of node_ID * string * string * Loc.position * string
  (* Transf_error (nid, trans_with_arg, arg_opt, loc, error_msg *)
Sylvain Dailler's avatar
Sylvain Dailler committed
40 41 42 43 44 45 46
  | 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
Sylvain Dailler's avatar
Sylvain Dailler committed
47
  | Parse_Or_Type_Error   of Loc.position * string
48
  | File_Saved            of string
Sylvain Dailler's avatar
Sylvain Dailler committed
49 50 51 52 53 54 55 56 57 58 59
  | Error                 of string
  | Open_File_Error       of string

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

60 61 62 63 64 65 66 67
(* Used to give colors to the parts of the source code that corresponds to the
   following property in the current task. For example, the code corresponding
   to the goal of the task will have Goal_color in the source code. *)
type color =
  | Neg_premise_color
  | Premise_color
  | Goal_color

Sylvain Dailler's avatar
Sylvain Dailler committed
68 69 70 71 72 73 74 75 76 77 78 79 80 81 82
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 *)
83 84 85
  | 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
86 87 88 89 90 91 92 93
  | 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 *)
94 95 96 97
  | Task         of node_ID * string * (Loc.position * color) list
  (* the node_ID's task together with information that allows to color the
     source code corresponding to different part of the task (premise, goal,
     etc) *)
98
  | File_contents of string * string
99
  (* File_contents (filename, contents) *)
Sylvain Dailler's avatar
Sylvain Dailler committed
100 101

type ide_request =
102 103 104 105
  | 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
Sylvain Dailler's avatar
Sylvain Dailler committed
106
  | Edit_req                of node_ID * prover
107
(*
108
  | Open_session_req        of string
109
 *)
110 111 112
  | Add_file_req            of string
  | Set_max_tasks_req       of int
  | Get_file_contents       of string
113
  | Get_task                of node_ID * bool
Sylvain Dailler's avatar
Sylvain Dailler committed
114 115
  | Focus_req               of node_ID
  | Unfocus_req
116 117 118
  | Remove_subtree          of node_ID
  | Copy_paste              of node_ID * node_ID
  | Copy_detached           of node_ID
119
  | Save_file_req           of string * string
120
  | Get_first_unproven_node of node_ID
121
  | Mark_obsolete_req       of node_ID
Sylvain Dailler's avatar
Sylvain Dailler committed
122
  | Get_Session_Tree_req
123
  | Clean_req
Sylvain Dailler's avatar
Sylvain Dailler committed
124 125 126 127
  | Save_req
  | Reload_req
  | Replay_req
  | Exit_req
128
  | Interrupt_req
129 130 131 132 133 134

(* Return true if the request modify the session *)
let modify_session (r: ide_request) =
  match r with
  | Command_req _ | Prove_req _ | Transform_req _ | Strategy_req _
  | Add_file_req _ | Remove_subtree _ | Copy_paste _ | Copy_detached _
Sylvain Dailler's avatar
Sylvain Dailler committed
135
  | Replay_req | Clean_req | Mark_obsolete_req _ | Edit_req _ -> true
136

137 138
  (*| Open_session_req _ *)
  | Set_max_tasks_req _ | Get_file_contents _
139 140
  | Get_task _ | Save_file_req _ | Get_first_unproven_node _
  | Get_Session_Tree_req | Save_req | Reload_req | Exit_req
Sylvain Dailler's avatar
Sylvain Dailler committed
141
  | Interrupt_req | Focus_req _ | Unfocus_req -> false