From 9f227961ae2219728e4cdd56e4d4c4e7165e4306 Mon Sep 17 00:00:00 2001 From: kim Date: Wed, 28 Apr 2010 06:45:00 +0000 Subject: [PATCH] Safety commit git-svn-id: svn+ssh://idea.nguyen.vg/svn/sxsi/trunk/xpathcomp@802 3cdefd35-fc62-479d-8e8d-bae585ffb9ca --- Makefile | 4 +- ata.ml | 136 +++++++++++++++++++++++++++++++++------------ ata.mli | 4 +- depend | 44 +++++++-------- finiteCofinite.ml | 22 ++++---- finiteCofinite.mli | 2 +- hcons.ml | 18 +++--- hcons.mli | 8 +-- hlist.ml | 4 +- hlist.mli | 2 +- memoizer.ml | 65 ---------------------- memoizer.mli | 5 -- ptset.ml | 20 +++---- ptset.mli | 3 +- tree.ml | 14 +++-- uid.ml | 8 +++ uid.mli | 3 + 17 files changed, 185 insertions(+), 177 deletions(-) delete mode 100644 memoizer.ml delete mode 100644 memoizer.mli create mode 100644 uid.ml create mode 100644 uid.mli diff --git a/Makefile b/Makefile index b033ed1..980f24b 100644 --- a/Makefile +++ b/Makefile @@ -3,8 +3,8 @@ DEBUG=false PROFILE=false VERBOSE=false -BASESRC=custom.ml memoizer.ml hcons.ml hlist.ml ptset.ml finiteCofinite.ml tag.ml tagSet.ml options.ml tree.ml ata.ml -BASEMLI=sigs.mli memoizer.mli hcons.mli hlist.mli ptset.mli finiteCofinite.mli tag.mli tagSet.mli options.mli tree.mli ata.mli +BASESRC=uid.ml custom.ml hcons.ml hlist.ml ptset.ml finiteCofinite.ml tag.ml tagSet.ml options.ml tree.ml ata.ml +BASEMLI=uid.mli sigs.mli hcons.mli hlist.mli ptset.mli finiteCofinite.mli tag.mli tagSet.mli options.mli tree.mli ata.mli MLSRCS = memory.ml $(BASESRC) ulexer.ml xPath.ml main.ml MLISRCS = memory.mli $(BASEMLI) ulexer.mli xPath.mli BASEOBJS= $(BASESRC:.ml=.cmx) diff --git a/ata.ml b/ata.ml index 3959ccf..8c3fa18 100644 --- a/ata.ml +++ b/ata.ml @@ -58,8 +58,8 @@ struct match f.pos with | False -> 0 | True -> 1 - | Or (f1,f2) -> HASHINT3(PRIME2,f1.Node.id, f2.Node.id) - | And (f1,f2) -> HASHINT3(PRIME3,f1.Node.id,f2.Node.id) + | Or (f1,f2) -> HASHINT3(PRIME2,Uid.to_int f1.Node.id, Uid.to_int f2.Node.id) + | And (f1,f2) -> HASHINT3(PRIME3,Uid.to_int f1.Node.id, Uid.to_int f2.Node.id) | Atom(d,p,s) -> HASHINT4(PRIME4,hash_const_variant d,vb p,s) end @@ -197,7 +197,9 @@ module Transition = struct type node = State.t*TagSet.t*bool*Formula.t*bool include Hcons.Make(struct type t = node - let hash (s,ts,m,f,b) = HASHINT5(s,TagSet.uid ts,Formula.uid f,vb m,vb b) + let hash (s,ts,m,f,b) = HASHINT5(s,Uid.to_int (TagSet.uid ts), + Uid.to_int (Formula.uid f), + vb m,vb b) let equal (s,ts,b,f,m) (s',ts',b',f',m') = s == s' && ts == ts' && b==b' && m==m' && f == f' end) @@ -284,7 +286,9 @@ module FormTable = Hashtbl.Make(struct let equal (f1,s1,t1) (f2,s2,t2) = f1 == f2 && s1 == s2 && t1 == t2 let hash (f,s,t) = - HASHINT3(Formula.uid f ,StateSet.uid s,StateSet.uid t) + HASHINT3(Uid.to_int (Formula.uid f), + Uid.to_int (StateSet.uid s), + Uid.to_int (StateSet.uid t)) end) module F = Formula @@ -332,7 +336,10 @@ module FTable = Hashtbl.Make(struct type t = Tag.t*Formlist.t*StateSet.t*StateSet.t let equal (tg1,f1,s1,t1) (tg2,f2,s2,t2) = tg1 == tg2 && f1 == f2 && s1 == s2 && t1 == t2;; - let hash (tg,f,s,t) = HASHINT4(tg,Formlist.uid f ,StateSet.uid s,StateSet.uid t);; + let hash (tg,f,s,t) = + HASHINT4(tg, Uid.to_int (Formlist.uid f), + Uid.to_int (StateSet.uid s), + Uid.to_int (StateSet.uid t)) end) @@ -817,11 +824,40 @@ END module SListTable = Hashtbl.Make(struct type t = SList.t let equal = (==) - let hash t = t.SList.Node.id + let hash t = Uid.to_int t.SList.Node.id end) - module TransCacheOld = + module TransCache = + struct + type cell = { key : int; + obj : Obj.t } + type 'a t = cell array + let dummy = { key = 0; obj = Obj.repr () } + let create n = Array.create 25000 dummy + let hash a b = HASHINT2(Obj.magic a, Uid.to_int b.SList.Node.id) + + let find_slot t key = + let rec loop i = + if (t.(i) != dummy) && (t.(i).key != key) + then loop ((i+1 mod 25000)) + else i + in loop (key mod 25000) + ;; + + let find t k1 k2 = + let i = find_slot t (hash k1 k2) in + if t.(i) == dummy then raise Not_found + else Obj.magic (t.(i).obj) + + let add t k1 k2 v = + let key = hash k1 k2 in + let i = find_slot t key in + t.(i)<- { key = key; obj = (Obj.repr v) } + + end + + module TransCache2 = struct type 'a t = Obj.t array SListTable.t let create n = SListTable.create n @@ -853,7 +889,7 @@ END end - module TransCache = + module TransCacheOld = struct external get : 'a array -> int ->'a = "%array_unsafe_get" external set : 'a array -> int -> 'a -> unit = "%array_unsafe_set" @@ -863,32 +899,22 @@ END let create n = Array.create n dummy_cell let dummy = fun _ _-> assert false let find h tag slist = - let tab = get h slist.SList.Node.id in + let tab = get h (Uid.to_int slist.SList.Node.id) in if tab == dummy_cell then raise Not_found else let res = get tab tag in if res == dummy then raise Not_found else res let add (h : t) tag slist (data : fun_tree) = - let tab = get h slist.SList.Node.id in + let tab = get h (Uid.to_int slist.SList.Node.id) in let tab = if tab == dummy_cell then let x = Array.create 10000 dummy in - (set h slist.SList.Node.id x;x) + (set h (Uid.to_int slist.SList.Node.id) x;x) else tab in set tab tag data end - module TransCache2 = struct - include Hashtbl.Make (struct - type t = Tag.t*SList.t - let equal (a,b) (c,d) = a==c && b==d - let hash (a,b) = HASHINT2((Obj.magic a), b.SList.Node.id) - end) - - let add h t s d = add h (t,s) d - let find h t s = find h (t,s) - end let td_trans = TransCache.create 10000 (* should be number of tags *number of states^2 in the document *) @@ -900,10 +926,10 @@ END module FllTable = Hashtbl.Make (struct type t = Formlistlist.t let equal = (==) - let hash t = t.Formlistlist.Node.id + let hash t = Uid.to_int t.Formlistlist.Node.id end) - module Fold2Res = struct + module Fold2ResOld = struct external get : 'a array -> int ->'a = "%array_unsafe_get" external set : 'a array -> int -> 'a -> unit = "%array_unsafe_set" external field1 : 'a -> 'b = "%field1" @@ -919,12 +945,12 @@ END let af = get h tag in if af == dummy then raise Not_found else - let as1 = get af fl.Formlistlist.Node.id in + let as1 = get af (Uid.to_int fl.Formlistlist.Node.id) in if as1 == dummy then raise Not_found else - let as2 = get as1 s1.SList.Node.id in + let as2 = get as1 (Uid.to_int s1.SList.Node.id) in if as2 == dummy then raise Not_found - else let v = get as2 s2.SList.Node.id in + else let v = get as2 (Uid.to_int s2.SList.Node.id) in if field1 v == 2 then raise Not_found else v @@ -939,33 +965,37 @@ END else x in let as1 = - let x = get af fl.Formlistlist.Node.id in + let x = get af (Uid.to_int fl.Formlistlist.Node.id) in if x == dummy then begin let y = Array.make 10000 dummy in - set af fl.Formlistlist.Node.id y;y + set af (Uid.to_int fl.Formlistlist.Node.id) y;y end else x in let as2 = - let x = get as1 s1.SList.Node.id in + let x = get as1 (Uid.to_int s1.SList.Node.id) in if x == dummy then begin let y = Array.make 10000 dummy_val in - set as1 s1.SList.Node.id y;y + set as1 (Uid.to_int s1.SList.Node.id) y;y end else x in - set as2 s2.SList.Node.id data + set as2 (Uid.to_int s2.SList.Node.id) data end + + - module Fold2Res2 = struct + module Fold2Res3 = struct include Hashtbl.Make(struct type t = Tag.t*Formlistlist.t*SList.t*SList.t let equal (a,b,c,d) (x,y,z,t) = a == x && b == y && c == z && d == t - let hash (a,b,c,d) = HASHINT4 (a,b.Formlistlist.Node.id, - c.SList.Node.id,d.SList.Node.id) + let hash (a,b,c,d) = HASHINT4 (a, + Uid.to_int b.Formlistlist.Node.id, + Uid.to_int c.SList.Node.id, + Uid.to_int d.SList.Node.id) end) let add h t f s1 s2 d = add h (t,f,s1,s2) d @@ -973,6 +1003,38 @@ END find h (t,f,s1,s2) end + module Fold2Res = + struct + type cell = { key : int; + obj : Obj.t } + type 'a t = cell array + let dummy = { key = 0; obj = Obj.repr () } + let create n = Array.create 25000 dummy + let hash a b c d = HASHINT4(Obj.magic a, + Uid.to_int b.Formlistlist.Node.id, + Uid.to_int c.SList.Node.id, + Uid.to_int d.SList.Node.id) + + let find_slot t key = + let rec loop i = + if (t.(i) != dummy) && (t.(i).key != key) + then loop ((i+1 mod 25000)) + else i + in loop (key mod 25000) + ;; + + let find t k1 k2 k3 k4 = + let i = find_slot t (hash k1 k2 k3 k4) in + if t.(i) == dummy then raise Not_found + else Obj.magic (t.(i).obj) + + let add t k1 k2 k3 k4 v = + let key = hash k1 k2 k3 k4 in + let i = find_slot t key in + t.(i)<- { key = key; obj = (Obj.repr v) } + + end + let h_fold2 = Fold2Res.create 10000 let top_down ?(noright=false) a tree t slist ctx slot_size = @@ -1189,7 +1251,7 @@ END if Ptss.mem s c.sets then { c with results = IMap.add s (RS.concat r (IMap.find s c.results)) c.results} else - { hash = HASHINT2(c.hash,Ptset.Int.uid s); + { hash = HASHINT2(c.hash,Uid.to_int (Ptset.Int.uid s)); sets = Ptss.add s c.sets; results = IMap.add s r c.results } @@ -1223,7 +1285,7 @@ END in let h,s = Ptss.fold - (fun s (ah,ass) -> (HASHINT2(ah,Ptset.Int.uid s), + (fun s (ah,ass) -> (HASHINT2(ah, Uid.to_int (Ptset.Int.uid s)), Ptss.add s ass)) (Ptss.union c1.sets c2.sets) (0,Ptss.empty) in @@ -1270,7 +1332,7 @@ END let h_trans = Hashtbl.create 4096 let get_up_trans slist ptag a tree = - let key = (HASHINT2(SList.uid slist,ptag)) in + let key = (HASHINT2(Uid.to_int slist.SList.Node.id ,ptag)) in try Hashtbl.find h_trans key with diff --git a/ata.mli b/ata.mli index 13e8431..125e34b 100644 --- a/ata.mli +++ b/ata.mli @@ -22,7 +22,7 @@ module Formula : type t val hash : t -> int - val uid : t -> int + val uid : t -> Uid.t val equal : t -> t -> bool val expr : t -> t expr val st : @@ -58,7 +58,7 @@ module Transition : val make : data -> t val node : t -> data val hash : t -> int - val uid : t -> int + val uid : t -> Uid.t val equal : t -> t -> bool module Infix : sig val ( ?< ) : State.t -> State.t diff --git a/depend b/depend index 62572f7..bd0968a 100644 --- a/depend +++ b/depend @@ -1,29 +1,29 @@ memory.cmo: memory.cmi memory.cmx: memory.cmi +uid.cmo: uid.cmi +uid.cmx: uid.cmi custom.cmo: sigs.cmi custom.cmx: sigs.cmi -memoizer.cmo: memoizer.cmi -memoizer.cmx: memoizer.cmi -hcons.cmo: hcons.cmi -hcons.cmx: hcons.cmi -hlist.cmo: hcons.cmi hlist.cmi -hlist.cmx: hcons.cmx hlist.cmi -ptset.cmo: hcons.cmi ptset.cmi -ptset.cmx: hcons.cmx ptset.cmi -finiteCofinite.cmo: sigs.cmi finiteCofinite.cmi -finiteCofinite.cmx: sigs.cmi finiteCofinite.cmi +hcons.cmo: uid.cmi hcons.cmi +hcons.cmx: uid.cmx hcons.cmi +hlist.cmo: uid.cmi hcons.cmi hlist.cmi +hlist.cmx: uid.cmx hcons.cmx hlist.cmi +ptset.cmo: uid.cmi hcons.cmi ptset.cmi +ptset.cmx: uid.cmx hcons.cmx ptset.cmi +finiteCofinite.cmo: uid.cmi ptset.cmi hcons.cmi finiteCofinite.cmi +finiteCofinite.cmx: uid.cmx ptset.cmx hcons.cmx finiteCofinite.cmi tag.cmo: tag.cmi tag.cmx: tag.cmi tagSet.cmo: tag.cmi ptset.cmi finiteCofinite.cmi tagSet.cmi tagSet.cmx: tag.cmx ptset.cmx finiteCofinite.cmx tagSet.cmi options.cmo: options.cmi options.cmx: options.cmi -tree.cmo: tag.cmi ptset.cmi options.cmi tree.cmi -tree.cmx: tag.cmx ptset.cmx options.cmx tree.cmi -ata.cmo: tree.cmi tagSet.cmi tag.cmi sigs.cmi ptset.cmi hlist.cmi hcons.cmi \ - ata.cmi -ata.cmx: tree.cmx tagSet.cmx tag.cmx sigs.cmi ptset.cmx hlist.cmx hcons.cmx \ - ata.cmi +tree.cmo: uid.cmi tag.cmi ptset.cmi options.cmi tree.cmi +tree.cmx: uid.cmx tag.cmx ptset.cmx options.cmx tree.cmi +ata.cmo: uid.cmi tree.cmi tagSet.cmi tag.cmi sigs.cmi ptset.cmi hlist.cmi \ + hcons.cmi ata.cmi +ata.cmx: uid.cmx tree.cmx tagSet.cmx tag.cmx sigs.cmi ptset.cmx hlist.cmx \ + hcons.cmx ata.cmi ulexer.cmo: ulexer.cmi ulexer.cmx: ulexer.cmi xPath.cmo: ulexer.cmi tagSet.cmi tag.cmi ata.cmi xPath.cmi @@ -31,16 +31,16 @@ xPath.cmx: ulexer.cmx tagSet.cmx tag.cmx ata.cmx xPath.cmi main.cmo: xPath.cmi ulexer.cmi tree.cmi tag.cmi options.cmi ata.cmi main.cmx: xPath.cmx ulexer.cmx tree.cmx tag.cmx options.cmx ata.cmx memory.cmi: +uid.cmi: sigs.cmi: -memoizer.cmi: -hcons.cmi: -hlist.cmi: hcons.cmi -ptset.cmi: hcons.cmi -finiteCofinite.cmi: sigs.cmi +hcons.cmi: uid.cmi +hlist.cmi: uid.cmi hcons.cmi +ptset.cmi: uid.cmi hcons.cmi +finiteCofinite.cmi: uid.cmi ptset.cmi tag.cmi: tagSet.cmi: tag.cmi ptset.cmi finiteCofinite.cmi options.cmi: tree.cmi: tag.cmi ptset.cmi -ata.cmi: tree.cmi tagSet.cmi tag.cmi sigs.cmi ptset.cmi hlist.cmi +ata.cmi: uid.cmi tree.cmi tagSet.cmi tag.cmi sigs.cmi ptset.cmi hlist.cmi ulexer.cmi: xPath.cmi: tagSet.cmi tag.cmi ata.cmi diff --git a/finiteCofinite.ml b/finiteCofinite.ml index 29ce60c..dc924cb 100644 --- a/finiteCofinite.ml +++ b/finiteCofinite.ml @@ -40,7 +40,7 @@ sig val choose : t -> elt val hash : t -> int val equal : t -> t -> bool - val uid : t -> int + val uid : t -> Uid.t val positive : t -> set val negative : t -> set val inj_positive : set -> t @@ -54,15 +54,15 @@ struct type node = Finite of E.t | CoFinite of E.t type set = E.t module Node = Hcons.Make(struct - type t = node - let equal a b = - match a,b with - (Finite(s1),Finite(s2)) - | (CoFinite(s1),CoFinite(s2)) -> E.equal s1 s2 - | _ -> false - let hash = function - Finite (s) -> HASHINT2(PRIME2,E.hash s) - | CoFinite(s) -> HASHINT2(PRIME7,E.hash s) + type t = node + let equal a b = + match a,b with + (Finite(s1),Finite(s2)) + | (CoFinite(s1),CoFinite(s2)) -> E.equal s1 s2 + | _ -> false + let hash = function + Finite (s) -> (E.hash s) lsl 1 + | CoFinite(s) -> ((E.hash s) lsl 1 ) lor 1 end) type t = Node.t let empty = Node.make (Finite E.empty) @@ -90,9 +90,11 @@ struct | CoFinite s -> not (E.mem x s) let singleton x = finite (E.singleton x) + let add e t = match t.Node.node with | Finite s -> finite (E.add e s) | CoFinite s -> cofinite (E.remove e s) + let remove e t = match t.Node.node with | Finite s -> finite (E.remove e s) | CoFinite s -> cofinite (E.add e s) diff --git a/finiteCofinite.mli b/finiteCofinite.mli index b8d8c1d..b0dccc8 100644 --- a/finiteCofinite.mli +++ b/finiteCofinite.mli @@ -33,7 +33,7 @@ module type S = val choose : t -> elt val hash : t -> int val equal : t -> t -> bool - val uid : t -> int + val uid : t -> Uid.t val positive : t -> set val negative : t -> set val inj_positive : set -> t diff --git a/hcons.ml b/hcons.ml index 35bc942..9226842 100644 --- a/hcons.ml +++ b/hcons.ml @@ -6,36 +6,34 @@ module type SA = val make : data -> t val node : t -> data val hash : t -> int - val uid : t -> int + val uid : t -> Uid.t val equal : t -> t -> bool end module type S = sig type data - type t = private { id : int; + type t = private { id : Uid.t; key : int; node : data } val make : data -> t val node : t -> data val hash : t -> int - val uid : t -> int + val uid : t -> Uid.t val equal : t -> t -> bool + end module Make (H : Hashtbl.HashedType) : S with type data = H.t = struct type data = H.t - type t = { id : int; + type t = { id : Uid.t; key : int; node : data } let node t = t.node - let hash t = t.key let uid t = t.id - let gen_uid = - let id = ref ~-1 in - fun () -> incr id;!id - let equal = (==) + let hash t = t.key + let equal t1 t2 = t1 == t2 module WH = Weak.Make( struct type _t = t type t = _t @@ -44,6 +42,6 @@ struct end) let pool = WH.create MED_H_SIZE let make x = - let cell = { id = gen_uid(); key = H.hash x; node = x } in + let cell = { id = Uid.make(); key = H.hash x; node = x } in WH.merge pool cell end diff --git a/hcons.mli b/hcons.mli index dcdcb69..bc72d33 100644 --- a/hcons.mli +++ b/hcons.mli @@ -5,20 +5,20 @@ module type SA = val make : data -> t val node : t -> data val hash : t -> int - val uid : t -> int + val uid : t -> Uid.t val equal : t -> t -> bool end module type S = sig type data - type t = private { id : int; - key : int; + type t = private { id : Uid.t; + key : int; node : data } val make : data -> t val node : t -> data val hash : t -> int - val uid : t -> int + val uid : t -> Uid.t val equal : t -> t -> bool end diff --git a/hlist.ml b/hlist.ml index 5509871..e3ad907 100644 --- a/hlist.ml +++ b/hlist.ml @@ -13,7 +13,7 @@ module type S = sig type data = Data.t type t = Node.t val hash : t -> int - val uid : t -> int + val uid : t -> Uid.t val make : data -> t val equal : t -> t -> bool val nil : t @@ -44,7 +44,7 @@ struct | _ -> false let hash = function | Nil -> 0 - | Cons(a,aa) -> HASHINT3(PRIME3,H.uid a, aa.Node.id) + | Cons(a,aa) -> HASHINT3(PRIME3,Uid.to_int (H.uid a),Uid.to_int( aa.Node.id)) end type data = Data.t type t = Node.t diff --git a/hlist.mli b/hlist.mli index 7210250..1ae44cf 100644 --- a/hlist.mli +++ b/hlist.mli @@ -12,7 +12,7 @@ module type S = sig type data = Data.t type t = Node.t val hash : t -> int - val uid : t -> int + val uid : t -> Uid.t val make : data -> t val equal : t -> t -> bool val nil : t diff --git a/memoizer.ml b/memoizer.ml deleted file mode 100644 index 861fbb6..0000000 --- a/memoizer.ml +++ /dev/null @@ -1,65 +0,0 @@ -(* - This module defines a wrapper builder which given a function - and creates its memoized version. The hashtable used to memoize - results is given as argument of the module, the keys of the table - are the argument of the function we want to wrap. - The tricky part is to do this also for recursive function where - each call can be memoized. - - See the technical report: - - "That About Wraps it Up: Using FIX to Handle Errors Without - Exceptions, and Other Programming Tricks" - - Bruce J. McAdam - - http://www.lfcs.inf.ed.ac.uk/reports/97/ECS-LFCS-97-375/ - - we give two wrapper builders: - - make , which builds a new function, memoized only at toplevel. The only - penalty here is the single look-up, which is supposed to be negligeble w.r.t - the actual computation (other wise there is little point in memoizing) - - - make_rec which acts as a fixpoint combinator and memoized each recursive call - of the function. The penalty is twofold: - 1) a look-up for every recursive call. - 2) the function has to be written in CPS, and is therefore compiled less - efficiently than its recursive non memoized function. - - Again, it is assumed that the same expensive computation will occur many time - to amortise these penalties. - -*) - -INCLUDE "utils.ml" - - -module Make ( H : Hashtbl.S ) = -struct - - - let make f = - let tbl = H.create BIG_H_SIZE in - fun arg -> - try - H.find tbl arg - with Not_found -> - let r = f arg in H.add tbl arg r;r - - - type 'a fix = Fix of ('a fix -> 'a) - - let make_rec f = - let tbl = H.create BIG_H_SIZE in - let unboxed = - function ((Fix f')as fix) -> - f (fun arg -> - try - H.find tbl arg - with - Not_found -> let r = f' fix arg - in H.add tbl arg r;r) - in unboxed (Fix unboxed) - -end -;; diff --git a/memoizer.mli b/memoizer.mli deleted file mode 100644 index dfba383..0000000 --- a/memoizer.mli +++ /dev/null @@ -1,5 +0,0 @@ -module Make (H : Hashtbl.S) : -sig - val make : (H.key -> 'a) -> H.key -> 'a - val make_rec : ((H.key -> 'a) -> H.key -> 'a) -> H.key -> 'a -end diff --git a/ptset.ml b/ptset.ml index 584ea0a..68f7e2e 100644 --- a/ptset.ml +++ b/ptset.ml @@ -14,7 +14,7 @@ sig val is_singleton : t -> bool val mem_union : t -> t -> t val hash : t -> int - val uid : t -> int + val uid : t -> Uid.t val uncons : t -> elt*t val from_list : elt list -> t val make : data -> t @@ -44,8 +44,8 @@ struct | _ -> false let hash = function | Empty -> 0 - | Leaf i -> HASHINT2(HALF_MAX_INT,H.uid i) - | Branch (b,i,l,r) -> HASHINT4(b,i,HNode.uid l, HNode.uid r) + | Leaf i -> HASHINT2(HALF_MAX_INT,Uid.to_int (H.uid i)) + | Branch (b,i,l,r) -> HASHINT4(b,i,Uid.to_int l.HNode.id, Uid.to_int r.HNode.id) end ;; @@ -79,7 +79,7 @@ struct | _ -> false let mem (k:elt) n = - let kid = H.uid k in + let kid = Uid.to_int (H.uid k) in let rec loop n = match HNode.node n with | Empty -> false | Leaf j -> k == j @@ -142,10 +142,10 @@ END let match_prefix k p m = (mask k m) == p let add k t = - let kid = H.uid k in + let kid = Uid.to_int (H.uid k) in let rec ins n = match HNode.node n with | Empty -> leaf k - | Leaf j -> if j == k then n else join kid (leaf k) (H.uid j) n + | Leaf j -> if j == k then n else join kid (leaf k) (Uid.to_int (H.uid j)) n | Branch (p,m,t0,t1) -> if match_prefix kid p m then if zero_bit kid m then @@ -158,7 +158,7 @@ END ins t let remove k t = - let kid = H.uid k in + let kid = Uid.to_int(H.uid k) in let rec rmv n = match HNode.node n with | Empty -> empty | Leaf j -> if k == j then empty else n @@ -177,7 +177,7 @@ END let equal a b = HNode.equal a b - let compare a b = (HNode.uid a) - (HNode.uid b) + let compare a b = (Uid.to_int (HNode.uid a)) - (Uid.to_int (HNode.uid b)) let rec merge s t = if (equal s t) (* This is cheap thanks to hash-consing *) @@ -386,8 +386,8 @@ struct include Make ( struct type t = int type data = t external hash : t -> int = "%identity" - external uid : t -> int = "%identity" - let equal : t -> t -> bool = (==) + external uid : t -> Uid.t = "%identity" + external equal : t -> t -> bool = "%eq" external make : t -> int = "%identity" external node : t -> int = "%identity" diff --git a/ptset.mli b/ptset.mli index 3b46f5c..fc95d4e 100644 --- a/ptset.mli +++ b/ptset.mli @@ -63,7 +63,7 @@ val intersect : t -> t -> bool val is_singleton : t -> bool val mem_union : t -> t -> t val hash : t -> int -val uid : t -> int +val uid : t -> Uid.t val uncons : t -> elt * t val from_list : elt list -> t val make : data -> t @@ -75,4 +75,5 @@ module Int : sig include S with type elt = int val print : Format.formatter -> t -> unit end + module Make ( H : Hcons.S ) : S with type elt = H.t diff --git a/tree.ml b/tree.ml index b6efb67..a034636 100644 --- a/tree.ml +++ b/tree.ml @@ -179,17 +179,17 @@ module MemUnion = Hashtbl.Make (struct let equal (x,y) (z,t) = x == z || y == t let equal a b = equal a b || equal b a let hash (x,y) = (* commutative hash *) - let x = Ptset.Int.uid x - and y = Ptset.Int.uid y + let x = Uid.to_int (Ptset.Int.uid x) + and y = Uid.to_int (Ptset.Int.uid y) in - if x <= y then HASHINT2(x,y) else HASHINT2(y,x) + if x <= y then HASHINT2(x,y) else HASHINT2(y,x) end) module MemAdd = Hashtbl.Make ( struct type t = Tag.t*Ptset.Int.t let equal (x,y) (z,t) = (x == z)&&(y == t) - let hash (x,y) = HASHINT2(x,Ptset.Int.uid y) + let hash (x,y) = HASHINT2(x,Uid.to_int (Ptset.Int.uid y)) end) module MemUpdate = struct @@ -198,7 +198,11 @@ include Hashtbl.Make ( type t = Tag.t*Ptset.Int.t*Ptset.Int.t*Ptset.Int.t*Ptset.Int.t let equal (a1,b1,c1,d1,e1) (a2,b2,c2,d2,e2) = a1==a2 && b1 == b2 && c1 == c2 && d1 == d2 && e1 == e2 - let hash (a,b,c,d,e) = HASHINT4(HASHINT2(a,Ptset.Int.uid b),Ptset.Int.uid c,Ptset.Int.uid d,Ptset.Int.uid e) + let hash (a,b,c,d,e) = + HASHINT4(HASHINT2(a,Uid.to_int (Ptset.Int.uid b)), + Uid.to_int (Ptset.Int.uid c), + Uid.to_int (Ptset.Int.uid d), + Uid.to_int (Ptset.Int.uid e)) end) end diff --git a/uid.ml b/uid.ml new file mode 100644 index 0000000..bb0fb18 --- /dev/null +++ b/uid.ml @@ -0,0 +1,8 @@ +type t = int + +let _id = ref ~-1 + +let make () = incr _id; !_id + +external to_int : t -> int = "%identity" + diff --git a/uid.mli b/uid.mli new file mode 100644 index 0000000..235869a --- /dev/null +++ b/uid.mli @@ -0,0 +1,3 @@ +type t = private int +val make : unit -> t +external to_int : t -> int = "%identity" -- 2.17.1