db.ml 25.8 KB
Newer Older
MARCHE Claude's avatar
db  
MARCHE Claude committed
1 2
(**************************************************************************)
(*                                                                        *)
3
(*  Copyright (C) 2010-2011                                               *)
4 5 6
(*    François Bobot                                                      *)
(*    Jean-Christophe Filliâtre                                           *)
(*    Claude Marché                                                       *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
7 8 9 10 11 12 13 14 15 16 17 18 19
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software is distributed in the hope that it will be useful,      *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.                  *)
(*                                                                        *)
(**************************************************************************)

20
open Why3
MARCHE Claude's avatar
db  
MARCHE Claude committed
21 22 23 24
open Sqlite3


type transaction_mode = | Deferred | Immediate | Exclusive
MARCHE Claude's avatar
MARCHE Claude committed
25

MARCHE Claude's avatar
db  
MARCHE Claude committed
26 27 28 29 30
type handle = {
  raw_db : Sqlite3.db;
  mutable in_transaction: int;
  busyfn: Sqlite3.db -> unit;
  mode: transaction_mode;
31
  db_name : string;
MARCHE Claude's avatar
db  
MARCHE Claude committed
32 33 34
}

let current_db = ref None
MARCHE Claude's avatar
MARCHE Claude committed
35 36

let current () =
MARCHE Claude's avatar
db  
MARCHE Claude committed
37 38 39 40
  match !current_db with
    | None -> failwith "Db.current: database not yet initialized"
    | Some x -> x

41
let is_initialized () = !current_db <> None
42 43
let db_name () = (current ()).db_name

MARCHE Claude's avatar
MARCHE Claude committed
44

MARCHE Claude's avatar
db  
MARCHE Claude committed
45 46 47 48
let default_busyfn (_db:Sqlite3.db) =
  prerr_endline "Db.default_busyfn WARNING: busy";
  (* Thread.delay (Random.float 1.) *)
  ignore (Unix.select [] [] [] (Random.float 1.))
MARCHE Claude's avatar
MARCHE Claude committed
49

MARCHE Claude's avatar
db  
MARCHE Claude committed
50
let raise_sql_error x = raise (Sqlite3.Error (Rc.to_string x))
MARCHE Claude's avatar
MARCHE Claude committed
51 52


MARCHE Claude's avatar
db  
MARCHE Claude committed
53 54 55
(* retry until a non-BUSY error code is returned *)
let rec db_busy_retry db fn =
  match fn () with
MARCHE Claude's avatar
MARCHE Claude committed
56
    | Rc.BUSY ->
MARCHE Claude's avatar
db  
MARCHE Claude committed
57
        db.busyfn db.raw_db; db_busy_retry db fn
MARCHE Claude's avatar
MARCHE Claude committed
58
    | x ->
MARCHE Claude's avatar
db  
MARCHE Claude committed
59
        x
MARCHE Claude's avatar
MARCHE Claude committed
60

MARCHE Claude's avatar
db  
MARCHE Claude committed
61 62 63 64 65
(* 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
MARCHE Claude's avatar
MARCHE Claude committed
66

MARCHE Claude's avatar
db  
MARCHE Claude committed
67
(* make sure a DONE is returned from the database *)
MARCHE Claude's avatar
MARCHE Claude committed
68
let db_must_done db fn =
MARCHE Claude's avatar
db  
MARCHE Claude committed
69 70 71
  match db_busy_retry db fn with
    | Rc.DONE -> ()
    | x -> raise_sql_error x
MARCHE Claude's avatar
MARCHE Claude committed
72

MARCHE Claude's avatar
db  
MARCHE Claude committed
73 74 75
(* request a transaction *)
let transaction db fn =
  let m = match db.mode with
MARCHE Claude's avatar
MARCHE Claude committed
76 77 78
    | Deferred -> "DEFERRED"
    | Immediate -> "IMMEDIATE"
    | Exclusive -> "EXCLUSIVE"
MARCHE Claude's avatar
db  
MARCHE Claude committed
79
  in
MARCHE Claude's avatar
MARCHE Claude committed
80 81
  try
    db_must_ok db
MARCHE Claude's avatar
db  
MARCHE Claude committed
82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100
      (fun () -> exec db.raw_db ("BEGIN " ^ m ^ " TRANSACTION"));
    assert (db.in_transaction = 0);
    db.in_transaction <- 1;
    let res = fn () in
    db_must_ok db (fun () -> exec db.raw_db "END TRANSACTION");
    assert (db.in_transaction = 1);
    db.in_transaction <- 0;
    res
  with
      e ->
        prerr_string "Db.transaction WARNING: exception: ";
        prerr_endline (Printexc.to_string e);
        prerr_endline "== exception backtrace ==";
        Printexc.print_backtrace stderr;
        prerr_endline "== end of backtrace ==";
        db_must_ok db (fun () -> exec db.raw_db "END TRANSACTION");
        assert (db.in_transaction = 1);
        db.in_transaction <- 0;
        raise e
MARCHE Claude's avatar
MARCHE Claude committed
101 102


MARCHE Claude's avatar
db  
MARCHE Claude committed
103 104 105 106 107 108 109 110 111 112
(* 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 []

113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132
(* iterate over a result set *)
let step_iter db stmt iterfn =
  let stepfn () = Sqlite3.step stmt in
  let rec fn () = match db_busy_retry db stepfn with
    | Sqlite3.Rc.ROW -> iterfn stmt; fn ()
    | Sqlite3.Rc.DONE -> ()
    | x -> raise_sql_error x
  in
  fn ()

(* iterate over a result set *)
let step_fold_gen db stmt iterfn start =
  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 start

MARCHE Claude's avatar
db  
MARCHE Claude committed
133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152
(* DB/SQL helpers *)

let bind db sql l =
  let stmt = Sqlite3.prepare db.raw_db sql in
  let _ =
    List.fold_left
      (fun i v -> db_must_ok db (fun () -> Sqlite3.bind stmt i v); succ i)
      1 l
  in stmt

let stmt_column_INT stmt i msg =
  match Sqlite3.column stmt i with
    | Sqlite3.Data.INT i -> i
    | _ -> failwith msg

let stmt_column_FLOAT stmt i msg =
  match Sqlite3.column stmt i with
    | Sqlite3.Data.FLOAT i -> i
    | _ -> failwith msg

153
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
154 155 156 157
let stmt_column_TEXT stmt i msg =
  match Sqlite3.column stmt i with
    | Sqlite3.Data.TEXT i -> i
    | _ -> failwith msg
MARCHE Claude's avatar
db  
MARCHE Claude committed
158
*)
MARCHE Claude's avatar
db  
MARCHE Claude committed
159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177

let stmt_column_int stmt i msg =
  match Sqlite3.column stmt i with
    | Sqlite3.Data.INT i -> Int64.to_int i
    | _ -> failwith msg

let int64_from_bool b =
  if b then 1L else 0L

let bool_from_int64 i =
  if i=0L then false else
    if i=1L then true else
      failwith "Db.bool_from_int64"

let stmt_column_bool stmt i msg =
  match Sqlite3.column stmt i with
    | Sqlite3.Data.INT i -> bool_from_int64 i
    | _ -> failwith msg

MARCHE Claude's avatar
db  
MARCHE Claude committed
178 179 180 181 182
let stmt_column_string stmt i msg =
  match Sqlite3.column stmt i with
    | Sqlite3.Data.TEXT i -> i
    | _ -> failwith msg

MARCHE Claude's avatar
db  
MARCHE Claude committed
183 184
(** Data *)

MARCHE Claude's avatar
MARCHE Claude committed
185
type prover_id =
MARCHE Claude's avatar
MARCHE Claude committed
186
    { prover_id : int64;
MARCHE Claude's avatar
db  
MARCHE Claude committed
187 188
      prover_name : string;
    }
MARCHE Claude's avatar
MARCHE Claude committed
189

190 191
let prover_name p = p.prover_name

MARCHE Claude's avatar
db  
MARCHE Claude committed
192

MARCHE Claude's avatar
db  
MARCHE Claude committed
193

MARCHE Claude's avatar
db  
MARCHE Claude committed
194 195 196
module Hprover = Hashtbl.Make
  (struct
     type t = prover_id
MARCHE Claude's avatar
MARCHE Claude committed
197 198
     let equal p1 p2 = p1.prover_id = p2.prover_id
     let hash p = Hashtbl.hash p.prover_id
MARCHE Claude's avatar
db  
MARCHE Claude committed
199 200 201
   end)

type transf_id =
MARCHE Claude's avatar
MARCHE Claude committed
202 203
    { transformation_id : int64;
      transformation_name : string;
MARCHE Claude's avatar
db  
MARCHE Claude committed
204 205
    }

MARCHE Claude's avatar
MARCHE Claude committed
206
let transf_name t = t.transformation_name
MARCHE Claude's avatar
db  
MARCHE Claude committed
207 208 209 210

module Htransf = Hashtbl.Make
  (struct
     type t = transf_id
MARCHE Claude's avatar
MARCHE Claude committed
211 212
     let equal t1 t2 = t1.transformation_id = t2.transformation_id
     let hash t = Hashtbl.hash t.transformation_id
MARCHE Claude's avatar
db  
MARCHE Claude committed
213 214 215 216 217 218
   end)




type proof_status =
219 220
  | Undone                      (** external proof attempt not done yet *)
  | Done of Call_provers.prover_answer  (** external proof attempt done *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
221

MARCHE Claude's avatar
MARCHE Claude committed
222 223 224
type proof_attempt = int64
(*
{
MARCHE Claude's avatar
db  
MARCHE Claude committed
225 226
    mutable proof_attempt_id : int;
    mutable prover : prover_id;
MARCHE Claude's avatar
db  
MARCHE Claude committed
227 228
    mutable timelimit : int;
    mutable memlimit : int;
MARCHE Claude's avatar
db  
MARCHE Claude committed
229
    mutable status : proof_status;
MARCHE Claude's avatar
db  
MARCHE Claude committed
230
    mutable result_time : float;
231
    mutable edited_as : string;
MARCHE Claude's avatar
db  
MARCHE Claude committed
232 233
    mutable proof_obsolete : bool;
}
MARCHE Claude's avatar
MARCHE Claude committed
234
*)
MARCHE Claude's avatar
db  
MARCHE Claude committed
235

MARCHE Claude's avatar
MARCHE Claude committed
236
(*
MARCHE Claude's avatar
MARCHE Claude committed
237
let prover _p = assert false (* p.prover *)
MARCHE Claude's avatar
MARCHE Claude committed
238
*)
239
(*
MARCHE Claude's avatar
MARCHE Claude committed
240
let status _p = assert false (* p.status *)
241
*)
MARCHE Claude's avatar
MARCHE Claude committed
242
(*
MARCHE Claude's avatar
MARCHE Claude committed
243
let proof_obsolete _p = assert false (* p.proof_obsolete *)
MARCHE Claude's avatar
MARCHE Claude committed
244
*)
245
(*
MARCHE Claude's avatar
MARCHE Claude committed
246
let time _p = assert false (* p.result_time *)
247
*)
MARCHE Claude's avatar
MARCHE Claude committed
248
let edited_as _p = assert false (* p.edited_as *)
MARCHE Claude's avatar
db  
MARCHE Claude committed
249

250
type transf = int64
MARCHE Claude's avatar
MARCHE Claude committed
251 252
and goal = int64

MARCHE Claude's avatar
db  
MARCHE Claude committed
253

MARCHE Claude's avatar
db  
MARCHE Claude committed
254

MARCHE Claude's avatar
MARCHE Claude committed
255
type theory = int64
MARCHE Claude's avatar
MARCHE Claude committed
256 257


MARCHE Claude's avatar
MARCHE Claude committed
258
type file = int64
MARCHE Claude's avatar
db  
MARCHE Claude committed
259

MARCHE Claude's avatar
MARCHE Claude committed
260
(*
MARCHE Claude's avatar
MARCHE Claude committed
261
let file_name _ = assert false
MARCHE Claude's avatar
MARCHE Claude committed
262
*)
MARCHE Claude's avatar
MARCHE Claude committed
263

MARCHE Claude's avatar
db  
MARCHE Claude committed
264 265 266 267



module ProverId = struct
MARCHE Claude's avatar
db  
MARCHE Claude committed
268 269

  let init db =
MARCHE Claude's avatar
MARCHE Claude committed
270
    let sql =
MARCHE Claude's avatar
db  
MARCHE Claude committed
271
      "CREATE TABLE IF NOT EXISTS prover \
MARCHE Claude's avatar
MARCHE Claude committed
272
       (prover_id INTEGER PRIMARY KEY AUTOINCREMENT,prover_name TEXT);"
MARCHE Claude's avatar
db  
MARCHE Claude committed
273 274
    in
    db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql);
MARCHE Claude's avatar
MARCHE Claude committed
275
    let sql =
MARCHE Claude's avatar
db  
MARCHE Claude committed
276
      "CREATE UNIQUE INDEX IF NOT EXISTS prover_name_idx \
MARCHE Claude's avatar
MARCHE Claude committed
277
       ON prover (prover_name)"
MARCHE Claude's avatar
db  
MARCHE Claude committed
278 279 280 281 282 283 284 285 286 287 288 289 290
    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
*)

MARCHE Claude's avatar
MARCHE Claude committed
291 292
  let add db name =
    transaction db
MARCHE Claude's avatar
db  
MARCHE Claude committed
293 294 295 296 297
      (fun () ->
         let sql = "INSERT INTO prover 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
MARCHE Claude's avatar
MARCHE Claude committed
298
         { prover_id = new_id ;
299
           prover_name = name }
MARCHE Claude's avatar
MARCHE Claude committed
300
      )
MARCHE Claude's avatar
db  
MARCHE Claude committed
301

302
  let from_name db name =
MARCHE Claude's avatar
db  
MARCHE Claude committed
303
    let sql =
304
      "SELECT prover.prover_id FROM prover \
MARCHE Claude's avatar
MARCHE Claude committed
305
       WHERE prover.prover_name=?"
MARCHE Claude's avatar
db  
MARCHE Claude committed
306 307 308 309
    in
    let stmt = bind db sql [Sqlite3.Data.TEXT name] in
    (* convert statement into record *)
    let of_stmt stmt =
MARCHE Claude's avatar
MARCHE Claude committed
310
      { prover_id = stmt_column_INT stmt 0 "ProverId.get: bad prover id";
311
        prover_name = name;
MARCHE Claude's avatar
db  
MARCHE Claude committed
312
      }
MARCHE Claude's avatar
MARCHE Claude committed
313
    in
MARCHE Claude's avatar
db  
MARCHE Claude committed
314 315 316 317 318 319 320 321
    (* 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 =
322
      "SELECT prover.prover_name FROM prover \
MARCHE Claude's avatar
MARCHE Claude committed
323
       WHERE prover.prover_id=?"
MARCHE Claude's avatar
db  
MARCHE Claude committed
324 325 326 327
    in
    let stmt = bind db sql [Sqlite3.Data.INT id] in
    (* convert statement into record *)
    let of_stmt stmt =
328
      { prover_id = id ;
329
        prover_name = stmt_column_string stmt 0
MARCHE Claude's avatar
db  
MARCHE Claude committed
330
          "ProverId.from_id: bad prover_name";
MARCHE Claude's avatar
db  
MARCHE Claude committed
331
      }
MARCHE Claude's avatar
MARCHE Claude committed
332
    in
MARCHE Claude's avatar
db  
MARCHE Claude committed
333 334 335 336 337 338 339 340 341 342
    (* 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

343
let prover_from_id id =
MARCHE Claude's avatar
db  
MARCHE Claude committed
344 345 346 347 348
  try
    Hashtbl.find prover_memo id
  with Not_found ->
    let p =
      let db = current () in
MARCHE Claude's avatar
db  
MARCHE Claude committed
349
      try ProverId.from_id db id
MARCHE Claude's avatar
db  
MARCHE Claude committed
350 351 352 353 354
      with Not_found -> assert false
    in
    Hashtbl.add prover_memo id p;
    p

355

MARCHE Claude's avatar
MARCHE Claude committed
356
let prover_from_name n =
357
  let db = current () in
MARCHE Claude's avatar
MARCHE Claude committed
358
  try ProverId.from_name db n
359 360 361 362
  with Not_found -> ProverId.add db n


(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
363 364 365 366 367 368 369
let prover e = get_prover_from_id e.prover

let get_prover name (* ~short ~long ~command ~driver *) =
  let db = current () in
(*
  let checksum = Digest.file driver in
*)
MARCHE Claude's avatar
db  
MARCHE Claude committed
370
  try ProverId.get db name (* ~short ~long ~command ~checksum *)
MARCHE Claude's avatar
MARCHE Claude committed
371
  with Not_found ->
MARCHE Claude's avatar
db  
MARCHE Claude committed
372
    ProverId.add db name (* ~short ~long ~command ~checksum *)
MARCHE Claude's avatar
MARCHE Claude committed
373

MARCHE Claude's avatar
db  
MARCHE Claude committed
374
*)
MARCHE Claude's avatar
MARCHE Claude committed
375

MARCHE Claude's avatar
db  
MARCHE Claude committed
376

MARCHE Claude's avatar
MARCHE Claude committed
377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408
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 ;
409
           transformation_name = name }
MARCHE Claude's avatar
MARCHE Claude committed
410 411 412 413 414 415 416 417 418 419 420
      )

  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";
421
        transformation_name = name;
MARCHE Claude's avatar
MARCHE Claude committed
422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438
      }
    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 ;
439
        transformation_name = stmt_column_string stmt 0
MARCHE Claude's avatar
MARCHE Claude committed
440 441 442 443 444 445 446 447 448 449 450
          "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

MARCHE Claude's avatar
MARCHE Claude committed
451
let transf_memo = Hashtbl.create 7
MARCHE Claude's avatar
MARCHE Claude committed
452

MARCHE Claude's avatar
MARCHE Claude committed
453
let transf_from_id id =
MARCHE Claude's avatar
MARCHE Claude committed
454
  try
MARCHE Claude's avatar
MARCHE Claude committed
455
    Hashtbl.find transf_memo id
MARCHE Claude's avatar
MARCHE Claude committed
456
  with Not_found ->
MARCHE Claude's avatar
MARCHE Claude committed
457
    let t =
MARCHE Claude's avatar
MARCHE Claude committed
458 459 460 461
      let db = current () in
      try TransfId.from_id db id
      with Not_found -> assert false
    in
MARCHE Claude's avatar
MARCHE Claude committed
462 463
    Hashtbl.add transf_memo id t;
    t
MARCHE Claude's avatar
MARCHE Claude committed
464 465 466 467 468 469 470

let transf_from_name n =
  let db = current () in
  try TransfId.from_name db n
  with Not_found -> TransfId.add db n


MARCHE Claude's avatar
db  
MARCHE Claude committed
471
let int64_from_status = function
472 473 474 475 476 477 478
  | Undone                        -> 0L
  | Done Call_provers.Valid       -> 1L
  | Done Call_provers.Timeout     -> 2L
  | Done (Call_provers.Unknown _) -> 3L
  | Done (Call_provers.Failure _) -> 4L
  | Done Call_provers.Invalid     -> 5L
  | Done Call_provers.HighFailure -> 6L
479

480 481 482 483 484 485 486 487
let status_array = [|
  Undone;
  Done Call_provers.Valid;
  Done Call_provers.Timeout;
  Done (Call_provers.Unknown "");
  Done (Call_provers.Failure "");
  Done Call_provers.Invalid;
  Done Call_provers.HighFailure; |]
MARCHE Claude's avatar
db  
MARCHE Claude committed
488

MARCHE Claude's avatar
MARCHE Claude committed
489
let status_from_int64 i =
MARCHE Claude's avatar
MARCHE Claude committed
490 491 492
  try
    status_array.(Int64.to_int i)
  with _ -> failwith "Db.status_from_int64"
MARCHE Claude's avatar
db  
MARCHE Claude committed
493 494 495 496

module External_proof = struct

  let init db =
MARCHE Claude's avatar
MARCHE Claude committed
497
    let sql =
MARCHE Claude's avatar
MARCHE Claude committed
498
      (* timelimit INTEGER, memlimit INTEGER,
MARCHE Claude's avatar
MARCHE Claude committed
499
         *)
500 501 502
      "CREATE TABLE IF NOT EXISTS external_proofs \
       (external_proof_id INTEGER PRIMARY KEY AUTOINCREMENT,\
        goal_id INTEGER,\
MARCHE Claude's avatar
MARCHE Claude committed
503 504
        prover_id INTEGER, \
        status INTEGER,\
MARCHE Claude's avatar
MARCHE Claude committed
505
        obsolete INTEGER,\
MARCHE Claude's avatar
MARCHE Claude committed
506 507
        time REAL,\
        edited_as TEXT);"
MARCHE Claude's avatar
db  
MARCHE Claude committed
508 509 510 511
    in
    db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)

  let delete db e =
512
    let sql = "DELETE FROM external_proofs WHERE external_proof_id=?" in
MARCHE Claude's avatar
MARCHE Claude committed
513 514
    let stmt = bind db sql [ Sqlite3.Data.INT e ] in
    ignore(step_fold db stmt (fun _ -> ()))
MARCHE Claude's avatar
db  
MARCHE Claude committed
515

MARCHE Claude's avatar
MARCHE Claude committed
516 517
  let add db (g : goal) (p: prover_id) =
    transaction db
MARCHE Claude's avatar
db  
MARCHE Claude committed
518
      (fun () ->
519 520
         let sql = "INSERT INTO external_proofs VALUES(NULL,?,?,0,0,0.0,\"\")" in
         let stmt = bind db sql [
MARCHE Claude's avatar
MARCHE Claude committed
521
           Sqlite3.Data.INT g;
MARCHE Claude's avatar
MARCHE Claude committed
522
           Sqlite3.Data.INT p.prover_id;
MARCHE Claude's avatar
MARCHE Claude committed
523
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
524 525
           Sqlite3.Data.INT (Int64.of_int e.timelimit);
           Sqlite3.Data.INT (Int64.of_int e.memlimit);
MARCHE Claude's avatar
MARCHE Claude committed
526 527
*)
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
528
           Sqlite3.Data.INT (int64_from_status e.status);
MARCHE Claude's avatar
MARCHE Claude committed
529
           Sqlite3.Data.INT (int64_from_bool e.proof_obsolete);
MARCHE Claude's avatar
db  
MARCHE Claude committed
530
           Sqlite3.Data.FLOAT e.result_time;
MARCHE Claude's avatar
MARCHE Claude committed
531 532
*)
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
533
           Sqlite3.Data.TEXT e.trace;
MARCHE Claude's avatar
MARCHE Claude committed
534
*)
MARCHE Claude's avatar
db  
MARCHE Claude committed
535 536
         ]
         in
537 538
         db_must_done db (fun () -> Sqlite3.step stmt);
         Sqlite3.last_insert_rowid db.raw_db)
MARCHE Claude's avatar
db  
MARCHE Claude committed
539

MARCHE Claude's avatar
MARCHE Claude committed
540
  let set_status db e stat time =
MARCHE Claude's avatar
MARCHE Claude committed
541
    transaction db
542
      (fun () ->
543 544 545 546
         let sql =
           "UPDATE external_proofs SET status=?,obsolete=0,time=? WHERE external_proof_id=?"
         in
         let stmt = bind db sql [
547 548 549 550 551
           Sqlite3.Data.INT (int64_from_status stat);
           Sqlite3.Data.FLOAT time;
           Sqlite3.Data.INT e;
         ]
         in
552
         db_must_done db (fun () -> Sqlite3.step stmt))
553

MARCHE Claude's avatar
MARCHE Claude committed
554 555 556
  let set_obsolete db e =
    transaction db
      (fun () ->
557 558 559 560
         let sql =
           "UPDATE external_proofs SET obsolete=1 WHERE external_proof_id=?"
         in
         let stmt = bind db sql [
MARCHE Claude's avatar
MARCHE Claude committed
561 562 563
           Sqlite3.Data.INT e;
         ]
         in
564
         db_must_done db (fun () -> Sqlite3.step stmt))
MARCHE Claude's avatar
MARCHE Claude committed
565

MARCHE Claude's avatar
MARCHE Claude committed
566 567 568
  let set_edited_as db e f =
    transaction db
      (fun () ->
569 570 571 572
         let sql =
           "UPDATE external_proofs SET edited_as=? WHERE external_proof_id=?"
         in
         let stmt = bind db sql [
MARCHE Claude's avatar
MARCHE Claude committed
573 574 575 576
           Sqlite3.Data.TEXT f;
           Sqlite3.Data.INT e;
         ]
         in
577
         db_must_done db (fun () -> Sqlite3.step stmt))
MARCHE Claude's avatar
MARCHE Claude committed
578

579 580 581 582 583 584
  let of_goal db g =
    let sql="SELECT prover_id,external_proof_id FROM external_proofs \
       WHERE external_proofs.goal_id=?"
    in
    let stmt = bind db sql [Sqlite3.Data.INT g] in
    let res = Hprover.create 7 in
MARCHE Claude's avatar
MARCHE Claude committed
585
    let of_stmt stmt =
586 587 588 589 590 591
      let pid = stmt_column_INT stmt 0 "External_proof.of_goal" in
      let a = stmt_column_INT stmt 1 "External_proof.of_goal" in
      Hprover.add res (prover_from_id pid) a
    in
    step_iter db stmt of_stmt;
    res
MARCHE Claude's avatar
MARCHE Claude committed
592

593
  let status_and_time db p =
MARCHE Claude's avatar
MARCHE Claude committed
594
    let sql="SELECT status,time,obsolete,edited_as FROM external_proofs \
595 596 597
       WHERE external_proofs.external_proof_id=?"
    in
    let stmt = bind db sql [Sqlite3.Data.INT p] in
MARCHE Claude's avatar
MARCHE Claude committed
598
    let of_stmt stmt =
599 600
      let status = stmt_column_INT stmt 0 "External_proof.status_and_time" in
      let t = stmt_column_FLOAT stmt 1 "External_proof.status_and_time" in
MARCHE Claude's avatar
MARCHE Claude committed
601
      let o = stmt_column_bool stmt 2 "External_proof.status_and_time" in
MARCHE Claude's avatar
MARCHE Claude committed
602 603
      let e = stmt_column_string stmt 3 "External_proof.status_and_time" in
      (status_from_int64 status, t, o, e)
604 605 606 607 608 609
    in
    match step_fold db stmt of_stmt with
      | [] -> raise Not_found
      | [x] -> x
      | _ -> assert false

MARCHE Claude's avatar
MARCHE Claude committed
610

MARCHE Claude's avatar
db  
MARCHE Claude committed
611 612
end

613
let status_and_time p = External_proof.status_and_time (current()) p
MARCHE Claude's avatar
db  
MARCHE Claude committed
614

615
let external_proofs g = External_proof.of_goal (current()) g
MARCHE Claude's avatar
db  
MARCHE Claude committed
616

MARCHE Claude's avatar
MARCHE Claude committed
617 618
let remove_proof_attempt e = External_proof.delete (current()) e

MARCHE Claude's avatar
db  
MARCHE Claude committed
619
module Goal = struct
MARCHE Claude's avatar
MARCHE Claude committed
620

MARCHE Claude's avatar
db  
MARCHE Claude committed
621
  let init db =
MARCHE Claude's avatar
MARCHE Claude committed
622
    let sql =
MARCHE Claude's avatar
MARCHE Claude committed
623 624
      "CREATE TABLE IF NOT EXISTS goals \
       (goal_id INTEGER PRIMARY KEY AUTOINCREMENT, \
625 626
        goal_theory INTEGER,\
        goal_transf INTEGER,\
MARCHE Claude's avatar
MARCHE Claude committed
627
        goal_name TEXT, task_checksum TEXT, proved INTEGER);"
628 629
        (* goal_transf is 0 for root goals
           goal_theory is 0 for subgoals *)
MARCHE Claude's avatar
MARCHE Claude committed
630 631
    in
    db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql);
MARCHE Claude's avatar
MARCHE Claude committed
632
(*
MARCHE Claude's avatar
MARCHE Claude committed
633
    let sql =
MARCHE Claude's avatar
MARCHE Claude committed
634
      "CREATE UNIQUE INDEX IF NOT EXISTS goal_theory_idx \
MARCHE Claude's avatar
MARCHE Claude committed
635
       ON goals (goal_theory)"
MARCHE Claude's avatar
MARCHE Claude committed
636 637 638
    in
    db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql);
*)
MARCHE Claude's avatar
MARCHE Claude committed
639
(*
MARCHE Claude's avatar
db  
MARCHE Claude committed
640 641 642 643 644
    let sql = "create table if not exists map_external_proofs_goal_external_proof (goal_id integer, external_proof_id integer, primary key(goal_id, external_proof_id));" in
    db_must_ok db (fun () -> Sqlite3.exec db.db sql);
    let sql = "create table if not exists map_transformations_goal_transf (goal_id integer, transf_id integer, primary key(goal_id, transf_id));" in
    db_must_ok db (fun () -> Sqlite3.exec db.db sql);
*)
MARCHE Claude's avatar
MARCHE Claude committed
645
    ()
MARCHE Claude's avatar
MARCHE Claude committed
646 647 648

  let add db (th:theory) (name : string) (sum:string) =
    transaction db
MARCHE Claude's avatar
db  
MARCHE Claude committed
649
      (fun () ->
650 651 652 653
         let sql =
           "INSERT INTO goals VALUES(NULL,?,0,?,?,0)"
         in
         let stmt = bind db sql [
MARCHE Claude's avatar
MARCHE Claude committed
654
           Sqlite3.Data.INT th;
MARCHE Claude's avatar
MARCHE Claude committed
655 656
           Sqlite3.Data.TEXT name;
           Sqlite3.Data.TEXT sum;
MARCHE Claude's avatar
db  
MARCHE Claude committed
657 658
         ]
         in
659 660
         db_must_done db (fun () -> Sqlite3.step stmt);
         Sqlite3.last_insert_rowid db.raw_db)
MARCHE Claude's avatar
db  
MARCHE Claude committed
661

662 663 664
  let add_as_subgoal db (tr:transf) (name : string) (sum:string) =
    transaction db
      (fun () ->
665 666 667 668
         let sql =
           "INSERT INTO goals VALUES(NULL,0,?,?,?,0)"
         in
         let stmt = bind db sql [
669 670 671 672 673
           Sqlite3.Data.INT tr;
           Sqlite3.Data.TEXT name;
           Sqlite3.Data.TEXT sum;
         ]
         in
674 675
         db_must_done db (fun () -> Sqlite3.step stmt);
         Sqlite3.last_insert_rowid db.raw_db)
676

MARCHE Claude's avatar
MARCHE Claude committed
677 678 679 680 681 682
  let delete db e =
    let sql = "DELETE FROM goals WHERE goal_id=?" in
    let stmt = bind db sql [ Sqlite3.Data.INT e ] in
    ignore(step_fold db stmt (fun _ -> ()))


MARCHE Claude's avatar
MARCHE Claude committed
683 684 685
  let set_task_checksum db g s =
    transaction db
      (fun () ->
686 687 688 689
         let sql =
           "UPDATE goals SET task_checksum=? WHERE goal_id=?"
         in
         let stmt = bind db sql [
MARCHE Claude's avatar
MARCHE Claude committed
690 691 692 693
           Sqlite3.Data.TEXT s;
           Sqlite3.Data.INT g;
         ]
         in
694
         db_must_done db (fun () -> Sqlite3.step stmt))
MARCHE Claude's avatar
MARCHE Claude committed
695 696


MARCHE Claude's avatar
MARCHE Claude committed
697 698 699 700 701
  let name db g =
    let sql="SELECT goal_name FROM goals \
       WHERE goals.goal_id=?"
    in
    let stmt = bind db sql [Sqlite3.Data.INT g] in
MARCHE Claude's avatar
MARCHE Claude committed
702
    let of_stmt stmt =
MARCHE Claude's avatar
MARCHE Claude committed
703 704 705 706 707 708 709
      (stmt_column_string stmt 0 "Goal.name")
    in
    match step_fold db stmt of_stmt with
      | [] -> raise Not_found
      | [x] -> x
      | _ -> assert false

MARCHE Claude's avatar
MARCHE Claude committed
710 711 712 713
  let task_checksum db g =
    let sql="SELECT task_checksum FROM goals WHERE goals.goal_id=?"
    in
    let stmt = bind db sql [Sqlite3.Data.INT g] in
MARCHE Claude's avatar
MARCHE Claude committed
714
    let of_stmt stmt =
MARCHE Claude's avatar
MARCHE Claude committed
715 716 717 718 719 720 721
      (stmt_column_string stmt 0 "Goal.task_checksum")
    in
    match step_fold db stmt of_stmt with
      | [] -> raise Not_found
      | [x] -> x
      | _ -> assert false

MARCHE Claude's avatar
MARCHE Claude committed
722
  let of_theory db th =
MARCHE Claude's avatar
MARCHE Claude committed
723 724 725 726
    let sql="SELECT goal_id,goal_name FROM goals \
       WHERE goals.goal_theory=?"
    in
    let stmt = bind db sql [Sqlite3.Data.INT th] in
727
    step_fold_gen db stmt
MARCHE Claude's avatar
MARCHE Claude committed
728 729 730 731 732
      (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
MARCHE Claude's avatar
MARCHE Claude committed
733

734
  let of_transf db tr =
MARCHE Claude's avatar
MARCHE Claude committed
735
    let sql="SELECT goal_id,task_checksum FROM goals \
736
       WHERE goals.goal_transf=?"
MARCHE Claude's avatar
db  
MARCHE Claude committed
737
    in
738
    let stmt = bind db sql [Sqlite3.Data.INT tr] in
739
    step_fold_gen db stmt
740 741
      (fun stmt acc ->
         let g = stmt_column_INT stmt 0 "Goal.of_transf" in
MARCHE Claude's avatar
MARCHE Claude committed
742 743
         let sum = stmt_column_string stmt 1 "Goal.of_transf" in
         Util.Mstr.add sum g acc)
744
      Util.Mstr.empty
MARCHE Claude's avatar
db  
MARCHE Claude committed
745 746 747

end

MARCHE Claude's avatar
MARCHE Claude committed
748
let goal_name g = Goal.name (current()) g
MARCHE Claude's avatar
MARCHE Claude committed
749
let task_checksum g = Goal.task_checksum (current()) g
MARCHE Claude's avatar
MARCHE Claude committed
750
let change_checksum g s = Goal.set_task_checksum (current()) g s
MARCHE Claude's avatar
MARCHE Claude committed
751 752 753

let goals th = Goal.of_theory (current()) th

754
let subgoals tr = Goal.of_transf (current()) tr
MARCHE Claude's avatar
MARCHE Claude committed
755

MARCHE Claude's avatar
MARCHE Claude committed
756 757
let remove_subgoal g = Goal.delete (current()) g

MARCHE Claude's avatar
MARCHE Claude committed
758

MARCHE Claude's avatar
db  
MARCHE Claude committed
759 760 761



MARCHE Claude's avatar
db  
MARCHE Claude committed
762 763


764 765 766 767
(* {transformations} *)



MARCHE Claude's avatar
db  
MARCHE Claude committed
768

MARCHE Claude's avatar
db  
MARCHE Claude committed
769 770 771 772
module Transf = struct


  let init db =
773 774 775 776 777
    let sql =
      "CREATE TABLE IF NOT EXISTS transformations \
       (transf_id INTEGER PRIMARY KEY AUTOINCREMENT, \
        transf_id_id INTEGER,\
        parent_goal INTEGER);"
MARCHE Claude's avatar
MARCHE Claude committed
778
    in
779
    db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)
MARCHE Claude's avatar
db  
MARCHE Claude committed
780

781
  let add db root_goal tr_id =
782 783
    transaction db
      (fun () ->
784 785 786 787
         let sql =
           "INSERT INTO transformations VALUES(NULL,?,?)"
         in
         let stmt = bind db sql [
788 789 790 791
           Sqlite3.Data.INT tr_id.transformation_id;
           Sqlite3.Data.INT root_goal;
         ]
         in
792 793
         db_must_done db (fun () -> Sqlite3.step stmt);
         Sqlite3.last_insert_rowid db.raw_db)
MARCHE Claude's avatar
db  
MARCHE Claude committed
794

MARCHE Claude's avatar
MARCHE Claude committed
795 796 797 798 799
  let delete db t =
    let sql = "DELETE FROM transformations WHERE transf_id=?" in
    let stmt = bind db sql [ Sqlite3.Data.INT t ] in
    ignore(step_fold db stmt (fun _ -> ()))

MARCHE Claude's avatar
MARCHE Claude committed
800 801 802 803 804 805 806 807 808 809 810 811 812
  let of_goal db g =
    let sql="SELECT transf_id,transf_id_id FROM transformations \
       WHERE transformations.parent_goal=?"
    in
    let stmt = bind db sql [Sqlite3.Data.INT g] in
    let res = Htransf.create 7 in
    let of_stmt stmt =
      let t = stmt_column_INT stmt 0 "Transf.of_goal" in
      let tid = stmt_column_INT stmt 1 "Transf.of_goal" in
      Htransf.add res (transf_from_id tid) t
    in
    step_iter db stmt of_stmt;
    res
MARCHE Claude's avatar
db  
MARCHE Claude committed
813

MARCHE Claude's avatar
db  
MARCHE Claude committed
814

MARCHE Claude's avatar
MARCHE Claude committed
815 816 817
end

let transformations g = Transf.of_goal (current()) g
MARCHE Claude's avatar
db  
MARCHE Claude committed
818

MARCHE Claude's avatar
MARCHE Claude committed
819 820
let remove_transformation t = Transf.delete (current()) t

MARCHE Claude's avatar
MARCHE Claude committed
821
module Theory = struct
MARCHE Claude's avatar
db  
MARCHE Claude committed
822 823

  let init db =
MARCHE Claude's avatar
MARCHE Claude committed
824
    let sql =
MARCHE Claude's avatar
MARCHE Claude committed
825 826 827
      "CREATE TABLE IF NOT EXISTS theories \
       (theory_id INTEGER PRIMARY KEY AUTOINCREMENT,\
        theory_file INTEGER, theory_name TEXT);" in
MARCHE Claude's avatar
db  
MARCHE Claude committed
828 829 830
    db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql);
    ()

MARCHE Claude's avatar
MARCHE Claude committed
831 832 833 834 835
  let name db th =
    let sql="SELECT theory_name FROM theories \
       WHERE theories.theory_id=?"
    in
    let stmt = bind db sql [Sqlite3.Data.INT th] in
MARCHE Claude's avatar
MARCHE Claude committed
836
    let of_stmt stmt =
MARCHE Claude's avatar
MARCHE Claude committed
837 838 839 840 841 842 843 844
      (stmt_column_string stmt 0 "Theory.name")
    in
    match step_fold db stmt of_stmt with
      | [] -> raise Not_found
      | [x] -> x
      | _ -> assert false

  let of_file db f =
845
    let sql="SELECT theory_name,theory_id FROM theories \
MARCHE Claude's avatar
MARCHE Claude committed
846 847 848
       WHERE theories.theory_file=?"
    in
    let stmt = bind db sql [Sqlite3.Data.INT f] in
849 850 851 852 853 854
    step_fold_gen db stmt
      (fun stmt acc ->
         let name = stmt_column_string stmt 0 "Theory.of_file" in
         let th = stmt_column_INT stmt 1 "Theory.of_file" in
         Util.Mstr.add name th acc)
      Util.Mstr.empty
MARCHE Claude's avatar
MARCHE Claude committed
855

MARCHE Claude's avatar
MARCHE Claude committed
856 857
  let add db file name =
    transaction db
MARCHE Claude's avatar
MARCHE Claude committed
858
      (fun () ->
MARCHE Claude's avatar
MARCHE Claude committed
859
         let sql = "INSERT INTO theories VALUES(NULL,?,?)" in
MARCHE Claude's avatar
MARCHE Claude committed
860
         let stmt = bind db sql
MARCHE Claude's avatar
MARCHE Claude committed
861 862 863 864
           [ Sqlite3.Data.INT file;
             Sqlite3.Data.TEXT name;
           ]
         in
MARCHE Claude's avatar
MARCHE Claude committed
865 866
         db_must_done db (fun () -> Sqlite3.step stmt);
         let new_id = Sqlite3.last_insert_rowid db.raw_db in
867
         new_id)
MARCHE Claude's avatar
MARCHE Claude committed
868 869
end

MARCHE Claude's avatar
MARCHE Claude committed
870 871 872 873
let theory_name th = Theory.name (current()) th

let theories f = Theory.of_file (current()) f

MARCHE Claude's avatar
MARCHE Claude committed
874 875 876 877
module Main = struct

  let init db =
    let sql = "CREATE TABLE IF NOT EXISTS files \
MARCHE Claude's avatar
MARCHE Claude committed
878
          (file_id INTEGER PRIMARY KEY AUTOINCREMENT,file_name TEXT);"
MARCHE Claude's avatar
MARCHE Claude committed
879 880 881
    in
    db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)

MARCHE Claude's avatar
d  
MARCHE Claude committed
882
  let all_files db =
MARCHE Claude's avatar
MARCHE Claude committed
883
    let sql="SELECT file_id,file_name FROM files" in
MARCHE Claude's avatar
db  
MARCHE Claude committed
884
    let stmt = Sqlite3.prepare db.raw_db sql in
MARCHE Claude's avatar
MARCHE Claude committed
885
    let of_stmt stmt =
MARCHE Claude's avatar
MARCHE Claude committed
886 887 888
      (stmt_column_INT stmt 0 "Db.all_files",
       stmt_column_string stmt 1 "Db.all_files")
    in
MARCHE Claude's avatar
MARCHE Claude committed
889
    step_fold db stmt of_stmt
MARCHE Claude's avatar
db  
MARCHE Claude committed
890

MARCHE Claude's avatar
MARCHE Claude committed
891 892
  let add db name =
    transaction db
MARCHE Claude's avatar
d  
MARCHE Claude committed
893
      (fun () ->
MARCHE Claude's avatar
MARCHE Claude committed
894
         let sql = "INSERT INTO files VALUES(NULL,?)" in
MARCHE Claude's avatar
d  
MARCHE Claude committed
895 896 897
         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
898
         new_id)
MARCHE Claude's avatar
db  
MARCHE Claude committed
899 900
end

MARCHE Claude's avatar
db  
MARCHE Claude committed
901

MARCHE Claude's avatar
db  
MARCHE Claude committed
902 903 904 905
let init_db ?(busyfn=default_busyfn) ?(mode=Immediate) db_name =
  match !current_db with
    | None ->
        let db = {
906 907 908 909
          raw_db = Sqlite3.db_open db_name;
          in_transaction = 0;
          mode = mode;
          busyfn = busyfn;
910
          db_name = db_name;
MARCHE Claude's avatar
MARCHE Claude committed
911
        }
912 913 914 915 916 917
        in
        current_db := Some db;
        ProverId.init db;
        TransfId.init db;
        External_proof.init db;
        Goal.init db;
918
        Transf.init db;
919 920
        Theory.init db;
        Main.init db
MARCHE Claude's avatar
db  
MARCHE Claude committed
921 922 923

    | Some _ -> failwith "Db.init_db: already opened"

MARCHE Claude's avatar
d  
MARCHE Claude committed
924

925
let init_base f = init_db ~mode:Deferred f
MARCHE Claude's avatar
db  
MARCHE Claude committed
926

MARCHE Claude's avatar
MARCHE Claude committed
927
let files () = List.rev (Main.all_files (current()))
MARCHE Claude's avatar
d  
MARCHE Claude committed
928

MARCHE Claude's avatar
MARCHE Claude committed
929
exception AlreadyExist
MARCHE Claude's avatar
MARCHE Claude committed
930

MARCHE Claude's avatar
MARCHE Claude committed
931
let add_proof_attempt g pid = External_proof.add (current()) g pid
MARCHE Claude's avatar
MARCHE Claude committed
932

MARCHE Claude's avatar
MARCHE Claude committed
933
let set_status a r t =
MARCHE Claude's avatar
MARCHE Claude committed
934
  External_proof.set_status (current()) a r t
MARCHE Claude's avatar
MARCHE Claude committed
935

936 937
let set_obsolete a =
  External_proof.set_obsolete (current()) a
MARCHE Claude's avatar
MARCHE Claude committed
938

939
let set_edited_as a f =
MARCHE Claude's avatar
MARCHE Claude committed
940
  External_proof.set_edited_as (current()) a f
941 942 943

let add_transformation g tr_id = Transf.add (current()) g tr_id

MARCHE Claude's avatar
MARCHE Claude committed
944 945
let add_goal th id sum = Goal.add (current()) th id sum

946 947
let add_subgoal tr id sum = Goal.add_as_subgoal (current()) tr id sum

MARCHE Claude's avatar
MARCHE Claude committed
948
let add_theory f th = Theory.add (current()) f th
MARCHE Claude's avatar
d  
MARCHE Claude committed
949 950

let add_file f = Main.add (current()) f
MARCHE Claude's avatar
db  
MARCHE Claude committed
951 952 953


(*
MARCHE Claude's avatar
MARCHE Claude committed
954
Local Variables:
955
compile-command: "unset LANG; make -C ../.. bin/why3ide.byte"
MARCHE Claude's avatar
MARCHE Claude committed
956
End:
MARCHE Claude's avatar
db  
MARCHE Claude committed
957
*)