reimporting data

drivers/coq.drv

@@ -82,7 +82,7 @@ end
 
 theory int.EuclideanDivision
 
-  prelude "Require Zdiv."
+  prelude "Require Import Zdiv."
 
   syntax logic div "(Zdiv %1 %2)"
   syntax logic mod "(Zmod %1 %2)"
@@ -91,7 +91,7 @@ end
 
 theory int.ComputerDivision
 
-  prelude "Require ZOdiv."
+  prelude "Require Import ZOdiv."
 
   syntax logic div "(ZOdiv %1 %2)"
   syntax logic mod "(ZOmod %1 %2)"

examples/use_api.ml

@@ -27,7 +27,7 @@ let alt_ergo =
     Util.Mstr.find "alt-ergo" provers 
   with Not_found ->
     eprintf "Prover alt-ergo not installed or not configured@.";
-    failwith "Cannot continue without alt-ergo installed"
+    exit 0
 
 let alt_ergo_driver = Driver.load_driver env alt_ergo.Whyconf.driver
 

src/core/env.mli

@@ -57,10 +57,10 @@ val read_channel : ?format:string -> read_channel
     the format is chosen according to [f]'s extension. 
     Beware that nothing ensures that [c] corresponds to the contents of [f] 
 
-    @raise [NoFormat] if [format] is not given and [f] has no extension
-    @raise [UnknownExtension s] if the extension [s] is not known in 
+    @raise NoFormat if [format] is not given and [f] has no extension
+    @raise UnknownExtension [s] if the extension [s] is not known in 
       any registered parser
-    @raise [UnknownFormat f] if the [format] is not registered
+    @raise UnknownFormat [f] if the [format] is not registered
 *)
 
 val read_file : ?format:string -> env -> string -> theory Mnm.t 

src/ide/db.ml

@@ -116,12 +116,12 @@ let bind db sql l =
       1 l
   in stmt
 
-(*
 let stmt_column_INT stmt i msg =
   match Sqlite3.column stmt i with
     | Sqlite3.Data.INT i -> i
     | _ -> failwith msg
 
+(*
 let stmt_column_FLOAT stmt i msg =
   match Sqlite3.column stmt i with
     | Sqlite3.Data.FLOAT i -> i
@@ -246,14 +246,12 @@ let subgoals t = t.subgoals
 
 type theory = int64
 
-let theory_name _ = assert false
 let goals _ = assert false
 let verified _ = assert false
 
 type file = int64 
 
 let file_name _ = assert false
-let theories _ = assert false
 
 
 
@@ -721,9 +719,17 @@ module Goal = struct
     let sql = 
       "CREATE TABLE IF NOT EXISTS goals \
        (goal_id INTEGER PRIMARY KEY AUTOINCREMENT, \
+        goal_theory INTEGER,
         goal_name TEXT, task_checksum TEXT, proved INTEGER);" 
     in
     db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql);
+(*
+    let sql = 
+      "CREATE UNIQUE INDEX IF NOT EXISTS goal_theory_idx \
+       ON goals (goal_theory)" 
+    in
+    db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql);
+*)
 (*
     let sql = "create table if not exists map_external_proofs_goal_external_proof (goal_id integer, external_proof_id integer, primary key(goal_id, external_proof_id));" in
     db_must_ok db (fun () -> Sqlite3.exec db.db sql);
@@ -749,13 +755,14 @@ module Goal = struct
     db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)
 *)
 
-  let add db (_th:theory) (name : string) (sum:string) = 
+  let add db (th:theory) (name : string) (sum:string) = 
     transaction db 
       (fun () ->
 	 let sql = 
-	   "INSERT INTO goals VALUES(NULL,?,?,0)" 
+	   "INSERT INTO goals VALUES(NULL,?,?,?,0)" 
 	 in
 	 let stmt = bind db sql [
+           Sqlite3.Data.INT th;
            Sqlite3.Data.TEXT name;
            Sqlite3.Data.TEXT sum;
          ]
@@ -1021,21 +1028,54 @@ end
 module Theory = struct
 
   let init db =
-    let sql = "CREATE TABLE IF NOT EXISTS theories (theory_name TEXT, theory_file INTEGER);" in
+    let sql = 
+      "CREATE TABLE IF NOT EXISTS theories \
+       (theory_id INTEGER PRIMARY KEY AUTOINCREMENT,\
+        theory_file INTEGER, theory_name TEXT);" in
     db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql);
     ()
 
+  let name db th =
+    let sql="SELECT theory_name FROM theories \
+       WHERE theories.theory_id=?"
+    in
+    let stmt = bind db sql [Sqlite3.Data.INT th] in
+    let of_stmt stmt = 
+      (stmt_column_string stmt 0 "Theory.name")
+    in
+    match step_fold db stmt of_stmt with
+      | [] -> raise Not_found
+      | [x] -> x
+      | _ -> assert false
+
+  let of_file db f =
+    let sql="SELECT theory_id FROM theories \
+       WHERE theories.theory_file=?"
+    in
+    let stmt = bind db sql [Sqlite3.Data.INT f] in
+    let of_stmt stmt = 
+      (stmt_column_INT stmt 0 "Theory.of_file")
+    in
+    step_fold db stmt of_stmt 
+
   let add db file name = 
     transaction db 
       (fun () ->
-         let sql = "INSERT INTO theories VALUES(?,?)" in
-         let stmt = bind db sql [ Sqlite3.Data.TEXT name ; 
-				  Sqlite3.Data.INT file ] in
+         let sql = "INSERT INTO theories VALUES(NULL,?,?)" in
+         let stmt = bind db sql 
+           [ Sqlite3.Data.INT file;
+             Sqlite3.Data.TEXT name;
+           ]
+         in
          db_must_done db (fun () -> Sqlite3.step stmt);
          let new_id = Sqlite3.last_insert_rowid db.raw_db in
 	 new_id)
 end
 
+let theory_name th = Theory.name (current()) th
+
+let theories f = Theory.of_file (current()) f
+
 module Main = struct
 
   let init db =
@@ -1043,17 +1083,22 @@ module Main = struct
           (file_id INTEGER PRIMARY KEY AUTOINCREMENT,file_name TEXT);" 
     in
     db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql);
+(*
     let sql = 
       "CREATE UNIQUE INDEX IF NOT EXISTS file_idx \
        ON files (file_id)" 
     in
     db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)
-
+*)
+    ()
 
   let all_files db =
-    let sql="SELECT file_name FROM files" in
+    let sql="SELECT file_id,file_name FROM files" in
     let stmt = Sqlite3.prepare db.raw_db sql in
-    let of_stmt stmt = stmt_column_string stmt 0 "Db.all_files" in
+    let of_stmt stmt = 
+      (stmt_column_INT stmt 0 "Db.all_files",
+       stmt_column_string stmt 1 "Db.all_files")
+    in
     step_fold db stmt of_stmt 
 
   let add db name = 
@@ -1103,7 +1148,8 @@ let root_goals () =
     
 *)
 
-let files _ = assert false
+let files () = 
+  Main.all_files (current())
 
 
 let prover_from_name n = 

src/ide/db.mli

@@ -112,8 +112,8 @@ val theories : file -> theory list
 val init_base : string -> unit
 (** opens or creates the current database, from given file name *)
 
-val files : unit -> file list
-(** returns the current set of files *)
+val files : unit -> (file * string) list
+(** returns the current set of files, with their filenames *)
 
 
 (** {2 Updates} *)

src/ide/gdbmain.ml

@@ -308,6 +308,21 @@ let task_checksum t =
   fprintf str_formatter "%a@." Pretty.print_task t;
   Digest.to_hex (Digest.string (flush_str_formatter ()))
 
+
+let info_window mt s =
+  let d = GWindow.message_dialog
+    ~message:s
+    ~message_type:mt
+    ~buttons:GWindow.Buttons.close
+    ~title:"Why3 info or error"
+    ~show:true () 
+  in
+  let (_ : GtkSignal.id) =
+    d#connect#response 
+      ~callback:(function `CLOSE | `DELETE_EVENT -> d#destroy ())
+  in
+  ()
+
 module Helpers = struct
 
   let image_of_result = function
@@ -363,9 +378,8 @@ module Helpers = struct
       (image_of_result s);
     if s = Scheduler.Success then set_proved a.proof_goal              
 
-  let add_theory mfile th =
+  let add_theory_row mfile th db_theory =
     let tname = th.Theory.th_name.Ident.id_string in
-    let db_theory = Db.add_theory mfile.file_db tname in
     let parent = mfile.file_row in
     let row = goals_model#append ~parent () in
     let mth = { theory = th; 
@@ -379,7 +393,14 @@ module Helpers = struct
     goals_model#set ~row ~column:icon_column !image_directory;
     goals_model#set ~row ~column:index_column (Row_theory mth);
     goals_model#set ~row ~column:visible_column true;
+    mth
+
+  let add_theory mfile th =
     let tasks = Task.split_theory th None None in
+    let tname = th.Theory.th_name.Ident.id_string in
+    let db_theory = Db.add_theory mfile.file_db tname in
+    let mth = add_theory_row mfile th db_theory in
+    let row = mth.theory_row in
     let goals =
       List.fold_left
         (fun acc t ->
@@ -410,11 +431,7 @@ module Helpers = struct
     if goals = [] then set_theory_proved mth;
     mth
     
-
-  let add_file f =
-    try
-      let theories = Env.read_file gconfig.env f in
-      let dbfile = Db.add_file f in
+  let add_file_row f dbfile =
       let parent = goals_model#append () in
       let mfile = { file_name = f; 
                     file_row = parent; 
@@ -428,6 +445,13 @@ module Helpers = struct
       goals_model#set ~row:parent ~column:icon_column !image_directory;
       goals_model#set ~row:parent ~column:index_column (Row_file mfile);
       goals_model#set ~row:parent ~column:visible_column true;
+      mfile
+
+  let add_file f =
+    try
+      let theories = Env.read_file gconfig.env f in
+      let dbfile = Db.add_file f in
+      let mfile = add_file_row f dbfile in
       let theories = 
 	Theory.Mnm.fold
           (fun thname t acc ->
@@ -441,27 +465,46 @@ module Helpers = struct
       mfile.theories <- List.rev theories;
       if theories = [] then set_file_verified mfile
     with e ->
-      eprintf "Error while reading file '%s': %a@." f 
-	Exn_printer.exn_printer e
+      fprintf str_formatter 
+        "@[Error while reading file@ '%s':@ %a@]" f
+	Exn_printer.exn_printer e;
+      let msg = flush_str_formatter () in
+      info_window `ERROR msg
 
 end
 
-(*
+(*********************************)
+(*  read previous data from db   *)
+(*********************************)
 
-TODO: read files from db
+let () =
+  let files = Db.files () in
+  List.iter
+    (fun (f,fn) -> 
+       eprintf "Reimporting file '%s'@." fn;
+       let theories = Env.read_file gconfig.env fn in
+       let mfile = Helpers.add_file_row fn f in
+       let ths = Db.theories f in
+       List.iter
+         (fun db_th ->
+            let tname = Db.theory_name db_th in
+            eprintf "Reimporting theory '%s'@."tname;
+            let th = Theory.Mnm.find tname theories in
+            let (_mth : Model.theory) = Helpers.add_theory_row mfile th db_th in
+            ( (* TODO *) )
+         )
+         ths
+    )
+    files
 
-*)
 
+(**********************)
+(* set up scheduler   *)
+(**********************)
 
 let () = 
   begin
     Scheduler.async := GtkThread.async;
-(*
-    match config.running_provers_max with
-      | None -> ()
-      | Some n -> 
-          if n >= 1 then Scheduler.maximum_running_proofs := n
-*)
     Scheduler.maximum_running_proofs := gconfig.max_running_processes
   end 
 
@@ -870,21 +913,6 @@ let () =
 (* Help menu *)
 (*************)
 
-(*
-let info_window t s () =
-  let d = GWindow.message_dialog
-    ~message:s
-    ~message_type:`INFO
-    ~buttons:GWindow.Buttons.close
-    ~title:t
-    ~show:true () 
-  in
-  let (_ : GtkSignal.id) =
-    d#connect#response 
-      ~callback:(function `CLOSE | `DELETE_EVENT -> d#destroy ())
-  in
-  ()
-*)
 
 let help_menu = factory#add_submenu "_Help" 
 let help_factory = new GMenu.factory help_menu ~accel_group