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           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