X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FstatefulProofEngine.ml;fp=helm%2Focaml%2Ftactics%2FstatefulProofEngine.ml;h=0000000000000000000000000000000000000000;hb=1696761e4b8576e8ed81caa905fd108717019226;hp=1c970249c78faed48ced7d1df0d7692d6cb7cf91;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;p=helm.git diff --git a/helm/ocaml/tactics/statefulProofEngine.ml b/helm/ocaml/tactics/statefulProofEngine.ml deleted file mode 100644 index 1c970249c..000000000 --- a/helm/ocaml/tactics/statefulProofEngine.ml +++ /dev/null @@ -1,263 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -let history_size = 20 - -exception History_failure -exception No_goal_left -exception Uri_redefinition -type event = [ `Proof_changed | `Proof_completed ] -let all_events = [ `Proof_changed; `Proof_completed ] -let default_events: event list = [ `Proof_changed ] - -type 'a observer = - (ProofEngineTypes.status * 'a) option -> (ProofEngineTypes.status * 'a) -> - unit -type observer_id = int - -exception Observer_failures of (observer_id * exn) list -exception Tactic_failure of exn -exception Data_failure of exn - -class ['a] history size = - let unsome = function Some x -> x | None -> assert false in - object (self) - - val history_data = Array.create (size + 1) None - - val mutable history_hd = 0 (* rightmost index *) - val mutable history_cur = 0 (* current index *) - val mutable history_tl = 0 (* leftmost index *) - - method private is_empty = history_data.(history_cur) = None - - method push (status: 'a) = - if self#is_empty then - history_data.(history_cur) <- Some status - else begin - history_cur <- (history_cur + 1) mod size; - history_data.(history_cur) <- Some status; - history_hd <- history_cur; (* throw away fake future line *) - if history_hd = history_tl then (* tail overwritten *) - history_tl <- (history_tl + 1) mod size - end - - method undo = function - | 0 -> unsome history_data.(history_cur) - | steps when steps > 0 -> - let max_undo_steps = - if history_cur >= history_tl then - history_cur - history_tl - else - history_cur + (size - history_tl) - in - if steps > max_undo_steps then - raise History_failure; - history_cur <- history_cur - steps; - if history_cur < 0 then (* fix underflow *) - history_cur <- size + history_cur; - unsome history_data.(history_cur) - | steps (* when steps > 0 *) -> self#redo ~-steps - - method redo = function - | 0 -> unsome history_data.(history_cur) - | steps when steps > 0 -> - let max_redo_steps = - if history_hd >= history_cur then - history_hd - history_cur - else - history_hd + (size - history_cur) - in - if steps > max_redo_steps then - raise History_failure; - history_cur <- (history_cur + steps) mod size; - unsome history_data.(history_cur) - | steps (* when steps > 0 *) -> self#undo ~-steps - - end - -class ['a] status - ?uri ~typ ?(body = Cic.Meta (1, [])) ?(metasenv = [1,[],typ]) - init_data compute_data () - = - let next_observer_id = - let next_id = ref 0 in - fun () -> - incr next_id; - !next_id - in - let initial_proof = ((uri: UriManager.uri option), metasenv, body, typ) in - let next_goal (goals, proof) = - match goals, proof with - | goal :: _, _ -> Some goal - | [], (_, (goal, _, _) :: _, _, _) -> - (* the tactic left no open goal: let's choose the first open goal *) - Some goal - | _, _ -> None - in - let initial_goal = next_goal ([], initial_proof) in - object (self) - - val mutable _proof = initial_proof - val mutable _goal = initial_goal - val mutable _data: 'a = init_data (initial_proof, initial_goal) - - (* event -> (id, observer) list *) - val observers = Hashtbl.create 7 - - (* assumption: all items in history are uncompleted proofs, thus option on - * goal could be ignored and goal are stored as bare integers *) - val history = new history history_size - - initializer - history#push self#internal_status - - method proof = _proof - method goal = - match _goal with Some goal -> goal | None -> raise No_goal_left - method private status = (_proof, self#active_goal) (* logic status *) - method private set_status (proof, goal) = - _proof <- proof; - _goal <- Some goal - - (* what will be kept in history *) - method private internal_status = (self#status, _data) - method private set_internal_status (status, data) = - self#set_status status; - _data <- data - - method set_goal goal = - let old_internal_status = self#internal_status in - _goal <- Some goal; - try - self#update_data old_internal_status; - history#push self#internal_status; - self#notify (Some old_internal_status) - with (Data_failure _) as exn -> - self#set_internal_status old_internal_status; - raise exn - - method uri = let (uri, _, _, _) = _proof in uri - method metasenv = let (_, metasenv, _, _) = _proof in metasenv - method body = let (_, _, body, _) = _proof in body - method typ = let (_, _, _, typ) = _proof in typ - - method set_uri uri = - let (old_uri, metasenv, body, typ) = _proof in - if old_uri <> None then - raise Uri_redefinition; - _proof <- (Some uri, metasenv, body, typ) - - method conjecture goal = - let (_, metasenv, _, _) = _proof in - CicUtil.lookup_meta goal metasenv - - method private active_goal = - match _goal with - | None -> raise No_goal_left - | Some goal -> goal - - method apply_tactic tactic = - let old_internal_status = self#internal_status in - let (new_proof, new_goals) = - try - tactic (_proof, self#active_goal) - with exn -> raise (Tactic_failure exn) - in - _proof <- new_proof; - _goal <- next_goal (new_goals, new_proof); - try - self#update_data old_internal_status; - history#push self#internal_status; - self#notify (Some old_internal_status) - with (Data_failure _) as exn -> - self#set_internal_status old_internal_status; - raise exn - - method proof_completed = _goal <> None - - method attach_observer ?(interested_in = default_events) observer - = - let id = next_observer_id () in - List.iter - (fun event -> - let prev_observers = - try Hashtbl.find observers event with Not_found -> [] - in - Hashtbl.replace observers event ((id, observer)::prev_observers)) - interested_in; - id - - method detach_observer id = - List.iter - (fun event -> - let prev_observers = - try Hashtbl.find observers event with Not_found -> [] - in - let new_observers = - List.filter (fun (id', _) -> id' <> id) prev_observers - in - Hashtbl.replace observers event new_observers) - all_events - - method private notify old_internal_status = - let cur_internal_status = (self#status, _data) in - let exns = ref [] in - let notify (id, observer) = - try - observer old_internal_status cur_internal_status - with exn -> exns := (id, exn) :: !exns - in - List.iter notify - (try Hashtbl.find observers `Proof_changed with Not_found -> []); - if self#proof_completed then - List.iter notify - (try Hashtbl.find observers `Proof_completed with Not_found -> []); - match !exns with - | [] -> () - | exns -> raise (Observer_failures exns) - - method private update_data old_internal_status = - (* invariant: _goal and/or _proof has been changed - * invariant: proof is not yet completed *) - let status = self#status in - try - _data <- compute_data old_internal_status status - with exn -> raise (Data_failure exn) - - method undo ?(steps = 1) () = - let ((proof, goal), data) = history#undo steps in - _proof <- proof; - _goal <- Some goal; - _data <- data; - self#notify None - - method redo ?(steps = 1) () = self#undo ~steps:~-steps () - - end - -let trivial_status ?uri ~typ ?body ?metasenv () = - new status ?uri ~typ ?body ?metasenv (fun _ -> ()) (fun _ _ -> ()) () -