better theory for array with length

Makefile.in

@@ -387,7 +387,7 @@ IDEMLI = $(addsuffix .mli, $(IDEMODULES))
 IDECMO = $(addsuffix .cmo, $(IDEMODULES))
 IDECMX = $(addsuffix .cmx, $(IDEMODULES))
 
-$(IDECMO) $(IDECMX): INCLUDES += -I src/ide
+$(IDECMO) $(IDECMX): INCLUDES += -I src/ide -I +sqlite3
 
 # build targets
 
@@ -712,11 +712,12 @@ clean::
 MODULESTODOC = core/ident core/ty core/term core/decl core/theory \
 	core/env core/task \
 	driver/whyconf driver/driver \
-	transform/introduction
+	transform/introduction \
+	ide/db
 
 FILESTODOC = $(addsuffix .mli, $(addprefix src/, $(MODULESTODOC)))
 
-apidoc:
+apidoc: $(FILESTODOC)
 	mkdir -p apidoc
 	$(OCAMLDOC) -d apidoc -html -keep-code $(INCLUDES) \
 		$(LIBINCLUDES) $(FILESTODOC)

src/ide/db.ml

@@ -38,7 +38,6 @@ let current () =
     | Some x -> x
 
 	      
-
 let default_busyfn (_db:Sqlite3.db) =
   prerr_endline "Db.default_busyfn WARNING: busy";
   (* Thread.delay (Random.float 1.) *)
@@ -46,36 +45,13 @@ let default_busyfn (_db:Sqlite3.db) =
   
 let raise_sql_error x = raise (Sqlite3.Error (Rc.to_string x))
   
-(*
-let try_finally fn finalfn =
-  try
-    let r = fn () in
-    finalfn ();
-    r
-  with e -> begin
-    prerr_string "Db.try_finally WARNING: exception: ";
-    prerr_endline (Printexc.to_string e);
-    prerr_endline "== exception backtrace ==";
-    Printexc.print_backtrace stderr;
-    prerr_endline "== end of backtrace ==";
-    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 -> 
-(*
-        prerr_endline "Db.db_busy_retry: BUSY";
-*)
         db.busyfn db.raw_db; db_busy_retry db fn
     | x -> 
-(*
-        prerr_string "Db.db_busy_retry: ";
-        prerr_endline (Rc.to_string x);
-*)
         x
        
 (* make sure an OK is returned from the database *)
@@ -177,104 +153,54 @@ let stmt_column_bool stmt i msg =
 
 type db_ident = int64 
 
-type loc_record = 
-    { mutable loc_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;
-    }
-
-
 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 *)
-
-let string_of_status = function
-  | Scheduled -> "Scheduled"
-  | Running -> "Running"
-  | Success -> "Success"
-  | Timeout -> "Timeout"
-  | Unknown -> "Unknown"
-  | HighFailure -> "HighFailure"
-
-let print_status fmt s = Format.fprintf fmt "%s" (string_of_status s)
+  | Failure (** external prover call failed *)
 
 type prover =
     { prover_id : db_ident;
       prover_name : string;
-(*
-      prover_short : string;
-      prover_long : string;
-      prover_command : string;
-      prover_driver_checksum : string;
-*)
     }
 
-let prover_name p = p.prover_name
+let prover_id p = p.prover_name
 
-type external_proof = {
+type proof_attempt = {
     mutable external_proof_id : db_ident;
     mutable prover : db_ident;
     mutable timelimit : int;
     mutable memlimit : int;
     mutable status : proof_attempt_status;
     mutable result_time : float;
-    mutable trace : string;
+    mutable edited_as : string;
     mutable proof_obsolete : bool;
 }
 
-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
+let prover p = p.prover
+let status p = p.status
+let proof_obsolete p = p.proof_obsolete
+let time p = p.result_time
+let edited_as p = p.edited_as
 
-type goal_origin =
-  | Goal of string * string
-(*
-  | VCfun of loc * explain * ...
-  | Subgoal of goal
-*)
-
-type transf_data =
-    { transf_name : string;
-      transf_action : Task.task Trans.tlist
+type transf =
+    { mutable transf_id : db_ident;
+      mutable transf_name : string;
+      mutable transf_subgoals : goal list;
     }
 
-
-type goal = {
+and goal = {
   mutable goal_id : db_ident;
-  mutable goal_origin : goal_origin;
-  mutable task : Task.task;
   mutable task_checksum: string;
   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 external_proofs : external_proof list;
-  mutable transformations : transf list;
-*)
-}
-
-and transf = {
-    mutable transf_id : db_ident;
-    mutable transf_data : transf_data;
-    mutable transf_obsolete : bool;
-    mutable subgoals : goal list;
+  mutable external_proofs : (int, proof_attempt) Hashtbl.t;
+  mutable transformations : (int, transf) Hashtbl.t;
 }
 
+val task_checksum : goal -> string (** checksum *)
+val proved : goal -> bool
+val external_proofs: (string, proof_attempt) Hashtbl.t
+val transformations : (string, transf) Hashtbl.t
 
 let goal_task g = g.task
 let goal_task_checksum g = g.task_checksum

src/ide/db.mli

@@ -19,12 +19,27 @@
 
 (** Proof database *)
 
-(** {1 data types} *)
+(** {2 data types} *)
 
-(** prover info *)
-type prover
+type file
+(** a database contains a (ordered?) set of files *)
 
-val prover_from_id : string -> prover
+type theory
+(** each files contains an ordered sequence of theories *)
+
+type goal
+(** each theory contains an ordered sequences of goals *)
+
+type proof_attempt 
+(** each goal has a set of proof attempts, indeed a map indexed
+    by provers *)
+
+type transf
+(** each goal also has a set of transformations, indeed a map indexed
+    by transformation names *)
+
+type prover
+(** a prover *)
 
 (** status of an external proof attempt *)
 type proof_status =
@@ -33,33 +48,42 @@ type proof_status =
   | Unknown (** external prover answered ``don't know'' or equivalent *)
   | Failure (** external prover call failed *)
 
-type proof_attempt 
-type goal
-type transf
-type theory
-type file
+(** parent of a goal: either a theory (for "toplevel" goals) 
+    or a transformation (for "subgoals") *)
+(* useful ?
 type goal_parent =
   | Theory of theory
   | Transf of transf
+*)
+
+(** {2 accessors} *)
+
+(** prover accessors *)
+val prover_id : prover -> string
 
 (** proof_attempt accessors *)
 val prover : proof_attempt -> prover
+(*
 val proof_goal : proof_attempt -> goal
+*)
 val status : proof_attempt -> proof_status
 val proof_obsolete : proof_attempt -> bool
 val time : proof_attempt -> float
 val edited_as : proof_attempt -> string
 
-
 (** goal accessors *)
+(*
 val parent : goal -> goal_parent
-val task : goal -> string (* checksum *)
+*)
+val task_checksum : goal -> string (** checksum *)
 val proved : goal -> bool
 val external_proofs: (string, proof_attempt) Hashtbl.t
 val transformations : (string, transf) Hashtbl.t
 
 (** transf accessors *)
+(*
 val parent_goal : transf -> goal
+*)
 val transf_name : transf -> string
 val subgoals : transf -> goal list
 
@@ -72,7 +96,7 @@ val verified : theory -> bool
 val file_name : file -> string
 val theories : file -> theory list
 
-(** {1 The persistent database} *)
+(** {2 The persistent database} *)
 
 val init_base : string -> unit
 (** opens or creates the current database, from given file name *)
@@ -81,8 +105,74 @@ val files : unit -> file list
 (** returns the current set of files *)
 
 
+(** {2 Updates} *)
+
+exception AlreadyExist
+
+(** {3 provers} *)
+val prover_from_id : string -> prover
+(** retrieves existing prover data from its name.
+    creates prover data if not existing yet *)
+
+(** {3 external proof attempts} *)
+
+val add_proof_attempt : goal -> prover -> proof_attempt
+(** adds a proof attempt for this prover, with status is set to Unknown.
+    @raise AlreadyExist if an attempt for the same prover
+    is already there *)
+
+(* todo: remove_proof_attempt *)
+
+val set_status : proof_attempt -> proof_status -> float -> unit
+(** sets the proof status for this prover, and its time.
+*)
+
+val set_obsolete : proof_attempt -> unit
+(** marks this proof as obsolete *)
+
+val set_edited_as : proof_attempt -> string -> unit
+(** sets the file name where this proof can be edited *)
+
+(** {3 transformations} *)
+
+val add_transformation : goal -> string -> goal list -> transf
+(** adds a transformation for this goal, with the given subgoals
+    @raise AlreadyExist if a transformation with the same name
+    is already there *)
+
+(* todo: remove_transformation *)
+
+(** {3 goals} *)
+
+val add_goal : theory -> string -> string -> goal
+(** [add_goal th id sum] adds to theory [th] a new goal named [id], with
+    [sum] as the checksum of its task. 
+    @raise AlreadyExist if a goal with the same id already exists
+    in this theory *)
+
+(* todo: remove_goal *)
+
+(** {3 theories} *)
+
+val add_theory : file -> string -> string -> unit
+(** [add_goal th id sum] adds to theory [th] a new goal named [id], with
+    [sum] as the checksum of its task.
+    @raise AlreadyExist if a goal with the same id already exists
+    in this theory *)
+
+(* todo: remove_theory *)
+
+
+(** {3 files} *)
+
+val add_file :  string -> file
+(** adds a file to the database.
+    @raise AlreadyExist if a file with the same id already exists *)
+
+(* todo: remove_file *)
+
+
 
-(** {1 Updates} *)
 
 
   

src/ide/gmain.ml

@@ -461,7 +461,7 @@ let rec prover_on_goal p g =
     with Not_found ->
       (* creating a new row *)
       let name = p.prover_name in
-      let prover_row = goals_model#append ~parent:row () 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);

theories/array.why

 
-theory Array
+theory Array (* "Theory of arrays" *)
 
   type t 'a 'b
 
@@ -22,28 +22,43 @@ theory Array
 
 end
 
-theory ArrayLength
+theory ArrayLength (* "Theory of arrays with length" *)
+
+(* these arrays
+
+  use import int.Int
 
   use export Array
 
   logic length (t int 'a) : int
 
+  axiom Length_non_negative (* "Array length is always non negative" *):
+    forall a : t int 'a. length a >= 0
+
   axiom Length_set : 
     forall a : t int 'a. forall k : int. forall v : 'a.
     length (set a k v) = length a
 
   logic create_const_length 'a int : t int 'a
+    (* [create_const_length x n] is the array of length n
+       with all cells initialized to x 
+       (not specified if n is negative)
+    *)     
 
   axiom Create_const_length_get : 
     forall b:'a. forall n i:int. get (create_const_length b n) i = b
 
   axiom Create_const_length_length : 
-    forall a : 'a. forall n : int. length (create_const_length a n) = n
+    forall a : 'a. forall n : int. 
+      (* premise needed to guaranty length >= 0 invariant *)
+       n >= 0 -> length (create_const_length a n) = n
 
   logic create_length int : t int 'a
 
   axiom Create_length_length : 
-    forall n : int. length (create_length n : t int 'a) = n
+    forall n : int. 
+      (* premise needed to guaranty length >= 0 invariant *)
+      n >=0 -> length (create_length n : t int 'a) = n
 
 end