server_utils.mli 3.79 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
val set_session_timelimit : int -> unit
(** sets the default timelimit in seconds. Initially set to 2. *)

val set_session_memlimit : int -> unit
(** sets the default mem in Mb. Initially set to 1000. *)


Sylvain Dailler's avatar
Sylvain Dailler committed
37 38 39 40 41 42 43 44 45
(** 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)
46
  | Qtask of (Controller_itp.controller -> Trans.naming_table -> string list -> string)
Sylvain Dailler's avatar
Sylvain Dailler committed
47

Sylvain Dailler's avatar
Sylvain Dailler committed
48 49
(* The first argument is not used: these functions are supposed to be given to a
   Qtask. *)
50
val print_id: 'a -> Trans.naming_table -> string list -> string
Sylvain Dailler's avatar
Sylvain Dailler committed
51
val search_id: search_both:bool -> 'a -> Trans.naming_table -> string list -> string
Sylvain Dailler's avatar
Sylvain Dailler committed
52

53
val list_strategies : Controller_itp.controller -> (string * string) list
Sylvain Dailler's avatar
Sylvain Dailler committed
54 55 56
val list_provers: Controller_itp.controller -> _ -> string
val list_transforms: unit -> (string * Pp.formatted) list
val list_transforms_query: _ -> _ -> string
57
(* val help_on_queries: Format.formatter -> (string * string * 'a) list -> unit *)
58 59
val load_strategies: Controller_itp.controller -> unit

Sylvain Dailler's avatar
Sylvain Dailler committed
60 61 62 63 64 65 66 67 68

(** 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
69
  | Edit         of Whyconf.prover
70
  | Get_ce
71
  | Bisect
72
  | Replay       of bool
Sylvain Dailler's avatar
Sylvain Dailler committed
73 74
  | Clean
  | Mark_Obsolete
75 76
  | Focus_req
  | Unfocus_req
Sylvain Dailler's avatar
Sylvain Dailler committed
77 78 79 80 81
  | Help_message of string
  | Query        of string
  | QError       of string
  | Other        of string * string list

82
val interp:
83
  (string * query) Wstdlib.Hstr.t ->
84
  Controller_itp.controller ->
85
  Session_itp.any option -> string -> command
86

87 88 89 90 91 92 93 94 95
(* 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
*)
96
val get_first_unproven_goal_around:
97 98 99 100 101 102
    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