printer/drivers for Alt-Ergo

drivers/alt_ergo.drv

+(* Driver for the most recent version of Alt-Ergo *)
+
 import "alt_ergo_bare.drv"
 
 theory BuiltIn
@@ -7,15 +9,11 @@ end
 
 theory int.EuclideanDivision
 
-  (* workaround for the "-1 % 32 = -1" bug *)
-  prelude "logic safe_modulo: int, int -> int"
-  prelude "axiom safe_modulo_def: forall x, y:int. x >= 0 and y > 0 -> safe_modulo(x,y) = x % y"
   syntax function div "(%1 / %2)"
-  syntax function mod "safe_modulo(%1,%2)"
+  syntax function mod "(%1 % %2)"
 
 end
 
-
 theory map.Map
   syntax type  map "(%1,%2) farray"
 

drivers/alt_ergo_0.92.drv

+(* Driver for Alt-Ergo version <= 0.92 *)
+
+import "alt_ergo_bare.drv"
+
+theory BuiltIn
+  meta "printer_option" "no_type_cast"
+end
+
+(*
+Local Variables:
+mode: why
+compile-command: "make -C .. bench"
+End:
+*)

drivers/alt_ergo_0.93.drv

+(* Driver for Alt-Ergo 0.93.
+   Differences wrt 0.92 are
+   - enumeration types
+   - maps
+*)
+
 import "alt_ergo_bare.drv"
 
 theory BuiltIn
   meta "eliminate_algebraic" "keep_enums"
+  meta "printer_option"      "no_type_cast"
 end
 
 theory map.Map

drivers/alt_ergo_0.94.drv

+(* Driver for Alt-Ergo 0.94.
+   Differences wrt 0.93 are
+   - record types
+   - Euclidean division
+*)
+
+import "alt_ergo_0.93.drv"
+
+theory BuiltIn
+  meta "eliminate_algebraic" "keep_recs"
+end
+
+theory int.EuclideanDivision
+
+  (* workaround for the "-1 % 32 = -1" bug *)
+  prelude "logic safe_modulo: int, int -> int"
+  prelude "axiom safe_modulo_def: forall x, y:int. x >= 0 and y > 0 -> safe_modulo(x,y) = x % y"
+  syntax function div "(%1 / %2)"
+  syntax function mod "safe_modulo(%1,%2)"
+
+end
+
+
+(*
+Local Variables:
+mode: why
+compile-command: "make -C .. bench"
+End:
+*)

drivers/alt_ergo_model.drv

+(* Driver for the current version of Alt-Ergo with models *)
 
-import "alt_ergo_bare.drv"
+import "alt_ergo.drv"
 
 theory BuiltIn
   meta "printer_option" "show_labels"
-  meta "eliminate_algebraic" "keep_enums"
-  meta "eliminate_algebraic" "keep_recs"
 end
 
 
-theory int.EuclideanDivision
-
-  syntax function div "(%1 / %2)"
-  syntax function mod "(%1 % %2)"
-
-end
-
-theory map.Map
-  syntax type  map "(%1,%2) farray"
-
-  syntax function get "(%1[%2])"
-  syntax function set "(%1[%2 <- %3])"
-
-  remove prop Select_eq
-  remove prop Select_neq
-end
-
 
 (*
 Local Variables:

share/provers-detection-data.conf.in

 [ATP alt-ergo-model]
 name = "Alt-Ergo"
+alternative = "models"
 exec = "alt-ergo"
 exec = "alt-ergo-0.95-dev"
 version_switch = "-version"
 version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
+version_ok = "0.95"
 version_ok = "0.95-dev"
 command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timelimit %t -model %f"
 driver = "drivers/alt_ergo_model.drv"
 editor = "altgr-ergo"
 
+[ATP alt-ergo]
+name = "Alt-Ergo"
+exec = "alt-ergo"
+exec = "alt-ergo-0.95"
+exec = "alt-ergo-0.95-dev"
+version_switch = "-version"
+version_regexp = "\\([0-9.]+\\(-dev\\)?\\)"
+version_ok = "0.95"
+version_ok = "0.95-dev"
+command = "'@LOCALBIN@why3-cpulimit' %T %m -s %e -timelimit %t %f"
+driver = "drivers/alt_ergo.drv"
+editor = "altgr-ergo"
+
 [ATP alt-ergo]
 name = "Alt-Ergo"
 exec = "alt-ergo"
@@ -17,7 +32,7 @@ version_switch = "-version"
 version_regexp = "\\([0-9.]+\\)"
 version_ok = "0.94"
 command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
-driver = "drivers/alt_ergo.drv"
+driver = "drivers/alt_ergo_0.94.drv"
 editor = "altgr-ergo"
 
 [ATP alt-ergo]
@@ -51,7 +66,7 @@ version_old = "0.91"
 version_old = "0.9"
 version_old = "0.8"
 command = "'@LOCALBIN@why3-cpulimit' %t %m -s %e %f"
-driver = "drivers/alt_ergo_bare.drv"
+driver = "drivers/alt_ergo_0.92.drv"
 
 [ATP cvc3]
 name = "CVC3"

src/driver/autodetection.ml

@@ -76,7 +76,7 @@ let prover_keys =
   List.fold_left add Sstr.empty
     ["name";"exec";"version_switch";"version_regexp";
      "version_ok";"version_old";"version_bad";"command";
-     "editor";"driver";"in_place";"message"]
+     "editor";"driver";"in_place";"message";"alternative";]
 
 let load_prover kind (id,section) =
   check_exhaustive section prover_keys;
@@ -84,7 +84,7 @@ let load_prover kind (id,section) =
   let prover = { kind = kind;
     prover_id = id;
     prover_name = get_string section "name";
-    prover_altern = get_string section ~default:"" "altern";
+    prover_altern = get_string section ~default:"" "alternative";
     execs = get_stringl section "exec";
     version_switch = get_string section ~default:"" "version_switch";
     version_regexp = get_string section ~default:"" "version_regexp";

src/printer/alt_ergo.ml

@@ -30,6 +30,7 @@ type info = {
   info_syn : syntax_map;
   info_ac  : Sls.t;
   info_show_labels : bool;
+  info_type_casts : bool;
   info_csm : lsymbol list Mls.t;
   info_pjs : Sls.t;
   info_axs : Spr.t;
@@ -85,6 +86,19 @@ and print_tyapp info fmt = function
   | [ty] -> fprintf fmt "%a " (print_type info) ty
   | tl -> fprintf fmt "(%a) " (print_list comma (print_type info)) tl
 
+(* can the type of a value be derived from the type of the arguments? *)
+let unambig_fs fs =
+  let rec lookup v ty = match ty.ty_node with
+    | Tyvar u when tv_equal u v -> true
+    | _ -> ty_any (lookup v) ty
+  in
+  let lookup v = List.exists (lookup v) fs.ls_args in
+  let rec inspect ty = match ty.ty_node with
+    | Tyvar u when not (lookup u) -> false
+    | _ -> ty_all inspect ty
+  in
+  inspect (Opt.get fs.ls_value)
+
 let rec print_term info fmt t = match t.t_node with
   | Tconst c ->
       let number_format = {
@@ -111,8 +125,11 @@ let rec print_term info fmt t = match t.t_node with
             (List.combine (Mls.find ls info.info_csm) tl)
       | None when Sls.mem ls info.info_pjs ->
           fprintf fmt "%a.%a" (print_tapp info) tl print_ident ls.ls_name
-      | None ->
+      | None when unambig_fs ls || not info.info_type_casts ->
           fprintf fmt "%a%a" print_ident ls.ls_name (print_tapp info) tl
+      | None ->
+          fprintf fmt "(%a%a : %a)" print_ident ls.ls_name (print_tapp info) tl
+             (print_type info) (t_type t)
     end
   | Tlet _ -> unsupportedTerm t
       "alt-ergo : you must eliminate let in term"
@@ -306,14 +323,15 @@ let add_projection (csm,pjs,axs) = function
       csm, Sls.add ls pjs, Spr.add pr axs
   | _ -> assert false
 
-let check_showlabels acc l =
-  match l with
-    | [Theory.MAstr s] ->
-      begin match s with
-        | "show_labels" -> true
-        | _ -> acc
-      end
-    | _ -> assert false
+let check_showlabels acc = function
+  | [Theory.MAstr "show_labels"] -> true
+  | [Theory.MAstr _] -> acc
+  | _ -> assert false
+
+let check_typecasts acc = function
+  | [Theory.MAstr "no_type_cast"] -> false
+  | [Theory.MAstr _] -> acc
+  | _ -> assert false
 
 (*
 let print_task_old pr thpr fmt task =
@@ -340,11 +358,12 @@ let () = register_printer "alt-ergo-old"
 *)
 
 let print_decls =
-  let print ac sl csm pjs axs sm fmt d =
+  let print ac sl tc csm pjs axs sm fmt d =
     let info = {
       info_syn = sm;
       info_ac  = ac;
       info_show_labels = sl;
+      info_type_casts = tc;
       info_csm = Mls.map Array.to_list csm;
       info_pjs = pjs;
       info_axs = axs;
@@ -353,10 +372,11 @@ let print_decls =
   Trans.on_tagged_ls meta_ac (fun ac ->
   Trans.on_meta meta_printer_option (fun args ->
     let sl = List.fold_left check_showlabels false args in
+    let tc = List.fold_left check_typecasts  true  args in
   Trans.on_meta Eliminate_algebraic.meta_proj (fun mal ->
     let csm,pjs,axs = List.fold_left
       add_projection (Mls.empty,Sls.empty,Spr.empty) mal in
-    Printer.sprint_decls (print ac sl csm pjs axs))))
+    Printer.sprint_decls (print ac sl tc csm pjs axs))))
 
 let print_task _env pr thpr _blacklist ?old:_ fmt task =
   (* In trans-based p-printing [forget_all] is a no-no *)