]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/statefulProofEngine.ml
New syntax.
[helm.git] / helm / ocaml / tactics / statefulProofEngine.ml
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 let history_size = 20
27
28 exception History_failure
29 exception No_goal_left
30 exception Uri_redefinition
31 type event = [ `Proof_changed | `Proof_completed ]
32 let all_events = [ `Proof_changed; `Proof_completed ]
33 let default_events: event list = [ `Proof_changed ]
34
35 type 'a observer =
36   (ProofEngineTypes.status * 'a) option -> (ProofEngineTypes.status * 'a) ->
37     unit
38 type observer_id = int
39
40 exception Observer_failures of (observer_id * exn) list
41 exception Tactic_failure of exn
42 exception Data_failure of exn
43
44 class ['a] history size =
45   let unsome = function Some x -> x | None -> assert false in
46   object (self)
47
48     val history_data = Array.create (size + 1) None
49
50     val mutable history_hd = 0  (* rightmost index *)
51     val mutable history_cur = 0 (* current index *)
52     val mutable history_tl = 0  (* leftmost index *)
53
54     method private is_empty = history_data.(history_cur) = None
55
56     method push (status: 'a) =
57       if self#is_empty then
58         history_data.(history_cur) <- Some status
59       else begin
60         history_cur <- (history_cur + 1) mod size;
61         history_data.(history_cur) <- Some status;
62         history_hd <- history_cur;  (* throw away fake future line *)
63         if history_hd = history_tl then (* tail overwritten *)
64           history_tl <- (history_tl + 1) mod size
65       end
66
67     method undo = function
68       | 0 -> unsome history_data.(history_cur)
69       | steps when steps > 0 ->
70           let max_undo_steps =
71             if history_cur >= history_tl then
72               history_cur - history_tl
73             else
74               history_cur + (size - history_tl)
75           in
76           if steps > max_undo_steps then
77             raise History_failure;
78           history_cur <- history_cur - steps;
79           if history_cur < 0 then (* fix underflow *)
80             history_cur <- size + history_cur;
81           unsome history_data.(history_cur)
82       | steps (* when steps > 0 *) -> self#redo ~-steps
83
84     method redo = function
85       | 0 -> unsome history_data.(history_cur)
86       | steps when steps > 0 ->
87           let max_redo_steps =
88             if history_hd >= history_cur then
89               history_hd - history_cur
90             else
91               history_hd + (size - history_cur)
92           in
93           if steps > max_redo_steps then
94             raise History_failure;
95           history_cur <- (history_cur + steps) mod size;
96           unsome history_data.(history_cur)
97       | steps (* when steps > 0 *) -> self#undo ~-steps
98
99   end
100
101 class ['a] status
102   ?uri ~typ ?(body = Cic.Meta (1, [])) ?(metasenv = [1,[],typ])
103   init_data compute_data ()
104   =
105   let next_observer_id =
106     let next_id = ref 0 in
107     fun () ->
108       incr next_id;
109       !next_id
110   in
111   let initial_proof = ((uri: UriManager.uri option), metasenv, body, typ) in
112   let next_goal (goals, proof) =
113     match goals, proof with
114     | goal :: _, _ -> Some goal
115     | [], (_, (goal, _, _) :: _, _, _) ->
116         (* the tactic left no open goal: let's choose the first open goal *)
117         Some goal
118     | _, _ -> None
119   in
120   let initial_goal = next_goal ([], initial_proof) in
121   object (self)
122
123     val mutable _proof = initial_proof
124     val mutable _goal = initial_goal
125     val mutable _data: 'a = init_data (initial_proof, initial_goal)
126
127       (* event -> (id, observer) list *)
128     val observers = Hashtbl.create 7
129
130       (* assumption: all items in history are uncompleted proofs, thus option on
131       * goal could be ignored and goal are stored as bare integers *)
132     val history = new history history_size
133
134     initializer
135       history#push self#internal_status
136
137     method proof = _proof
138     method goal =
139       match _goal with Some goal -> goal | None -> raise No_goal_left
140     method private status = (_proof, self#active_goal)  (* logic status *)
141     method private set_status (proof, goal) =
142       _proof <- proof;
143       _goal <- Some goal
144
145       (* what will be kept in history *)
146     method private internal_status = (self#status, _data)
147     method private set_internal_status (status, data) =
148       self#set_status status;
149       _data <- data
150
151     method set_goal goal =
152       let old_internal_status = self#internal_status in
153       _goal <- Some goal;
154       try
155         self#update_data old_internal_status;
156         history#push self#internal_status;
157         self#notify (Some old_internal_status)
158       with (Data_failure _) as exn ->
159         self#set_internal_status old_internal_status;
160         raise exn
161
162     method uri      = let (uri, _, _, _)      = _proof in uri
163     method metasenv = let (_, metasenv, _, _) = _proof in metasenv
164     method body     = let (_, _, body, _)     = _proof in body
165     method typ      = let (_, _, _, typ)      = _proof in typ
166
167     method set_uri uri =
168       let (old_uri, metasenv, body, typ) = _proof in
169       if old_uri <> None then
170         raise Uri_redefinition;
171       _proof <- (Some uri, metasenv, body, typ)
172
173     method conjecture goal =
174       let (_, metasenv, _, _) = _proof in
175       CicUtil.lookup_meta goal metasenv
176
177     method private active_goal =
178       match _goal with
179       | None -> raise No_goal_left
180       | Some goal -> goal
181
182     method apply_tactic tactic =
183       let old_internal_status = self#internal_status in
184       let (new_proof, new_goals) =
185         try
186           ProofEngineTypes.apply_tactic tactic (_proof, self#active_goal)
187         with exn -> raise (Tactic_failure exn)
188       in
189       _proof <- new_proof;
190       _goal <- next_goal (new_goals, new_proof);
191       try
192         self#update_data old_internal_status;
193         history#push self#internal_status;
194         self#notify (Some old_internal_status)
195       with (Data_failure _) as exn ->
196         self#set_internal_status old_internal_status;
197         raise exn
198
199     method proof_completed = _goal <> None
200
201     method attach_observer ?(interested_in = default_events) observer
202       =
203       let id = next_observer_id () in
204       List.iter
205         (fun event ->
206           let prev_observers =
207             try Hashtbl.find observers event with Not_found -> []
208           in
209           Hashtbl.replace observers event ((id, observer)::prev_observers))
210         interested_in;
211       id
212
213     method detach_observer id =
214       List.iter
215         (fun event ->
216           let prev_observers =
217             try Hashtbl.find observers event with Not_found -> []
218           in
219           let new_observers =
220             List.filter (fun (id', _) -> id' <> id) prev_observers
221           in
222           Hashtbl.replace observers event new_observers)
223         all_events
224
225     method private notify old_internal_status =
226       let cur_internal_status = (self#status, _data) in
227       let exns = ref [] in
228       let notify (id, observer) =
229         try
230           observer old_internal_status cur_internal_status
231         with exn -> exns := (id, exn) :: !exns
232       in
233       List.iter notify
234         (try Hashtbl.find observers `Proof_changed with Not_found -> []);
235       if self#proof_completed then
236         List.iter notify
237           (try Hashtbl.find observers `Proof_completed with Not_found -> []);
238       match !exns with
239       | [] -> ()
240       | exns -> raise (Observer_failures exns)
241
242     method private update_data old_internal_status =
243       (* invariant: _goal and/or _proof has been changed
244        * invariant: proof is not yet completed *)
245       let status = self#status in
246       try
247         _data <- compute_data old_internal_status status
248       with exn -> raise (Data_failure exn)
249
250     method undo ?(steps = 1) () =
251       let ((proof, goal), data) = history#undo steps in
252       _proof <- proof;
253       _goal <- Some goal;
254       _data <- data;
255       self#notify None
256
257     method redo ?(steps = 1) () = self#undo ~steps:~-steps ()
258
259   end
260
261 let trivial_status ?uri ~typ ?body ?metasenv () =
262   new status ?uri ~typ ?body ?metasenv (fun _ -> ()) (fun _ _ -> ()) ()
263