aboutsummaryrefslogtreecommitdiff
path: root/lib/pp.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2014-11-06 18:50:41 +0100
committerPierre-Marie Pédrot2014-11-10 11:53:22 +0100
commit791b6a26a23b71cc1cba364977cc825028c8ebc9 (patch)
treecaa2d5d483e8df6e010d0fdedce57241b420a376 /lib/pp.ml
parente760752eeba4593a5f9bb7b123454cd54f40eff9 (diff)
Adding a dynamic tag type in Pp.
Diffstat (limited to 'lib/pp.ml')
-rw-r--r--lib/pp.ml31
1 files changed, 31 insertions, 0 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index c47d638337..a00e70237c 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -37,6 +37,37 @@ end = struct
let map = List.map
end
+module Tag :
+sig
+ type t
+ type 'a key
+ val create : string -> 'a key
+ val inj : 'a -> 'a key -> t
+ val prj : t -> 'a key -> 'a option
+end =
+struct
+ (** See module {Dyn} for more details. *)
+
+ type t = int * Obj.t
+
+ type 'a key = int
+
+ let dyntab = ref (Int.Map.empty : string Int.Map.t)
+
+ let create (s : string) =
+ let hash = Hashtbl.hash s in
+ let () = assert (not (Int.Map.mem hash !dyntab)) in
+ let () = dyntab := Int.Map.add hash s !dyntab in
+ hash
+
+ let inj x h = (h, Obj.repr x)
+
+ let prj (nh, rv) h =
+ if Int.equal h nh then Some (Obj.magic rv)
+ else None
+
+end
+
open Pp_control
(* This should not be used outside of this file. Use