time stamps

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@92 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 42 insertions, 0 deletions

diff --git a/lib/stamps.ml b/lib/stamps.ml
new file mode 100644
index 000000000..0441d2de1
--- /dev/null
+++ b/lib/stamps.ml
@@ -0,0 +1,21 @@
+
+(* $Id$ *)
+
+let new_stamp = 
+  let stamp_ctr = ref 0 in
+  fun () -> incr stamp_ctr; !stamp_ctr
+
+type 'a timestamped = { stamp : int; ed : 'a }
+
+let ts_stamp st = st.stamp
+let ts_mod f st = { stamp = new_stamp(); ed = f st.ed }
+let ts_it st = st.ed
+let ts_mk v = { stamp = new_stamp(); ed = v}
+let ts_eq st1 st2 = st1.stamp = st2.stamp
+
+type 'a idstamped = 'a timestamped
+
+let ids_mod f st = { stamp = st.stamp; ed = f st.ed}
+let ids_it = ts_it
+let ids_mk = ts_mk
+let ids_eq = ts_eq
diff --git a/lib/stamps.mli b/lib/stamps.mli
new file mode 100644
index 000000000..1eb624d57
--- /dev/null
+++ b/lib/stamps.mli
@@ -0,0 +1,21 @@
+
+(* $Id$ *)
+
+(* Time stamps. *)
+
+type 'a timestamped
+
+(* [ts_mod] gives a ['b timestamped] with a new stamp *)
+val ts_mod : ('a -> 'b) -> 'a timestamped -> 'b timestamped
+val ts_it : 'a timestamped -> 'a
+val ts_mk : 'a -> 'a timestamped
+val ts_eq : 'a timestamped -> 'a timestamped -> bool
+val ts_stamp : 'a timestamped -> int
+
+type 'a idstamped
+
+(* [ids_mod] gives a ['b stamped] with the same stamp *)
+val ids_mod : ('a -> 'b) -> 'a idstamped -> 'b idstamped
+val ids_it : 'a idstamped -> 'a
+val ids_mk : 'a -> 'a idstamped
+val ids_eq : 'a idstamped -> 'a idstamped -> bool