whyconf.mli 4.73 KB
Newer Older
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)

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

22 23
open Util

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

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

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

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

46
val save_config : config -> unit
Francois Bobot's avatar
Francois Bobot committed
47 48
(** [save_config config] save the configuration *)

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

53 54 55 56 57 58 59 60 61 62
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

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

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

type config_prover = {
  name    : string;   (* "Alt-Ergo v2.95 (special)" *)
  command : string;   (* "exec why-limit %t %m alt-ergo %f" *)
  driver  : string;   (* "/usr/local/share/why/drivers/ergo-spec.drv" *)
  version : string;   (* "v2.95" *)
  editor  : string;   (* Interative theorem prover *)
}

93
val get_provers : config  -> config_prover Mstr.t
Francois Bobot's avatar
Francois Bobot committed
94 95
(** [get_main config] get the prover family stored in the Rc file. The
    keys are the unique ids of the prover (argument of the family) *)
96 97

val set_provers : config -> config_prover Mstr.t -> config
Francois Bobot's avatar
Francois Bobot committed
98 99
(** [set_provers config provers] replace all the family prover by the
    one given *)
100

Francois Bobot's avatar
Francois Bobot committed
101
(** Access to the Rc.t *)
102
val get_section : config -> string -> Rc.section option
Francois Bobot's avatar
Francois Bobot committed
103 104
(** [get_section config name] Same as {!Rc.get_section} except name
    must not be "main" *)
105
val get_family  : config -> string -> Rc.family
Francois Bobot's avatar
Francois Bobot committed
106 107
(** [get_family config name] Same as {!Rc.get_family} except name
    must not be prover *)
108 109

val set_section : config -> string -> Rc.section -> config
Francois Bobot's avatar
Francois Bobot committed
110 111
(** [set_section config name] Same as {!Rc.set_section} except name
    must not be "main" *)
112
val set_family  : config -> string -> Rc.family  -> config
Francois Bobot's avatar
Francois Bobot committed
113 114
(** [set_family config name] Same as {!Rc.set_family} except name
    must not be prover *)