From: Stefano Zacchiroli Date: Mon, 4 Oct 2004 09:37:07 +0000 (+0000) Subject: - splitted out History module X-Git-Tag: V_0_0_10~103 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c71d85e81edbf2643df8267dbcf90d22031c9ea9;p=helm.git - splitted out History module - exported all_events - status is now a pair proof * goal _option_ so that completed proofs have their entry in the history and could be passed to observers - added set_metasenv method to change imperatively metasenv - added explicit notification method notify --- diff --git a/helm/ocaml/tactics/statefulProofEngine.ml b/helm/ocaml/tactics/statefulProofEngine.ml index 94710c412..13c1ac514 100644 --- a/helm/ocaml/tactics/statefulProofEngine.ml +++ b/helm/ocaml/tactics/statefulProofEngine.ml @@ -23,84 +23,26 @@ * http://helm.cs.unibo.it/ *) -let history_size = 20 +let default_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 proof_status = ProofEngineTypes.proof * ProofEngineTypes.goal option + +type 'a observer = (proof_status * 'a) option -> (proof_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 () + ?(history_size = default_history_size) + ?uri ~typ ~body ~metasenv init_data compute_data () = let next_observer_id = let next_id = ref 0 in @@ -129,18 +71,21 @@ class ['a] status (* 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 + val history = new History.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) = + method private status = (_proof, _goal) (* logic status *) + method private set_status (proof, (goal: int option)) = _proof <- proof; - _goal <- Some goal + _goal <- goal + + method goal = + match _goal with + | Some goal -> goal + | None -> raise No_goal_left (* what will be kept in history *) method private internal_status = (self#status, _data) @@ -154,7 +99,7 @@ class ['a] status try self#update_data old_internal_status; history#push self#internal_status; - self#notify (Some old_internal_status) + self#private_notify (Some old_internal_status) with (Data_failure _) as exn -> self#set_internal_status old_internal_status; raise exn @@ -164,6 +109,10 @@ class ['a] status method body = let (_, _, body, _) = _proof in body method typ = let (_, _, _, typ) = _proof in typ + method set_metasenv metasenv = + let (uri, _, body, typ) = _proof in + _proof <- (uri, metasenv, body, typ) + method set_uri uri = let (old_uri, metasenv, body, typ) = _proof in if old_uri <> None then @@ -174,16 +123,11 @@ class ['a] status 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 - ProofEngineTypes.apply_tactic tactic (_proof, self#active_goal) + ProofEngineTypes.apply_tactic tactic (_proof, self#goal) with exn -> raise (Tactic_failure exn) in _proof <- new_proof; @@ -191,12 +135,12 @@ class ['a] status try self#update_data old_internal_status; history#push self#internal_status; - self#notify (Some old_internal_status) + self#private_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 proof_completed = _goal = None method attach_observer ?(interested_in = default_events) observer = @@ -222,7 +166,7 @@ class ['a] status Hashtbl.replace observers event new_observers) all_events - method private notify old_internal_status = + method private private_notify old_internal_status = let cur_internal_status = (self#status, _data) in let exns = ref [] in let notify (id, observer) = @@ -250,14 +194,16 @@ class ['a] status method undo ?(steps = 1) () = let ((proof, goal), data) = history#undo steps in _proof <- proof; - _goal <- Some goal; + _goal <- goal; _data <- data; - self#notify None + self#private_notify None method redo ?(steps = 1) () = self#undo ~steps:~-steps () + method notify = self#private_notify None + end -let trivial_status ?uri ~typ ?body ?metasenv () = - new status ?uri ~typ ?body ?metasenv (fun _ -> ()) (fun _ _ -> ()) () +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 index 9a4cf7825..4198876ca 100644 --- a/helm/ocaml/tactics/statefulProofEngine.mli +++ b/helm/ocaml/tactics/statefulProofEngine.mli @@ -28,19 +28,22 @@ exception No_goal_left exception Uri_redefinition - (** can't undo/redo one or more actions *) -exception History_failure - type event = [ `Proof_changed | `Proof_completed ] +val all_events: event list + + (** from our point of view a status is the status of an incomplete proof, thus + * we have an optional goal which is None if the proof is not yet completed + * (i.e. some goal is still open) *) +type proof_status = ProofEngineTypes.proof * ProofEngineTypes.goal option + (** 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 + * was triggered by a time travel by the means of undo/redo actions or by an + * external "#notify" invocation. Embedded status is the status _before_ the + * current change. Second status is the status reached _after_ the current + * change. *) +type 'a observer = (proof_status * 'a) option -> (proof_status * 'a) -> unit (** needed to detach previously attached observers *) type observer_id @@ -57,10 +60,11 @@ exception Data_failure of exn (** {2 OO interface} *) class ['a] status: + ?history_size:int -> (** default 20 *) ?uri:UriManager.uri -> - typ:Cic.term -> ?body:Cic.term -> ?metasenv:Cic.metasenv -> - (ProofEngineTypes.proof * ProofEngineTypes.goal option -> 'a) -> - (ProofEngineTypes.status * 'a -> ProofEngineTypes.status -> 'a) -> + typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv -> + (proof_status -> 'a) -> (* init data *) + (proof_status * 'a -> proof_status -> 'a) -> (* update data *) unit -> object @@ -69,13 +73,16 @@ class ['a] status: method body: Cic.term method typ: Cic.term + (** change metasenv _without_ triggering any notification *) + method set_metasenv: Cic.metasenv -> unit + (** 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 set_goal: int -> unit (** @raise Data_failure *) method uri: UriManager.uri option method set_uri: UriManager.uri -> unit (** @raise Uri_redefinition *) @@ -100,11 +107,14 @@ class ['a] status: method detach_observer: observer_id -> unit + (** force a notification to all observer, old status is passed as None *) + method notify: unit + end val trivial_status: ?uri:UriManager.uri -> - typ:Cic.term -> ?body:Cic.term -> ?metasenv:Cic.metasenv -> + typ:Cic.term -> body:Cic.term -> metasenv:Cic.metasenv -> unit -> unit status