Commit 25fc83ec authored by MARCHE Claude's avatar MARCHE Claude
Browse files

manager state

parent 376a001a
......@@ -246,7 +246,7 @@ src/manager/orm_schema.ml: $(ORM_CMO)
MANAGER_CMO := db.cmo
MANAGER_CMO := $(addprefix src/manager/,$(MANAGER_CMO))
$(MANAGER_CMO): INCLUDES=-I src/manager -I +sqlite3 -I +threads
$(MANAGER_CMO): INCLUDES=-I src/core -I src/driver -I src/manager -I +sqlite3 -I +threads
$(MANAGER_CMO): $(LIBCMI)
bin/manager.byte: $(LIBCMA) $(MANAGER_CMO)
......
......@@ -87,7 +87,7 @@ let step_fold db stmt iterfn =
type db_ident = int64
type loc_record =
{ mutable id : db_ident option;
{ mutable loc_id : db_ident option;
(** when None, the record has never been stored in database yet *)
mutable file : string;
mutable line : int;
......@@ -96,6 +96,93 @@ type loc_record =
}
type proof_attempt_status =
| Scheduled (** external proof attempt is scheduled *)
| Running (** external proof attempt is in progress *)
| Success (** external proof attempt succeeded *)
| Timeout (** external proof attempt was interrupted *)
| Unknown (** external prover answered ``don't know'' or equivalent *)
| HighFailure (** external prover call failed *)
type prover_data =
{ prover_name : string;
driver : Driver.driver;
}
type external_proof = {
mutable external_proof_id : db_ident option;
mutable prover : prover_data;
mutable timelimit : int;
mutable memlimit : int;
mutable status : proof_attempt_status;
mutable result_time : float;
mutable trace : string;
mutable proof_obsolete : bool;
}
let prover e = e.prover
let timelimit e = e.timelimit
let memlimit e = e.memlimit
let status e = e.status
let result_time e = e.result_time
let trace e = e.trace
let proof_obsolete e = e.proof_obsolete
type goal_origin =
| Goal of Decl.prsymbol
(*
| VCfun of loc * explain * ...
| Subgoal of goal
*)
type transf_data =
{ transf_name : string;
transf_action : Task.task Register.tlist_reg
}
type goal = {
mutable id : db_ident option;
mutable task : Task.task;
mutable task_checksum: string;
(*
mutable parent : transf option;
*)
mutable proved : bool;
(** invariant: g.proved == true iff
exists attempts a in g.attempts, a.obsolete == false and
(a = External e and e.result == Valid or
a = Transf(gl) and forall g in gl, g.proved)
*)
mutable observers: (bool -> unit) list;
(** observers that wants to be notified by any changes of the proved status *)
(*
mutable name : string;
*)
mutable external_proofs : external_proof list;
mutable transformations : transf list;
}
and transf = {
mutable id : int64 option;
mutable transf_data : transf_data;
mutable transf_obsolete : bool;
mutable subgoals : goal list;
}
let goal_task g = g.task
let goal_task_checksum g = g.task_checksum
let external_proofs g = g.external_proofs
let transformations g = g.transformations
let goal_proved g = g.proved
let transf_data t = t.transf_data
let transf_obsolete t = t.transf_obsolete
let subgoals t = t.subgoals
module Loc = struct
let init db =
......@@ -105,7 +192,7 @@ module Loc = struct
(* object definition *)
let create (* ?id *) ~file ~line ~start ~stop : loc_record =
{
id = None (* id *);
loc_id = None (* id *);
file = file;
line = line;
start = start;
......@@ -114,20 +201,20 @@ module Loc = struct
(* admin functions *)
let delete db loc =
match loc.id with
match loc.loc_id with
| None -> ()
| Some id ->
let sql = "DELETE FROM loc 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 _ -> ()));
loc.id <- None
loc.loc_id <- None
let save db loc =
let save db (loc : loc_record) =
transaction db
(fun () ->
(* insert any foreign-one fields into their table and get id *)
let curobj_id = match loc.id with
let curobj_id = match loc.loc_id with
| None ->
(* insert new record *)
let sql = "INSERT INTO loc VALUES(NULL,?,?,?,?)" in
......@@ -146,7 +233,7 @@ module Loc = struct
(let v = Int64.of_int loc.stop in Sqlite3.Data.INT v));
db_must_done db (fun () -> Sqlite3.step stmt);
let new_id = Sqlite3.last_insert_rowid db.raw_db in
loc.id <- Some new_id;
loc.loc_id <- Some new_id;
new_id
| Some id ->
(* update *)
......@@ -251,7 +338,7 @@ module Loc = struct
(* convert statement into an ocaml object *)
let of_stmt stmt =
{ (* native fields *)
id = (match Sqlite3.column stmt 0 with
loc_id = (match Sqlite3.column stmt 0 with
| Sqlite3.Data.NULL -> None
| Sqlite3.Data.INT i -> Some i
| x ->
......@@ -286,55 +373,26 @@ module Loc = struct
end
module External_proof = struct
let int64_from_bool b =
if b then 1L else 0L
type t = {
mutable id : int64 option;
mutable prover : string;
mutable timelimit : int64;
mutable memlimit : int64;
mutable status : int64;
mutable result_time : float;
mutable trace : string;
mutable obsolete : int64;
}
let int64_from_pas = function
| Scheduled -> 1L
| Running -> 2L
| Success -> 3L
| Timeout -> 4L
| Unknown -> 5L
| HighFailure -> 6L
let save db t : int64 =
assert false
module External_proof = struct
let delete db t : unit =
assert false
let init db =
let sql = "create table if not exists external_proof (id integer primary key autoincrement,prover text,timelimit integer,memlimit integer,status integer,result_time real,trace text,obsolete integer);" in
db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)
(*
(* object definition *)
let t ?(id=None) ~prover ~timelimit ~memlimit ~status ~result_time ~trace ~obsolete db : t = object
(* get functions *)
val mutable _id = id
method id : int64 option = _id
val mutable _prover = prover
method prover : string = _prover
val mutable _timelimit = timelimit
method timelimit : int64 = _timelimit
val mutable _memlimit = memlimit
method memlimit : int64 = _memlimit
val mutable _status = status
method status : int64 = _status
val mutable _result_time = result_time
method result_time : float = _result_time
val mutable _trace = trace
method trace : string = _trace
val mutable _obsolete = obsolete
method obsolete : int64 = _obsolete
*)
(* admin functions *)
let delete db e =
match e.id with
let delete db e =
match e.id with
| None -> ()
| Some id ->
let sql = "DELETE FROM external_proof WHERE id=?" in
......@@ -343,59 +401,58 @@ module External_proof = struct
ignore(step_fold db stmt (fun _ -> ()));
e.id <- None
let save db e =
transaction db
(fun () ->
(* insert any foreign-one fields into their table and get id *)
let curobj_id = match e.id with
| None -> (* insert new record *)
let sql =
"INSERT INTO external_proof VALUES(NULL,?,?,?,?,?,?,?)"
in
let stmt = Sqlite3.prepare db.raw_db sql in
db_must_ok db
(fun () -> Sqlite3.bind stmt 1
(let v = e.prover in Sqlite3.Data.TEXT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 2
(let v = e.timelimit in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 3
(let v = e.memlimit in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 4
(let v = e.status in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 5
(let v = e.result_time in Sqlite3.Data.FLOAT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 6
(let v = e.trace in Sqlite3.Data.TEXT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 7
(let v = e.obsolete in Sqlite3.Data.INT v));
db_must_done db
(fun () -> Sqlite3.step stmt);
let new_id = Sqlite3.last_insert_rowid db.raw_db in
e.id <- Some new_id;
new_id
| Some id -> (* update *)
let save db (e : external_proof) =
transaction db
(fun () ->
let curobj_id = match e.external_proof_id with
| None -> (* insert new record *)
let sql =
"INSERT INTO external_proof VALUES(NULL,?,?,?,?,?,?,?)"
in
let stmt = Sqlite3.prepare db.raw_db sql in
db_must_ok db
(fun () -> Sqlite3.bind stmt 1
(let v = e.prover.prover_name in Sqlite3.Data.TEXT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 2
(let v = Int64.of_int e.timelimit in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 3
(let v = Int64.of_int e.memlimit in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 4
(let v = int64_from_pas e.status in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 5
(let v = e.result_time in Sqlite3.Data.FLOAT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 6
(let v = e.trace in Sqlite3.Data.TEXT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 7
(let v = int64_from_bool e.proof_obsolete in Sqlite3.Data.INT v));
db_must_done db
(fun () -> Sqlite3.step stmt);
let new_id = Sqlite3.last_insert_rowid db.raw_db in
e.external_proof_id <- Some new_id;
new_id
| Some id -> (* update *)
let sql =
"UPDATE external_proof SET prover=?,timelimit=?,memlimit=?,status=?,result_time=?,trace=?,obsolete=? WHERE id=?"
in
let stmt = Sqlite3.prepare db.raw_db sql in
db_must_ok db
(fun () -> Sqlite3.bind stmt 1
(let v = e.prover in Sqlite3.Data.TEXT v));
(let v = e.prover.prover_name in Sqlite3.Data.TEXT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 2
(let v = e.timelimit in Sqlite3.Data.INT v));
(let v = Int64.of_int e.timelimit in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 3
(let v = e.memlimit in Sqlite3.Data.INT v));
(let v = Int64.of_int e.memlimit in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 4
(let v = e.status in Sqlite3.Data.INT v));
(let v = int64_from_pas e.status in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 5
(let v = e.result_time in Sqlite3.Data.FLOAT v));
......@@ -404,7 +461,7 @@ module External_proof = struct
(let v = e.trace in Sqlite3.Data.TEXT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 7
(let v = e.obsolete in Sqlite3.Data.INT v));
(let v = int64_from_bool e.proof_obsolete in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 8 (Sqlite3.Data.INT id));
db_must_done db (fun () -> Sqlite3.step stmt);
......@@ -523,32 +580,6 @@ module External_proof = struct
end
type proof_attempt_status =
| Running (** external proof attempt is in progress *)
| Success (** external proof attempt succeeded *)
| Timeout (** external proof attempt was interrupted *)
| Unknown (** external prover answered ``don't know'' or equivalent *)
| HighFailure (** external prover call failed *)
type goal = {
mutable id : int64 option;
mutable task_checksum : string;
mutable parent : transf option;
mutable name : string;
mutable pos : loc_record;
mutable external_proofs : External_proof.t list;
mutable transformations : transf list;
mutable proved : int64;
}
and transf = {
mutable id : int64 option;
mutable name : string;
mutable obsolete : int64;
mutable subgoals : goal list;
}
module Goal = struct
type t = goal
......@@ -829,7 +860,6 @@ end
module Transf = struct
type t = transf
(*
let init db =
......@@ -998,3 +1028,18 @@ let create ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
*)
db
exception AlreadyAttempted
let try_prover ~timelimit:int ?memlimit:int (g : goal) (d: prover_data) : unit =
assert false (* TODO *)
let add_transformation (g : goal) (t : transf) : unit =
assert false (* TODO *)
let add_or_replace_goal (g : goal) : unit =
assert false (* TODO *)
let read_db_from_file (file : string) : goal list =
assert false (* TODO *)
......@@ -26,17 +26,25 @@ val raw: handle -> Sqlite3.db
*)
(** {2 data} *)
(** The following define records which can be stored in the database
with the respective [save] functions, or removed by calling
[delete]. Changes are not committed to the database until
[save] is invoked. *)
(* {2 proof attempts and transformations} *)
(** {2 Current proof state} *)
(*
type db_ident (* = int64 *)
(** hidden type for record unique identifiers *)
*)
type loc_record = private
(*
type loc_record
*)
(*= private
{ mutable id : db_ident option;
(** when None, the record has never been stored in database yet *)
mutable file : string;
......@@ -44,196 +52,144 @@ type loc_record = private
mutable start : int;
mutable stop : int;
}
module Loc : sig
val save: handle -> loc_record -> db_ident
(** [save db loc] saves [loc] in database [db]. The record is created
if it does not exist yet. {!save}
@return the index of the saved record, which is also equal to loc.id
*)
val delete: handle -> loc_record -> unit
(** [delete db loc] removes the record from database {!delete} *)
val create :
(* ?id:int64 -> *)
file:string ->
line:int ->
start:int ->
stop:int ->
loc_record
(** Can be used to construct a new object. If [id] is not specified, it will be automatically assigned the first time [save] is called on the object. The object is not committed to the database until [save] is invoked. The [save] method will also return the [id] assigned to the object.
@raise Sql_error if a database error is encountered
*)
val get :
?id:int64 ->
?file:string ->
?line:int64 ->
?start:int64 ->
?stop:int64 ->
?custom_where:string * Sqlite3.Data.t list -> handle -> loc_record list
(** Used to retrieve objects from the database. If an argument is specified, it is included in the search criteria (all fields are ANDed together).
@raise Sql_error if a database error is encountered
*)
end
(** {2 proof attempts and transformations} *)
*)
(** status of an external proof attempt *)
type proof_attempt_status =
| Scheduled (** external proof attempt is scheduled *)
| Running (** external proof attempt is in progress *)
| Success (** external proof attempt succeeded *)
| Timeout (** external proof attempt was interrupted *)
| Unknown (** external prover answered ``don't know'' or equivalent *)
| HighFailure (** external prover call failed *)
type prover_data =
{ prover_name : string;
driver : Driver.driver;
}
type external_proof
val prover : external_proof -> prover_data
val timelimit : external_proof -> int
val memlimit : external_proof -> int
val status : external_proof -> proof_attempt_status
val result_time : external_proof -> float
val trace : external_proof -> string
val proof_obsolete : external_proof -> bool
(*
type goal_origin =
| Goal of Decl.prsymbol
(*
| VCfun of loc * explain * ...
| Subgoal of goal
*)
*)
type transf_data =
{ transf_name : string;
transf_action : Task.task Register.tlist_reg
}
type transf
type goal
val goal_task : goal -> Task.task
val goal_task_checksum: goal -> string
(*
module External_proof : sig
type t = <
id : int64 option;
set_id : int64 option -> unit;
prover : string;
set_prover : string -> unit;
timelimit : int64;
set_timelimit : int64 -> unit;
memlimit : int64;
set_memlimit : int64 -> unit;
status : int64;
set_status : int64 -> unit;
result_time : float;
set_result_time : float -> unit;
trace : string;
set_trace : string -> unit;
obsolete : int64;
set_obsolete : int64 -> unit;
save: int64; delete: unit
>
(** An object which can be stored in the database with the [save] method call, or removed by calling [delete]. Fields can be accessed via the approriate named method and set via the [set_] methods. Changes are not committed to the database until [save] is invoked.
*)
val t :
?id:int64 option ->
prover:string ->
timelimit:int64 ->
memlimit:int64 ->
status:int64 ->
result_time:float ->
trace:string ->
obsolete:int64 ->
Init.t -> t
(** Can be used to construct a new object. If [id] is not specified, it will be automatically assigned the first time [save] is called on the object. The object is not committed to the database until [save] is invoked. The [save] method will also return the [id] assigned to the object.
@raise Sql_error if a database error is encountered
*)
val get :
?id:int64 option ->
?prover:string option ->
?timelimit:int64 option ->
?memlimit:int64 option ->
?status:int64 option ->
?result_time:float option ->
?trace:string option ->
?obsolete:int64 option ->
?custom_where:string * Sqlite3.Data.t list -> Init.t -> t list
(** Used to retrieve objects from the database. If an argument is specified, it is included in the search criteria (all fields are ANDed together).
@raise Sql_error if a database error is encountered
*)
end
module Goal : sig
type t = <
id : int64 option;
set_id : int64 option -> unit;
task_checksum : string;
set_task_checksum : string -> unit;
parent : Transf.t;
set_parent : Transf.t -> unit;
name : string;
set_name : string -> unit;
pos : Loc.t;
set_pos : Loc.t -> unit;
external_proofs : External_proof.t list;
set_external_proofs : External_proof.t list -> unit;
transformations : Transf.t list;
set_transformations : Transf.t list -> unit;
proved : int64;
set_proved : int64 -> unit;
save: int64; delete: unit
>
(** An object which can be stored in the database with the [save] method call, or removed by calling [delete]. Fields can be accessed via the approriate named method and set via the [set_] methods. Changes are not committed to the database until [save] is invoked.
*)
val t :
?id:int64 option ->
task_checksum:string ->
parent:Transf.t ->
name:string ->
pos:Loc.t ->
external_proofs:External_proof.t list ->
transformations:Transf.t list ->
proved:int64 ->
Init.t -> t
(** Can be used to construct a new object. If [id] is not specified, it will be automatically assigned the first time [save] is called on the object. The object is not committed to the database until [save] is invoked. The [save] method will also return the [id] assigned to the object.
@raise Sql_error if a database error is encountered
*)
val get :
?id:int64 option ->
?task_checksum:string option ->
?name:string option ->
?proved:int64 option ->
?custom_where:string * Sqlite3.Data.t list -> Init.t -> t list
(** Used to retrieve objects from the database. If an argument is specified, it is included in the search criteria (all fields are ANDed together).
@raise Sql_error if a database error is encountered
*)
end
module Transf : sig
type t = <
id : int64 option;
set_id : int64 option -> unit;
name : string;
set_name : string -> unit;
obsolete : int64;
set_obsolete : int64 -> unit;
subgoals : Goal.t list;
set_subgoals : Goal.t list -> unit;
save: int64; delete: unit
>