helm/ocaml/tactics/statefulProofEngine.mli

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 (** Stateful handling of proof status *)
  27
  28 exception No_goal_left
  29 exception Uri_redefinition
  30
  31   (** can't undo/redo one or more actions *)
  32 exception History_failure
  33
  34 type event = [ `Proof_changed | `Proof_completed ]
  35
  36   (** Proof observer. First callback argument is Some extended_status
  37   * when a 'real 'change of the proof happened and None when Proof_changed event
  38   * was triggered by a time travel by the means of undo/redo actions. Embedded
  39   * status is the status _before_ the current change. Second status is the
  40   * status reached _after_ the current change. *)
  41 type 'a observer =
  42   (ProofEngineTypes.status * 'a) option -> (ProofEngineTypes.status * 'a) ->
  43     unit
  44
  45   (** needed to detach previously attached observers *)
  46 type observer_id
  47
  48   (** tactic application failed. @see apply_tactic *)
  49 exception Tactic_failure of exn
  50
  51   (** one or more observers failed. @see apply_tactic *)
  52 exception Observer_failures of (observer_id * exn) list
  53
  54   (** failure while updating internal data (: 'a). @see apply_tactic *)
  55 exception Data_failure of exn
  56
  57 (** {2 OO interface} *)
  58
  59 class ['a] status:
  60   ?uri:UriManager.uri ->
  61   typ:Cic.term -> ?body:Cic.term -> ?metasenv:Cic.metasenv ->
  62   (ProofEngineTypes.proof * ProofEngineTypes.goal option -> 'a) ->
  63   (ProofEngineTypes.status * 'a -> ProofEngineTypes.status -> 'a) ->
  64   unit ->
  65   object
  66
  67     method proof: ProofEngineTypes.proof
  68     method metasenv: Cic.metasenv
  69     method body: Cic.term
  70     method typ: Cic.term
  71
  72     (** goal -> conjecture
  73     * @raise CicUtil.Meta_not_found *)
  74     method conjecture: int -> Cic.conjecture
  75
  76     method proof_completed: bool
  77     method goal: int              (** @raise No_goal_left *)
  78     method set_goal: int -> unit  (** @raise No_goal_left *)
  79
  80     method uri: UriManager.uri option
  81     method set_uri: UriManager.uri -> unit  (** @raise Uri_redefinition *)
  82
  83     (** @raise Tactic_failure
  84     * @raise Observer_failures
  85     * @raise Data_failure
  86     *
  87     * In case of tactic failure, internal status is left unchanged.
  88     * In case of observer failures internal status will be changed and is
  89     * granted that all observer will be invoked collecting their failures.
  90     * In case of data failure, internal status is left unchanged (rolling back
  91     * last tactic application if needed)
  92     *)
  93     method apply_tactic: ProofEngineTypes.tactic -> unit
  94
  95     method undo: ?steps:int -> unit -> unit
  96     method redo: ?steps:int -> unit -> unit
  97
  98     method attach_observer:
  99       ?interested_in:(event list) -> 'a observer -> observer_id
 100
 101     method detach_observer: observer_id -> unit
 102
 103   end
 104
 105 val trivial_status:
 106   ?uri:UriManager.uri ->
 107   typ:Cic.term -> ?body:Cic.term -> ?metasenv:Cic.metasenv ->
 108   unit ->
 109     unit status
 110