From ac98a7a410b73ee1ee6ba9db015735343bffc692 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= Date: Sun, 22 Jan 2012 19:48:59 -0600 Subject: [PATCH] use prover instead of string as key for provers --- src/bench/benchdb.ml | 2 +- src/bench/benchrc.ml | 4 +- src/bench/whybench.ml | 9 ++- src/driver/autodetection.ml | 9 ++- src/driver/whyconf.ml | 98 ++++++++++++++++++++++++++++--- src/driver/whyconf.mli | 31 +++++++++- src/ide/gmain.ml | 21 +++---- src/ide/html_session.ml | 5 +- src/ide/replay.ml | 11 ++-- src/ide/stats.ml | 11 ++-- src/main.ml | 14 ++--- src/session/session.ml | 82 +++++++------------------- src/session/session.mli | 34 ++--------- src/session/session_scheduler.ml | 4 +- src/session/session_scheduler.mli | 4 +- src/session/session_tools.ml | 9 +-- 16 files changed, 199 insertions(+), 149 deletions(-) diff --git a/src/bench/benchdb.ml b/src/bench/benchdb.ml index 69f269a4f..0fa9a3086 100644 --- a/src/bench/benchdb.ml +++ b/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*) diff --git a/src/bench/benchrc.ml b/src/bench/benchrc.ml index 41170dd82..2d93d3536 100644 --- a/src/bench/benchrc.ml +++ b/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; diff --git a/src/bench/whybench.ml b/src/bench/whybench.ml index d3799a1a7..08c75af8a 100644 --- a/src/bench/whybench.ml +++ b/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 "@[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; diff --git a/src/driver/autodetection.ml b/src/driver/autodetection.ml index e93206d8a..b76e2b9ea 100644 --- a/src/driver/autodetection.ml +++ b/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 diff --git a/src/driver/whyconf.ml b/src/driver/whyconf.ml index cc4fd6774..9ce91ea74 100644 --- a/src/driver/whyconf.ml +++ b/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} + diff --git a/src/driver/whyconf.mli b/src/driver/whyconf.mli index e8458baa7..cc4439033 100644 --- a/src/driver/whyconf.mli +++ b/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 diff --git a/src/ide/gmain.ml b/src/ide/gmain.ml index 34c78b020..817cea55f 100644 --- a/src/ide/gmain.ml +++ b/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 " ^ p.S.prover_name ^ + b#misc#set_tooltip_markup ("Start " ^ p.C.prover_name ^ " on the selected goals"); (* 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 () diff --git a/src/ide/html_session.ml b/src/ide/html_session.ml index 7d4b2183e..f67b17762 100644 --- a/src/ide/html_session.ml +++ b/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 "Undone" diff --git a/src/ide/replay.ml b/src/ide/replay.ml index 8b87f5505..0775bc652 100644 --- a/src/ide/replay.ml +++ b/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 *) diff --git a/src/ide/stats.ml b/src/ide/stats.ml index 41aa56e49..9732f6b8c 100644 --- a/src/ide/stats.ml +++ b/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 diff --git a/src/main.ml b/src/main.ml index eb8a84d3d..bb6d4a5cc 100644 --- a/src/main.ml +++ b/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 "@[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; diff --git a/src/session/session.ml b/src/session/session.ml index 376f3f053..fa7d38792 100644 --- a/src/session/session.ml +++ b/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@[@]" - 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 let save fname session = @@ -416,7 +386,7 @@ let save fname session = fprintf fmt "@\n"; fprintf fmt "@\n"; fprintf fmt "@[" fname; - let provers,_ = Sprover.fold (save_prover fmt) (get_provers session) + let provers,_ = Sprover.fold (save_prover fmt) (get_used_provers session) (Mprover.empty,0) in PHstr.iter (save_file provers fmt) session.session_files; fprintf fmt "@]@\n"; @@ -841,7 +811,7 @@ let load_file session old_provers f = let prover_id = string_attribute_def "prover_id" f id in let name = string_attribute "name" f in let version = string_attribute "version" f in - let p = {prover_id = prover_id; + let p = {C.prover_id = prover_id; prover_name = name; prover_version = version} in Util.Mstr.add id p old_provers @@ -1072,10 +1042,10 @@ let add_registered_transformation ~keygen env_session tr_name g = let load_prover eS prover = try - PHstr.find eS.loaded_provers prover.prover_id + PHprover.find eS.loaded_provers prover with Not_found -> let provers = Whyconf.get_provers eS.whyconf in - let r = Util.Mstr.find_option prover.prover_id provers in + let r = Mprover.find_option prover provers in let r = match r with | None -> None | Some pr -> @@ -1083,21 +1053,9 @@ let load_prover eS prover = Some { prover_config = pr; prover_driver = dr} in - PHstr.add eS.loaded_provers prover.prover_id r; + PHprover.add eS.loaded_provers prover r; r -let is_prover_known eS prover = - Util.Mstr.mem prover.prover_id (Whyconf.get_provers eS.whyconf) - -let get_known_provers eS = - Util.Mstr.fold (fun pid p acc -> - Sprover.add - {prover_id = pid; - prover_name = p.Whyconf.name; - prover_version = p.Whyconf.version} - acc) - (Whyconf.get_provers eS.whyconf) Sprover.empty - let () = Exn_printer.register (fun fmt exn -> match exn with @@ -1510,7 +1468,7 @@ let update_session ~keygen ~allow_obsolete old_session env whyconf = let new_env_session = { session = new_session; env = env; whyconf = whyconf; - loaded_provers = PHstr.create 5; + loaded_provers = PHprover.create 5; } in let obsolete = PHstr.fold (fun _ old_file acc -> dprintf debug "[Load] file '%s'@\n" old_file.file_name; diff --git a/src/session/session.mli b/src/session/session.mli index b7caa30ab..38bcc41b9 100644 --- a/src/session/session.mli +++ b/src/session/session.mli @@ -28,23 +28,7 @@ val debug : Debug.flag (** The debug flag "session" *) module PHstr : Util.PrivateHashtbl with type key = string -(** {2 Prover's data} *) - -type prover = private - { 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 PHprover : Util.PrivateHashtbl with type key = prover +module PHprover : Util.PrivateHashtbl with type key = Whyconf.prover (** {2 Proof attempts} *) @@ -94,7 +78,7 @@ type 'a goal = private and 'a proof_attempt = private { proof_key : 'a; - proof_prover : prover; + proof_prover : Whyconf.prover; proof_parent : 'a goal; mutable proof_state : proof_attempt_status; mutable proof_timelimit : int; @@ -178,7 +162,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 = private { env : Env.env; @@ -186,15 +170,9 @@ type 'a env_session = private loaded_provers : loaded_provers; session : 'a session} -val load_prover : 'a env_session -> prover -> loaded_prover option +val load_prover : 'a env_session -> Whyconf.prover -> loaded_prover option (** load a prover *) -val is_prover_known : 'a env_session -> prover -> bool -(** test if a prover is detected *) - -val get_known_provers : 'a env_session -> Sprover.t -(** get the set of known provers *) - (** {2 Update session} *) type 'key keygen = ?parent:'key -> unit -> 'key @@ -238,7 +216,7 @@ val proof_verified : 'key proof_attempt -> bool (** Return true if the proof is not obsolete and the result is valid *) -val get_provers : 'a session -> Sprover.t +val get_used_provers : 'a session -> Whyconf.Sprover.t (** Get the set of provers which appear in the session *) (** {2 Modificator} *) @@ -276,7 +254,7 @@ val add_external_proof : timelimit:int -> edit:string option -> 'key goal -> - prover -> + Whyconf.prover -> proof_attempt_status -> 'key proof_attempt diff --git a/src/session/session_scheduler.ml b/src/session/session_scheduler.ml index 03d1596d1..3c8e6deb3 100644 --- a/src/session/session_scheduler.ml +++ b/src/session/session_scheduler.ml @@ -352,7 +352,7 @@ let redo_external_proof eS eT ?timelimit g a = | None -> Debug.dprintf debug "[Info] Can't redo an external proof since the prover %a is not \ loaded@." - print_prover a.proof_prover + Whyconf.print_prover a.proof_prover | Some p -> if a.proof_edited_as = None && p.prover_config.Whyconf.interactive then set_proof_state ~notify ~obsolete:false (Undone Unedited) a @@ -551,7 +551,7 @@ let check_external_proof eS eT todo a = match load_prover eS ap with | None -> dprintf debug "[sched] prover not found : %a-%s@." - print_prover ap ap.prover_id; + Whyconf.print_prover ap ap.Whyconf.prover_id; Todo._done todo (g,ap,Prover_not_installed) (* set_proof_state ~notify ~obsolete:false a Undone *) | Some p -> diff --git a/src/session/session_scheduler.mli b/src/session/session_scheduler.mli index 19f718700..3aae7b88d 100644 --- a/src/session/session_scheduler.mli +++ b/src/session/session_scheduler.mli @@ -100,7 +100,7 @@ module Make(O: OBSERVER) : sig val run_prover : O.key env_session -> t -> context_unproved_goals_only:bool -> - timelimit:int -> prover -> O.key any -> unit + timelimit:int -> Whyconf.prover -> O.key any -> unit (** [run_prover p a] runs prover [p] on all goals under [a] the proof attempts are only scheduled for running, and they will be started asynchronously when processors are available @@ -156,7 +156,7 @@ module Make(O: OBSERVER) : sig val check_all: O.key env_session -> t -> - callback:((Ident.ident * prover * report) list -> unit) -> unit + callback:((Ident.ident * Whyconf.prover * report) list -> unit) -> unit (** [check_all ()] reruns all the proofs of the session, and reports for all proofs the current result and the new one (does not change the session state) diff --git a/src/session/session_tools.ml b/src/session/session_tools.ml index e62207174..2207ad401 100644 --- a/src/session/session_tools.ml +++ b/src/session/session_tools.ml @@ -17,13 +17,14 @@ (* *) (**************************************************************************) +open Whyconf open Session (** convert unknown prover *) let unknown_to_known_provers provers pu () = let module M = struct exception Perfect_prover_found of prover end in try - Sprover.fold (fun pk acc -> + Mprover.fold (fun pk _ acc -> if pk.prover_name = pu.prover_name then begin if pk.prover_version = pu.prover_version then raise (M.Perfect_prover_found pk); @@ -33,9 +34,9 @@ let unknown_to_known_provers provers pu () = with M.Perfect_prover_found pk -> [pk] let convert_unknown_prover ~keygen env_session = - let known_provers = get_known_provers env_session in - let provers = get_provers env_session.session in - let unknown_provers = Sprover.diff provers known_provers in + let known_provers = get_provers env_session.whyconf in + let provers = get_used_provers env_session.session in + let unknown_provers = Mprover.set_diff provers known_provers in if not (Sprover.is_empty unknown_provers) then begin (** construct the list of compatible provers for each unknown provers *) let unknown_provers = -- GitLab