whyconf.mli 8.28 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   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
(** Managing the configuration of Why3 *)
Francois Bobot's avatar
Francois Bobot committed
13

14
open Stdlib
15

16
(** {2 General configuration} *)
17

18
type config
Francois Bobot's avatar
Francois Bobot committed
19 20 21 22 23 24
(** A configuration linked to an rc file. Whyconf gives access to
    every sections of the rc file ({!Whyconf.get_section},
    {!Whyconf.set_section}, {!Whyconf.get_family},
    {!Whyconf.set_family}) but the section main and the family prover
    which are dealt by it ({!Whyconf.get_main}, {!Whyconf.set_main},
    {!Whyconf.get_provers}, {!Whyconf.set_provers} *)
25

26
exception ConfigFailure of string (* filename *) * string
27
exception DuplicateShortcut of string
28

Francois Bobot's avatar
Francois Bobot committed
29 30
val read_config : string option -> config
(** [read_config conf_file] :
31 32 33 34 35 36 37 38 39 40 41 42 43
    - If conf_file is given, then
      - if it is an empty string, an empty config is loaded,
      - if the file doesn't exist, Rc.CannotOpen is raised,
      - otherwise the content of the file is parsed and returned.
    - If conf_file is None and the WHY3CONFIG environment
      variable exists, then the above steps are executed with
      the content of the variable (possibly empty).
    - If neither conf_file nor WHY3CONFIG are present, the file
      "$HOME/.why3.conf" (or "$USERPROFILE/.why3.conf" under
      Windows) is checked for existence:
      - if present, the content is parsed and returned,
      - otherwise, we return the built-in default_config with a
        default configuration filename. *)
Francois Bobot's avatar
Francois Bobot committed
44

45
val merge_config : config -> string -> config
46
(** [merge_config config filename] merge the content of [filename]
47
    into [config] *)
48

49
val save_config : config -> unit
Francois Bobot's avatar
Francois Bobot committed
50 51
(** [save_config config] save the configuration *)

52
val default_config : string -> config
Francois Bobot's avatar
Francois Bobot committed
53 54
(** [ default_config filename ] create a default configuration which is going
    to be saved in [ filename ]*)
55

56 57 58 59 60 61 62 63 64 65
val get_conf_file : config -> string
(** [get_conf_file config] get the rc file corresponding to this
    configuration *)
(* val set_conf_file : config -> string -> config *)
(* (\** [set_conf_file config] set the rc file corresponding to this *)
(*     configuration *\) *)

(** {2 Main section} *)
type main

66
val get_main    : config  -> main
Francois Bobot's avatar
Francois Bobot committed
67
(** [get_main config] get the main section stored in the Rc file *)
68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87

val set_main    : config -> main                 -> config
(** [set_main config main] replace the main section by the given one *)

val libdir: main -> string
val datadir: main -> string
val loadpath: main -> string list
val timelimit: main -> int
val memlimit: main -> int
val running_provers_max: main -> int
val set_limits: main -> int -> int -> int -> main

val plugins : main -> string list
val pluginsdir : main -> string
val set_plugins : main -> string list -> main
val add_plugin : main -> string -> main
val load_plugins : main -> unit

(** {2 Provers} *)

88 89 90
(** {3 Prover's identifier} *)

type prover =
91 92 93
    { prover_name : string; (* "Alt-Ergo" *)
      prover_version : string; (* "2.95" *)
      prover_altern : string; (* "special" *)
94
    }
95
    (** record of necessary data for a given external prover *)
96 97

val print_prover : Format.formatter -> prover -> unit
98 99
val print_prover_parseable_format : Format.formatter -> prover -> unit
val prover_parseable_format : prover -> string
100

101
(** Printer for prover *)
102
module Prover   : OrderedHashedType with type t = prover
103 104 105
module Mprover  : Extmap.S with type key = prover
module Sprover  : Extset.S with module M = Mprover
module Hprover  : Exthtbl.S with type key = prover
106 107 108

(** {3 Prover configuration} *)

109
type config_prover = {
110
  prover : prover;  (* unique name for session *)
111 112
  command : string;   (* "exec why-limit %t %m alt-ergo %f" *)
  driver  : string;   (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
113
  in_place: bool;     (* verification should be performed in-place *)
114
  editor  : string;   (* Dedicated editor *)
115
  interactive : bool; (* Interactive theorem prover *)
116 117
  extra_options : string list;
  extra_drivers : string list;
118 119
}

120 121 122
val get_complete_command : config_prover -> string
(** add the extra_options to the command *)

123
val get_provers : config  -> config_prover Mprover.t
124
(** [get_provers config] get the prover family stored in the Rc file. The
Francois Bobot's avatar
Francois Bobot committed
125
    keys are the unique ids of the prover (argument of the family) *)
126

127
val set_provers : config ->
128
  ?shortcuts:Mprover.key Mstr.t -> config_prover Mprover.t -> config
Francois Bobot's avatar
Francois Bobot committed
129 130
(** [set_provers config provers] replace all the family prover by the
    one given *)
131

132 133 134
val is_prover_known : config -> prover -> bool
(** test if a prover is detected *)

135 136 137 138 139 140
val get_prover_shortcuts : config -> prover Mstr.t
(** return the prover shortcuts *)

val set_prover_shortcuts : config -> prover Mstr.t -> config
(** set the prover shortcuts *)

141
type config_editor = {
MARCHE Claude's avatar
MARCHE Claude committed
142
  editor_name : string;
143 144 145 146
  editor_command : string;
  editor_options : string list;
}

147
module Meditor : Extmap.S with type key = string
148 149 150 151

val set_editors : config -> config_editor Meditor.t -> config
(** replace the set of editors *)

152 153 154
val get_editors : config -> config_editor Meditor.t
(** returns the set of editors *)

155 156 157 158
val editor_by_id : config -> string -> config_editor
(** return the configuration of the editor if found, otherwise return
    Not_found *)

159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180

(** prover upgrade policy *)

type prover_upgrade_policy =
  | CPU_keep
  | CPU_upgrade of prover
  | CPU_duplicate of prover

val set_prover_upgrade_policy :
  config -> prover -> prover_upgrade_policy -> config
(** [set_prover_upgrade c p cpu] sets or updates the policy to follow if the
    prover [p] is absent from the system *)

val get_prover_upgrade_policy : config -> prover -> prover_upgrade_policy
(** [get_prover_upgrade config] returns a map providing the policy to
    follow for each absent prover (if it has already been decided
    by the user and thus stored in the config) *)

val get_policies : config -> prover_upgrade_policy Mprover.t

val set_policies : config -> prover_upgrade_policy Mprover.t -> config

181 182 183 184
(** filter prover *)
type filter_prover

val mk_filter_prover :
185
  ?version:string -> ?altern:string -> (* name *) string -> filter_prover
186 187 188 189 190 191 192 193 194 195 196 197 198 199

val print_filter_prover :
  Format.formatter -> filter_prover -> unit

val parse_filter_prover : string -> filter_prover
(** parse the string representing a filter_prover:
    - "name,version,altern"
    - "name,version" -> "name,version,^.*"
    - "name,,altern" -> "name,^.*,altern"
    - "name" -> "name,^.*,^.*"

    regexp must start with ^. Partial match will be used.
*)

200 201 202
val filter_prover_with_shortcut : config -> filter_prover -> filter_prover
(** resolve prover shortcut in filter *)

203 204 205 206
val filter_prover : filter_prover -> prover -> bool
(** test if the prover match the filter prover *)

val filter_provers : config -> filter_prover -> config_prover Mprover.t
207
(** Get all the provers that match this filter *)
208 209 210 211 212 213 214 215 216 217 218

exception ProverNotFound  of config * filter_prover
exception ProverAmbiguity of config * filter_prover * config_prover  Mprover.t
exception ParseFilterProver of string

val filter_one_prover : config -> filter_prover -> config_prover
(** find the uniq prover that verify the filter. If it doesn't exists
    raise ProverNotFound or raise ProverAmbiguity *)

val why3_regexp_of_string : string -> Str.regexp

219 220
(** {2 For accesing other parts of the configuration } *)

Francois Bobot's avatar
Francois Bobot committed
221
(** Access to the Rc.t *)
222
val get_section : config -> string -> Rc.section option
Francois Bobot's avatar
Francois Bobot committed
223 224
(** [get_section config name] Same as {!Rc.get_section} except name
    must not be "main" *)
225
val get_family  : config -> string -> Rc.family
Francois Bobot's avatar
Francois Bobot committed
226 227
(** [get_family config name] Same as {!Rc.get_family} except name
    must not be prover *)
228 229

val set_section : config -> string -> Rc.section -> config
Francois Bobot's avatar
Francois Bobot committed
230 231
(** [set_section config name] Same as {!Rc.set_section} except name
    must not be "main" *)
232
val set_family  : config -> string -> Rc.family  -> config
Francois Bobot's avatar
Francois Bobot committed
233 234
(** [set_family config name] Same as {!Rc.set_family} except name
    must not be prover *)