package why3

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 = {
  1. provers : (string * string * string) list;
  2. transformations : transformation list;
  3. strategies : (string * strategy) list;
  4. commands : string list;
}
type message_notification =
  1. | Proof_error of node_ID * string
  2. | Transf_error of bool * node_ID * string * string * Loc.position * string * string
  3. | Strat_error of node_ID * string
  4. | Replay_Info of string
  5. | Query_Info of node_ID * string
  6. | Query_Error of node_ID * string
  7. | Information of string
  8. | Task_Monitor of int * int * int
  9. | Parse_Or_Type_Error of Loc.position * Loc.position * string
  10. | File_Saved of string
  11. | Error of string
  12. | Open_File_Error of string
type node_type =
  1. | NRoot
  2. | NFile
  3. | NTheory
  4. | NTransformation
  5. | NGoal
  6. | NProofAttempt
type color =
  1. | Neg_premise_color
  2. | Premise_color
  3. | Goal_color
  4. | Error_color
  5. | Error_line_color
  6. | Error_font_color
  7. | Search_color
type update_info =
  1. | Proved of bool
  2. | Name_change of string
  3. | Proof_status_change of Controller_itp.proof_attempt_status * bool * Call_provers.resource_limit
type notification =
  1. | Reset_whole_tree
  2. | New_node of node_ID * node_ID * node_type * string * bool
  3. | Node_change of node_ID * update_info
  4. | Remove of node_ID
  5. | Next_Unproven_Node_Id of node_ID * node_ID
  6. | Initialized of global_information
  7. | Saving_needed of bool
  8. | Saved
  9. | Message of message_notification
  10. | Dead of string
  11. | Task of node_ID * string * (Loc.position * color) list * Loc.position option * string
  12. | File_contents of string * string * Env.fformat * bool
  13. | Source_and_ce of string * (Loc.position * color) list * Loc.position option * Env.fformat
  14. | Ident_notif_loc of Loc.position
type next_unproved_node_strat =
  1. | Prev
  2. | Next
  3. | Clever
type ide_request =
  1. | Command_req of node_ID * string
  2. | Add_file_req of string
  3. | Set_config_param of string * int
  4. | Set_prover_policy of Whyconf.prover * Whyconf.prover_upgrade_policy
  5. | Get_file_contents of string
  6. | Get_task of node_ID * bool * bool
  7. | Remove_subtree of node_ID
  8. | Copy_paste of node_ID * node_ID
  9. | Save_file_req of string * string
  10. | Get_first_unproven_node of next_unproved_node_strat * node_ID
  11. | Find_ident_req of Loc.position
  12. | Unfocus_req
  13. | Save_req
  14. | Reload_req
  15. | Check_need_saving_req
  16. | Exit_req
  17. | Interrupt_req
  18. | Reset_proofs_req
  19. | Get_global_infos
val print_request : Format.formatter -> ide_request -> unit
val print_msg : Format.formatter -> message_notification -> unit
val print_notify : Format.formatter -> notification -> unit
OCaml

Innovation. Community. Security.