API doc

Makefile.in

@@ -89,7 +89,7 @@ BINARYL=bin/whyl.$(OCAMLBEST)
 
 TOOLS=bin/why-cpulimit
 
-all: .depend $(BINARY) $(BINARYL) $(TOOLS)
+all: .depend $(BINARY) $(BINARYL) $(TOOLS) apidoc
 
 # refrain parallel make (-j nn) from starting ocaml compilation too early 
 *.cm*: .depend
@@ -407,16 +407,21 @@ doc/main.html: doc/main.tex doc/version.tex
 	make -C doc main.html
 
 
-# API HTML DOC
+# API DOC
 ##############
 
-OCAMLDOCSRC = intf/model.mli $(WHYCONFIGCMO:.cmo=.ml) $(WHYCONFIGCMI:.cmi=.mli)
-	# $(JCCMO:.cmo=.ml) $(JCCMI:.cmi=.mli) 
+APIDOCSRC = $(UTIL_CMO:.cmo=.mli) $(CORE_CMO:.cmo=.mli) \
+	src/driver/call_provers.mli \
+	src/driver/driver.mli \
+	manager/db.mli
 
-apidoc: $(OCAMLDOCSRC)
-	mkdir -p ocamldoc
-	rm -f ocamldoc/* 
-	$(OCAMLDOC) -d ocamldoc -html $(INCLUDES) @INCLUDEGTK2@ $(OCAMLDOCSRC)
+.PHONY: apidoc
+
+apidoc: $(APIDOCSRC)
+	rm -f apidoc/* 
+	mkdir -p apidoc
+	$(OCAMLDOC) -d apidoc -html -I src/util -I src/core -I src/driver \
+		$(APIDOCSRC)
 
 
 # special rules

manager/db.mli

@@ -2,9 +2,39 @@
 
 (** {1 Proof manager database} *)
 
-(** {2 proof goals in a proof project} *)
 
-type goal
+(** {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 *)
+
+(** a proof attempt by some external provers *)
+type external_proof =
+  { prover : Driver.driver; (** prover driver *)
+    timelimit : int; (** CPU limit given in seconds *)
+    status : proof_attempt_status; (** the current state *)
+    result_time : float ; (** CPU time for that run *)
+    trace : string; 
+      (** any kind of trace returned by the prover.
+          when redoing the same attempt, the former trace is sent again *)
+    obsolete : bool;
+      (** when true, goal as changed after that proof attempt *)
+  } 
+
+type transf = Task.task Register.tlist_reg
+
+(** an proof attempt is either an external proof or a transformation 
+    into subtasks *)
+type attempt =
+  | External of external_proof
+  | Transf of transf
+
+(** {2 proof goals in a proof project} *)
 
 type theory_lemma_identifier
 
@@ -14,82 +44,85 @@ type explain
 
 type identifier
 
-type origin =
+type goal_origin =
   | Lemma of theory_lemma_identifier
   | VCfun of loc * explain * identifier
   | Subgoal of goal
 
-val origin : goal -> origin
+and goal =
+    {
+      origin : goal_origin;
+      attempts : attempt list;
+      proved : bool;
+      (** invariant: g.proved == true iff
+             exists attempts a in g.attempts, 
+      (a = External e and e.result == Valid and a.obsolete == false) or
+      (a = Transf(gl) and forall g in gl, g.proved
+      *)
+      observers: (bool -> unit) list;
+      (** observers that wants to be notified by any changes of the proved status *)
+    }
 
-type proof_result = Valid | Timeout | Failed  
 
-type prover_id
+(** {2 database for a proof project} *)
 
-type proof_attempt =
-  { proved_id : prover_id;
-      (* prover identifier *)
-    timelimit : int;
-      (* CPU limit in seconds *)
-    obsolete : bool;
-      (* when true, goal as changed after that proof attempt *)
-    result : proof_result;
-    result_time : float ;
-      (* CPU time for the prover run *)
-    trace : string 
-      (* any kind of trace for the prover. For an interactive prover, 
-	 gives the file name for the current proof script *)
-  } 
+type proof_db
 
-type tactic =
-  | Attempt of proof_attempt
-  | Split of goal * goal
+val get_goals : proof_db -> goal list
 
-val tactics : goal -> tactic list
+val get_subtask : proof_db -> string -> proof_db list
 
-val proved : goal -> bool
-(** proved(g) == true iff
-   exists tactic t in tactics(g), 
-      (t = Attempt a and a.result == Valid and a.obsolete == false) or
-      (t = Split(g1,g2)) and proved(g1) and proved(g2)
-*)
+(** {2 attempts to solve goals} *)
 
+exception AlreadyAttempted
 
-(** {2 database for a proof project} *)
+val try_prover : goal -> Driver.driver -> timelimit:int -> proof_db -> unit
+  (** attempts to prove goal with the given prover. This function adds
+      a new corresponding attempt for that goal, sets its current
+      status to Running, launches the prover in a separate process and
+      returns immediately.
 
-type proof_db
+      Upon termination of the external process, the prover's answer is
+      retrieved and database is updated. The [proved] field of the
+      goal is updated, and also these of any goal affected, according
+      to invariant above. Goal observers are notified of any change
+      of goal statuses.
 
-val get_goals : proof_db -> goal list
+      @param timelimit CPU time limit given for that attempt
 
-val get_subtask : proof_db -> string -> proof_db list
+      @raise AlreadyAttempted if there already exists an external proof
+      attempt with the same driver and time limit, or with a different
+      time limit and a result different from Timeout
 
-(** {2 add a proof attempt} *)
 
+  *)
 
-exception AlreadyAttempted
+val add_transformation: goal -> transf -> proof_db -> unit
+  (** adds a transformation on the goal. This function adds a new
+      corresponding attempt for that goal, computes the subgoals and
+      and them in the database. In the case where no subgoal is
+      genereated, the [proved] field is updated, and those of parent
+      goals.
+
+      @raise AlreadyAttempted if this transformation has already been attempted
 
-val try_prover : proof_db -> goal -> prover_id -> timelimit:int -> unit
-(** (try_prover db g p t) attempts to prove goal g with prover p within time limit t
+  *)
 
-    if their already exist a proof attempt with the same prover and time limit, 
-    and with a different time limit and a result different from Timeout, then raise
-    AlreadyAttempted. Otherwise, runs the prover, and updates the database accordingly to its
-    result. (do not return until the result is obtained ???) 
 
-    Note: the invariant above is maintained, that is proved status are updated for any goal
-    that depend on this result
+(** TODO: removal of attempts *)
 
-*)
+(* {2 goal updates} *)
 
-(** {2 Update goals in a project} *)
+val add_or_replace_goal: proof_db -> goal -> unit 
+  (** updates the database with the new goal.  If a goal with the same
+      origin already exists, it is checked whether the task to
+      prove is different or not. If it is the same, proof attempts are
+      preserved. If not the same, former proof attempts are marked as
+      obsolete.
+  *)
 
-val goal_update: proof_db -> goal -> unit 
-(** updates the database with the new goal. If a goal with the same origin already exists, it is checked
-whether the formula to prove is different or not. If it is the same, proof attempts are preserved. If not the same,
-former proof attempts are marked as obsolete. 
-*)
+(** TODO: full update, removing goals that are not pertinetn anymore *)
 
-val mark_all_as_obsolete : proof_db -> goal -> unit
-(** mark all goals as obsolete *)
 
   
 

src/driver/driver.mli

@@ -17,19 +17,26 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Drivers for calling external provers *)
+
 open Format
 open Ident
 open Task
 open Trans
 open Env
 
-(** creating drivers *)
+(** {2 creating drivers} *)
 
 type driver
 
+
 val load_driver : string -> env -> driver
+(** loads a driver from a file
+    @param string driver file name 
+    @param env TODO
+*)
 
-(** querying drivers *)
+(** {2 querying drivers} *)
 
 type translation =
   | Remove
@@ -38,9 +45,11 @@ type translation =
 
 val syntax_arguments : string -> (formatter -> 'a -> unit) -> 
   formatter -> 'a list -> unit
-  (* syntax_argument templ print_arg fmt l print in the formatter fmt
+  (** (syntax_argument templ print_arg fmt l) prints in the formatter fmt
      the list l using the template templ and the printer print_arg *)
-  (** registering printers *)
+
+
+(** {2 registering printers} *)
 
 type printer = (ident -> translation) -> formatter -> task -> unit
 
@@ -52,19 +61,18 @@ val register_transform_l : string -> task Register.tlist_reg  -> unit
 val list_printers   : unit -> string list
 val list_transforms : unit -> string list
 
-(** using drivers *)
+(** {2 using drivers} *)
 
-(** transform task *)
 val apply_transforms : driver -> task -> task list
+(** transform task *)
 
-(** print_task *)
 val print_task : driver -> formatter -> task -> unit
+(** print a task *)
 
 val filename_of_goal : driver -> string -> string -> task -> string
-(* filename_of_goal filename theory_name ctxt *)
+(** filename_of_goal filename theory_name ctxt *)
 
-type prover_answer =
-    Call_provers.prover_answer =
+type prover_answer = Call_provers.prover_answer =
   | Valid
   | Invalid
   | Unknown of string
@@ -72,14 +80,16 @@ type prover_answer =
   | Timeout
   | HighFailure
 
-val call_prover :
-  ?debug:bool -> (* if on print on stderr the commandline
-                    and the output of the prover *)
-  ?timeout:int -> (* specify the time limit given to the prover,
-                     if not set unlimited time *)
-  driver ->       (* the driver to use *)
-  task ->      (* the task to prove with a goal as the last declaration *)
+val call_prover : ?debug:bool -> ?timeout:int -> driver -> task -> 
   Call_provers.prover_result
+(** calls a prover on a given task
+    @param debug if on, prints on stderr the command line and the output of the prover 
+    @param timeout specifies the CPU time limit given to the prover,
+                     if not set: unlimited time
+    @param driver the driver to use
+    @param task the task to prove with a goal as the last declaration
+    @return the prover's answer
+  *)
 
 val call_prover_on_file :
   ?debug:bool ->
@@ -96,7 +106,7 @@ val call_prover_on_formatter :
   (formatter -> unit) ->
   Call_provers.prover_result
 
-(* error reporting *)
+(** {2 error reporting} *)
 
 type error