whyconf.mli 8.33 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
MARCHE Claude's avatar
MARCHE Claude committed
3
(*  Copyright (C) 2010-2012                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
MARCHE Claude committed
7
(*    Guillaume Melquiond                                                 *)
8 9 10 11 12 13 14 15 16 17 18 19 20
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

21
(** Managing the configuration of Why3 *)
Francois Bobot's avatar
Francois Bobot committed
22

23 24
open Util

25
(** {2 General configuration} *)
MARCHE Claude's avatar
MARCHE Claude committed
26

27
type config
Francois Bobot's avatar
Francois Bobot committed
28 29 30 31 32 33
(** 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} *)
34

35 36
exception ConfigFailure of string (* filename *) * string

Francois Bobot's avatar
Francois Bobot committed
37 38
val read_config : string option -> config
(** [read_config conf_file] :
39
    - If conf_file is given and the file doesn't exist Rc.CannotOpen is
40
    raised.
41 42
    - If "$WHY3CONFIG" is given and the file doesn't exist Rc.CannotOpen
    is raised
43 44
    - otherwise we try reading "$HOME/.why3.conf" (or
    "$USERPROFILE/.why3.conf" under Windows) and, if not present, we return
45
    the built-in default_config with default configuration filename *)
Francois Bobot's avatar
Francois Bobot committed
46

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

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

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

58 59 60 61 62 63 64 65 66 67
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

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

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

90 91 92
(** {3 Prover's identifier} *)

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

val print_prover : Format.formatter -> prover -> unit
100 101
val print_prover_parsable_format : Format.formatter -> prover -> unit

102
(** Printer for prover *)
103
module Prover   : Util.OrderedHash with type t = prover
104 105 106 107 108 109
module Mprover  : Stdlib.Map.S with type key = prover
module Sprover  : Mprover.Set
module Hprover  : Hashtbl.S with type key = prover

(** {3 Prover configuration} *)

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

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

125
val set_provers : config -> config_prover Mprover.t -> config
Francois Bobot's avatar
Francois Bobot committed
126 127
(** [set_provers config provers] replace all the family prover by the
    one given *)
128

129 130 131
val is_prover_known : config -> prover -> bool
(** test if a prover is detected *)

132 133 134 135 136 137
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 *)

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

module Meditor : Stdlib.Map.S with type key = string

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

149 150 151
val get_editors : config -> config_editor Meditor.t
(** returns the set of editors *)

152 153 154 155
val editor_by_id : config -> string -> config_editor
(** return the configuration of the editor if found, otherwise return
    Not_found *)

156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177

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

178 179 180 181
(** filter prover *)
type filter_prover

val mk_filter_prover :
182
  ?version:string -> ?altern:string -> (* name *) string -> filter_prover
183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212

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

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
(** test if the prover match the filter prover *)

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

213 214
(** {2 For accesing other parts of the configuration } *)

Francois Bobot's avatar
Francois Bobot committed
215
(** Access to the Rc.t *)
216
val get_section : config -> string -> Rc.section option
Francois Bobot's avatar
Francois Bobot committed
217 218
(** [get_section config name] Same as {!Rc.get_section} except name
    must not be "main" *)
219
val get_family  : config -> string -> Rc.family
Francois Bobot's avatar
Francois Bobot committed
220 221
(** [get_family config name] Same as {!Rc.get_family} except name
    must not be prover *)
222 223

val set_section : config -> string -> Rc.section -> config
Francois Bobot's avatar
Francois Bobot committed
224 225
(** [set_section config name] Same as {!Rc.set_section} except name
    must not be "main" *)
226
val set_family  : config -> string -> Rc.family  -> config
Francois Bobot's avatar
Francois Bobot committed
227 228
(** [set_family config name] Same as {!Rc.set_family} except name
    must not be prover *)