* http://helm.cs.unibo.it/
*)
-val proofStatus:
- typ:Cic.term -> ?metasenv:Cic.metasenv -> ?uri:UriManager.uri -> unit ->
- MatitaTypes.proofStatus
-
- (** inverse function of proofStatus#toString / proofStatus#toOutchan *)
-val proofStatus_of_string: string -> MatitaTypes.proofStatus
-
+ (** 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:
- typ:Cic.term -> ?metasenv:Cic.metasenv -> ?uri:UriManager.uri -> unit ->
+ ?uri:UriManager.uri ->
+ metasenv:Cic.metasenv -> typ:Cic.term ->
+ unit ->
MatitaTypes.proof
-(** {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 ->
- MatitaTypes.proofStatus -> MatitaTypes.command
-
-val reflexivity: MatitaTypes.proofStatus -> MatitaTypes.command
-val symmetry: MatitaTypes.proofStatus -> MatitaTypes.command
-val transitivity: Cic.term -> MatitaTypes.proofStatus -> MatitaTypes.command
-
-val exists: MatitaTypes.proofStatus -> MatitaTypes.command
-val split: MatitaTypes.proofStatus -> MatitaTypes.command
-val left: MatitaTypes.proofStatus -> MatitaTypes.command
-val right: MatitaTypes.proofStatus -> MatitaTypes.command
-
-val assumption: MatitaTypes.proofStatus -> MatitaTypes.command
+ (** current proof handler *)
+class type currentProof =
+ object
+ 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
+
+val currentProof: unit -> currentProof
+
+ (** currentProof singleton instance *)
+val instance: unit -> currentProof