Skip to content

GitLab

Commit ff634837 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

db

parent a3eb1d19
Hide whitespace changes
Inline Side-by-side
Makefile.in
View file @ ff634837
......@@ -230,8 +230,8 @@ ORM_CMO := $(addprefix src/orm/,$(ORM_CMO))
$(ORM_CMO): INCLUDES=-I src/orm -I +sqlite3
src/manager/db.ml: $(ORM_CMO) src/manager/orm_schema.ml
ocaml -I src/orm src/manager/orm_schema.ml
# src/manager/db.ml: $(ORM_CMO) src/manager/orm_schema.ml
# ocaml -I src/orm src/manager/orm_schema.ml
src/manager/orm_schema.ml: $(ORM_CMO)
......
src/manager/db.ml
View file @ ff634837
(* autogenerated by sql_orm *)
module Sql_access = struct
(*
* Copyright (c) 2009 Anil Madhavapeddy <anil@recoil.org>
*
* Permission to use, copy, modify, and distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
*
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
*)
open Sqlite3
open Printf
type transaction_mode = [
|`Deferred
|`Immediate
|`Exclusive
]
type state = {
db : db;
mutable in_transaction: int;
busyfn: db -> unit;
mode: transaction_mode;
}
let default_busyfn (db:Sqlite3.db) =
print_endline "WARNING: busy";
Thread.delay (Random.float 1.)
let raise_sql_error x =
raise (Sqlite3.Error (Rc.to_string x))
open Sqlite3
open Printf
let try_finally fn finalfn =
try
let r = fn () in
finalfn ();
r
with e -> begin
print_endline (sprintf "WARNING: exception: %s" (Printexc.to_string e));
finalfn ();
raise e
end
type transaction_mode = | Deferred | Immediate | Exclusive
(* retry until a non-BUSY error code is returned *)
let rec db_busy_retry db fn =
match fn () with
|Rc.BUSY ->
db.busyfn db.db;
db_busy_retry db fn;
|x -> x
type state = {
db : db;
mutable in_transaction: int;
busyfn: db -> unit;
mode: transaction_mode;
}
(* make sure an OK is returned from the database *)
let db_must_ok db fn =
match db_busy_retry db fn with
|Rc.OK -> ()
|x -> raise_sql_error x
let default_busyfn (db:Sqlite3.db) =
print_endline "WARNING: busy";
Thread.delay (Random.float 1.)
(* make sure a DONE is returned from the database *)
let db_must_done db fn =
match db_busy_retry db fn with
|Rc.DONE -> ()
|x -> raise_sql_error x
let raise_sql_error x = raise (Sqlite3.Error (Rc.to_string x))
(* request a transaction *)
let transaction db fn =
let m = match db.mode with
|`Deferred -> "DEFERRED" |`Immediate -> "IMMEDIATE" |`Exclusive -> "EXCLUSIVE" in
try_finally (fun () ->
if db.in_transaction = 0 then (
db_must_ok db (fun () -> exec db.db (sprintf "BEGIN %s TRANSACTION" m));
);
db.in_transaction <- db.in_transaction + 1;
fn ();
) (fun () ->
if db.in_transaction = 1 then (
db_must_ok db (fun () -> exec db.db "END TRANSACTION");
);
db.in_transaction <- db.in_transaction - 1
)
let try_finally fn finalfn =
try
let r = fn () in
finalfn ();
r
with e -> begin
print_endline (sprintf "WARNING: exception: %s" (Printexc.to_string e));
finalfn ();
raise e
end
(* retry until a non-BUSY error code is returned *)
let rec db_busy_retry db fn =
match fn () with
| Rc.BUSY -> db.busyfn db.db; db_busy_retry db fn
| x -> x
(* make sure an OK is returned from the database *)
let db_must_ok db fn =
match db_busy_retry db fn with
| Rc.OK -> ()
| x -> raise_sql_error x
(* make sure a DONE is returned from the database *)
let db_must_done db fn =
match db_busy_retry db fn with
| Rc.DONE -> ()
| x -> raise_sql_error x
(* request a transaction *)
let transaction db fn =
let m = match db.mode with
| Deferred -> "DEFERRED"
| Immediate -> "IMMEDIATE"
| Exclusive -> "EXCLUSIVE"
in
try_finally
(fun () ->
if db.in_transaction = 0 then
begin
db_must_ok db
(fun () -> exec db.db (sprintf "BEGIN %s TRANSACTION" m))
end;
db.in_transaction <- db.in_transaction + 1;
fn ();
)
(fun () ->
if db.in_transaction = 1 then
begin
db_must_ok db (fun () -> exec db.db "END TRANSACTION")
end;
db.in_transaction <- db.in_transaction - 1
)
(* iterate over a result set *)
let step_fold db stmt iterfn =
let stepfn () = Sqlite3.step stmt in
let rec fn a = match db_busy_retry db stepfn with
|Sqlite3.Rc.ROW -> fn (iterfn stmt :: a)
|Sqlite3.Rc.DONE -> a
|x -> raise_sql_error x
in
fn []
end
(* iterate over a result set *)
let step_fold db stmt iterfn =
let stepfn () = Sqlite3.step stmt in
let rec fn a = match db_busy_retry db stepfn with
| Sqlite3.Rc.ROW -> fn (iterfn stmt :: a)
| Sqlite3.Rc.DONE -> a
| x -> raise_sql_error x
in
fn []
open Sql_access
module Loc = struct
type t = <
id : int64 option;
set_id : int64 option -> unit;
file : string;
set_file : string -> unit;
line : int64;
set_line : int64 -> unit;
start : int64;
set_start : int64 -> unit;
stop : int64;
set_stop : int64 -> unit;
save: int64; delete: unit
>
type t = {
mutable id : int64 option;
mutable file : string;
mutable line : int64;
mutable start : int64;
mutable stop : int64;
}
let init db =
let sql = "create table if not exists loc (id integer primary key autoincrement,file text,line integer,start integer,stop integer);" in
......@@ -121,117 +98,156 @@ module Loc = struct
()
(* object definition *)
let t ?(id=None) ~file ~line ~start ~stop db : t = object
(* get functions *)
val mutable _id = id
method id : int64 option = _id
val mutable _file = file
method file : string = _file
val mutable _line = line
method line : int64 = _line
val mutable _start = start
method start : int64 = _start
val mutable _stop = stop
method stop : int64 = _stop
(* set functions *)
method set_id v =
_id <- v
method set_file v =
_file <- v
method set_line v =
_line <- v
method set_start v =
_start <- v
method set_stop v =
_stop <- v
(* admin functions *)
method delete =
match _id with
|None -> ()
|Some id ->
let sql = "DELETE FROM loc WHERE id=?" in
let stmt = Sqlite3.prepare db.db sql in
db_must_ok db (fun () -> Sqlite3.bind stmt 1 (Sqlite3.Data.INT id));
ignore(step_fold db stmt (fun _ -> ()));
_id <- None
method save = transaction db (fun () ->
(* insert any foreign-one fields into their table and get id *)
let _curobj_id = match _id with
|None -> (* insert new record *)
let sql = "INSERT INTO loc VALUES(NULL,?,?,?,?)" in
let stmt = Sqlite3.prepare db.db sql in
db_must_ok db (fun () -> Sqlite3.bind stmt 1 (let v = _file in Sqlite3.Data.TEXT v));
db_must_ok db (fun () -> Sqlite3.bind stmt 2 (let v = _line in Sqlite3.Data.INT v));
db_must_ok db (fun () -> Sqlite3.bind stmt 3 (let v = _start in Sqlite3.Data.INT v));
db_must_ok db (fun () -> Sqlite3.bind stmt 4 (let v = _stop in Sqlite3.Data.INT v));
db_must_done db (fun () -> Sqlite3.step stmt);
let __id = Sqlite3.last_insert_rowid db.db in
_id <- Some __id;
__id
|Some id -> (* update *)
let sql = "UPDATE loc SET file=?,line=?,start=?,stop=? WHERE id=?" in
let stmt = Sqlite3.prepare db.db sql in
db_must_ok db (fun () -> Sqlite3.bind stmt 1 (let v = _file in Sqlite3.Data.TEXT v));
db_must_ok db (fun () -> Sqlite3.bind stmt 2 (let v = _line in Sqlite3.Data.INT v));
db_must_ok db (fun () -> Sqlite3.bind stmt 3 (let v = _start in Sqlite3.Data.INT v));
db_must_ok db (fun () -> Sqlite3.bind stmt 4 (let v = _stop in Sqlite3.Data.INT v));
db_must_ok db (fun () -> Sqlite3.bind stmt 5 (Sqlite3.Data.INT id));
db_must_done db (fun () -> Sqlite3.step stmt);
id
in
_curobj_id
)
end
let t ?id ~file ~line ~start ~stop db : t =
{
id = id;
file = file;
line = line;
start = start;
stop = stop;
}
(* admin functions *)
let delete db loc =
match loc.id with
| None -> ()
| Some id ->
let sql = "DELETE FROM loc WHERE id=?" in
let stmt = Sqlite3.prepare db.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
let save db loc =
transaction db
(fun () ->
(* insert any foreign-one fields into their table and get id *)
let curobj_id = match loc.id with
| None ->
(* insert new record *)
let sql = "INSERT INTO loc VALUES(NULL,?,?,?,?)" in
let stmt = Sqlite3.prepare db.db sql in
db_must_ok db
(fun () -> Sqlite3.bind stmt 1
(let v = loc.file in Sqlite3.Data.TEXT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 2
(let v = loc.line in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 3
(let v = loc.start in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 4
(let v = loc.stop in Sqlite3.Data.INT v));
db_must_done db (fun () -> Sqlite3.step stmt);
let new_id = Sqlite3.last_insert_rowid db.db in
loc.id <- Some new_id;
new_id
| Some id ->
(* update *)
let sql =
"UPDATE loc SET file=?,line=?,start=?,stop=? WHERE id=?"
in
let stmt = Sqlite3.prepare db.db sql in
db_must_ok db
(fun () -> Sqlite3.bind stmt 1
(let v = loc.file in Sqlite3.Data.TEXT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 2
(let v = loc.line in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 3
(let v = loc.start in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 4
(let v = loc.stop in Sqlite3.Data.INT v));
db_must_ok db
(fun () -> Sqlite3.bind stmt 5 (Sqlite3.Data.INT id));
db_must_done db (fun () -> Sqlite3.step stmt);
id
in
curobj_id)
(* General get function for any of the columns *)
let get ?(id=None) ?(file=None) ?(line=None) ?(start=None) ?(stop=None) ?(custom_where=("",[])) db =
let get ?id ?file ?line ?start ?stop ?(custom_where=("",[])) db =
(* assemble the SQL query string *)
let q = "" in
let _first = ref true in
let f () = match !_first with |true -> _first := false; " WHERE " |false -> " AND " in
let q = match id with |None -> q |Some b -> q ^ (f()) ^ "loc.id=?" in
let q = match file with |None -> q |Some b -> q ^ (f()) ^ "loc.file=?" in
let q = match line with |None -> q |Some b -> q ^ (f()) ^ "loc.line=?" in
let q = match start with |None -> q |Some b -> q ^ (f()) ^ "loc.start=?" in
let q = match stop with |None -> q |Some b -> q ^ (f()) ^ "loc.stop=?" in
let q = match custom_where with |"",_ -> q |w,_ -> q ^ (f()) ^ "(" ^ w ^ ")" in
let sql="SELECT loc.id, loc.file, loc.line, loc.start, loc.stop FROM loc " ^ q in
let first = ref true in
let f () = if !first then (first := false; " WHERE ") else " AND "
in
let q = match id with
| None -> q | Some b -> q ^ (f()) ^ "loc.id=?" in
let q = match file with
| None -> q | Some b -> q ^ (f()) ^ "loc.file=?" in
let q = match line with
| None -> q | Some b -> q ^ (f()) ^ "loc.line=?" in
let q = match start with
| None -> q | Some b -> q ^ (f()) ^ "loc.start=?" in
let q = match stop with
| None -> q | Some b -> q ^ (f()) ^ "loc.stop=?" in
let q = match custom_where with
| "",_ -> q | w,_ -> q ^ (f()) ^ "(" ^ w ^ ")" in
let sql =
"SELECT loc.id, loc.file, loc.line, loc.start, loc.stop FROM loc " ^ q
in
let stmt=Sqlite3.prepare db.db sql in
(* bind the position variables to the statement *)
let bindpos = ref 1 in
ignore(match id with |None -> () |Some v ->
db_must_ok db (fun () -> Sqlite3.bind stmt !bindpos (Sqlite3.Data.INT v));
incr bindpos
);
ignore(match file with |None -> () |Some v ->
db_must_ok db (fun () -> Sqlite3.bind stmt !bindpos (Sqlite3.Data.TEXT v));
incr bindpos
);
ignore(match line with |None -> () |Some v ->
db_must_ok db (fun () -> Sqlite3.bind stmt !bindpos (Sqlite3.Data.INT v));
incr bindpos
);
ignore(match start with |None -> () |Some v ->
db_must_ok db (fun () -> Sqlite3.bind stmt !bindpos (Sqlite3.Data.INT v));
incr bindpos
);
ignore(match stop with |None -> () |Some v ->
db_must_ok db (fun () -> Sqlite3.bind stmt !bindpos (Sqlite3.Data.INT v));
incr bindpos
);
ignore(match custom_where with |_,[] -> () |_,eb ->
List.iter (fun b ->
db_must_ok db (fun () -> Sqlite3.bind stmt !bindpos b);
incr bindpos
) eb);
(* convert statement into an ocaml object *)
begin
match id with
| None -> ()
| Some v ->
db_must_ok db
(fun () -> Sqlite3.bind stmt !bindpos (Sqlite3.Data.INT v));
incr bindpos
end;
begin
match file with
| None -> ()
| Some v ->
db_must_ok db
(fun () -> Sqlite3.bind stmt !bindpos (Sqlite3.Data.TEXT v));
incr bindpos
end;
begin
match line with
| None -> ()
| Some v ->
db_must_ok db
(fun () -> Sqlite3.bind stmt !bindpos (Sqlite3.Data.INT v));
incr bindpos
end;
begin
match start with
| None -> ()
| Some v ->
db_must_ok db
(fun () -> Sqlite3.bind stmt !bindpos (Sqlite3.Data.INT v));
incr bindpos
end;
begin
match stop with
| None -> ()
| Some v ->
db_must_ok db
(fun () -> Sqlite3.bind stmt !bindpos (Sqlite3.Data.INT v));
incr bindpos
end;
begin
match custom_where with
| _,[] -> ()
| _,eb ->
List.iter
(fun b ->
db_must_ok db (fun () -> Sqlite3.bind stmt !bindpos b);
incr bindpos) eb
end;
(* convert statement into an ocaml object *)
let of_stmt stmt =
t
(* native fields *)
~id:(
?id:(
(match Sqlite3.column stmt 0 with
|Sqlite3.Data.NULL -> None
|x -> Some (match x with |Sqlite3.Data.INT i -> i |x -> (try Int64.of_string (Sqlite3.Data.to_string x) with _ -> failwith "error: loc id")))
......@@ -264,6 +280,7 @@ module Loc = struct
end
(*
module External_proof = struct
type t = <
id : int64 option;
......@@ -929,17 +946,25 @@ module Transf = struct
end
module Init = struct
type t = state
type transaction_mode = [`Exclusive |`Deferred |`Immediate ]
let t ?(busyfn=default_busyfn) ?(mode=`Immediate) db_name =
let db = {db=Sqlite3.db_open db_name; in_transaction=0; mode=mode; busyfn=busyfn } in
Loc.init db;
*)
type handle = state
let create ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
let db = {
db = Sqlite3.db_open db_name;
in_transaction = 0;
mode = mode;
busyfn = busyfn }
in
Loc.init db;
(*
External_proof.init db;
Goal.init db;
Transf.init db;
db
*)
db
let db handle = handle.db
end
let raw db = db.db
src/manager/db.mli
View file @ ff634837
(* autogenerated by sql_orm *)
(** Use the [[Init]] module to open a new database handle. Each object type has its own module with functions to create, modify, save and destroy objects of that type into the SQLite database
*)
module Init : sig
type t
type transaction_mode = [`Exclusive |`Deferred |`Immediate ]
(** Database handle which can be used to create and retrieve objects
*)
val t :
?busyfn:(Sqlite3.db -> unit) -> ?mode:transaction_mode ->
string -> t
(** [t db_name] open a Sqlite3 database with filename [db_name] and create any tables if they are missing. @return a database handle which can be used to create and retrieve objects in the database.
@raise Sql_error if a database error is encountered
*)
val db: t -> Sqlite3.db
(** [db handle] @return the underlying Sqlite3 database handle for the connection, for advanced queries.
*)
end
(** Use the [[Init]] module to open a new database handle. Each
object type has its own module with functions to create, modify, save
and destroy objects of that type into the SQLite database *)
type transaction_mode = | Deferred | Immediate | Exclusive
type handle
(** Database handle which can be used to create and retrieve objects *)
val create :
?busyfn:(Sqlite3.db -> unit) -> ?mode:transaction_mode ->
string -> handle
(** [create db_name] opens a Sqlite3 database with filename
[db_name] and create any tables if they are missing.
@return a
database handle which can be used to create and retrieve objects in
the database. @raise Sql_error if a database error is
encountered *)
val raw: handle -> Sqlite3.db
(** [raw db] @return the underlying Sqlite3 database for the
connection, for advanced queries. *)
module Loc : sig
type t = <
id : int64 option;
set_id : int64 option -> unit;
file : string;
set_file : string -> unit;
line : int64;
set_line : int64 -> unit;
start : int64;
set_start : int64 -> unit;
stop : int64;
set_stop : 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.
*)
type t = {
mutable id : int64 option;
mutable file : string;
mutable line : int64;
mutable start : int64;
mutable stop : int64;
}
(** A record which can be stored in the database with the [save]
function, or removed by calling [delete]. Changes are not
committed to the database until [save] is invoked. *)
val save: t -> int64
val delete: t -> unit
val t :
?id:int64 option ->
?id:int64 ->
file:string ->
line:int64 ->
start:int64 ->
stop: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
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 ->
?file:string option ->
?line:int64 option ->
?start:int64 option ->
?stop:int64 option ->
?custom_where:string * Sqlite3.Data.t list -> Init.t -> t list