output-dir : Le nom du but n'est plus inutilement modifie lors de la génération du nom de fichier

src/core/ident.ml

@@ -117,6 +117,9 @@ let id_unique (indices,values,san0) ?(sanitizer = same) id =
     Hashtbl.replace values id.id_tag name;
     name
 
+let string_unique printer s =
+  id_unique printer (id_register (id_fresh s))
+
 let forget_id (indices,values,_) id =
   try
     let name = Hashtbl.find values id.id_tag in

src/core/ident.mli

@@ -78,6 +78,9 @@ val create_ident_printer :
 val id_unique :
   ident_printer -> ?sanitizer : (string -> string) -> ident -> string
 
+(* Uniquify string *)
+val string_unique : ident_printer -> string -> string
+
 (* forget an ident *)
 val forget_id : ident_printer -> ident -> unit
 

src/driver/driver.ml

@@ -395,7 +395,7 @@ let print_task drv fmt task = match drv.drv_raw.drv_printer with
 
 let regexp_filename = Str.regexp "%\\([a-z]\\)"
 
-let filename_of_goal drv ident_printer filename theory_name task =
+let filename_of_goal drv filename theory_name task =
   match drv.drv_raw.drv_filename with
     | None -> errorm "no filename syntax given"
     | Some f -> 
@@ -405,7 +405,7 @@ let filename_of_goal drv ident_printer filename theory_name task =
           match i with
             | "f" -> filename
             | "t" -> theory_name
-            | "s" -> id_unique ident_printer pr_name
+            | "s" -> pr_name.id_short
             | _ -> errorm "substitution variable are only %%f %%t and %%s" in
         global_substitute regexp_filename repl_fun f
 
@@ -423,7 +423,7 @@ let call_prover ?debug ?timeout drv task =
   let filename = 
     match drv.drv_raw.drv_filename with
       | None -> None
-      | Some _ -> Some (filename_of_goal drv file_printer "" "" task) in
+      | Some _ -> Some (filename_of_goal drv "why" "call_prover" task) in
   let formatter fmt = print_task drv fmt task in
   call_prover_on_formatter ?debug ?timeout ?filename drv formatter
 

src/driver/driver.mli

@@ -66,9 +66,8 @@ val apply_transforms : driver -> task -> task list
 (** print_task *)
 val print_task : printer
 
-val filename_of_goal : driver -> Ident.ident_printer ->
-  string -> string -> task -> string
-(* filename_of_goal printer file_ident theory_ident ctxt *)
+val filename_of_goal : driver -> string -> string -> task -> string
+(* filename_of_goal filename theory_name ctxt *)
 
 type prover_answer =
     Call_provers.prover_answer =

src/main.ml

@@ -199,7 +199,7 @@ let print_theory_namespace fmt th =
   let module P = Prtree.Make(T) in
   P.print fmt (T.Namespace (th.th_name.Ident.id_short, th.th_export))
 
-let do_file env drv filename_printer file =
+let do_file env drv src_filename_printer dest_filename_printer file =
   if !parse_only then begin
     let filename,c = if file = "-" 
     then "stdin",stdin
@@ -266,21 +266,22 @@ let do_file env drv filename_printer file =
                   try
                     Filename.chop_extension file 
                   with Invalid_argument _ -> file in
-                Ident.id_unique filename_printer 
-                  (Ident.id_register (Ident.id_fresh file)) in
-              let ident_printer = Ident.create_ident_printer 
-                ~sanitizer:file_sanitizer [] in
+                Ident.string_unique src_filename_printer file in
               List.iter 
                 (fun (th,task,drv) ->
-                   let cout = 
-                     if dir = "-" 
-                     then stdout
-                     else
-                       let filename = 
-                         Driver.filename_of_goal drv ident_printer 
-                           file th.th_name.Ident.id_short task in
-                       let filename = Filename.concat dir filename in
-                       open_out filename in
+                   let dest = 
+                     Driver.filename_of_goal drv 
+                       file th.th_name.Ident.id_short task in
+                   (* Uniquify the filename before the extension if it exists*)
+                   let i = 
+                     try String.rindex dest '.' 
+                     with Not_found -> String.length dest in
+                   let name,ext = String.sub dest 0 i, 
+                     String.sub dest i (String.length dest- i) in
+                   let name = Ident.string_unique dest_filename_printer name in
+                   let filename = name^ext in
+                   let filename = Filename.concat dir filename in
+                   let cout = open_out filename in
                    let fmt = formatter_of_out_channel cout in
                    fprintf fmt "%a@?" (Driver.print_task drv) task;
                    close_out cout) goals
@@ -327,9 +328,12 @@ let () =
           (Pp.print_list Pp.newline Pp.string) (Driver.list_transforms ());
         exit 0          
       end;
-    let filename_printer = Ident.create_ident_printer 
+    let src_filename_printer = Ident.create_ident_printer 
       ~sanitizer:file_sanitizer [] in
-    Queue.iter (do_file env drv filename_printer) files
+    let dest_filename_printer = Ident.create_ident_printer 
+      ~sanitizer:file_sanitizer [] in
+    Queue.iter (do_file env drv src_filename_printer dest_filename_printer)
+      files
   with e when not !debug ->
     eprintf "%a@." report e;
     exit 1

theories/comparison.why

+
+theory Abs
+
+  type t
+  logic ge(t,t)
+  logic neg(t) : t
+  logic zero : t
+
+  logic abs(t) : t
+
+  axiom Pos: forall x:t. ge(x,zero) -> abs(x) = x
+  axiom Neg: forall x:t. not ge(x,zero) -> abs(x) = neg(x)
+
+(*
+  logic abs(x : t) : t 
+  axiom Abs_def : if ge(x,zero) then abs(x)=x else abs(x)=neg(x)
+*)
+end
+
+theory MinMax
+
+  type t
+  logic ge(t,t)
+
+  logic min(tty,t) : t
+  logic max(t,t) : t
+
+  axiom Max_is_ge   : forall x,y:t. ge(max(x,y),x) and ge(max(x,y),y)
+  axiom Max_is_some : forall x,y:t. max(x,y) = x or max(x,y) = y
+  axiom Min_is_le   : forall x,y:t. ge(x,min(x,y)) and ge(y,min(x,y))
+  axiom Min_is_some : forall x,y:t. min(x,y) = x or min(x,y) = y
+
+(*
+  axiom Max_x : forall x,y:t. ge(x,y) -> max(x,y) = x
+  axiom Max_y : forall x,y:t. ge(y,x) -> max(x,y) = y
+  axiom Min_y : forall x,y:t. ge(x,y) -> min(x,y) = y
+  axiom Min_x : forall x,y:t. ge(y,x) -> min(x,y) = x
+*)
+
+
+(*
+  logic min(x:t,y:t) : t 
+  axiom Min_def : if ge(x,y) then min(x,y)=y else min(x,y)=x 
+  logic max(x:t,y:t) : t
+  axiom Max_def : if ge(x,y) then max(x,y)=x else max(x,y)=y 
+*)
+
+end

theories/programs.why

@@ -9,7 +9,7 @@ theory Prelude
   logic ref ('a)     : 'a ref
   logic (!_)('a ref) : 'a
 
-  type  unit
+  use export unit.Unit
   logic ignore('a) : unit
 
   type  label

theories/unit.why

+theory Unit
+
+  type unit = Unit
+
+end