server_utils.mli 3.59 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2019   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10
(*                                                                  *)
(*  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.                           *)
(*                                                                  *)
(********************************************************************)
11 12


13 14 15
val get_session_dir : allow_mkdir:bool -> string Queue.t -> string
(** [get_session_dir q] analyses the queue of filenames [q] and
    returns the session directory from it.
Sylvain Dailler's avatar
Sylvain Dailler committed
16

17 18 19 20
    If the first element of the queue [q] is a directory, it is used as the
    session dir, and removed from the queue. If it is an existing file, the
    name obtained by removing the extension is used as the session dir; the
    file stays in the queue.
21

22 23
    In the other cases, the function raises [Invalid_arg s] with some
    appropriate explanation [s].
Sylvain Dailler's avatar
Sylvain Dailler committed
24

25 26
    The so computed session directory is created if it does not exist and
    [allow_mkdir] is true.
Sylvain Dailler's avatar
Sylvain Dailler committed
27

28
 *)
Sylvain Dailler's avatar
Sylvain Dailler committed
29 30 31 32 33 34 35 36 37 38

(** Simple queries *)

(* The id you are trying to use is undefined *)
exception Undefined_id of string
(* Bad number of arguments *)
exception Number_of_arguments

type query =
  | Qnotask of (Controller_itp.controller -> string list -> string)
39
  | Qtask of (Controller_itp.controller -> Trans.naming_table -> string list -> string)
Sylvain Dailler's avatar
Sylvain Dailler committed
40

Sylvain Dailler's avatar
Sylvain Dailler committed
41 42
(* The first argument is not used: these functions are supposed to be given to a
   Qtask. *)
43
val print_id: 'a -> Trans.naming_table -> string list -> string
Sylvain Dailler's avatar
Sylvain Dailler committed
44
val search_id: search_both:bool -> 'a -> Trans.naming_table -> string list -> string
Sylvain Dailler's avatar
Sylvain Dailler committed
45

46
val list_strategies : Controller_itp.controller -> (string * string) list
Sylvain Dailler's avatar
Sylvain Dailler committed
47 48 49
val list_provers: Controller_itp.controller -> _ -> string
val list_transforms: unit -> (string * Pp.formatted) list
val list_transforms_query: _ -> _ -> string
50
(* val help_on_queries: Format.formatter -> (string * string * 'a) list -> unit *)
51 52
val load_strategies: Controller_itp.controller -> unit

Sylvain Dailler's avatar
Sylvain Dailler committed
53 54 55 56 57 58 59 60 61

(** Command line parsing tools *)

val return_prover: string -> Whyconf.config -> Whyconf.config_prover option

type command =
  | Transform    of string * Trans.gentrans * string list
  | Prove        of Whyconf.config_prover * Call_provers.resource_limit
  | Strategies   of string
62
  | Edit         of Whyconf.prover
63
  | Get_ce
64
  | Bisect
65
  | Replay       of bool
Sylvain Dailler's avatar
Sylvain Dailler committed
66 67
  | Clean
  | Mark_Obsolete
68 69
  | Focus_req
  | Unfocus_req
Sylvain Dailler's avatar
Sylvain Dailler committed
70 71 72 73 74
  | Help_message of string
  | Query        of string
  | QError       of string
  | Other        of string * string list

75
val interp:
76
  (string * query) Wstdlib.Hstr.t ->
77
  Controller_itp.controller ->
78
  Session_itp.any option -> string -> command
79

80 81 82 83 84 85 86 87 88
(* Find the first unproven goal around the node given.
   @param always_send: if true then always returns something
   @param proved     : oracle for proved node
   @param children   : returns the list children of a node
   @param get_parent : returns the parent of a node
   @param is_goal    : answer true iff a given node is a goal
   @param is_pa      : answer true iff a given node is a proof attempt
   @param node       : node_id
*)
89
val get_first_unproven_goal_around:
90 91 92 93 94 95
    always_send:bool ->
      proved:('a -> bool) ->
        children:('a -> 'a list) ->
          get_parent:('a -> 'a option) ->
            is_goal:('a -> bool) ->
              is_pa:('a -> bool) -> 'a -> 'a option