]> matita.cs.unibo.it Git - helm.git/blob - components/tactics/statefulProofEngine.mli
unified: some theorems on Lift started
[helm.git] / components / 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 type event = [ `Proof_changed | `Proof_completed ]
32
33 val all_events: event list
34
35   (** from our point of view a status is the status of an incomplete proof, thus
36   * we have an optional goal which is None if the proof is not yet completed
37   * (i.e. some goal is still open) *)
38 type proof_status = ProofEngineTypes.proof * ProofEngineTypes.goal option
39
40   (** Proof observer. First callback argument is Some extended_status
41   * when a 'real 'change of the proof happened and None when Proof_changed event
42   * was triggered by a time travel by the means of undo/redo actions or by an
43   * external "#notify" invocation. Embedded status is the status _before_ the
44   * current change. Second status is the status reached _after_ the current
45   * change. *)
46 type 'a observer = (proof_status * 'a) option -> (proof_status * 'a) -> unit
47
48   (** needed to detach previously attached observers *)
49 type observer_id
50
51   (** tactic application failed. @see apply_tactic *)
52 exception Tactic_failure of exn
53
54   (** one or more observers failed. @see apply_tactic *)
55 exception Observer_failures of (observer_id * exn) list
56
57   (** failure while updating internal data (: 'a). @see apply_tactic *)
58 exception Data_failure of exn
59
60 (** {2 OO interface} *)
61
62 class ['a] status:
63   ?history_size:int ->  (** default 20 *)
64   ?uri:UriManager.uri ->
65   typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv ->
66   attrs:Cic.attribute list ->
67   (proof_status -> 'a) -> (* init data *)
68   (proof_status * 'a -> proof_status -> 'a) ->  (* update data *)
69   unit ->
70   object
71
72     method proof: ProofEngineTypes.proof
73     method metasenv: Cic.metasenv
74     method body: Cic.term
75     method typ: Cic.term
76     method attrs: Cic.attribute list
77
78     (** change metasenv _without_ triggering any notification *)
79     method set_metasenv: Cic.metasenv -> unit
80
81     (** goal -> conjecture
82     * @raise CicUtil.Meta_not_found *)
83     method conjecture: int -> Cic.conjecture
84
85     method proof_completed: bool
86     method goal: int              (** @raise No_goal_left *)
87     method set_goal: int -> unit  (** @raise Data_failure *)
88
89     method uri: UriManager.uri option
90     method set_uri: UriManager.uri -> unit  (** @raise Uri_redefinition *)
91
92     (** @raise Tactic_failure
93     * @raise Observer_failures
94     * @raise Data_failure
95     *
96     * In case of tactic failure, internal status is left unchanged.
97     * In case of observer failures internal status will be changed and is
98     * granted that all observer will be invoked collecting their failures.
99     * In case of data failure, internal status is left unchanged (rolling back
100     * last tactic application if needed)
101     *)
102     method apply_tactic: ProofEngineTypes.tactic -> unit
103
104     method undo: ?steps:int -> unit -> unit
105     method redo: ?steps:int -> unit -> unit
106
107     method attach_observer:
108       ?interested_in:(event list) -> 'a observer -> observer_id
109
110     method detach_observer: observer_id -> unit
111
112     (** force a notification to all observer, old status is passed as None *)
113     method notify: unit
114
115   end
116
117 val trivial_status:
118   ?uri:UriManager.uri ->
119   typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv ->
120   attrs:Cic.attribute list ->
121   unit ->
122     unit status
123