* 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 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 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 assumption: proofStatus -> MatitaTypes.command
-