Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
a17ef403
Commit
a17ef403
authored
Oct 01, 2010
by
MARCHE Claude
Browse files
more db
parent
48e970e0
Changes
3
Hide whitespace changes
Inline
Side-by-side
src/ide/db.ml
View file @
a17ef403
...
...
@@ -158,18 +158,23 @@ let stmt_column_string stmt i msg =
(** Data *)
type
prover_id
=
type
prover_id
=
int64
(*
{ prover_id : int;
prover_name : string;
}
*)
let
prover_name
_p
=
assert
false
(* p.prover_name *)
let
prover_name
p
=
p
.
prover_name
module
Hprover
=
Hashtbl
.
Make
(
struct
type
t
=
prover_id
let
equal
p1
p2
=
p1
.
prover_id
==
p2
.
prover_id
let
hash
p
=
Hashtbl
.
hash
p
.
prover_id
let
equal
_
p1
_
p2
=
assert
false
(*
p1.prover_id == p2.prover_id
*)
let
hash
_
p
=
assert
false
(*
Hashtbl.hash p.prover_id
*)
end
)
type
transf_id
=
...
...
@@ -190,6 +195,7 @@ module Htransf = Hashtbl.Make
type
proof_status
=
|
Undone
(** external proof attempt no done yet *)
|
Success
(** external proof attempt succeeded *)
|
Timeout
(** external proof attempt was interrupted *)
|
Unknown
(** external prover answered ``don't know'' or equivalent *)
...
...
@@ -233,7 +239,7 @@ and goal = int64
let
task_checksum
_g
=
assert
false
let
proved
_g
=
assert
false
let
external_proofs
_g
=
assert
false
let
external_proofs
_g
=
Hprover
.
create
7
(* TODO !!! *)
let
transformations
_g
=
assert
false
...
...
@@ -285,9 +291,14 @@ module ProverId = struct
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
})
prover_name = name }
*)
)
(*
let get db name =
let sql =
"SELECT prover.prover_id, prover.prover_name FROM prover \
...
...
@@ -305,7 +316,9 @@ module ProverId = struct
| [] -> raise Not_found
| [x] -> x
| _ -> assert false
*)
(*
let from_id db id =
let sql =
"SELECT prover.prover_id, prover.prover_name FROM prover \
...
...
@@ -324,6 +337,7 @@ module ProverId = struct
| [] -> raise Not_found
| [x] -> x
| _ -> assert false
*)
end
...
...
@@ -529,32 +543,35 @@ end
*)
let
status_array
=
[
|
Undone
;
Success
;
Timeout
;
Unknown
;
Failure
|
]
let
int64_from_status
=
function
|
Undone
->
0
L
|
Success
->
1
L
|
Timeout
->
2
L
|
Unknown
->
3
L
|
Failure
->
4
L
let
status_from_int64
i
=
if
i
=
1
L
then
Success
else
if
i
=
2
L
then
Timeout
else
if
i
=
3
L
then
Unknown
else
if
i
=
4
L
then
Failure
else
failwith
"Db.status_from_int64"
(*
try
status_array
.
(
Int64
.
to_int
i
)
with
_
->
failwith
"Db.status_from_int64"
module
External_proof
=
struct
let
init
db
=
let
sql
=
(* timelimit INTEGER, memlimit INTEGER,
edited_as TEXT, obsolete INTEGER *)
"CREATE TABLE IF NOT EXISTS external_proof \
(external_proof_id INTEGER PRIMARY KEY AUTOINCREMENT,\
prover INTEGER,timelimit INTEGER,memlimit INTEGER,\
status INTEGER,result_time REAL,trace TEXT,obsolete INTEGER);"
(goal_id INTEGER,\
prover_id INTEGER, \
status INTEGER,\
result_time REAL);"
in
db_must_ok
db
(
fun
()
->
Sqlite3
.
exec
db
.
raw_db
sql
)
(*
let delete db e =
let id = e.external_proof_id in
assert (id <> 0L);
...
...
@@ -562,26 +579,33 @@ module External_proof = struct
let stmt = bind db sql [ Sqlite3.Data.INT id ] in
ignore(step_fold db stmt (fun _ -> ()));
e.external_proof_id <- 0L
*)
let add db (
e
:
external_proof
) =
let
add
db
(
g
:
goal
)
(
p
:
prover_id
)
=
transaction
db
(
fun
()
->
assert (e.external_proof_id = 0L);
let sql = "INSERT INTO external_proof VALUES(NULL,?,?,?,?,?,?,?)" in
let
sql
=
"INSERT INTO external_proof VALUES(?,0,0,?)"
in
let
stmt
=
bind
db
sql
[
Sqlite3.Data.INT e.prover ;
Sqlite3
.
Data
.
INT
g
;
Sqlite3
.
Data
.
INT
p
;
(*
Sqlite3.Data.INT (Int64.of_int e.timelimit);
Sqlite3.Data.INT (Int64.of_int e.memlimit);
*)
(*
Sqlite3.Data.INT (int64_from_status e.status);
Sqlite3.Data.FLOAT e.result_time;
*)
(*
Sqlite3.Data.TEXT e.trace;
Sqlite3.Data.INT (int64_from_bool e.proof_obsolete);
*)
]
in
db_must_done
db
(
fun
()
->
Sqlite3
.
step
stmt
);
let new_id = Sqlite3.last_insert_rowid db.raw_db in
e.external_proof_id <- new_id)
Sqlite3
.
last_insert_rowid
db
.
raw_db
)
(*
let set_status db e stat =
try
...
...
@@ -705,9 +729,9 @@ module External_proof = struct
stmt_column_bool stmt 7
"External_Proof.fromids: bad proof_obsolete";
})
*)
end
*)
...
...
@@ -1181,16 +1205,21 @@ let files () =
Main
.
all_files
(
current
()
)
let
prover_from_name
n
=
let
prover_from_name
_n
=
assert
false
(*
let db = current () in
try ProverId.get db n
with Not_found -> ProverId.add db n
*)
let
transf_from_name
_n
=
assert
false
exception
AlreadyExist
let
add_proof_attempt
_
=
assert
false
let
add_proof_attempt
_g
_pid
=
assert
false
(*
External_proof.add (current()) g pid
*)
let
set_status
_
=
assert
false
...
...
src/ide/db.mli
View file @
a17ef403
...
...
@@ -51,6 +51,7 @@ type transf
(** status of an external proof attempt *)
type
proof_status
=
|
Undone
|
Success
(** external proof attempt succeeded *)
|
Timeout
(** external proof attempt was interrupted *)
|
Unknown
(** external prover answered ``don't know'' or equivalent *)
...
...
src/ide/gdbmain.ml
View file @
a17ef403
...
...
@@ -126,6 +126,7 @@ module Model = struct
{
prover
:
prover_data
;
proof_goal
:
goal
;
proof_row
:
Gtk
.
tree_iter
;
proof_db
:
Db
.
proof_attempt
;
mutable
status
:
Scheduler
.
proof_attempt_status
;
mutable
proof_obsolete
:
bool
;
mutable
time
:
float
;
...
...
@@ -339,17 +340,17 @@ module Helpers = struct
f
.
file_verified
<-
true
;
let
row
=
f
.
file_row
in
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
goals_model
#
set
~
row
~
column
:
status_column
!
image_yes
;
if
!
toggle_hide_proved_goals
then
goals_model
#
set
~
row
~
column
:
visible_column
false
let
set_theory_proved
t
=
t
.
verified
<-
true
;
let
row
=
t
.
theory_row
in
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
;
goals_model
#
set
~
row
~
column
:
status_column
!
image_yes
;
if
!
toggle_hide_proved_goals
then
goals_model
#
set
~
row
~
column
:
visible_column
false
;
let
f
=
t
.
theory_parent
in
if
List
.
for_all
(
fun
t
->
t
.
verified
)
f
.
theories
then
set_file_verified
f
...
...
@@ -358,9 +359,9 @@ module Helpers = struct
let
row
=
g
.
goal_row
in
g
.
proved
<-
true
;
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
;
goals_model
#
set
~
row
~
column
:
status_column
!
image_yes
;
if
!
toggle_hide_proved_goals
then
goals_model
#
set
~
row
~
column
:
visible_column
false
;
match
g
.
parent
with
|
Theory
t
->
if
List
.
for_all
(
fun
g
->
g
.
proved
)
t
.
goals
then
...
...
@@ -374,10 +375,37 @@ module Helpers = struct
let
set_proof_status
a
s
=
a
.
status
<-
s
;
let
row
=
a
.
proof_row
in
goals_model
#
set
~
row
~
column
:
Model
.
status_column
goals_model
#
set
~
row
~
column
:
status_column
(
image_of_result
s
);
if
s
=
Scheduler
.
Success
then
set_proved
a
.
proof_goal
let
add_external_proof_row
g
p
db_proof
=
let
parent
=
g
.
goal_row
in
let
name
=
p
.
prover_name
in
let
row
=
goals_model
#
prepend
~
parent
()
in
goals_model
#
set
~
row
~
column
:
icon_column
!
image_prover
;
goals_model
#
set
~
row
~
column
:
name_column
(
name
^
" "
^
p
.
prover_version
);
goals_model
#
set
~
row
~
column
:
visible_column
true
;
goals_view
#
expand_row
(
goals_model
#
get_path
parent
);
let
a
=
{
prover
=
p
;
proof_goal
=
g
;
proof_row
=
row
;
proof_db
=
db_proof
;
status
=
Scheduler
.
Scheduled
;
proof_obsolete
=
false
;
time
=
0
.
0
;
output
=
""
;
edited_as
=
""
;
}
in
goals_model
#
set
~
row
~
column
:
index_column
(
Row_proof_attempt
a
);
Hashtbl
.
add
g
.
external_proofs
p
.
prover_id
a
;
a
let
add_goal_row
mth
name
t
db_goal
=
let
parent
=
mth
.
theory_row
in
let
row
=
goals_model
#
append
~
parent
()
in
...
...
@@ -394,8 +422,10 @@ module Helpers = struct
goals_model
#
set
~
row
~
column
:
icon_column
!
image_file
;
goals_model
#
set
~
row
~
column
:
index_column
(
Row_goal
goal
);
goals_model
#
set
~
row
~
column
:
visible_column
true
;
mth
.
goals
<-
goal
::
mth
.
goals
;
goal
let
add_theory_row
mfile
th
db_theory
=
let
tname
=
th
.
Theory
.
th_name
.
Ident
.
id_string
in
let
parent
=
mfile
.
file_row
in
...
...
@@ -425,13 +455,11 @@ module Helpers = struct
let
name
=
id
.
Ident
.
id_string
in
let
sum
=
task_checksum
t
in
let
db_goal
=
Db
.
add_goal
db_theory
name
sum
in
let
goal
=
add_goal_row
mth
name
t
db_goal
in
goal
::
acc
)
let
goal
=
add_goal_row
mth
name
t
db_goal
in
goal
::
acc
)
[]
(
List
.
rev
tasks
)
in
mth
.
goals
<-
List
.
rev
goals
;
if
goals
=
[]
then
set_theory_proved
mth
;
mth
...
...
@@ -483,7 +511,7 @@ end
let
()
=
let
files
=
Db
.
files
()
in
List
.
iter
List
.
iter
(
fun
(
f
,
fn
)
->
eprintf
"Reimporting file '%s'@."
fn
;
let
theories
=
Env
.
read_file
gconfig
.
env
fn
in
...
...
@@ -494,9 +522,14 @@ let () =
let
tname
=
Db
.
theory_name
db_th
in
eprintf
"Reimporting theory '%s'@."
tname
;
let
th
=
Theory
.
Mnm
.
find
tname
theories
in
(* TODO: capturer Not_found, cad detecter si la theorie a ete supprmee du fichier *)
(* on pourrait retrouver l'ordre des theories dans le fichier source
en comparant les locations des idents de ces theories *)
let
mth
=
Helpers
.
add_theory_row
mfile
th
db_th
in
let
goals
=
Db
.
goals
db_th
in
let
tasks
=
List
.
rev
(
Task
.
split_theory
th
None
None
)
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
...
...
@@ -508,14 +541,16 @@ let () =
eprintf
"gname = %s, taskname = %s@."
gname
taskname
;
assert
false
;
end
;
let
(
_mg
:
Model
.
goal
)
=
Helpers
.
add_goal_row
mth
gname
t
db_goal
in
let
_goal
=
Helpers
.
add_goal_row
mth
gname
t
db_goal
in
let
_external_proofs
=
Db
.
external_proofs
db_goal
in
()
)
goals
tasks
)
ths
ths
;
(* TODO: detecter d'eventuelles nouvelles theories, qui seraient donc
dans [theories] mais pas dans [ths]
*)
)
files
...
...
@@ -559,33 +594,13 @@ let redo_external_proof g a =
g
.
Model
.
task
let
rec
prover_on_goal
p
g
=
let
row
=
g
.
Model
.
goal_row
in
let
id
=
p
.
prover_id
in
let
a
=
try
Hashtbl
.
find
g
.
Model
.
external_proofs
id
with
Not_found
->
(* creating a new row *)
let
name
=
p
.
prover_name
in
let
prover_row
=
goals_model
#
prepend
~
parent
:
row
()
in
goals_model
#
set
~
row
:
prover_row
~
column
:
Model
.
icon_column
!
image_prover
;
goals_model
#
set
~
row
:
prover_row
~
column
:
Model
.
name_column
(
name
^
" "
^
p
.
prover_version
);
goals_model
#
set
~
row
:
prover_row
~
column
:
Model
.
visible_column
true
;
goals_view
#
expand_row
(
goals_model
#
get_path
row
);
let
a
=
{
Model
.
prover
=
p
;
Model
.
proof_goal
=
g
;
Model
.
proof_row
=
prover_row
;
Model
.
status
=
Scheduler
.
Scheduled
;
Model
.
proof_obsolete
=
false
;
Model
.
time
=
0
.
0
;
Model
.
output
=
""
;
Model
.
edited_as
=
""
;
}
in
goals_model
#
set
~
row
:
prover_row
~
column
:
Model
.
index_column
(
Model
.
Row_proof_attempt
a
);
Hashtbl
.
add
g
.
Model
.
external_proofs
id
a
;
a
let
db_prover
=
Db
.
prover_from_name
id
in
let
db_pa
=
Db
.
add_proof_attempt
g
.
Model
.
goal_db
db_prover
in
Helpers
.
add_external_proof_row
g
p
db_pa
in
redo_external_proof
g
a
;
List
.
iter
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment