diff options
| -rw-r--r-- | checker/check.mllib | 4 | ||||
| -rw-r--r-- | dev/printers.mllib | 4 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 4 | ||||
| -rw-r--r-- | kernel/names.ml | 10 | ||||
| -rw-r--r-- | kernel/names.mli | 1 | ||||
| -rw-r--r-- | lib/cString.ml | 3 | ||||
| -rw-r--r-- | lib/cString.mli | 5 | ||||
| -rw-r--r-- | lib/clib.mllib | 2 | ||||
| -rw-r--r-- | lib/lib.mllib | 2 |
9 files changed, 20 insertions, 15 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index e493cec03..1bc23734a 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -8,14 +8,14 @@ Segmenttree Unicodetable Unicode Errors +Hashset +Hashcons CObj CList CString CArray Util Option -Hashset -Hashcons CUnix System Envars diff --git a/dev/printers.mllib b/dev/printers.mllib index e6ecb8c56..29fa827dc 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -10,14 +10,14 @@ Segmenttree Unicodetable Unicode Errors +Hashset +Hashcons CObj CList CString CArray Util Bigint -Hashset -Hashcons Dyn CUnix System diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 50eac6e76..9a7bfed0f 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -7,13 +7,13 @@ Pp Loc Compat Errors +Hashset +Hashcons CList CString CArray Util Bigint -Hashset -Hashcons Predicate Option Segmenttree diff --git a/kernel/names.ml b/kernel/names.ml index c4e632a3a..1917f8f40 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -22,8 +22,6 @@ open Pp open Errors open Util -let hcons_string = Hashcons.simple_hcons Hashcons.Hstring.generate () - (** {6 Identifiers } *) type identifier = string @@ -38,7 +36,7 @@ let check_ident x = let id_of_string s = let () = check_ident_soft s in let s = String.copy s in - hcons_string s + String.hcons s let string_of_id id = String.copy id @@ -504,13 +502,13 @@ module Hconstruct = Hashcons.Make( let hash = Hashtbl.hash end) -let hcons_ident = hcons_string +let hcons_ident = String.hcons let hcons_name = Hashcons.simple_hcons Hname.generate hcons_ident let hcons_dirpath = Hashcons.simple_hcons Hdir.generate hcons_ident let hcons_uid = Hashcons.simple_hcons Huniqid.generate (hcons_ident,hcons_dirpath) let hcons_mp = - Hashcons.simple_hcons Hmod.generate (hcons_dirpath,hcons_uid,hcons_string) -let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,hcons_dirpath,hcons_string) + Hashcons.simple_hcons Hmod.generate (hcons_dirpath,hcons_uid,String.hcons) +let hcons_kn = Hashcons.simple_hcons Hkn.generate (hcons_mp,hcons_dirpath,String.hcons) let hcons_con = Hashcons.simple_hcons Hcn.generate hcons_kn let hcons_mind = Hashcons.simple_hcons Hcn.generate hcons_kn let hcons_ind = Hashcons.simple_hcons Hind.generate hcons_mind diff --git a/kernel/names.mli b/kernel/names.mli index 3eb070380..0f37c8055 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -220,7 +220,6 @@ val eq_egr : evaluable_global_reference -> evaluable_global_reference (** {6 Hash-consing } *) -val hcons_string : string -> string val hcons_ident : identifier -> identifier val hcons_name : name -> name val hcons_dirpath : dir_path -> dir_path diff --git a/lib/cString.ml b/lib/cString.ml index b34b21957..59a6d17c6 100644 --- a/lib/cString.ml +++ b/lib/cString.ml @@ -60,6 +60,7 @@ sig val is_sub : string -> string -> int -> bool module Set : Set.S with type elt = t module Map : Map.S with type key = t + val hcons : string -> string end include String @@ -178,3 +179,5 @@ end module Set = Set.Make(Self) module Map = Map.Make(Self) + +let hcons = Hashcons.simple_hcons Hashcons.Hstring.generate () diff --git a/lib/cString.mli b/lib/cString.mli index 18679d310..c9ff60f76 100644 --- a/lib/cString.mli +++ b/lib/cString.mli @@ -88,12 +88,17 @@ sig val is_sub : string -> string -> int -> bool (** [is_sub p s off] tests whether [s] contains [p] at offset [off]. *) + (** {6 Generic operations} **) + module Set : Set.S with type elt = t (** Finite sets on [string] *) module Map : Map.S with type key = t (** Finite maps on [string] *) + val hcons : string -> string + (** Hashconsing on [string] *) + end include ExtS diff --git a/lib/clib.mllib b/lib/clib.mllib index 1f4707fda..d40df73a0 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -3,6 +3,8 @@ Pp_control Pp Coq_config Deque +Hashset +Hashcons CObj CList CString diff --git a/lib/lib.mllib b/lib/lib.mllib index f557bd7d7..372d8ddf3 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -3,8 +3,6 @@ Xml_parser Loc Errors Bigint -Hashset -Hashcons Dyn Segmenttree Unicodetable |