Commit 4b6bea69 authored by François Bobot's avatar François Bobot

prover shortcuts: the shortcuts information can be in the prover section in...

prover shortcuts: the shortcuts information can be in the prover section in order to reduce the number of section in why3.conf
parent 1b16ce5e
......@@ -456,6 +456,5 @@ let add_prover_binary config id path =
add_prover_with_uniq_id p provers in
let provers = Mprover.fold fold detected provers in
let shortcuts = convert_shortcuts env in
let config = set_prover_shortcuts config shortcuts in
let config = set_provers config provers in
let config = set_provers config ~shortcuts provers in
config
......@@ -235,7 +235,7 @@ let set_main rc main =
exception NonUniqueId
let set_prover _ prover family =
let set_prover _ (prover,shortcuts) family =
let section = empty_section in
let section = set_string section "name" prover.prover.prover_name in
let section = set_string section "command" prover.command in
......@@ -246,25 +246,49 @@ let set_prover _ prover family =
let section = set_string section "editor" prover.editor in
let section = set_bool section "interactive" prover.interactive in
let section = set_bool section "in_place" prover.in_place in
let section = set_stringl section "shortcut" shortcuts in
("config", section)::family
let set_provers rc provers =
let family = Mprover.fold set_prover provers [] in
set_family rc "prover" family
let set_prover_shortcut shortcut prover family =
let set_prover_shortcut prover shortcuts family =
let section = empty_section in
let section = set_string section "name" prover.prover_name in
let section = set_string section "version" prover.prover_version in
let section =
set_string ~default:"" section "alternative" prover.prover_altern in
let section = set_string section "shortcut" shortcut in
let section = set_stringl section "shortcut" shortcuts in
("definition", section)::family
let set_prover_shortcuts rc shortcuts =
let family = Mstr.fold set_prover_shortcut shortcuts [] in
let family = Mprover.fold set_prover_shortcut shortcuts [] in
set_family rc "shortcut" family
let set_provers_shortcuts rc shortcuts provers =
(** inverse the shortcut map *)
let shortcuts = Mstr.fold (fun shortcut prover acc ->
Mprover.change (function
| None -> Some [shortcut]
| Some l -> Some (shortcut::l)) prover acc) shortcuts Mprover.empty in
(** the shortcut to unknown prover *)
let shortcuts_prover_unknown = Mprover.set_diff shortcuts provers in
let rc = set_prover_shortcuts rc shortcuts_prover_unknown in
(** merge the known *)
let _,shortcuts_provers_known =
Mprover.mapi_fold (fun k v acc ->
let acc = Mprover.next_ge_enum k acc in
match Mprover.val_enum acc with
| None -> acc,(v,[])
| Some (ks,vs) ->
let c = Prover.compare k ks in
if c = 0 then acc,(v,vs)
else (* c < 0 *) acc,(v,[])
) provers (Mprover.start_enum shortcuts) in
let rc = set_provers rc shortcuts_provers_known in
rc
let set_editor id editor (ids, family) =
if Sstr.mem id ids then raise NonUniqueId;
let section = empty_section in
......@@ -306,7 +330,17 @@ let set_policies rc policy =
let absolute_filename = Sysutil.absolutize_filename
let load_prover dirname provers (_,section) =
exception DuplicateShortcut of string
let add_prover_shortcuts acc prover shortcuts =
List.fold_left (fun acc shortcut ->
if shortcut.[0] = '^' then
invalid_arg "prover shortcut can't start with a ^";
Mstr.add_new (DuplicateShortcut shortcut) shortcut prover acc
) acc shortcuts
let load_prover dirname (provers,shortcuts) (_,section) =
let name = get_string section "name" in
let version = get_string ~default:"" section "version" in
let altern = get_string ~default:"" section "alternative" in
......@@ -316,7 +350,7 @@ let load_prover dirname provers (_,section) =
prover_altern = altern;
}
in
Mprover.add prover
let provers = Mprover.add prover
{ prover = prover;
command = get_string section "command";
driver = absolute_filename dirname (get_string section "driver");
......@@ -325,7 +359,10 @@ let load_prover dirname provers (_,section) =
interactive = get_bool ~default:false section "interactive";
extra_options = [];
extra_drivers = [];
} provers
} provers in
let lshort = get_stringl section ~default:[] "shortcut" in
let shortcuts = add_prover_shortcuts shortcuts prover lshort in
provers,shortcuts
let load_shortcut acc (_,section) =
let name = get_string section "name" in
......@@ -335,11 +372,7 @@ let load_shortcut acc (_,section) =
let prover = { prover_name = name;
prover_version = version;
prover_altern= altern} in
List.fold_left (fun acc shortcut ->
if shortcut.[0] = '^' then
invalid_arg "prover shortcut can't start with a ^";
Mstr.add shortcut prover acc
) acc shortcuts
add_prover_shortcuts acc prover shortcuts
let load_editor editors (id, section) =
Meditor.add id
......@@ -412,9 +445,10 @@ let get_config (filename,rc) =
| Some main -> rc, load_main dirname main
in
let provers = get_family rc "prover" in
let provers = List.fold_left (load_prover dirname) Mprover.empty provers in
let shortcuts = get_family rc "shortcut" in
let shortcuts = List.fold_left load_shortcut Mstr.empty shortcuts in
let provers,shortcuts = List.fold_left (load_prover dirname)
(Mprover.empty,Mstr.empty) provers in
let fam_shortcuts = get_family rc "shortcut" in
let shortcuts = List.fold_left load_shortcut shortcuts fam_shortcuts in
let editors = get_family rc "editor" in
let editors = List.fold_left load_editor Meditor.empty editors in
let policy = get_family rc "uninstalled_prover" in
......@@ -552,8 +586,9 @@ let merge_config config filename =
extra_drivers = drv @ c.extra_drivers })
provers
) config.provers prover_modifiers in
let provers =
List.fold_left (load_prover dirname) provers (get_family rc "prover") in
let provers,shortcuts =
List.fold_left (load_prover dirname)
(provers,config.prover_shortcuts) (get_family rc "prover") in
(** modify editors *)
let editor_modifiers = get_family rc "editor_modifiers" in
let editors = List.fold_left
......@@ -566,7 +601,8 @@ let merge_config config filename =
) config.editors editor_modifiers in
(** add editors *)
let editors = List.fold_left load_editor editors (get_family rc "editor") in
{ config with main = main; provers = provers; editors = editors }
{ config with main = main; provers = provers;
prover_shortcuts = shortcuts; editors = editors }
let save_config config =
let filename = config.conf_file in
......@@ -586,15 +622,17 @@ let set_main config main =
main = main;
}
let set_provers config provers =
let set_provers config ?shortcuts provers =
let shortcuts = def_option config.prover_shortcuts shortcuts in
{config with
config = set_provers config.config provers;
config = set_provers_shortcuts config.config shortcuts provers;
provers = provers;
prover_shortcuts = shortcuts;
}
let set_prover_shortcuts config shortcuts =
{config with
config = set_prover_shortcuts config.config shortcuts;
config = set_provers_shortcuts config.config shortcuts config.provers;
prover_shortcuts = shortcuts;
}
......@@ -668,4 +706,7 @@ let () = Exn_printer.register (fun fmt e -> match e with
fprintf fmt
"Syntax error prover identification '%s' : \
name[,version[,alternative]|,,alternative]" s
| DuplicateShortcut s ->
fprintf fmt
"Shortcut %s appears two times in the configuration file" s
| _ -> raise e)
......@@ -33,6 +33,7 @@ type config
{!Whyconf.get_provers}, {!Whyconf.set_provers} *)
exception ConfigFailure of string (* filename *) * string
exception DuplicateShortcut of string
val read_config : string option -> config
(** [read_config conf_file] :
......@@ -122,7 +123,8 @@ val get_provers : config -> config_prover Mprover.t
(** [get_provers config] get the prover family stored in the Rc file. The
keys are the unique ids of the prover (argument of the family) *)
val set_provers : config -> config_prover Mprover.t -> config
val set_provers : config ->
?shortcuts:Mprover.key Util.Mstr.t -> config_prover Mprover.t -> config
(** [set_provers config provers] replace all the family prover by the
one given *)
......
......@@ -80,6 +80,12 @@ module type S =
val add_new : exn -> key -> 'a -> 'a t -> 'a t
val keys: 'a t -> key list
val values: 'a t -> 'a list
type 'a enumeration
val val_enum : 'a enumeration -> (key * 'a) option
val start_enum : 'a t -> 'a enumeration
val next_enum : 'a enumeration -> 'a enumeration
val start_ge_enum : key -> 'a t -> 'a enumeration
val next_ge_enum : key -> 'a enumeration -> 'a enumeration
module type Set =
sig
......@@ -617,6 +623,37 @@ module Make(Ord: OrderedType) = struct
fold (fun _ _ n -> if n < 0 then raise Exit else n-1) m n = 0
with Exit -> false
let start_enum s = cons_enum s End
let val_enum = function
| End -> None
| More (v,d,_,_) -> Some (v,d)
let next_enum = function
| End -> End
| More(_,_,r,e) -> cons_enum r e
let rec cons_ge_enum k m e =
match m with
Empty -> e
| Node(l, v, d, r, _) ->
let c = Ord.compare k v in
if c = 0 then More(v,d,r,e)
else if c < 0 then cons_ge_enum k l (More(v, d, r, e))
else (* c > 0 *) cons_ge_enum k r e
let start_ge_enum k m = cons_ge_enum k m End
let rec next_ge_enum k r0 = function
| End -> start_ge_enum k r0
| More(v,_,r,e) as e0 ->
let c = Ord.compare k v in
if c = 0 then e0
else if c < 0 then cons_ge_enum k r0 e0
else (* c > 0 *) next_ge_enum k r e
let next_ge_enum k e = next_ge_enum k Empty e
module type Set =
sig
type elt = key
......
......@@ -286,6 +286,27 @@ module type S =
to the ordering [Ord.compare] of the keys, where [Ord] is the argument
given to {!Map.Make}. *)
(** enumeration: zipper style *)
type 'a enumeration
val val_enum : 'a enumeration -> (key * 'a) option
(** get the current key value pair of the enumeration, return None
if the enumeration reach the end *)
val start_enum : 'a t -> 'a enumeration
(** start the enumeration of the given map *)
val next_enum : 'a enumeration -> 'a enumeration
(** get the next step of the enumeration *)
val start_ge_enum : key -> 'a t -> 'a enumeration
(** start the enumeration of the given map at the first key which
is greater or equal than the given one *)
val next_ge_enum : key -> 'a enumeration -> 'a enumeration
(** get the next (or same) step of the enumeration which key is
greater or equal to the given key *)
module type Set =
sig
type elt = key
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment