From b45cda99d6c378e02a3cc13135f7807c96df1fc9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Claude=20March=C3=A9?= Date: Tue, 26 Oct 2010 15:45:42 +0000 Subject: [PATCH] transf dans db --- src/ide/db.ml | 114 ++++++++++++++++++++++++++++++++++++--- src/ide/db.mli | 4 ++ src/ide/gdbmain.ml | 120 ++++++++++++++++++++++++++++++++++++++++-- tests/test-claude.why | 6 +-- 4 files changed, 229 insertions(+), 15 deletions(-) diff --git a/src/ide/db.ml b/src/ide/db.ml index ff90c0514..fef91215e 100644 --- a/src/ide/db.ml +++ b/src/ide/db.ml @@ -195,17 +195,17 @@ module Hprover = Hashtbl.Make end) type transf_id = - { transf_id : int; - transf_name : string; + { transformation_id : int64; + transformation_name : string; } -let transf_name t = t.transf_name +let transf_name t = t.transformation_name module Htransf = Hashtbl.Make (struct type t = transf_id - let equal t1 t2 = t1.transf_id == t2.transf_id - let hash t = Hashtbl.hash t.transf_id + let equal t1 t2 = t1.transformation_id = t2.transformation_id + let hash t = Hashtbl.hash t.transformation_id end) @@ -232,7 +232,9 @@ type proof_attempt = int64 } *) +(* let prover _p = assert false (* p.prover *) +*) (* let status _p = assert false (* p.status *) *) @@ -278,7 +280,9 @@ type theory = int64 type file = int64 +(* let file_name _ = assert false +*) @@ -393,6 +397,103 @@ let get_prover name (* ~short ~long ~command ~driver *) = *) +module TransfId = struct + + let init db = + let sql = + "CREATE TABLE IF NOT EXISTS transformation \ + (transformation_id INTEGER PRIMARY KEY AUTOINCREMENT,transformation_name TEXT);" + in + db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql); + let sql = + "CREATE UNIQUE INDEX IF NOT EXISTS transformation_name_idx \ + ON transformation (transformation_name)" + in + db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql) + +(* + let delete db pr = + let id = pr.prover_id in + let sql = "DELETE FROM prover WHERE id=?" in + let stmt = Sqlite3.prepare db.raw_db sql in + db_must_ok db (fun () -> Sqlite3.bind stmt 1 (Sqlite3.Data.INT id)); + ignore (step_fold db stmt (fun _ -> ())); + pr.prover_id <- 0L +*) + + let add db name = + transaction db + (fun () -> + let sql = "INSERT INTO transformation 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 + { transformation_id = new_id ; + transformation_name = name } + ) + + let from_name db name = + let sql = + "SELECT transformation.transformation_id FROM transformation \ + WHERE transformation.transformation_name=?" + in + let stmt = bind db sql [Sqlite3.Data.TEXT name] in + (* convert statement into record *) + let of_stmt stmt = + { transformation_id = stmt_column_INT stmt 0 "TransfId.from_name: bad transformation id"; + transformation_name = name; + } + in + (* execute the SQL query *) + match step_fold db stmt of_stmt with + | [] -> raise Not_found + | [x] -> x + | _ -> assert false + + let from_id db id = + let sql = + "SELECT transformation.transformation_name FROM transformation \ + WHERE transformation.transformation_id=?" + in + let stmt = bind db sql [Sqlite3.Data.INT id] in + (* convert statement into record *) + let of_stmt stmt = + { transformation_id = id ; + transformation_name = stmt_column_string stmt 0 + "TransfId.from_id: bad transformation name"; + } + in + (* execute the SQL query *) + match step_fold db stmt of_stmt with + | [] -> raise Not_found + | [x] -> x + | _ -> assert false + +end + +(* +let prover_memo = Hashtbl.create 7 + +let prover_from_id id = + try + Hashtbl.find prover_memo id + with Not_found -> + let p = + let db = current () in + try TransfId.from_id db id + with Not_found -> assert false + in + Hashtbl.add prover_memo id p; + p +*) + +let transf_from_name n = + let db = current () in + try TransfId.from_name db n + with Not_found -> TransfId.add db n + + + (* module Loc = struct @@ -1280,6 +1381,7 @@ let init_db ?(busyfn=default_busyfn) ?(mode=Immediate) db_name = in current_db := Some db; ProverId.init db; + TransfId.init db; External_proof.init db; Goal.init db; (* @@ -1295,8 +1397,6 @@ let init_base f = init_db ~mode:Exclusive f let files () = List.rev (Main.all_files (current())) -let transf_from_name _n = assert false - exception AlreadyExist let add_proof_attempt g pid = External_proof.add (current()) g pid diff --git a/src/ide/db.mli b/src/ide/db.mli index 267e56967..789a3180f 100644 --- a/src/ide/db.mli +++ b/src/ide/db.mli @@ -74,7 +74,9 @@ val prover_name : prover_id -> string val transf_name : transf_id -> string (** proof_attempt accessors *) +(* val prover : proof_attempt -> prover_id +*) (* val proof_goal : proof_attempt -> goal *) @@ -110,7 +112,9 @@ val verified : theory -> bool *) (** file accessors *) +(* val file_name : file -> string +*) val theories : file -> theory list (** {2 The persistent database} *) diff --git a/src/ide/gdbmain.ml b/src/ide/gdbmain.ml index 76f1db055..6807d34cb 100644 --- a/src/ide/gdbmain.ml +++ b/src/ide/gdbmain.ml @@ -446,6 +446,67 @@ module Helpers = struct goal + let add_transformation_row parent g subgoals = + let row = goals_model#append ~parent () in + let goal_name = goals_model#get ~row:parent ~column:Model.name_column in + goals_model#set ~row ~column:Model.visible_column + true; + goals_model#set ~row ~column:Model.name_column + "split"; + goals_model#set ~row ~column:Model.icon_column + !image_transf; + let transf_id_split = Db.transf_from_name "split_goal" in + 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 = row; + Model.transf_db = db_transf; + subgoals = []; + } + in + goals_model#set ~row ~column:Model.index_column + (Model.Row_transformation tr); + g.Model.transformations <- tr :: g.Model.transformations; + 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:row () + in + let sum = task_checksum subtask in + let subtask_db = Db.add_subgoal db_transf subgoal_name sum in + (* TODO: call add_goal_row *) + 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; + } + in + goals_model#set ~row:subtask_row + ~column:Model.index_column (Model.Row_goal goal); + goals_model#set ~row:subtask_row + ~column:Model.visible_column true; + goals_model#set ~row:subtask_row + ~column:Model.name_column subgoal_name; + goals_model#set ~row:subtask_row + ~column:Model.icon_column !image_file; + (goal :: acc, count+1)) + ([],1) subgoals + in + tr.Model.subgoals <- List.rev goals; + goals_view#expand_row (goals_model#get_path parent) + let add_theory_row mfile th db_theory = let tname = th.Theory.th_name.Ident.id_string in let parent = mfile.file_row in @@ -712,13 +773,65 @@ let prover_on_selected_goals pr = (prover_on_selected_goal_or_children pr) goals_view#selection#get_selected_rows + + + (*****************************************************) -(* method: split all unproved goals *) +(* method: split selected goals *) (*****************************************************) let split_transformation = Trans.lookup_transform_l "split_goal" gconfig.env let intro_transformation = Trans.lookup_transform "introduce_premises" gconfig.env +let split_goal g = + if not g.Model.proved then + let row = g.Model.goal_row in + let callback subgoals = + if List.length subgoals >= 2 then + Helpers.add_transformation_row row g subgoals + in + Scheduler.apply_transformation_l ~callback + split_transformation g.Model.task + +let rec split_goal_or_children g = + if not g.Model.proved then + begin + match g.Model.transformations with + | [] -> split_goal g + | l -> + List.iter (fun t -> + List.iter split_goal_or_children + t.Model.subgoals) l + 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 + | Model.Row_goal g -> + split_goal_or_children g + | Model.Row_theory th -> + List.iter split_goal_or_children th.Model.goals + | Model.Row_file file -> + List.iter + (fun th -> + List.iter split_goal_or_children th.Model.goals) + file.Model.theories + | Model.Row_proof_attempt a -> + split_goal_or_children a.Model.proof_goal + | Model.Row_transformation tr -> + List.iter split_goal_or_children tr.Model.subgoals + + +let split_selected_goals () = + List.iter + split_selected_goal_or_children + goals_view#selection#get_selected_rows + + +(*****************************************************) +(* method: split all unproved goals *) +(*****************************************************) + let split_unproved_goals () = let transf_id_split = Db.transf_from_name "split_goal" in List.iter @@ -796,6 +909,7 @@ let split_unproved_goals () = ) [] (* !Model.all *) + (*********************************) (* add a new file in the project *) (*********************************) @@ -1000,8 +1114,8 @@ let () = let () = let add_item_split () = ignore(tools_factory#add_image_item - ~label:"Split unproved goals" - ~callback:split_unproved_goals + ~label:"Split selection" + ~callback:split_selected_goals () : GMenu.image_menu_item) in add_refresh_provers add_item_split; add_item_split () diff --git a/tests/test-claude.why b/tests/test-claude.why index 4a2c6fcb9..5f512b5cb 100644 --- a/tests/test-claude.why +++ b/tests/test-claude.why @@ -4,7 +4,7 @@ theory TestInt goal Test0 : true - goal Test0_5 : false + goal Test0_5 : true -> false goal Test1: 2+2 = 4 @@ -12,17 +12,13 @@ theory TestInt goal Test3: 1<>0 -(* goal Test4: 1=2 -> 3=4 -*) goal Test5: forall x:int. x <> 0 -> x*x > 0 goal Test6: 2+3 = 5 and (forall x:int. x*x >= 0) -(* goal Test7: 0 = 1 /\ 2 = 3 /\ 4 = 5 /\ 6 = 7 -*) (* goal Test8: 3+3=7 -- GitLab