transf dans db

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

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} *)

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 ()

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