Previous  Up  Next

Module Itp_communication

module Itp_communication: sig .. end

Communication protocol for the ITP server

type transformation = string * string 
type strategy = string 
type node_ID = int 
val root_node : node_ID
val is_root : node_ID -> bool
type global_information = {
   provers : (string * string * string) list;
   transformations : transformation list;
   strategies : (string * strategy) list;
   commands : string list;
}

Global information known when server process has started and that can be shared with the IDE through communication

type message_notification =
| Proof_error of node_ID * string
| Transf_error of bool * node_ID * string * string * Loc.position * string
* string		 (*

Transf_error (is_fatal, nid, trans_with_arg, arg_opt, loc, error_msg, doc_of_transf

*)
| Strat_error of node_ID * string
| Replay_Info of string
| Query_Info of node_ID * string
| Query_Error of node_ID * string (*

General information

*)
| Information of string (*

Number of task scheduled, running, etc

*)
| Task_Monitor of int * int * int (*

A file was read or reloaded and now contains a parsing or typing error. second loc is relative to the session file

*)
| Parse_Or_Type_Error of Loc.position * Loc.position * string (*

File_Saved f f was saved

*)
| File_Saved of string (*

An error happened that could not be identified in server

*)
| Error of string
| Open_File_Error of string 
type node_type =
| NRoot
| NFile
| NTheory
| NTransformation
| NGoal
| NProofAttempt 
type color =
| Neg_premise_color
| Premise_color
| Goal_color
| Error_color
| Error_line_color
| Error_font_color
| Search_color

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 update_info =
| Proved of bool
| Name_change of string
| Proof_status_change of Controller_itp.proof_attempt_status * bool * Call_provers.resource_limit 
type notification =
| Reset_whole_tree
| 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

*)
| 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

*)
| Initialized of global_information (*

initial global data

*)
| Saving_needed of bool (*

the session needs saving when argument is true

*)
| Saved (*

the session was just 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
* (Loc.position * color) list * Loc.position option
* string		 (*

n, s, list_loc, goal_loc, lang with

  • n the node_ID's task,
  • s the task to be displayed
  • list_loc a list of location to color the source,
  • goal_loc the location of the goal,
  • lang the language to load in Why3ide for syntax coloring
*)
| File_contents of string * string * Env.fformat * bool (*

File_contents (filename, contents, format, read_only)

*)
| Source_and_ce of string * (Loc.position * color) list * Loc.position option
* Env.fformat		 (*

Source interleaved with counterexamples: contents and list color loc, loc of the goal, format of the source

*)
| Ident_notif_loc of Loc.position (*

Answer the position where an ident is defined

*) 
type next_unproved_node_strat =
| Prev
| Next
| Clever 
type config_param =
| Max_tasks of int
| Timelimit of float
| Memlimit of int 
type ide_request =
| Command_req of node_ID * string
| Add_file_req of string
| Set_config_param of config_param
| Set_prover_policy of Whyconf.prover * Whyconf.prover_upgrade_policy
| Get_file_contents of string
| Get_task of node_ID * bool * bool * bool (*

Get_task(id,full_ctx,show_clones,show_loc) requests for the text of the task in node id. When full_ctx is true then the full context is show. When show_clones is true then declarations for used and cloned theories, together with metas, are show in comments. When show_loc is false the locations are not returned.

*)
| Remove_subtree of node_ID
| Copy_paste of node_ID * node_ID
| Save_file_req of string * string (*

Save_file_req(filename, content_of_file) saves the file

*)
| Get_first_unproven_node of next_unproved_node_strat * node_ID
| Find_ident_req of Loc.position (*

Find_ident_req (position)

*)
| Unfocus_req
| Save_req
| Export_as_zip
| Reload_req
| Check_need_saving_req
| Exit_req
| Interrupt_req
| Reset_proofs_req (*

Remove all proofattempt and transformations even proved ones

*)
| Get_global_infos 
val print_request : Stdlib.Format.formatter -> ide_request -> unit
val print_msg : Stdlib.Format.formatter -> message_notification -> unit
val print_notify : Stdlib.Format.formatter -> notification -> unit