snapshot, notably:

[helm.git] / helm / matita / matitaProof.mli

diff --git a/helm/matita/matitaProof.mli b/helm/matita/matitaProof.mli
index e9df2c1406a61ca647351858237278cda625778e..9ed6221917d215277b6783435b788bb4ebeb51b9 100644 (file)
--- a/helm/matita/matitaProof.mli
+++ b/helm/matita/matitaProof.mli
@@ -23,52 +23,37 @@
  * http://helm.cs.unibo.it/
  *)
 
-class proofStatus: uri:UriManager.uri -> typ:Cic.term ->
+  (** create a new proof object. Typecheck the resulting sequent.
+    * @param typ goal type
+    * @param metasenv metasenv returned by the disambiguator, this will not be
+    * the final metasenv of the first sequence, meta corresponding to typ will
+    * be added
+    * @param uri new proof uri *)
+val proof:
+  ?uri:UriManager.uri ->
+  metasenv:Cic.metasenv -> typ:Cic.term ->
+  unit ->
+    MatitaTypes.proof
+
+  (** current proof handler *)
+class type currentProof =
   object
-    inherit MatitaTypes.subject
-
-      (** {3 properties} *)
-
-    method proof: ProofEngineTypes.proof
-    method setProof: ProofEngineTypes.proof -> unit
-
-    method goal: ProofEngineTypes.goal option
-    method setGoal: ProofEngineTypes.goal option -> unit
-
-      (** @raise MatitaTypes.No_proof *)
-    method status: ProofEngineTypes.status (* proof, goal *)
-    method setStatus: ProofEngineTypes.status -> unit
-
-      (** {3 actions} *)
-
-    (** return a pair of "xml" (as defined in Xml module) representing the *
-     * current proof type and body, respectively *)
-    method to_xml: Xml.token Stream.t * Xml.token Stream.t
+    inherit MatitaTypes.currentProof
+    
+      (** add an observer to the current observer list. All observers will be
+      * attached to each new proof (method "start") created by this object
+      *)
+    method addObserver: unit StatefulProofEngine.observer -> unit
+
+      (** connect as the first event handler for a given event (abort or quit).
+      * If the event handler returns true, handler processing stops, otherwise
+      * continue with the next handler
+      *)
+    method connect: [`Abort|`Quit] -> (unit -> bool) -> unit
   end
 
-class proof: uri:UriManager.uri -> typ:Cic.term ->
-  object
-      (** {3 status} *)
-    method status: proofStatus
-    method setStatus: proofStatus -> unit
-  end
-
-(** {2 tactic commands builders} *)
-
-(* TODO Zack: these are just some examples, a lot of other tactics/tacticals
- * must be added here *)
-
-val intros: ?namer:MatitaTypes.namer ->
-                  proofStatus -> MatitaTypes.command
-
-val reflexivity:  proofStatus -> MatitaTypes.command
-val symmetry:     proofStatus -> MatitaTypes.command
-val transitivity: Cic.term -> proofStatus -> MatitaTypes.command
-
-val exists:       proofStatus -> MatitaTypes.command
-val split:        proofStatus -> MatitaTypes.command
-val left:         proofStatus -> MatitaTypes.command
-val right:        proofStatus -> MatitaTypes.command
+val currentProof: unit -> currentProof
 
-val assumption:   proofStatus -> MatitaTypes.command
+  (** currentProof singleton instance *)
+val instance: unit -> currentProof