use prover instead of string as key for provers

src/bench/benchdb.ml

@@ -55,7 +55,7 @@ let rec goal whyconf env path dbgoal wgoal =
       let prover_name = Db.prover_name prover_id in
       let driver,command =
         try
-          let p = Mstr.find prover_name (Whyconf.get_provers whyconf) in
+          let p = Whyconf.prover_by_id whyconf prover_name in
           p.Whyconf.driver ,p.Whyconf.command
         with
       (* TODO add exceptions pehaps inside rc.ml in fact*)

src/bench/benchrc.ml

@@ -75,7 +75,7 @@ let read_tools absf wc map (name,section) =
   (* provers *)
   let provers = get_stringl ~default:[] section "prover" in
   let find_provers s =
-    try let p = Mstr.find s (get_provers wc) in
+    try let p = prover_by_id wc s in
         s,p.driver ,p.command
     with
       (* TODO add exceptions pehaps inside rc.ml in fact*)
@@ -90,7 +90,7 @@ let read_tools absf wc map (name,section) =
   let load_driver (n,d,c) = n,Driver.load_driver env d,c in
   let provers = List.map load_driver provers in
   let create_tool (n,driver,command) =
-    { tval = {tool_name = name; prover_name = n; tool_db =
+    { tval = {Bench.tool_name = name; prover_name = n; tool_db =
         if Db.is_initialized () then Some (Db.prover_from_name n) else None};
       ttrans = transforms;
       tdriver = driver;

src/bench/whybench.ml

@@ -247,8 +247,9 @@ let () =
   if !opt_list_provers then begin
     opt_list := true;
     let config = read_config !opt_config in
-    let print fmt s prover = fprintf fmt "%s (%s)@\n" s prover.name in
-    let print fmt m = Mstr.iter (print fmt) m in
+    let print fmt prover _ = fprintf fmt "%s (%s)@\n"
+      prover.prover_id prover.prover_name in
+    let print fmt m = Mprover.iter (print fmt) m in
     let provers = get_provers config in
     printf "@[<hov 2>Known provers:@\n%a@]@." print provers
   end;
@@ -333,9 +334,7 @@ let () =
 
 
   let map_prover s =
-    let prover = try Mstr.find s (get_provers config) with
-      | Not_found -> eprintf "Prover %s not found.@." s; exit 1
-    in
+    let prover = prover_by_id config s in
     { B.tval   = {B.tool_name = "cmdline"; prover_name = s; tool_db = None};
       ttrans   = [Trans.identity,None];
       tdriver  = load_driver env prover.driver;

src/driver/autodetection.ml

@@ -180,7 +180,10 @@ let detect_prover main acc l =
       with Not_found -> None
     in
     let prover = Util.list_first detect_execs l in
-    Mstr.add prover_id prover acc
+    let prover_id = {Whyconf.prover_id = prover_id;
+                     prover_name = prover.name;
+                     prover_version = prover.version} in
+    Mprover.add prover_id prover acc
   with Not_found ->
     eprintf "Prover %s not found.@." prover_id;
     acc
@@ -202,7 +205,7 @@ let run_auto_detection config =
   let l = read_auto_detection_data main in
   let cmp p q = String.compare p.prover_id q.prover_id in
   let l = Util.list_part cmp l in
-  let detect = List.fold_left (detect_prover main) Mstr.empty l in
-  let length = Mstr.cardinal detect in
+  let detect = List.fold_left (detect_prover main) Mprover.empty l in
+  let length = Mprover.cardinal detect in
   eprintf "%d provers detected.@." length;
   set_provers config detect

src/driver/whyconf.ml

@@ -20,6 +20,7 @@
 open Format
 open Util
 open Rc
+open Stdlib
 
 (* magicnumber for the configuration :
   - 0 before the magic number
@@ -50,6 +51,45 @@ let default_conf_file =
     | None -> Filename.concat (Rc.get_home_dir ()) ".why3.conf"
     | Some d -> Filename.concat d "why3.conf"
 
+(* Prover *)
+
+type prover =
+    { prover_id : string;
+      prover_name : string;
+      prover_version : string;
+    }
+
+let print_prover fmt p =
+  Format.fprintf fmt "%s(%s)" p.prover_name p.prover_version
+
+module Prover = struct
+  type t = prover
+  let compare s1 s2 =
+    if s1 == s2 then 0 else
+    let c = String.compare s1.prover_id s2.prover_id in
+    if c <> 0 then c else
+    let c = String.compare s1.prover_name s2.prover_name in
+    if c <> 0 then c else
+    let c = String.compare s1.prover_version s2.prover_version in
+    c
+
+  let equal s1 s2 =
+    s1.prover_id = s2.prover_id &&
+      s1.prover_name = s2.prover_name &&
+      s1.prover_version = s2.prover_version
+
+  let hash s1 =
+    2 * Hashtbl.hash s1.prover_id +
+      3 * Hashtbl.hash s1.prover_name +
+      5 * Hashtbl.hash s1.prover_version
+
+
+end
+
+module Mprover = Map.Make(Prover)
+module Sprover = Mprover.Set
+module Hprover = Hashtbl.Make(Prover)
+
 (* Configuration file *)
 
 type config_prover = {
@@ -128,7 +168,7 @@ type config = {
   conf_file : string;       (* "/home/innocent_user/.why3.conf" *)
   config    : Rc.t;
   main      : main;
-  provers   : config_prover Mstr.t;
+  provers   : config_prover Mprover.t;
 }
 
 let default_main =
@@ -157,7 +197,7 @@ let set_main rc main =
   let section = set_stringl section "plugin" main.plugins in
   set_section rc "main" section
 
-let set_prover id prover family =
+let set_prover prover_id prover family =
   let section = empty_section in
   let section = set_string section "name" prover.name in
   let section = set_string section "command" prover.command in
@@ -165,20 +205,27 @@ let set_prover id prover family =
   let section = set_string section "version" prover.version in
   let section = set_string section "editor" prover.editor in
   let section = set_bool section "interactive" prover.interactive in
-  (id,section)::family
+  (prover_id.prover_id,section)::family
 
 let set_provers rc provers =
-  let family = Mstr.fold set_prover provers [] in
+  let family = Mprover.fold set_prover provers [] in
   set_family rc "prover" family
 
 let absolute_filename = Sysutil.absolutize_filename
 
 let load_prover dirname provers (id,section) =
-  Mstr.add id
-    { name    = get_string section "name";
+  let version = get_string ~default:"" section "version" in
+  let name = get_string section "name" in
+  let prover =
+    { prover_id = id;
+      prover_name = name;
+      prover_version = version }
+  in
+  Mprover.add prover
+    { name    = name;
       command = get_string section "command";
       driver  = absolute_filename dirname (get_string section "driver");
-      version = get_string ~default:"" section "version";
+      version = version;
       editor  = get_string ~default:"" section "editor";
       interactive = get_bool ~default:false section "interactive";
     } provers
@@ -224,7 +271,7 @@ 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) Mstr.empty provers in
+  let provers = List.fold_left (load_prover dirname) Mprover.empty provers in
   { conf_file = filename;
     config    = rc;
     main      = main;
@@ -268,9 +315,43 @@ let set_provers config provers =
     provers = provers;
   }
 
+(*******)
+
 let set_conf_file config conf_file = {config with conf_file = conf_file}
 let get_conf_file config           =  config.conf_file
 
+(*******)
+
+let is_prover_known whyconf prover =
+  Mprover.mem prover (get_provers whyconf)
+
+exception ProverNotFound of config * string
+exception ProverAmbiguity of config * string * prover list
+
+let prover_by_id whyconf id =
+  let potentials =
+    Mprover.filter (fun p _ -> p.prover_id = id) whyconf.provers in
+  match Mprover.keys potentials with
+    | [] -> raise (ProverNotFound(whyconf,id))
+    | [_] -> snd (Mprover.choose potentials)
+    |  l -> raise (ProverAmbiguity(whyconf,id,l))
+
+let () = Exn_printer.register
+  (fun fmt exn ->
+    match exn with
+      | ProverNotFound (config,s) ->
+        fprintf fmt "Prover '%s' not found in %s@."
+          s (get_conf_file config)
+      | ProverAmbiguity (config,s,l) ->
+        fprintf fmt "More than one provers corresponds to '%s' in %s:@.%a@."
+          s (get_conf_file config)
+          (Pp.print_list Pp.newline print_prover) l
+      | e -> raise e
+  )
+
+
+(******)
+
 let get_section config name = assert (name <> "main");
   get_section config.config name
 
@@ -283,3 +364,4 @@ let set_section config name section = assert (name <> "main");
 
 let set_family config name section = assert (name <> "prover");
   {config with config = set_family config.config name section}
+

src/driver/whyconf.mli

@@ -82,6 +82,26 @@ val load_plugins : main -> unit
 
 (** {2 Provers} *)
 
+(** {3 Prover's identifier} *)
+
+type prover =
+    { prover_id : string;
+      prover_name : string;
+      prover_version : string;
+    }
+    (** record of necessary data for a given external prover
+        In the future prover_id will disappear.
+    *)
+
+val print_prover : Format.formatter -> prover -> unit
+(** Printer for prover *)
+
+module Mprover  : Stdlib.Map.S with type key = prover
+module Sprover  : Mprover.Set
+module Hprover  : Hashtbl.S with type key = prover
+
+(** {3 Prover configuration} *)
+
 type config_prover = {
   name    : string;   (* "Alt-Ergo v2.95 (special)" *)
   command : string;   (* "exec why-limit %t %m alt-ergo %f" *)
@@ -91,14 +111,21 @@ type config_prover = {
   interactive : bool; (* Interative theorem prover *)
 }
 
-val get_provers : config  -> config_prover Mstr.t
+val get_provers : config  -> config_prover Mprover.t
 (** [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) *)
 
-val set_provers : config -> config_prover Mstr.t -> config
+val set_provers : config -> config_prover Mprover.t -> config
 (** [set_provers config provers] replace all the family prover by the
     one given *)
 
+val is_prover_known : config -> prover -> bool
+(** test if a prover is detected *)
+
+val prover_by_id : config -> string -> config_prover
+
+(** {2 For accesing other parts of the configuration } *)
+
 (** Access to the Rc.t *)
 val get_section : config -> string -> Rc.section option
 (** [get_section config name] Same as {!Rc.get_section} except name

src/ide/gmain.ml

@@ -31,6 +31,7 @@ open Whyconf
 open Gconfig
 open Util
 open Debug
+module C = Whyconf
 
 let debug = register_flag "gui"
 
@@ -133,20 +134,20 @@ let source_text fname =
 (* loading WhyIDE configuration *)
 (********************************)
 
-let loadpath = (Whyconf.loadpath (get_main ())) @ List.rev !includes
+let loadpath = (C.loadpath (get_main ())) @ List.rev !includes
 
 let gconfig =
   let c = Gconfig.config () in
   c.env <- Env.create_env loadpath;
 (*
-  let provers = Whyconf.get_provers c.Gconfig.config in
+  let provers = C.get_provers c.Gconfig.config in
   c.provers <-
     Util.Mstr.fold (Session.get_prover_data c.env) provers Util.Mstr.empty;
 *)
   c
 
 let () =
-  Whyconf.load_plugins (get_main ())
+  C.load_plugins (get_main ())
 
 let () =
   Debug.Opt.set_flags_selected ();
@@ -544,7 +545,7 @@ let init =
          | S.File f -> Filename.basename f.S.file_name
          | S.Proof_attempt a ->
            let p = a.S.proof_prover in
-           p.Session.prover_name ^ " " ^ p.Session.prover_version
+           p.C.prover_name ^ " " ^ p.C.prover_version
          | S.Transf tr -> tr.S.transf_name);
     notify any
 
@@ -612,7 +613,7 @@ let info_window ?(callback=(fun () -> ())) mt s =
 
 (* check if provers are present *)
 let () =
-  if Util.Mstr.is_empty (Whyconf.get_provers gconfig.Gconfig.config) then
+  if C.Mprover.is_empty (C.get_provers gconfig.Gconfig.config) then
     begin
       info_window `ERROR
         "No prover configured.\nPlease run 'why3config --detect-provers' first"
@@ -989,16 +990,16 @@ let () = add_refresh_provers (fun () ->
 
 let () =
   let add_item_provers () =
-    S.Sprover.iter
-      (fun p ->
-         let n = p.S.prover_name ^ " " ^ p.S.prover_version in
+    C.Mprover.iter
+      (fun p _ ->
+         let n = p.C.prover_name ^ " " ^ p.C.prover_version in
          let (_ : GMenu.image_menu_item) =
            tools_factory#add_image_item ~label:n
              ~callback:(fun () -> prover_on_selected_goals p)
              ()
          in
          let b = GButton.button ~packing:provers_box#add ~label:n () in
-         b#misc#set_tooltip_markup ("Start <tt>" ^ p.S.prover_name ^
+         b#misc#set_tooltip_markup ("Start <tt>" ^ p.C.prover_name ^
            "</tt> on the <b>selected goals</b>");
 
 (* prend de la place pour rien
@@ -1009,7 +1010,7 @@ let () =
            b#connect#pressed
              ~callback:(fun () -> prover_on_selected_goals p)
          in ())
-      (S.get_known_provers !env_session)
+      (C.get_provers gconfig.Gconfig.config)
   in
   add_refresh_provers add_item_provers "Add in tools menu and provers box";
   add_item_provers ()

src/ide/html_session.ml

@@ -19,6 +19,7 @@
 
 open Format
 open Why3
+module C = Whyconf
 
 let files = Queue.create ()
 let opt_version = ref false
@@ -152,7 +153,7 @@ let run_file (context : context) print_session f =
 module Simple =
 struct
 
-  let print_prover fmt pd = fprintf fmt "%s" pd.prover_name
+  let print_prover fmt pd = fprintf fmt "%s" pd.C.prover_name
 
   let print_proof_status fmt = function
     | Undone _ -> fprintf fmt "Undone"
@@ -222,7 +223,7 @@ struct
     then fprintf fmt "class='verified'"
     else fprintf fmt "class='notverified'"
 
-  let print_prover fmt pd = fprintf fmt "%s" pd.prover_name
+  let print_prover fmt pd = fprintf fmt "%s" pd.C.prover_name
 
   let print_proof_status fmt = function
     | Undone _ -> fprintf fmt "<span class='notverified'>Undone</span>"

src/ide/replay.ml

@@ -21,6 +21,7 @@
 open Format
 open Why3
 module S = Session
+module C = Whyconf
 
 let includes = ref []
 let file = ref None
@@ -183,7 +184,7 @@ let init =
         | S.File f -> Filename.basename f.S.file_name
         | S.Proof_attempt a ->
           let p = a.S.proof_prover in
-          p.S.prover_name ^ " " ^ p.S.prover_version
+          p.C.prover_name ^ " " ^ p.C.prover_version
         | S.Transf tr -> tr.S.transf_name
     in
     (* eprintf "Item '%s' loaded@." name *)
@@ -339,7 +340,7 @@ let rec provers_latex_stats provers theory =
   S.theory_iter_proof_attempt (fun a ->
     Hashtbl.replace provers a.S.proof_prover a.S.proof_prover) theory
 
-let prover_name a = a.S.prover_name ^ " " ^ a.S.prover_version
+let prover_name a = a.C.prover_name ^ " " ^ a.C.prover_version
 
 let protect s =
   let b = Buffer.create 7 in
@@ -498,7 +499,7 @@ let print_head n depth provers fmt =
         (depth + 1)
   else
     fprintf fmt "\\hline Proof obligations ";
-  List.iter (fun a -> fprintf fmt "& \\provername{%s} " a.S.prover_name)
+  List.iter (fun a -> fprintf fmt "& \\provername{%s} " a.C.prover_name)
     provers;
   fprintf fmt "\\\\ @."
 
@@ -549,7 +550,7 @@ let theory_latex_stat n table dir t =
   let provers = Hashtbl.fold (fun _ pr acc -> pr :: acc)
     provers [] in
   let provers =
-    List.sort (fun p1 p2 -> String.compare p1.S.prover_name p2.S.prover_name)
+    List.sort (fun p1 p2 -> String.compare p1.C.prover_name p2.C.prover_name)
       provers in
   let depth = theory_depth  t in
   let name = t.S.theory_name.Ident.id_string in
@@ -571,7 +572,7 @@ let print_latex_statistics n table dir session =
   S.PHstr.iter (fun _ f -> file_latex_stat n table dir f) files
 
 let print_report (g,p,r) =
-  printf "   goal '%s', prover '%a': " g.Ident.id_string S.print_prover p;
+  printf "   goal '%s', prover '%a': " g.Ident.id_string C.print_prover p;
   match r with
   | M.Result(new_res,old_res) ->
     (* begin match !opt_smoke with *)

src/ide/stats.ml

@@ -16,6 +16,7 @@
 open Format
 open Why3
 open Util
+module C = Whyconf
 
 open Session
 
@@ -142,7 +143,7 @@ let rec stats_of_goal prefix_name stats goal =
             begin
               match result.Call_provers.pr_answer with
                 | Call_provers.Valid ->
-                    (prover.prover_name, result.Call_provers.pr_time) :: acc
+                    (prover.C.prover_name, result.Call_provers.pr_time) :: acc
                 | _ ->
                   acc
             end
@@ -176,11 +177,11 @@ let stats_of_file stats _ file =
   List.iter (stats_of_theory file stats) theories
 
 let fill_prover_data stats session =
-  Sprover.iter
+  C.Sprover.iter
     (fun prover ->
-      Hashtbl.add stats.prover_data prover.prover_id
-        (prover.prover_name ^ " " ^ prover.prover_version))
-    (get_provers session)
+      Hashtbl.add stats.prover_data prover.C.prover_id
+        (prover.C.prover_name ^ " " ^ prover.C.prover_version))
+    (get_used_provers session)
 
 let extract_stats_from_file stats fname =
   let project_dir = get_project_dir fname in

src/main.ml

@@ -257,8 +257,9 @@ let () = try
   if !opt_list_provers then begin
     opt_list := true;
     let config = read_config !opt_config in
-    let print fmt s prover = fprintf fmt "%s (%s)@\n" s prover.name in
-    let print fmt m = Mstr.iter (print fmt) m in
+    let print fmt prover _ = fprintf fmt "%s (%s)@\n"
+      prover.prover_id prover.prover_name in
+    let print fmt m = Mprover.iter (print fmt) m in
     let provers = get_provers config in
     printf "@[<hov 2>Known provers:@\n%a@]@." print provers
   end;
@@ -319,12 +320,9 @@ let () = try
   if !opt_memlimit  = None then opt_memlimit  := Some (Whyconf.memlimit main);
   begin match !opt_prover with
   | Some s ->
-      let prover = try Mstr.find s (get_provers config) with
-        | Not_found -> eprintf "Prover '%s' not found in %s@."
-            s (Whyconf.get_conf_file config); exit 1
-      in
-      opt_command := Some prover.command;
-      opt_driver := Some prover.driver
+    let prover = Whyconf.prover_by_id config s in
+    opt_command := Some prover.command;
+    opt_driver := Some prover.driver
   | None ->
       ()
   end;

src/session/session.ml

@@ -20,49 +20,17 @@
 open Stdlib
 open Debug
 
+module Mprover = Whyconf.Mprover
+module Sprover = Whyconf.Sprover
+module PHprover = Whyconf.Hprover
+module C = Whyconf
+
 let debug = Debug.register_flag "session"
 
 (** {2 Type definitions} *)
 
 module PHstr = Util.Hstr
 
-type prover =
-    { prover_id : string;
-      prover_name : string;
-      prover_version : string;
-    }
-
-let print_prover fmt p =
-  Format.fprintf fmt "%s(%s)" p.prover_name p.prover_version
-
-module Prover = struct
-  type t = prover
-  let compare s1 s2 =
-    if s1 == s2 then 0 else
-    let c = String.compare s1.prover_id s2.prover_id in
-    if c <> 0 then c else
-    let c = String.compare s1.prover_name s2.prover_name in
-    if c <> 0 then c else
-    let c = String.compare s1.prover_version s2.prover_version in
-    c
-
-  let equal s1 s2 =
-    s1.prover_id = s2.prover_id &&
-      s1.prover_name = s2.prover_name &&
-      s1.prover_version = s2.prover_version
-
-  let hash s1 =
-    2 * Hashtbl.hash s1.prover_id +
-      3 * Hashtbl.hash s1.prover_name +
-      5 * Hashtbl.hash s1.prover_version
-
-
-end
-
-module Mprover = Map.Make(Prover)
-module Sprover = Mprover.Set
-module PHprover = Hashtbl.Make(Prover)
-
 type undone_proof =
     | Scheduled (** external proof attempt is scheduled *)
     | Interrupted
@@ -92,7 +60,7 @@ type 'a goal =
 
 and 'a proof_attempt =
     { proof_key : 'a;
-      proof_prover : prover;
+      proof_prover : Whyconf.prover;
       proof_parent : 'a goal;
       mutable proof_state : proof_attempt_status;
       mutable proof_timelimit : int;
@@ -143,7 +111,7 @@ type loaded_prover =
     { prover_config : Whyconf.config_prover;
       prover_driver : Driver.driver}
 
-type loaded_provers = loaded_prover option PHstr.t
+type loaded_provers = loaded_prover option PHprover.t
 
 type 'a env_session =
     { env : Env.env;
@@ -203,7 +171,8 @@ let iter_transf f t =
   List.iter (fun g -> f g) t.transf_goals
 
 let goal_iter f g =
-  PHprover.iter (fun _ a -> f (Proof_attempt a)) g.goal_external_proofs;
+  PHprover.iter
+    (fun _ a -> f (Proof_attempt a)) g.goal_external_proofs;
   PHstr.iter (fun _ t -> f (Transf t)) g.goal_transformations
 
 let transf_iter f t =
@@ -239,7 +208,8 @@ module PTreeT = struct
           if g.goal_task = None
           then g.goal_name.Ident.id_string^"*"
           else g.goal_name.Ident.id_string
-        | Proof_attempt pr -> Pp.string_of_wnl print_prover pr.proof_prover
+        | Proof_attempt pr ->
+          Pp.string_of_wnl Whyconf.print_prover pr.proof_prover
         | Transf tr -> tr.transf_name in
       let l = ref [] in
       iter (fun a -> l := (Any a)::!l) t;
@@ -279,7 +249,7 @@ let load_env_session ?(includes=[]) session conf_path_opt =
   { session = session;
     env = env;
     whyconf = config;
-    loaded_provers = PHstr.create 5;
+    loaded_provers = PHprover.create 5;
   }
 
 (************************)
@@ -299,7 +269,7 @@ and get_session_trans transf = get_session_goal transf.transf_parent
 
 let get_session_proof_attempt pa = get_session_goal pa.proof_parent
 
-let get_provers session =
+let get_used_provers session =
   let sprover = ref Sprover.empty in
   session_iter_proof_attempt
     (fun pa -> sprover := Sprover.add pa.proof_prover !sprover)
@@ -407,7 +377,7 @@ let save_file provers fmt _ f =
 let save_prover fmt p (provers,id) =
   fprintf fmt "@\n@[<v 1><prover@ id=\"%i\"@ prover_id=\"%s\" \
 name=\"%s\"@ version=\"%s\"/>@]"
-    id p.prover_id p.prover_name p.prover_version;
+    id p.C.prover_id p.C.prover_name p.C.prover_version;
   Mprover.add p id provers, id+1