prover identification: use shortcuts

   shortcuts are defined in why3.conf. They are automatically
   generated using two mechanism:
   - a shortcut section in prover-detection-data.conf creates a shortcut
   for the first prover that match the regexp

   - the identifier used as family argument for the prover section in
   prover-detection-data.conf is used as shortcut for the prover. If
   different sections use the same argument the first one that match an
   existing prover is used for the shortcut.

bench/bench

@@ -87,10 +87,10 @@ bad_programs () {
 valid_goals () {
     for f in $1/*.mlw; do
 	echo -n "  "$f"... "
-	if $pgml -L modules -t 10 -P Alt-Ergo $f | grep -q -v Valid; then
+	if $pgml -L modules -t 10 -P alt-ergo $f | grep -q -v Valid; then
 	    echo "valid test $f failed!"
 	    echo "$pgml -P alt-ergo $f"
-	    $pgml -L modules -t 10 -P Alt-Ergo $f
+	    $pgml -L modules -t 10 -P alt-ergo $f
 	    exit 1
        else 
 	    echo "ok"

share/provers-detection-data.conf.in

@@ -306,3 +306,7 @@ command = "emacs23 --eval \"(setq coq-load-path '((\\\"%l/coq\\\" \\\"Why3\\\"))
 [editor altgr-ergo]
 name = "AltGr-Ergo"
 command = "altgr-ergo %f"
+
+[shortcut shortcut1]
+name="Alt-Ergo"
+shortcut="altergo"

src/coq-tactic/test.v

@@ -3,7 +3,7 @@ Require Export ZArith.
 Open Scope Z_scope.
 Require Export List.
 
-Ltac ae := why3 "Alt-Ergo".
+Ltac ae := why3 "alt-ergo".
 
 Section S0.
   Variable a:Set->Set.

src/coq-tactic/why3tac.ml

@@ -1108,7 +1108,7 @@ let tr_top_decl = function
   | _, Lib.FrozenState _ -> ()
 
 let pr_fp fp =
-  pr_str (Pp.string_of_wnl Whyconf.print_filter_prover_no_regexp fp)
+  pr_str (Pp.string_of_wnl Whyconf.print_filter_prover fp)
 
 let why3tac ?(timelimit=timelimit) s gl =
   (* print_dep Format.err_formatter; *)

src/driver/autodetection.ml

@@ -126,12 +126,45 @@ let load rc =
   let tps = List.fold_left (cons (load_prover ITP)) atps itps in
   tps
 
+let load_prover_shortcut acc (_, section) =
+  let name = get_string section "name" in
+  let version = get_stringo section "version" in
+  let altern = get_stringo section "alternative" in
+  let shortcuts = get_stringl section "shortcut" in
+  let fp = mk_filter_prover ?version ?altern name in
+  List.fold_left (fun acc shortcut ->
+    (fp,shortcut)::acc
+  ) acc shortcuts
+
+type env =
+  {
+    (** memoization of (exec_name,version_switch)
+        -> Some output | None doesn't exists *)
+    prover_output : ((string * string),string option) Hashtbl.t;
+    (** existing executable table:
+        exec_name -> | Some prover_config unknown version (neither good or bad)
+                     | None               there is a good version *)
+    prover_unknown_version : (string, config_prover option) Hashtbl.t;
+    (** string -> prover *)
+    prover_shortcuts : (string, prover) Hashtbl.t;
+    mutable possible_prover_shortcuts : (filter_prover * string) list;
+  }
+
+let create_env shortcuts =
+{ prover_output = Hashtbl.create 10;
+  prover_unknown_version = Hashtbl.create 10;
+  prover_shortcuts = Hashtbl.create 5;
+  possible_prover_shortcuts = shortcuts;
+ }
+
 let read_auto_detection_data main =
   let filename = Filename.concat (Whyconf.datadir main)
     "provers-detection-data.conf" in
   try
     let rc = Rc.from_file filename in
-    List.rev (load rc)
+    let shortcuts =
+      List.fold_left load_prover_shortcut [] (get_family rc "shortcut") in
+    List.rev (load rc), create_env shortcuts
   with
     | Failure "lexing" ->
         Loc.errorm "Syntax error in provers-detection-data.conf@."
@@ -174,21 +207,6 @@ let sanitize_exec =
   in
   sanitizer first rest
 
-type env =
-  {
-    (** memoization of (exec_name,version_switch)
-        -> Some output | None doesn't exists *)
-    prover_output : ((string * string),string option) Hashtbl.t;
-    (** existing executable table:
-        exec_name -> | Some prover_config unknown version (neither good or bad)
-                     | None               there is a good version *)
-    prover_unknown_version : (string, config_prover option) Hashtbl.t;
-  }
-
-let create_env () =
-{ prover_output = Hashtbl.create 10;
-  prover_unknown_version = Hashtbl.create 10 }
-
 let ask_prover_version exec_name version_switch =
   let out = Filename.temp_file "out" "" in
   let cmd = sprintf "%s %s" exec_name version_switch in
@@ -255,6 +273,19 @@ let add_prover_with_uniq_id prover provers =
   let prover = {prover with Wc.prover = prover_id} in
   Mprover.add prover_id prover provers
 
+let add_prover_shortcuts env prover =
+  let rec aux = function
+    | [] -> []
+    | (fp,s)::l when filter_prover fp prover ->
+      Hashtbl.replace env.prover_shortcuts s prover;
+      aux l
+    | a::l -> a::(aux l) in
+  env.possible_prover_shortcuts <- aux env.possible_prover_shortcuts
+
+let add_id_prover_shortcut env id prover =
+  if not (Hashtbl.mem env.prover_shortcuts id) then
+    Hashtbl.replace env.prover_shortcuts id prover
+
 let detect_exec env main data acc exec_name =
   let s = ask_prover_version env exec_name data.version_switch in
   match s with
@@ -318,6 +349,8 @@ let detect_exec env main data acc exec_name =
         (def_option (if old then " (it is an old version)." else ", Ok.")
            data.message);
       known_version env exec_name;
+      add_prover_shortcuts env prover;
+      add_id_prover_shortcut env data.prover_id prover;
       add_prover_with_uniq_id prover_config acc
     end
     else (unknown_version env exec_name prover_config; acc)
@@ -338,23 +371,32 @@ let detect_unknown env detected =
       add_prover_with_uniq_id prover_config acc)
     env.prover_unknown_version detected
 
+let convert_shortcuts env =
+  Hashtbl.fold (fun s p acc ->
+    Mstr.add s p acc
+  ) env.prover_shortcuts Mstr.empty
+
 let run_auto_detection config =
   let main = get_main config in
-  let l = read_auto_detection_data main in
-  let env = create_env () in
-  let detect = List.fold_left (detect_prover env main) Mprover.empty l in
-  let length_detected = Mprover.cardinal detect in
-  let detect = detect_unknown env detect in
-  let length_unsupported_version = Mprover.cardinal detect - length_detected in
+  let l,env = read_auto_detection_data main in
+  let detected = List.fold_left (detect_prover env main) Mprover.empty l in
+  let length_detected = Mprover.cardinal detected in
+  let detected = detect_unknown env detected in
+  let length_unsupported_version =
+    Mprover.cardinal detected - length_detected in
   eprintf
     "%d provers detected and %d provers detected with unsupported version@."
     length_detected length_unsupported_version;
-  set_provers (set_editors config (read_editors main)) detect
+  let shortcuts = convert_shortcuts env in
+  let config = set_editors config (read_editors main) in
+  let config = set_prover_shortcuts config shortcuts in
+  let config = set_provers config detected in
+  config
 
 let list_prover_ids () =
   let config = default_config "/dev/null" in
   let main = get_main config in
-  let l = read_auto_detection_data main in
+  let l,_ = read_auto_detection_data main in
   let s = List.fold_left (fun s p -> Sstr.add p.prover_id s) Sstr.empty l in
   Sstr.elements s
 
@@ -374,12 +416,20 @@ let get_altern id path =
   let alt = Filename.basename path in
   get_suffix id alt
 
+let add_existing_shortcuts env shortcuts =
+  let aux shortcut prover =
+    Hashtbl.replace env.prover_shortcuts shortcut prover;
+    env.possible_prover_shortcuts <-
+    List.filter (fun (_,s) -> s = shortcut) env.possible_prover_shortcuts
+  in
+  Mstr.iter aux shortcuts
+
 let add_prover_binary config id path =
   let main = get_main config in
-  let l = read_auto_detection_data main in
+  let l,env = read_auto_detection_data main in
+  add_existing_shortcuts env (get_prover_shortcuts config);
   let l = List.filter (fun p -> p.prover_id = id) l in
   if l = [] then Loc.errorm "Unknown prover id: %s" id;
-  let env = create_env () in
   let detected = List.fold_left
     (fun acc data -> detect_exec env main data acc path) Mprover.empty l in
   let detected = detect_unknown env detected in
@@ -399,4 +449,7 @@ let add_prover_binary config id path =
     let p = {p with prover = prover_id} in
     add_prover_with_uniq_id p provers in
   let provers = Mprover.fold fold detected provers in
-  set_provers config provers
+  let shortcuts = convert_shortcuts env in
+  let config = set_prover_shortcuts config shortcuts in
+  let config = set_provers config provers in
+  config

src/driver/whyconf.ml

@@ -201,6 +201,7 @@ type config = {
   config    : Rc.t;
   main      : main;
   provers   : config_prover Mprover.t;
+  prover_shortcuts : prover Mstr.t;
   editors   : config_editor Meditor.t;
   provers_upgrade_policy : prover_upgrade_policy Mprover.t;
 }
@@ -250,6 +251,19 @@ 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 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
+  ("definition", section)::family
+
+let set_prover_shortcuts rc shortcuts =
+  let family = Mstr.fold set_prover_shortcut shortcuts [] in
+  set_family rc "shortcut" family
+
 let set_editor id editor (ids, family) =
   if Sstr.mem id ids then raise NonUniqueId;
   let section = empty_section in
@@ -312,6 +326,20 @@ let load_prover dirname provers (_,section) =
       extra_drivers = [];
     } provers
 
+let load_shortcut acc (_,section) =
+  let name = get_string section "name" in
+  let version = get_string section "version" in
+  let altern = get_string ~default:"" section "alternative" in
+  let shortcuts = get_stringl section "shortcut" in
+  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
+
 let load_editor editors (id, section) =
   Meditor.add id
     { editor_name = get_string ~default:id section "name";
@@ -384,6 +412,8 @@ let get_config (filename,rc) =
   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 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
@@ -392,6 +422,7 @@ let get_config (filename,rc) =
     config    = rc;
     main      = main;
     provers   = provers;
+    prover_shortcuts = shortcuts;
     editors   = editors;
     provers_upgrade_policy = policy;
   }
@@ -414,31 +445,31 @@ let read_config conf_file =
     raise (ConfigFailure (fst filenamerc, Buffer.contents b))
 
 (** filter prover *)
+type regexp_desc = { reg : Str.regexp; desc : string}
+
+let mk_regexp s = { reg = why3_regexp_of_string s; desc = s}
+
 type filter_prover =
-  { filter_name    : Str.regexp; filter_desc_name    : string;
-    filter_version : Str.regexp; filter_desc_version : string;
-    filter_altern  : Str.regexp; filter_desc_altern  : string;
+  { filter_name    : regexp_desc;
+    filter_version : regexp_desc option;
+    filter_altern  : regexp_desc option;
   }
 
-let mk_filter_prover ?(version="^") ?(altern="^") ~name =
-  let reg = why3_regexp_of_string in
-  { filter_name    = reg name    ; filter_desc_name    = name;
-    filter_version = reg version ; filter_desc_version = version;
-    filter_altern  = reg altern  ; filter_desc_altern  = altern}
+let mk_filter_prover ?version ?altern name =
+  begin match version with
+  | Some "" -> invalid_arg "mk_filter_prover: version can't be an empty string"
+  | _ -> () end;
+  { filter_name    = mk_regexp name;
+    filter_version = option_map mk_regexp version;
+    filter_altern  = option_map mk_regexp altern;
+  }
 
 let print_filter_prover fmt fp =
-  fprintf fmt "%s,%s,%s"
-    fp.filter_desc_name fp.filter_desc_version fp.filter_desc_altern
-
-let print_filter_prover_no_regexp fmt fp =
-  let all s = s = "^" in
-  fprintf fmt "%s%s%s"
-    fp.filter_desc_name
-    (if all fp.filter_desc_version then
-        (if all fp.filter_desc_altern then "" else ",")
-     else "," ^ fp.filter_desc_version)
-    (if all fp.filter_desc_altern then ""
-     else ("," ^ fp.filter_desc_altern))
+  match fp.filter_version, fp.filter_altern with
+  | None  , None -> fprintf fmt "%s" fp.filter_name.desc
+  | Some v, None -> fprintf fmt "%s,%s" fp.filter_name.desc v.desc
+  | None  , Some a -> fprintf fmt "%s,,%s" fp.filter_name.desc a.desc
+  | Some v, Some a -> fprintf fmt "%s,%s,%s" fp.filter_name.desc v.desc a.desc
 
 exception ProverNotFound  of config * filter_prover
 exception ProverAmbiguity of config * filter_prover * config_prover  Mprover.t
@@ -446,46 +477,42 @@ exception ParseFilterProver of string
 
 let parse_filter_prover s =
   let sl = Util.split_string_rev s ',' in
-  let match_all = Str.regexp "" in
-  let reg = why3_regexp_of_string in
   (* reverse order *)
   match sl with
-  | [name] ->
-    {filter_name    = reg name    ; filter_desc_name    = name;
-     filter_version = match_all   ; filter_desc_version = "^";
-     filter_altern  = match_all  ; filter_desc_altern   = "^"}
-  | [version;name] ->
-    {filter_name    = reg name    ; filter_desc_name    = name;
-     filter_version = reg version ; filter_desc_version = version;
-     filter_altern  = match_all   ; filter_desc_altern  = "^"}
-  | [altern;"";name] ->
-    {filter_name    = reg name    ; filter_desc_name    = name;
-     filter_version = match_all   ; filter_desc_version = "^";
-     filter_altern  = reg altern  ; filter_desc_altern  = altern}
-  | [altern;version;name] ->
-    {filter_name    = reg name    ; filter_desc_name    = name;
-     filter_version = reg version ; filter_desc_version = version;
-     filter_altern  = reg altern  ; filter_desc_altern  = altern}
+  | [name] -> mk_filter_prover name
+  | [version;name] -> mk_filter_prover ~version name
+  | [altern;"";name] -> mk_filter_prover ~altern name
+  | [altern;version;name] -> mk_filter_prover ~version ~altern name
   | _ -> raise (ParseFilterProver s)
 
 let filter_prover fp p =
-  let check schema s = Str.string_match schema s 0 in
-  check fp.filter_name p.prover_name
-  && check fp.filter_version p.prover_version
-  && check fp.filter_altern p.prover_altern
+  let check s schema = Str.string_match schema.reg s 0 in
+  check p.prover_name fp.filter_name
+  && option_apply true (check p.prover_version) fp.filter_version
+  && option_apply true (check p.prover_altern) fp.filter_altern
 
 let filter_provers whyconf fp =
-  Mprover.filter (fun p _ -> filter_prover fp p) whyconf.provers
-
-let filter_one_prover config fp =
-  let provers = Mprover.filter (fun k _ -> filter_prover fp k)
-    config.provers in
+  try
+    if fp.filter_version = None && fp.filter_altern = None then
+      let prover = (Mstr.find fp.filter_name.desc whyconf.prover_shortcuts) in
+      try
+        let prover_config = Mprover.find prover whyconf.provers in
+        Mprover.singleton prover prover_config
+      with Not_found ->
+        (** shortcut send to nothing *)
+        Mprover.empty
+    else raise Not_found
+  with Not_found ->
+    Mprover.filter (fun p _ -> filter_prover fp p) whyconf.provers
+
+let filter_one_prover whyconf fp =
+  let provers = filter_provers whyconf fp in
   if Mprover.is_num_elt 1 provers then
     snd (Mprover.choose provers)
   else if Mprover.is_empty provers then
-    raise $ ProverNotFound (config,fp)
+    raise $ ProverNotFound (whyconf,fp)
   else
-    raise $ ProverAmbiguity (config,fp,provers)
+    raise $ ProverAmbiguity (whyconf,fp,provers)
 
 (** merge config *)
 
@@ -504,13 +531,9 @@ let merge_config config filename =
   (** modify provers *)
   let create_filter_prover section =
     let name = get_string section "name" in
-    let version = get_string ~default:"^" section "version" in
-    let altern = get_string ~default:"^" section "alternative" in
-    { filter_name = why3_regexp_of_string name;
-      filter_version = why3_regexp_of_string version;
-      filter_altern = why3_regexp_of_string altern;
-      filter_desc_name = ""; filter_desc_version = ""; filter_desc_altern = "";
-    } in
+    let version = get_stringo section "version" in
+    let altern = get_stringo section "alternative" in
+    mk_filter_prover ?version ?altern name in
   let prover_modifiers = get_family rc "prover_modifiers" in
   let prover_modifiers =
     List.map (fun (_,sec) -> create_filter_prover sec, sec) prover_modifiers in
@@ -551,6 +574,7 @@ let save_config config =
 
 let get_main config = config.main
 let get_provers config = config.provers
+let get_prover_shortcuts config = config.prover_shortcuts
 let get_policies config = config.provers_upgrade_policy
 let get_prover_upgrade_policy config p =
   Mprover.find p config.provers_upgrade_policy
@@ -567,6 +591,12 @@ let set_provers config provers =
     provers = provers;
   }
 
+let set_prover_shortcuts config shortcuts =
+  {config with
+    config = set_prover_shortcuts config.config shortcuts;
+    prover_shortcuts = shortcuts;
+  }
+
 let set_editors config editors =
   { config with
     config = set_editors config.config editors;
@@ -626,10 +656,10 @@ let () = Exn_printer.register (fun fmt e -> match e with
   | NonUniqueId ->
     Format.fprintf fmt "InternalError : two provers share the same id"
   | ProverNotFound (config,fp) ->
-    fprintf fmt "No prover in %s corresponds to %a@."
+    fprintf fmt "No prover in %s corresponds to \"%a\"@."
       (get_conf_file config) print_filter_prover fp
   | ProverAmbiguity (config,fp,provers ) ->
-    fprintf fmt "More than one prover in %s correspond to %a: %a@."
+    fprintf fmt "More than one prover@ in %s@ correspond@ to \"%a\":@ %a@."
       (get_conf_file config) print_filter_prover fp
       (Pp.print_iter2 Mprover.iter Pp.space Pp.nothing print_prover Pp.nothing)
       provers

src/driver/whyconf.mli

@@ -129,6 +129,12 @@ val set_provers : config -> config_prover Mprover.t -> config
 val is_prover_known : config -> prover -> bool
 (** test if a prover is detected *)
 
+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 *)
+
 type config_editor = {
   editor_name : string;
   editor_command : string;
@@ -173,14 +179,11 @@ val set_policies : config -> prover_upgrade_policy Mprover.t -> config
 type filter_prover
 
 val mk_filter_prover :
-  ?version:string -> ?altern:string -> name:string -> filter_prover
+  ?version:string -> ?altern:string -> (* name *) string -> filter_prover
 
 val print_filter_prover :
   Format.formatter -> filter_prover -> unit
 
-val print_filter_prover_no_regexp :
-  Format.formatter -> filter_prover -> unit
-
 val parse_filter_prover : string -> filter_prover
 (** parse the string representing a filter_prover:
     - "name,version,altern"