more db

Makefile.in

@@ -464,7 +464,7 @@ clean::
 APIDOCSRC = $(UTIL_CMO:.cmo=.mli) $(CORE_CMO:.cmo=.mli) \
 	src/driver/call_provers.mli \
 	src/driver/driver.mli \
-	src/manager/state.mli
+	src/manager/db.mli
 
 .PHONY: apidoc
 
@@ -472,7 +472,7 @@ apidoc: $(APIDOCSRC)
 	rm -f apidoc/* 
 	mkdir -p apidoc
 	$(OCAMLDOC) -d apidoc -html -I src/util -I src/core -I src/driver \
-		$(APIDOCSRC)
+			-I +sqlite3 $(APIDOCSRC)
 
 
 # special rules

src/manager/db.ml

@@ -82,24 +82,30 @@ let step_fold db stmt iterfn =
   fn []
 
 
-module Loc = struct
+(** Data *)
 
-  type t = {
-    mutable id : int64 option;
-    mutable file : string;
-    mutable line : int64;
-    mutable start : int64;
-    mutable stop : int64;
-  }
+type db_ident = int64 
+
+type loc_record = 
+    { mutable id : db_ident option;
+      (** when None, the record has never been stored in database yet *)
+      mutable file : string;
+      mutable line : int;
+      mutable start : int;
+      mutable stop : int;
+    }
+
+
+module Loc = struct
 
   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
     db_must_ok db (fun () -> Sqlite3.exec db.raw_db sql)
 
   (* object definition *)
-  let create ?id ~file ~line ~start ~stop : t = 
+  let create (* ?id *) ~file ~line ~start ~stop : loc_record = 
     { 
-      id = id;
+      id = None (* id *);
       file = file;
       line = line;
       start = start;
@@ -131,13 +137,13 @@ module Loc = struct
                     (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));
+                    (let v = Int64.of_int 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));
+                    (let v = Int64.of_int 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));
+                    (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;
@@ -153,13 +159,13 @@ module Loc = struct
                     (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));
+                    (let v = Int64.of_int 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));
+                    (let v = Int64.of_int 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));
+                    (let v = Int64.of_int 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);
@@ -244,36 +250,36 @@ module Loc = struct
     end;
   (* convert statement into an ocaml object *)
     let of_stmt stmt =
-      create
-	(* native fields *)
-	?id:(match Sqlite3.column stmt 0 with
+      { (* native fields *)
+	id = (match Sqlite3.column stmt 0 with
                | Sqlite3.Data.NULL -> None
                | Sqlite3.Data.INT i -> Some i 
 	       | x -> 
 		   try Some (Int64.of_string (Sqlite3.Data.to_string x))
-		   with _ -> failwith "error: loc id")
-	~file:(match Sqlite3.column stmt 1 with
+		   with _ -> failwith "error: loc id") ;
+	file = (match Sqlite3.column stmt 1 with
 		 | Sqlite3.Data.NULL -> failwith "null of_stmt"
-		 | x -> Sqlite3.Data.to_string x)
-	~line:(match Sqlite3.column stmt 2 with
+		 | x -> Sqlite3.Data.to_string x) ;
+	line = (match Sqlite3.column stmt 2 with
 		 | Sqlite3.Data.NULL -> failwith "null of_stmt"
-		 | Sqlite3.Data.INT i -> i 
+		 | Sqlite3.Data.INT i -> Int64.to_int i 
 		 | x -> 
-		     try Int64.of_string (Sqlite3.Data.to_string x) 
-		     with _ -> failwith "error: loc line")
-	~start:(match Sqlite3.column stmt 3 with
+		     try int_of_string (Sqlite3.Data.to_string x) 
+		     with _ -> failwith "error: loc line") ;
+	start = (match Sqlite3.column stmt 3 with
 		  | Sqlite3.Data.NULL -> failwith "null of_stmt"
-		  | Sqlite3.Data.INT i -> i 
+		  | Sqlite3.Data.INT i -> Int64.to_int i 
 		  | x -> 
-		      try Int64.of_string (Sqlite3.Data.to_string x) 
-		      with _ -> failwith "error: loc start")
-	~stop:(match Sqlite3.column stmt 4 with
+		      try int_of_string (Sqlite3.Data.to_string x) 
+		      with _ -> failwith "error: loc start") ;
+	stop = (match Sqlite3.column stmt 4 with
 		 | Sqlite3.Data.NULL -> failwith "null of_stmt"
-		 | Sqlite3.Data.INT i -> i 
+		 | Sqlite3.Data.INT i -> Int64.to_int i 
 		 | x -> 
-		     try Int64.of_string (Sqlite3.Data.to_string x) 
+		     try int_of_string (Sqlite3.Data.to_string x) 
 		     with _ -> failwith "error: loc stop")
 	(* foreign fields *)
+      }
     in 
     (* execute the SQL query *)
     step_fold db stmt of_stmt
@@ -516,12 +522,20 @@ 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.t;
+  mutable pos : loc_record;
   mutable external_proofs : External_proof.t list;
   mutable transformations : transf list;
   mutable proved : int64;

src/manager/db.mli

 
 
-type transaction_mode = | Deferred | Immediate | Exclusive
+(** {1 Proof manager database} *)
+
+(** {2 The persistent database} *)
 
 type handle
   (** Database handle which can be used to create and retrieve objects *)
 
+type transaction_mode = | Deferred | Immediate | Exclusive
+
 val create :
   ?busyfn:(Sqlite3.db -> unit) -> ?mode:transaction_mode ->
   string -> handle
@@ -21,34 +25,50 @@ val raw: handle -> Sqlite3.db
       connection, for advanced queries.  *)
 *)
 
-module Loc : sig
 
-  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.  *)
+(** {2 data} *)
 
-  val save: handle -> t -> int64 
+(** 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.  *)
 
-  val delete: handle -> t -> unit
+type db_ident (* = int64 *)
+(** hidden type for record unique identifiers *)
 
+type loc_record = private
+    { mutable id : db_ident option;
+      (** when None, the record has never been stored in database yet *)
+      mutable file : string;
+      mutable line : int;
+      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 ->
+ (*   ?id:int64 -> *)
     file:string ->
-    line:int64 ->
-    start:int64 ->
-    stop:int64 ->
-    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
-    *)
+    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 ->
@@ -56,13 +76,25 @@ module Loc : sig
     ?line:int64 ->
     ?start:int64 ->
     ?stop:int64 ->
-    ?custom_where:string * Sqlite3.Data.t list -> handle -> t list
+    ?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 =
+  | 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 *)
+
+
 (*
 module External_proof : sig
   type t = <
@@ -203,3 +235,5 @@ module Transf : sig
 
 end
 *)
+
+

theories/real.why

@@ -258,6 +258,11 @@ theory Trigonometry
 
   logic pi : real
 
+  axiom Pi_interval:
+   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038196
+   < pi <
+   3.14159265358979323846264338327950288419716939937510582097494459230781640628620899862803482534211706798214808651328230664709384460955058223172535940812848111745028410270193852110555964462294895493038197
+
   axiom Cos_pi: cos(pi) = -1.0
   axiom Sin_pi: sin(pi) = 0.0