relative paths for files stored in database, preliminary support for inline...

relative paths for files stored in database, preliminary support for inline transformation in the IDE

CHANGES

 
-
-  o better Gappa output: support for sqrt, for negative constants
+  o [IDE] source file names are stored in database as relative paths
+    to the database, so that databases are now easier to move from a
+    machine to another (e.g when they are stored in source control
+    repositories)
+  o better Gappa output: support for sqrt, for
+    negative constants
 
 version 0.63, Dec 21, 2010
 ==========================

ROADMAP

 
-
-
-
-
-
-
 = Roadmap for second release, as early as possible in 2011 =
 
 * fix local installation
-* ajouter "invalid" comme cas de resultats de preuve
-* utiliser call_provers.proof_result dans gmain
-* file names in DB
-** use only file names relative to the db file
-** ou alors interdire d'avoir plusieurs fichiers dans la meme base
+** fix local executables names (DONE)
+
+* fix problems with .why.conf
+** if we distribute the current state, users who already have a ~/.why.conf
+will get a error message because of missing loadpath to modules
+** generally speaking, we should rethink the design of that .why.conf: avoid
+   absolute paths,
+  
 * proof replay
-** in IDE
+** in IDE: replay all obsolete but previously successful proofs
 ** in whybench
 ** add replay of existing proofs in "make bench" to detect regression
 
+* IDE: implement "inline" (use transformation inline_goal)
+** partially done
+** problem 1: detect that transformation did nothing
 
+* IDE: debug "hide proved goals" feature
 
+* IDE: ajouter "invalid" comme cas de resultats de preuve
+  (utiliser call_provers.proof_result dans gmain)
 
+* IDE, file names in DB: use only file names relative to the db file (DONE)
 
 
 
@@ -33,10 +37,6 @@
 * Coq realizations of theories
 
 
-
-
-
-
 = Papers to write =
 
 * Encodings and transformations (Andrei+Francois, CADE 2011, deadline January 2011)
@@ -50,6 +50,12 @@
 
 
 
+
+
+
+
+
+
 = Roadmap for December 2010 =
 
 == Documentation ==

doc/manual.tex

@@ -56,7 +56,7 @@
 \vfill
 
 \begin{LARGE}
-  Version \whyversion{}, December 2010
+  Version \whyversion{}, February 2011
 \end{LARGE}
 
 \vfill
@@ -80,7 +80,7 @@ $^2$ INRIA Saclay - \^Ile-de-France, ProVal, Orsay, F-91893
 
 \bigskip
 
-  \textcopyright 2010 Univ Paris-Sud, CNRS, INRIA
+  \textcopyright 2010-2011 Univ Paris-Sud, CNRS, INRIA
 
   This work has been partly supported by the `U3CAT' national ANR project
   (ANR-08-SEGI-021-08, \url{http://frama-c.cea.fr/u3cat}) and by the
@@ -134,7 +134,26 @@ Lescuyer, Sim\~ao Melo de Sousa, Asma Tafat.
 
 \section*{Release notes}
 
-\paragraph{Version 0.63}
+\subsection*{Version 0.6?}
+
+\paragraph{new features}
+
+\begin{itemize}
+\item 
+\item better Gappa output: support for sqrt, for negative constants
+\end{itemize}
+
+\paragraph{bug fixes}
+
+\begin{itemize}
+\item Fixed local installation
+  \begin{itemize}
+  \item executable names are now identical to when they are installed
+  \end{itemize}
+\item IDE: source file names are stored as paths relative to the database
+\end{itemize}
+
+\subsection*{Version 0.63}
 First public release. The main new features with respect to Why 2.xx
 are the following.
 \begin{enumerate}

examples/hello_proof.why

@@ -2,7 +2,7 @@ theory HelloProof "My very first Why3 theory"
 
   goal G1 : true
 
-  goal G2 : (true -> false) and (true or false)
+  goal G2 : (false -> false) and (true or false)
 
   use import int.Int
 

examples/programs/binary_search.mlw

@@ -16,7 +16,7 @@ module M
   exception Not_found (* raised to signal a search failure *)
 
   let binary_search (a :array int) (v : int) =
-    { forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] }
+    { (* forall i1 i2 : int. 0 <= i1 <= i2 < length a -> a[i1] <= a[i2] *) }
     try
       let l = ref 0 in
       let u = ref (length a - 1) in

examples/programs/isqrt.mlw

@@ -5,13 +5,13 @@ module M
 
   logic sqr (x:int) : int = x * x
 
-  let isqrt (x:int) =
+  let isqrt (x:int) : int =
     { x >= 0 }
     let count = ref 0 in
     let sum = ref 1 in
     while !sum <= x do
       invariant { count >= 0 and x >= sqr count and sum = sqr (count+1) }
-      variant   { x - sum }
+      variant   { x - count }
       count := !count + 1;
       sum := !sum + 2 * !count + 1
     done;

src/ide/gconfig.ml

@@ -209,7 +209,7 @@ let iconname_no = "delete32"
 let iconname_directory = "folder32"
 let iconname_file = "file32"
 let iconname_prover = "wizard32"
-let iconname_transf = "cutb32"
+let iconname_transf = "configure32"
 let iconname_editor = "edit32"
 let iconname_remove = "deletefile32"
 
@@ -401,6 +401,6 @@ let () = eprintf "end of configuration initialization@."
 
 (*
 Local Variables:
-compile-command: "unset LANG; make -C ../.. bin/whyide.opt"
+compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
 End:
 *)

src/ide/gmain.ml

@@ -20,24 +20,6 @@
 
 (* TODO:
 
-* bug: the file names are stored as relative, so if you restart
-from another directory, they are not found
-  but on the other hand, storing them as relative helps if you change
-   the machine
-  Solution: store the name relative to the database, e.g if
-
-  dir/file.why
-  dir/T/project.db
-
-  then project.db should store "../file.why", and running the interface
-  from any dir as
-
-  > why3db foo/dir/T
-
-  should read the file by concating foo/dir to ../file.why
-
-* When DB contains an edited proof, use the file for the run
-
 * when proof attempt is finished and is it the one currently selected,
 the new output should be displayed on upper-right window
 
@@ -196,7 +178,8 @@ let project_dir, file_to_read =
             with Invalid_argument _ -> fname
           in
           eprintf "Info: using '%s' as directory for the project@." d;
-          d, Some fname
+          d, Some (Filename.concat Filename.parent_dir_name
+		     (Filename.basename fname))
         end
     end
   else
@@ -206,7 +189,7 @@ let () =
   if not (Sys.file_exists project_dir) then
     begin
       eprintf "Info: '%s' does not exists. Creating directory of that name \
- for the project@." fname;
+ for the project@." project_dir;
       Unix.mkdir project_dir 0o777
     end
 
@@ -221,6 +204,7 @@ let () =
 
 
 let read_file fn =
+  let fn = Filename.concat project_dir fn in 
   let theories = Env.read_file gconfig.env fn in
   let theories =
     Theory.Mnm.fold
@@ -243,6 +227,7 @@ let read_file fn =
 
 module Model = struct
 
+(* TODO: remove, see below *)
   type proof_attempt_status =
     | Scheduled (** external proof attempt is scheduled *)
     | Running (** external proof attempt is in progress *)
@@ -258,9 +243,12 @@ module Model = struct
         proof_row : Gtk.tree_iter;
         proof_db : Db.proof_attempt;
         mutable status : proof_attempt_status;
-        mutable proof_obsolete : bool;
         mutable time : float;
         mutable output : string;
+(* TODO: replace the 3 fields above with
+	mutable proof_result : Call_provers.prover_result
+*)
+        mutable proof_obsolete : bool;
         mutable edited_as : string;
       }
 
@@ -727,7 +715,7 @@ module Helpers = struct
     goal
 
 
-  let add_transformation_row g db_transf (*subgoals*) =
+  let add_transformation_row g db_transf tr_name =
     let parent = g.Model.goal_row in
     let row = goals_model#append ~parent () in
     let tr = { Model.parent_goal = g;
@@ -737,7 +725,7 @@ module Helpers = struct
                subgoals = [];
              }
     in
-    goals_model#set ~row ~column:Model.name_column "split";
+    goals_model#set ~row ~column:Model.name_column tr_name;
     goals_model#set ~row ~column:Model.icon_column !image_transf;
     goals_model#set ~row ~column:Model.index_column
       (Model.Row_transformation tr);
@@ -847,6 +835,7 @@ let apply_trans t task =
 *)
 
 let split_transformation = Trans.lookup_transform_l "split_goal" gconfig.env
+let inline_transformation = Trans.lookup_transform "inline_goal" gconfig.env
 let intro_transformation = Trans.lookup_transform "introduce_premises" gconfig.env
 
 let rec reimport_any_goal parent gname t db_goal goal_obsolete =
@@ -885,9 +874,8 @@ let rec reimport_any_goal parent gname t db_goal goal_obsolete =
     (fun tr_id tr ->
        let trname = Db.transf_name tr_id in
        eprintf "Reimporting transformation %s for goal %s @." trname gname;
-       assert (trname = "split_goal"); (* TODO *)
        let subgoals = Trans.apply split_transformation t in
-       let mtr = Helpers.add_transformation_row goal tr in
+       let mtr = Helpers.add_transformation_row goal tr trname in
        let db_subgoals = Db.subgoals tr in
        let reimported_goals,db_subgoals,_ =
          List.fold_left
@@ -1197,8 +1185,9 @@ let split_goal g =
           (GtkThread.sync Db.add_transformation)
             g.Model.goal_db transf_id_split
         in
-        let tr = (GtkThread.sync Helpers.add_transformation_row) g db_transf
- (* subgoals *) in
+        let tr = (GtkThread.sync Helpers.add_transformation_row) 
+	  g db_transf "split_goal" 
+	in
         let goal_name = g.Model.goal_name in
         let fold = (fun (acc,count) subtask ->
              let _id = (Task.task_goal subtask).Decl.pr_name in
@@ -1220,6 +1209,41 @@ let split_goal g =
     Scheduler.apply_transformation_l ~callback
       split_transformation g.Model.task
 
+let inline_goal g =
+  if not g.Model.proved then
+    let callback subgoal =
+      ignore (Thread.create (fun subgoal ->
+	(* if List.length subgoals >= 2 then *)
+        let transf_id_inline =
+          (GtkThread.sync Db.transf_from_name) "inline_goal" in
+        let db_transf =
+          (GtkThread.sync Db.add_transformation)
+            g.Model.goal_db transf_id_inline
+        in
+        let tr = (GtkThread.sync Helpers.add_transformation_row) 
+	  g db_transf "inline_goal"
+	in
+        let goal_name = g.Model.goal_name in
+        let fold = (fun (acc,count) subtask ->
+             let _id = (Task.task_goal subtask).Decl.pr_name in
+             let subgoal_name =
+               goal_name ^ "." ^ (string_of_int count)
+             in
+             let sum = task_checksum subtask in
+             let subtask_db = Db.add_subgoal db_transf subgoal_name sum in
+             let goal =
+               Helpers.add_goal_row (Model.Transf tr) subgoal_name subtask
+                 subtask_db
+             in
+             (goal :: acc, count+1)) in
+        let goals,_ = List.fold_left (GtkThread.sync fold) ([],1) [subgoal]
+        in
+        tr.Model.subgoals <- List.rev goals;
+        Hashtbl.add g.Model.transformations "inline" tr) subgoal)
+    in
+    Scheduler.apply_transformation ~callback
+      inline_transformation g.Model.task
+
 let rec split_goal_or_children g =
   if not g.Model.proved then
     begin
@@ -1232,6 +1256,18 @@ let rec split_goal_or_children g =
       if !r then split_goal g
     end
 
+let rec inline_goal_or_children g =
+  if not g.Model.proved then
+    begin
+      let r = ref true in
+      Hashtbl.iter 
+	(fun _ t ->
+	   r := false;
+           List.iter inline_goal_or_children
+             t.Model.subgoals) g.Model.transformations;
+      if !r then inline_goal g
+    end
+
 let split_selected_goal_or_children row =
   let row = filter_model#get_iter row in
   match filter_model#get ~row ~column:Model.index_column with
@@ -1250,6 +1286,23 @@ let split_selected_goal_or_children row =
         List.iter split_goal_or_children tr.Model.subgoals
 
 
+let inline_selected_goal_or_children row =
+  let row = filter_model#get_iter row in
+  match filter_model#get ~row ~column:Model.index_column with
+    | Model.Row_goal g ->
+        inline_goal_or_children g
+    | Model.Row_theory th ->
+        List.iter inline_goal_or_children th.Model.goals
+    | Model.Row_file file ->
+        List.iter
+          (fun th ->
+             List.iter inline_goal_or_children th.Model.goals)
+          file.Model.theories
+    | Model.Row_proof_attempt a ->
+        inline_goal_or_children a.Model.proof_goal
+    | Model.Row_transformation tr ->
+        List.iter inline_goal_or_children tr.Model.subgoals
+
 let split_selected_goals () =
   ignore (Thread.create (fun () ->
     List.iter
@@ -1257,6 +1310,13 @@ let split_selected_goals () =
       goals_view#selection#get_selected_rows) ())
 
 
+let inline_selected_goals () =
+  ignore (Thread.create (fun () ->
+    List.iter
+      inline_selected_goal_or_children
+      goals_view#selection#get_selected_rows) ())
+
+
 (*********************************)
 (* add a new file in the project *)
 (*********************************)
@@ -1271,7 +1331,65 @@ let filter_why_files () =
     ~name:"Why3 source files"
     ~patterns:[ "*.why"; "*.mlw"] ()
 
+(* return the absolute path of a given file name.
+   this code has been designed to be architecture-independant so
+   be very careful if you modify this *)
+let path_of_file f =
+  let rec aux acc f =
+(*
+    Format.printf "aux %s@." f;
+    let _ = read_line () in
+*)
+    let d = Filename.dirname f in
+    if d = Filename.current_dir_name then
+      (* f is relative to the current dir *)
+      aux (f::acc) (Sys.getcwd ())
+    else
+      let b = Filename.basename f in
+      if b=Filename.current_dir_name then acc else
+	if f=b then b::acc else
+	  aux (b::acc) d
+  in
+  aux [] f
 
+(*
+let test x = (Filename.dirname x, Filename.basename x)
+
+let _ = test "file"
+let _ = test "/file"
+let _ = test "/"
+let _ = test "f1/f2"
+let _ = test "/f1/f2"
+
+let p1 = path_of_file "/bin/bash"
+
+let p1 = path_of_file "../src/f.why"
+  *)
+
+let relativize_filename base f =
+  let rec aux ab af =
+    match ab,af with	
+      | x::rb, y::rf when x=y -> aux rb rf
+      | _ -> 
+	  let rec aux2 acc p =
+	    match p with
+	      | [] -> acc
+	      | _::rb -> aux2 (Filename.parent_dir_name::acc) rb
+	  in aux2 af ab
+  in
+  let rec rebuild l =
+    match l with
+      | [] -> ""
+      | [x] -> x
+      | x::l -> Filename.concat x (rebuild l)
+  in
+  rebuild (aux (path_of_file base) (path_of_file f))
+
+(*
+let p1 = relativize_filename "/bin/bash" "src/f.why"
+
+let p1 = relativize_filename "test" "/home/cmarche/recherche/why3/src/ide/f.why"
+*)
 let select_file () =
   let d = GWindow.file_chooser_dialog ~action:`OPEN
     ~title:"Why3: Add file in project"
@@ -1287,6 +1405,7 @@ let select_file () =
         match d#filename with
           | None -> ()
           | Some f ->
+	      let f = relativize_filename project_dir f in
               eprintf "Adding file '%s'@." f;
               try
                 Helpers.add_file f
@@ -1303,7 +1422,7 @@ let select_file () =
 
 
 let not_implemented () =
-  info_window `INFO "This feature is not yet implemented, sorry"
+  info_window `INFO "This feature is not yet implemented, sorry."
 
 (*************)
 (* File menu *)
@@ -1526,13 +1645,13 @@ let () =
   in ()
 
 let () =
-  let b = GButton.button ~packing:transf_box#add ~label:"(Inline)" () in
-(*
+  let b = GButton.button ~packing:transf_box#add ~label:"Inline" () in
+(**)
   let i = GMisc.image ~pixbuf:(!image_transf) () in
   let () = b#set_image i#coerce in
-*)
+(**)
   let (_ : GtkSignal.id) =
-    b#connect#pressed ~callback:not_implemented
+    b#connect#pressed ~callback:inline_selected_goals
   in ()
 
 
@@ -1918,6 +2037,6 @@ let () = GtkThread.main ()
 
 (*
 Local Variables:
-compile-command: "unset LANG; make -C ../.. bin/whyide.byte"
+compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
 End:
 *)

src/printer/coq.ml

@@ -358,15 +358,41 @@ let print_next_proof ?def ch fmt =
     | End_of_file -> print_empty_proof ?def fmt
     | Exit -> fprintf fmt "@\n"
 
-let realization ~old ?def fmt info =
-  if info.realization then
+let produce_remaining_proofs ~old fmt =
+  match old with
+    | None -> ()
+    | Some ch ->
+  try
+    while true do
+      let s = input_line ch in
+      if s = proof_begin then
+        begin
+          fprintf fmt "(* OBSOLETE PROOF *)@\n";
+          try while true do
+            let s = input_line ch in
+            if s = proof_end then 
+	      begin
+		fprintf fmt "(* END OF OBSOLETE PROOF *)@\n@\n";
+		raise Exit
+	      end;
+            fprintf fmt "%s@\n" s;
+          done
+	  with Exit -> ()
+        end
+    done
+  with
+    | End_of_file -> fprintf fmt "@\n"
+
+let realization ~old ?def fmt produce_realization =
+  if produce_realization then
     begin match old with
-      | None -> assert false; print_empty_proof ?def fmt
+      | None -> print_empty_proof ?def fmt
       | Some ch -> print_next_proof ?def ch fmt
     end
   else
     fprintf fmt "@\n"
 
+
 let print_type_decl ~old info fmt (ts,def) =
   if is_ts_tuple ts then () else
   match def with
@@ -375,7 +401,7 @@ let print_type_decl ~old info fmt (ts,def) =
             fprintf fmt "@[<hov 2>%a %a : %aType.@]@\n%a"
 	      definition info
               print_ts ts print_params_list ts.ts_args
-	      (realization ~old ~def:true) info
+	      (realization ~old ~def:true) info.realization
         | Some ty ->
             fprintf fmt "@[<hov 2>Definition %a %a :=@ %a.@]@\n@\n"
               print_ts ts (print_arrow_list print_tv_binder) ts.ts_args
@@ -422,7 +448,7 @@ let print_logic_decl ~old info fmt (ls,ld) =
             print_params all_ty_params
             (print_arrow_list (print_ty info)) ls.ls_args
             (print_ls_type ~arrow:(ls.ls_args <> []) info) ls.ls_value
-	    (realization ~old ~def:true) info
+	    (realization ~old ~def:true) info.realization
   end;
   print_implicits fmt ls ty_vars_args ty_vars_value all_ty_params;
   fprintf fmt "@\n"
@@ -457,16 +483,9 @@ let print_pkind info fmt = function
 
 let print_proof ~old info fmt = function
   | Plemma | Pgoal ->
-      begin match old with
-        | None -> print_empty_proof fmt
-        | Some ch -> print_next_proof ch fmt
-      end
+      realization ~old fmt true
   | Paxiom ->
-      if info.realization then
-	begin match old with
-          | None -> print_empty_proof fmt
-          | Some ch -> print_next_proof ch fmt
-	end
+      realization ~old fmt info.realization 
   | Pskip -> ()
 
 let print_decl ~old info fmt d = match d.d_node with
@@ -475,10 +494,6 @@ let print_decl ~old info fmt d = match d.d_node with
   | Dind il   -> print_list nothing (print_ind_decl info) fmt il
   | Dprop (_,pr,_) when Sid.mem pr.pr_name info.info_rem -> ()
   | Dprop (k,pr,f) ->
- (*
-     fprintf fmt "@\n@\n(* YOU MAY EDIT BELOW *)@\n@\n@\n";
-      fprintf fmt "(* DO NOT EDIT BELOW *)@\n@\@\n";
- *)
       let params = f_ty_freevars Stv.empty f in
       fprintf fmt "@[<hov 2>%a %a : %a%a.@]@\n%a"
         (print_pkind info) k
@@ -512,9 +527,10 @@ open Theory
 
 let print_tdecl ~old info fmt d = match d.td_node with
   | Decl d -> print_decl ~old info fmt d
-  | Use _ -> ()
-  | Meta _ -> ()
-  | Clone _ -> ()
+  | Use t -> 
+      fprintf fmt "Require Import %s.@\n@\n" (id_unique iprinter t.th_name)
+  | Meta _ -> assert false (* TODO ? *)
+  | Clone _ -> assert false (* TODO *)
 
 let print_tdecls ~old info fmt dl =
   fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_tdecl ~old info)) dl
@@ -534,7 +550,8 @@ let print_theory _env pr thpr ~old fmt th =
     realization = true;
   } 
   in
-  print_tdecls ~old info fmt th.th_decls
+  print_tdecls ~old info fmt th.th_decls;
+  produce_remaining_proofs ~old fmt
 
 
 (*

tests/test-claude.why

@@ -120,14 +120,41 @@ theory TestRealize
 
   type t
 
-  logic f t : t
-
   logic p t t
 
-  axiom P_sym: forall x y:t. p x y <-> p y x
+  axiom P_arefl: forall x:t. not (p x x)
+
+(*
+  axiom P_total: forall x y:t. p x y or p y x or x=y
+
+  logic f t : t
 
   axiom A : forall x:t. p (f x) x
 
-  lemma B : forall x:t. p x (f x)
+  lemma B : forall x:t. not (p x (f x))
+