Commit 907ba72a authored by MARCHE Claude's avatar MARCHE Claude

more in db

parent f2dd6dad
......@@ -217,20 +217,25 @@ type transf =
mutable subgoals : goal list;
}
and goal = {
and goal = int64
(*
{
mutable goal_id : int;
mutable task_checksum: string;
mutable proved : bool;
mutable external_proofs : proof_attempt Hprover.t;
mutable transformations : transf Htransf.t;
}
*)
(** goal accessors *)
let task_checksum g = g.task_checksum
let proved g = g.proved
let external_proofs g = g.external_proofs
let transformations g = g.transformations
let task_checksum _g = assert false
let proved _g = assert false
let external_proofs _g = assert false
let transformations _g = assert false
(** transf accessors *)
......@@ -239,7 +244,7 @@ let subgoals t = t.subgoals
type theory
type theory = int64
let theory_name _ = assert false
let goals _ = assert false
......@@ -710,29 +715,24 @@ end
(*
module Goal = struct
type t = goal
let hash g = Hashtbl.hash g.goal_id
let equal g1 g2 = g1.goal_id = g2.goal_id
let compare g1 g2 = Pervasives.compare g1.goal_id g2.goal_id
(*
let init db =
let sql = "create table if not exists goal (id integer primary key autoincrement,task_checksum text,parent_id integer,name text,pos_id integer,proved integer);" in
db_must_ok db (fun () -> Sqlite3.exec db.db sql);
let sql =
"CREATE TABLE IF NOT EXISTS goals \
(goal_id INTEGER PRIMARY KEY AUTOINCREMENT, \
goal_name TEXT, task_checksum TEXT, proved INTEGER);"
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);
let sql = "create table if not exists map_transformations_goal_transf (goal_id integer, transf_id integer, primary key(goal_id, transf_id));" in
db_must_ok db (fun () -> Sqlite3.exec db.db sql);
()
*)
()
(*
let init db =
(* TODO: store the goal origin too *)
let sql =
......@@ -747,27 +747,23 @@ module Goal = struct
PRIMARY KEY(goal_id, prover_id));"
in
db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)
*)
let add db (g : goal) =
let add db (_th:theory) (name : string) (sum:string) =
transaction db
(fun () ->
assert (g.goal_id = 0L);
let sql =
"INSERT INTO goal VALUES(NULL,?,?)"
"INSERT INTO goals VALUES(NULL,?,?,0)"
in
let stmt = bind db sql [
Sqlite3.Data.TEXT g.task_checksum;
Sqlite3.Data.INT (int64_from_bool g.proved);
Sqlite3.Data.TEXT name;
Sqlite3.Data.TEXT sum;
]
in
db_must_done db (fun () -> Sqlite3.step stmt);
let new_id = Sqlite3.last_insert_rowid db.raw_db in
(*
Format.eprintf "Db.Goal.add: add a new goal with id=%Ld@." new_id;
*)
g.goal_id <- new_id)
Sqlite3.last_insert_rowid db.raw_db)
(*
let get_all_external_proofs db g =
let sql="SELECT map_goal_prover_external_proof.external_proof_id \
FROM map_goal_prover_external_proof WHERE goal_id=?"
......@@ -825,7 +821,9 @@ module Goal = struct
);
e
*)
(*
let set_proved db g b =
transaction db
(fun () ->
......@@ -839,19 +837,20 @@ module Goal = struct
]
in
db_must_done db (fun () -> Sqlite3.step stmt))
*)
(*
let from_id _db _id : goal =
assert false
(*
let sql="SELECT goal.id, goal.task_checksum, goal.parent_id, goal.name, goal.pos_id, goal.proved, goal_pos.id, goal_pos.file, goal_pos.line, goal_pos.start, goal_pos.stop, goal_parent.id, goal_parent.name, goal_parent.obsolete FROM goal LEFT JOIN transf AS goal_parent ON (goal_parent.id = goal.parent_id) LEFT JOIN loc AS goal_pos ON (goal_pos.id = goal.pos_id) " ^ q in
let stmt=Sqlite3.prepare db.db sql in
*)
*)
end
*)
(*
let external_proofs g =
......@@ -1019,13 +1018,38 @@ end
*)
module Main = struct
module Theory = struct
let init db =
let sql = "CREATE TABLE IF NOT EXISTS files (file_name TEXT);" in
let sql = "CREATE TABLE IF NOT EXISTS theories (theory_name TEXT, theory_file INTEGER);" in
db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql);
()
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
db_must_done db (fun () -> Sqlite3.step stmt);
let new_id = Sqlite3.last_insert_rowid db.raw_db in
new_id)
end
module Main = struct
let init db =
let sql = "CREATE TABLE IF NOT EXISTS files \
(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 stmt = Sqlite3.prepare db.raw_db sql in
......@@ -1035,16 +1059,11 @@ module Main = struct
let add db name =
transaction db
(fun () ->
let sql = "INSERT INTO files VALUES(?)" in
let sql = "INSERT INTO files VALUES(NULL,?)" in
let stmt = bind db sql [ 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
(*
{ prover_id = Int64.to_int new_id ;
prover_name = name }
*)
)
new_id)
end
......@@ -1063,9 +1082,12 @@ let init_db ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
(*
Loc.init db;
External_proof.init db;
*)
Goal.init db;
(*
Transf.init db;
*)
Theory.init db;
Main.init db
| Some _ -> failwith "Db.init_db: already opened"
......@@ -1084,7 +1106,6 @@ let root_goals () =
let files _ = assert false
let prover_from_name n =
let db = current () in
try ProverId.get db n
......@@ -1101,8 +1122,10 @@ let set_status _ = assert false
let set_obsolete _ = assert false
let set_edited_as _ = assert false
let add_transformation _ = assert false
let add_goal _ = assert false
let add_theory _ = assert false
let add_goal th id sum = Goal.add (current()) th id sum
let add_subgoal _ = assert false
let add_theory f th = Theory.add (current()) f th
let add_file f = Main.add (current()) f
......
......@@ -151,9 +151,10 @@ val set_edited_as : proof_attempt -> string -> unit
(** {3 transformations} *)
val add_transformation : goal -> string -> goal list -> transf
(** adds a transformation for this goal, with the given subgoals
@raise AlreadyExist if a transformation with the same name
val add_transformation : goal -> transf_id -> transf
(** adds a transformation for this goal.
subgoals must be added afterwards by [add_subgoal]
@raise AlreadyExist if a transformation with the same id
is already there *)
(* todo: remove_transformation *)
......@@ -166,15 +167,20 @@ val add_goal : theory -> string -> string -> goal
@raise AlreadyExist if a goal with the same id already exists
in this theory *)
val add_subgoal : transf -> string -> string -> goal
(** [add_subgoal t id sum] adds to transf [t] a new subgoal named [id], with
[sum] as the checksum of its task.
@raise AlreadyExist if a goal with the same id already exists
as subgoal of this transf *)
(* todo: remove_goal *)
(** {3 theories} *)
val add_theory : file -> string -> string -> unit
(** [add_goal th id sum] adds to theory [th] a new goal named [id], with
[sum] as the checksum of its task.
@raise AlreadyExist if a goal with the same id already exists
in this theory *)
val add_theory : file -> string -> theory
(** [add_theory f id] adds to file f a theory named [th].
@raise AlreadyExist if a theory with the same id already exists
in this file *)
(* todo: remove_theory *)
......
......@@ -141,6 +141,7 @@ module Model = struct
{ parent : goal_parent;
task: Task.task;
goal_row : Gtk.tree_iter;
goal_db : Db.goal;
mutable proved : bool;
external_proofs: (string, proof_attempt) Hashtbl.t;
mutable transformations : transf list;
......@@ -152,19 +153,23 @@ module Model = struct
transf : Task.task Trans.trans;
*)
transf_row : Gtk.tree_iter;
transf_db : Db.transf;
mutable subgoals : goal list;
}
and theory =
{ theory : Theory.theory;
theory_row : Gtk.tree_iter;
theory_db : Db.theory;
theory_parent : file;
mutable goals : goal list;
mutable verified : bool;
}
type file =
and file =
{ file_name : string;
file_row : Gtk.tree_iter;
file_db : Db.file;
mutable theories: theory list;
mutable file_verified : bool;
}
......@@ -299,6 +304,10 @@ let (_ : GtkSignal.id) =
let goals_model,filter_model,goals_view =
Model.create ~packing:scrollview#add ()
let task_checksum t =
fprintf str_formatter "%a@." Pretty.print_task t;
Digest.to_hex (Digest.string (flush_str_formatter ()))
module Helpers = struct
let image_of_result = function
......@@ -325,9 +334,10 @@ module Helpers = struct
goals_view#collapse_row (goals_model#get_path row);
goals_model#set ~row ~column:Model.status_column !image_yes;
if !Model.toggle_hide_proved_goals then
goals_model#set ~row ~column:Model.visible_column false
(* TODO: check if all_theories are verified,
if yes, call set_file proved *)
goals_model#set ~row ~column:Model.visible_column false;
let f = t.theory_parent in
if List.for_all (fun t -> t.verified) f.theories then
set_file_verified f
let rec set_proved g =
let row = g.goal_row in
......@@ -355,10 +365,13 @@ module Helpers = struct
let add_theory mfile th =
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;
theory_row = row;
theory_db = db_theory;
theory_parent = mfile;
goals = [] ;
verified = false }
in
......@@ -373,9 +386,12 @@ module Helpers = struct
let id = (Task.task_goal t).Decl.pr_name in
let name = id.Ident.id_string in
let row = goals_model#append ~parent:row () in
let sum = task_checksum t in
let db_goal = Db.add_goal db_theory name sum in
let goal = { parent = Theory mth;
task = t ;
goal_row = row;
goal_db = db_goal;
external_proofs = Hashtbl.create 7;
transformations = [];
proved = false;
......@@ -398,10 +414,11 @@ module Helpers = struct
let add_file f =
try
let theories = Env.read_file gconfig.env f in
let _dbfile = Db.add_file f in
let dbfile = Db.add_file f in
let parent = goals_model#append () in
let mfile = { file_name = f;
file_row = parent;
file_db = dbfile;
theories = [] ;
file_verified = false }
in
......@@ -562,6 +579,7 @@ let split_transformation = Trans.lookup_transform_l "split_goal" gconfig.env
let intro_transformation = Trans.lookup_transform "introduce_premises" gconfig.env
let split_unproved_goals () =
let transf_id_split = Db.transf_from_name "split_goal" in
List.iter
(fun th ->
List.iter
......@@ -578,12 +596,16 @@ let split_unproved_goals () =
"split";
goals_model#set ~row:split_row ~column:Model.icon_column
!image_transf;
let db_transf =
Db.add_transformation g.Model.goal_db transf_id_split
in
let tr =
{ Model.parent_goal = g;
(*
Model.transf = split_transformation;
*)
Model.transf_row = split_row;
Model.transf_db = db_transf;
subgoals = [];
}
in
......@@ -593,12 +615,18 @@ let split_unproved_goals () =
let goals,_ = List.fold_left
(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 subtask_row =
goals_model#append ~parent:split_row ()
in
let sum = task_checksum subtask in
let subtask_db = Db.add_subgoal db_transf subgoal_name sum in
let goal = { Model.parent = Model.Transf tr;
Model.task = subtask ;
Model.goal_row = subtask_row;
Model.goal_db = subtask_db;
Model.external_proofs = Hashtbl.create 7;
Model.transformations = [];
Model.proved = false;
......@@ -609,8 +637,7 @@ let split_unproved_goals () =
goals_model#set ~row:subtask_row
~column:Model.visible_column true;
goals_model#set ~row:subtask_row
~column:Model.name_column
(goal_name ^ "." ^ (string_of_int count));
~column:Model.name_column subgoal_name;
goals_model#set ~row:subtask_row
~column:Model.icon_column !image_file;
(goal :: acc, count+1))
......@@ -672,7 +699,7 @@ let file_menu = factory#add_submenu "_File"
let file_factory = new GMenu.factory file_menu ~accel_group
let (_ : GMenu.image_menu_item) =
file_factory#add_image_item ~label:"_Add file" ~callback:select_file
file_factory#add_image_item ~key:GdkKeysyms._A ~label:"_Add file" ~callback:select_file
()
let (_ : GMenu.image_menu_item) =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment