splitted History module out of StatefulProofEngine

diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend
index 242671197dbba22a25c922740e9ff67ae09d7acc..972c7071cba7380a31725bf77e4b6026de428219 100644 (file)
--- 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 3b0392f16b880e213636d5d3bba2b8101a66a060..2a4e59872e8bd2cf81f366a653950d6bf26e0ce0 100644 (file)
--- 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 (file)
index 0000000..3a966b5
--- /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 (file)
index 0000000..86bad46
--- /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
+