From: Stefano Zacchiroli Date: Mon, 17 May 2004 12:30:19 +0000 (+0000) Subject: first check in of statefulProofEngine X-Git-Tag: V_0_0_9~51 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e4b873cd8511753e65319d02fcdd5473214f42a5 first check in of statefulProofEngine --- diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 581663cd2..d1863019c 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -12,6 +12,7 @@ equalityTactics.cmi: proofEngineTypes.cmo discriminationTactics.cmi: proofEngineTypes.cmo ring.cmi: proofEngineTypes.cmo fourierR.cmi: proofEngineTypes.cmo +statefulProofEngine.cmi: proofEngineTypes.cmo proofEngineReduction.cmo: proofEngineReduction.cmi proofEngineReduction.cmx: proofEngineReduction.cmi proofEngineHelpers.cmo: proofEngineHelpers.cmi @@ -82,3 +83,5 @@ fourierR.cmo: equalityTactics.cmi fourier.cmi primitiveTactics.cmi \ fourierR.cmx: equalityTactics.cmx fourier.cmx primitiveTactics.cmx \ proofEngineHelpers.cmx proofEngineTypes.cmx reductionTactics.cmx ring.cmx \ tacticals.cmx fourierR.cmi +statefulProofEngine.cmo: statefulProofEngine.cmi +statefulProofEngine.cmx: statefulProofEngine.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index c5ab120c1..2aeb6fda3 100644 --- a/helm/ocaml/tactics/Makefile +++ b/helm/ocaml/tactics/Makefile @@ -10,7 +10,7 @@ INTERFACE_FILES = \ primitiveTactics.mli tacticChaser.mli variousTactics.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ equalityTactics.mli discriminationTactics.mli ring.mli fourier.mli \ - fourierR.mli + fourierR.mli statefulProofEngine.mli IMPLEMENTATION_FILES = proofEngineTypes.ml $(INTERFACE_FILES:%.mli=%.ml) include ../Makefile.common diff --git a/helm/ocaml/tactics/statefulProofEngine.ml b/helm/ocaml/tactics/statefulProofEngine.ml new file mode 100644 index 000000000..1c970249c --- /dev/null +++ b/helm/ocaml/tactics/statefulProofEngine.ml @@ -0,0 +1,263 @@ +(* 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 _ _ -> ()) () + diff --git a/helm/ocaml/tactics/statefulProofEngine.mli b/helm/ocaml/tactics/statefulProofEngine.mli new file mode 100644 index 000000000..9a4cf7825 --- /dev/null +++ b/helm/ocaml/tactics/statefulProofEngine.mli @@ -0,0 +1,110 @@ +(* 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/ + *) + +(** Stateful handling of proof status *) + +exception No_goal_left +exception Uri_redefinition + + (** can't undo/redo one or more actions *) +exception History_failure + +type event = [ `Proof_changed | `Proof_completed ] + + (** Proof observer. First callback argument is Some extended_status + * when a 'real 'change of the proof happened and None when Proof_changed event + * was triggered by a time travel by the means of undo/redo actions. Embedded + * status is the status _before_ the current change. Second status is the + * status reached _after_ the current change. *) +type 'a observer = + (ProofEngineTypes.status * 'a) option -> (ProofEngineTypes.status * 'a) -> + unit + + (** needed to detach previously attached observers *) +type observer_id + + (** tactic application failed. @see apply_tactic *) +exception Tactic_failure of exn + + (** one or more observers failed. @see apply_tactic *) +exception Observer_failures of (observer_id * exn) list + + (** failure while updating internal data (: 'a). @see apply_tactic *) +exception Data_failure of exn + +(** {2 OO interface} *) + +class ['a] status: + ?uri:UriManager.uri -> + typ:Cic.term -> ?body:Cic.term -> ?metasenv:Cic.metasenv -> + (ProofEngineTypes.proof * ProofEngineTypes.goal option -> 'a) -> + (ProofEngineTypes.status * 'a -> ProofEngineTypes.status -> 'a) -> + unit -> + object + + method proof: ProofEngineTypes.proof + method metasenv: Cic.metasenv + method body: Cic.term + method typ: Cic.term + + (** goal -> conjecture + * @raise CicUtil.Meta_not_found *) + method conjecture: int -> Cic.conjecture + + method proof_completed: bool + method goal: int (** @raise No_goal_left *) + method set_goal: int -> unit (** @raise No_goal_left *) + + method uri: UriManager.uri option + method set_uri: UriManager.uri -> unit (** @raise Uri_redefinition *) + + (** @raise Tactic_failure + * @raise Observer_failures + * @raise Data_failure + * + * In case of tactic failure, internal status is left unchanged. + * In case of observer failures internal status will be changed and is + * granted that all observer will be invoked collecting their failures. + * In case of data failure, internal status is left unchanged (rolling back + * last tactic application if needed) + *) + method apply_tactic: ProofEngineTypes.tactic -> unit + + method undo: ?steps:int -> unit -> unit + method redo: ?steps:int -> unit -> unit + + method attach_observer: + ?interested_in:(event list) -> 'a observer -> observer_id + + method detach_observer: observer_id -> unit + + end + +val trivial_status: + ?uri:UriManager.uri -> + typ:Cic.term -> ?body:Cic.term -> ?metasenv:Cic.metasenv -> + unit -> + unit status +