+++ /dev/null
-(* 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 _ _ -> ()) ()
-
projects / helm.git / blobdiff