From: Stefano Zacchiroli Date: Mon, 4 Oct 2004 09:37:28 +0000 (+0000) Subject: splitted History module out of StatefulProofEngine X-Git-Tag: V_0_0_10~102 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=530ba8fae13eca642122731be5a7b36f0b809edb;p=helm.git splitted History module out of StatefulProofEngine --- diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend index 242671197..972c7071c 100644 --- a/helm/ocaml/tactics/.depend +++ b/helm/ocaml/tactics/.depend @@ -16,8 +16,6 @@ fourierR.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi -proofEngineTypes.cmo: proofEngineTypes.cmi -proofEngineTypes.cmx: proofEngineTypes.cmi newConstraints.cmo: newConstraints.cmi newConstraints.cmx: newConstraints.cmi match_concl.cmo: newConstraints.cmi match_concl.cmi @@ -92,5 +90,9 @@ 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: proofEngineTypes.cmi statefulProofEngine.cmi -statefulProofEngine.cmx: proofEngineTypes.cmx statefulProofEngine.cmi +history.cmo: history.cmi +history.cmx: history.cmi +statefulProofEngine.cmo: history.cmi proofEngineTypes.cmi \ + statefulProofEngine.cmi +statefulProofEngine.cmx: history.cmx proofEngineTypes.cmx \ + statefulProofEngine.cmi diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile index 3b0392f16..2a4e59872 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 statefulProofEngine.mli + fourierR.mli history.mli statefulProofEngine.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) include ../Makefile.common diff --git a/helm/ocaml/tactics/history.ml b/helm/ocaml/tactics/history.ml new file mode 100644 index 000000000..3a966b56f --- /dev/null +++ b/helm/ocaml/tactics/history.ml @@ -0,0 +1,84 @@ +(* 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/ + *) + +exception History_failure + +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 + diff --git a/helm/ocaml/tactics/history.mli b/helm/ocaml/tactics/history.mli new file mode 100644 index 000000000..86bad463f --- /dev/null +++ b/helm/ocaml/tactics/history.mli @@ -0,0 +1,35 @@ +(* 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/ + *) + +exception History_failure + +class ['a] history : + int -> + object + method push : 'a -> unit + method redo : int -> 'a + method undo : int -> 'a + end +