Commit 636f6a58 authored by MARCHE Claude's avatar MARCHE Claude

new goals added in db

parent d08a847c
......@@ -4,8 +4,8 @@
== Documentation ==
* API: Andrei + Francois
* tools: WhyML (JC), IDE (Claude
* semantics:
* tools: WhyML (JC), IDE (Claude)
* semantics:
* tutorial for API:
** build a task
** call a prover
......
......@@ -896,7 +896,7 @@ module Goal = struct
| _ -> assert false
let of_theory db th =
let sql="SELECT goal_id FROM goals \
(* let sql="SELECT goal_id FROM goals \
WHERE goals.goal_theory=?"
in
let stmt = bind db sql [Sqlite3.Data.INT th] in
......@@ -904,7 +904,19 @@ module Goal = struct
(stmt_column_INT stmt 0 "Goal.of_theory")
in
List.rev (step_fold db stmt of_stmt)
*)
let sql="SELECT goal_id,goal_name FROM goals \
WHERE goals.goal_theory=?"
in
let stmt = bind db sql [Sqlite3.Data.INT th] in
step_fold_gen db stmt
(fun stmt acc ->
let g = stmt_column_INT stmt 0 "Goal.of_theory" in
let n = stmt_column_string stmt 1 "Goal.of_theory" in
Util.Mstr.add n g acc)
Util.Mstr.empty
(*
let get_all_external_proofs db g =
......
......@@ -104,7 +104,7 @@ val subgoals : transf -> goal list
(** theory accessors *)
val theory_name : theory -> string
val goals : theory -> goal list
val goals : theory -> goal Why.Util.Mstr.t
(*
val verified : theory -> bool
*)
......
......@@ -359,7 +359,12 @@ module Helpers = struct
goals_model#set ~row ~column:visible_column false;
let f = t.theory_parent in
if propagate then
if List.for_all (fun t -> t.verified) f.theories then
if List.for_all (fun t ->
(*
let tname = t.theory.Theory.th_name.Ident.id_string in
eprintf "checking theory %s@." tname;
*)
t.verified) f.theories then
set_file_verified f
let rec set_proved ~propagate g =
......@@ -456,6 +461,7 @@ 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;
mfile.theories <- mth :: mfile.theories;
mth
let add_theory mfile th =
......@@ -545,27 +551,27 @@ let () =
let goals = Db.goals db_th in
let tasks = List.rev (Task.split_theory th None None) in
let theory_proved = ref true in
(* TODO: remplacer iter2 par un parcours intelligent
en detectant d'eventuelles nouvelles tasks *)
List.iter2
(fun db_goal t ->
let gname = Db.goal_name db_goal in
let taskname =
List.iter
(fun t ->
let gname =
(Task.task_goal t).Decl.pr_name.Ident.id_string
in
if gname <> taskname then
begin
eprintf "gname = %s, taskname = %s@." gname taskname;
assert false;
end;
let sum = task_checksum t in
let db_sum = Db.task_checksum db_goal in
let goal_obsolete = sum <> db_sum in
if goal_obsolete then
begin
eprintf "Goal %s.%s has changed@." tname gname;
Db.change_checksum db_goal sum
end;
let db_goal,goal_obsolete =
try
let dbg = Util.Mstr.find gname goals in
let db_sum = Db.task_checksum dbg in
let goal_obsolete = sum <> db_sum in
if goal_obsolete then
begin
eprintf "Goal %s.%s has changed@." tname gname;
Db.change_checksum dbg sum
end;
dbg,goal_obsolete
with Not_found ->
let dbg = Db.add_goal db_th gname sum in
dbg,false
in
let goal = Helpers.add_goal_row mth gname t db_goal in
let external_proofs = Db.external_proofs db_goal in
let proved = ref false in
......@@ -579,7 +585,9 @@ let () =
let obsolete = goal_obsolete or o in
let s = match s with
| Db.Undone -> Scheduler.HighFailure
| Db.Success -> proved := true; Scheduler.Success
| Db.Success ->
if not obsolete then proved := true;
Scheduler.Success
| Db.Unknown -> Scheduler.Unknown
| Db.Timeout -> Scheduler.Timeout
| Db.Failure -> Scheduler.HighFailure
......@@ -593,7 +601,8 @@ let () =
if !proved then Helpers.set_proved ~propagate:false goal
else theory_proved := false;
)
goals tasks;
tasks;
(* TODO: what to do with remaining goals in Db ??? *)
if !theory_proved then Helpers.set_theory_proved ~propagate:false mth
else file_proved := false
)
......
......@@ -12,13 +12,21 @@ 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
*)
end
......@@ -48,7 +56,7 @@ theory TestReal
use import real.Abs
goal RealAbs1: forall x:real. 100.0 >= abs x >= 1.0 -> x*x >= 1.0
goal RealAbs1: forall x:real. 100.0 >= abs x >= 2.0 -> x*x >= 4.0
end
......@@ -70,11 +78,13 @@ theory TestList
logic x : list int
(*
goal Test1:
match x with
| Nil -> 1 = 0 /\ 2 = 3
| Cons _ Nil -> 4 = 5 and 6 = 7
| Cons _ _ -> 8 = 9 /\ 10 = 11
end
*)
end
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