Commit 9c9b2bde authored by Pietro Abate's avatar Pietro Abate

[r2005-05-05 22:42:31 by afrisch] Empty log message

Original author: afrisch
Date: 2005-05-05 22:43:43+00:00
parent 93aa81c2
......@@ -24,7 +24,7 @@ sig
val trivially_disjoint: t -> t -> bool
end
module Make(X : Custom.T) =
module MakeOld(X : Custom.T) =
struct
type elem = X.t
type t =
......@@ -392,3 +392,181 @@ struct
d
*)
end
module Make(X : Custom.T) =
struct
type elem = X.t
type t =
| Zero
| One
| Branch of elem * t * t * int * t
type node = t
let neg = function
| Zero -> One | One -> Zero
| Branch (_,_,_,_,neg) -> neg
let id = function
| Zero -> 0
| One -> 1
| Branch (_,_,_,id,_) -> id
(* Internalization + detection of useless branching *)
let max_id = ref 2 (* Must be >= 2 *)
module W = Weak.Make(
struct
type t = node
let hash = function
| Zero | One -> assert false
| Branch (v,yes,no,_,_) ->
1 + 17*X.hash v + 257*(id yes) + 65537*(id no)
let equal x y = (x == y) || match x,y with
| Branch (v1,yes1,no1,id1,_), Branch (v2,yes2,no2,id2,_) ->
(id1 == 0 || id2 == 0) && X.equal v1 v2 &&
(yes1 == yes2) && (no1 == no2)
| _ -> assert false
end)
let table = W.create 16383
type branch =
{ v : X.t; yes : node; no : node; mutable id : int; neg : branch }
let mk v yes no =
if yes == no then yes
else
let rec pos = Branch (v,yes,no,0,Branch (v,neg yes,neg no,0,pos)) in
let x = W.merge table pos in
let pos : branch = Obj.magic x in
if (pos.id == 0)
then (let n = !max_id in
max_id := succ n;
pos.id <- n;
pos.neg.id <- (-n));
x
let atom v = mk v One Zero
let dummy = Obj.magic (ref 0)
let memo_size = 16383
let memo_keys = Array.make memo_size (Obj.magic dummy)
let memo_vals = Array.make memo_size (Obj.magic dummy)
let memo_occ = Array.make memo_size 0
let eg2 (x1,y1) (x2,y2) = x1 == x2 && y1 == y2
let rec cup x1 x2 = if (x1 == x2) then x1 else match x1,x2 with
| One, x | x, One -> One
| Zero, x | x, Zero -> x
| Branch (v1,yes1,no1,id1,neg1), Branch (v2,yes2,no2,id2,neg2) ->
if (x1 == neg2) then One
else
let k,h =
if id1<id2 then (x1,x2),id1+65537*id2 else (x2,x1),id2+65537*id1 in
let h = (h land max_int) mod memo_size in
let i = memo_occ.(h) in
let k' = memo_keys.(h) in
if (k' != dummy) && (eg2 k k')
then (memo_occ.(h) <- succ i; memo_vals.(h))
else
let r =
let c = X.compare v1 v2 in
if (c = 0) then mk v1 (cup yes1 yes2) (cup no1 no2)
else if (c < 0) then mk v1 (cup yes1 x2) (cup no1 x2)
else mk v2 (cup yes2 x1) (cup no2 x1) in
if (i = 0) then (memo_keys.(h) <- k; memo_vals.(h) <- r;
memo_occ.(h) <- 1)
else memo_occ.(h) <- pred i;
r
let cap x1 x2 = neg (cup (neg x1) (neg x2))
let diff x1 x2 = neg (cup (neg x1) x2)
let rec iter f = function
| Branch (x,p,n,_,_) -> f x; iter f p; iter f n
| _ -> ()
let rec dump ppf = function
| One -> Format.fprintf ppf "+"
| Zero -> Format.fprintf ppf "-"
| Branch (x,p,n,_,_) ->
Format.fprintf ppf "%a(@[%a,%a@])"
X.dump x dump p dump n
let rec print f ppf = function
| One -> Format.fprintf ppf "Any"
| Zero -> Format.fprintf ppf "Empty"
| Branch (x,p,n,_,_) ->
let flag = ref false in
let b () = if !flag then Format.fprintf ppf " | " else flag := true in
(match p with
| One -> b(); Format.fprintf ppf "%a" f x
| Zero -> ()
| _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
(match n with
| One -> b (); Format.fprintf ppf "@[~%a@]" f x
| Zero -> ()
| _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
let print a f = function
| One -> [ fun ppf -> Format.fprintf ppf "%s" a ]
| Zero -> []
| c -> [ fun ppf -> print f ppf c ]
let rec get accu pos neg = function
| One -> (pos,neg) :: accu
| Zero -> accu
| Branch (x,p,n,_,_) ->
(*OPT: can avoid creating this list cell when pos or neg =False *)
let accu = get accu (x::pos) neg p in
let accu = get accu pos (x::neg) n in
accu
let get x = get [] [] [] x
let compute ~empty ~full ~cup ~cap ~diff ~atom b =
let rec aux = function
| One -> full
| Zero -> empty
| Branch(x,p,n,_,_) ->
let p = cap (atom x) (aux p)
and n = diff (aux n) (atom x) in
cup p n
in
aux b
let empty = Zero
let full = One
let rec serialize t = function
| (Zero | One) as b ->
Serialize.Put.bool t true; Serialize.Put.bool t (b = One)
| Branch (x,p,n,_,_) ->
Serialize.Put.bool t false;
X.serialize t x;
serialize t p;
serialize t n
let rec deserialize t =
if Serialize.Get.bool t then
if Serialize.Get.bool t then One else Zero
else
let x = X.deserialize t in
let p = deserialize t in
let n = deserialize t in
let x = atom x in
cup (cap x p) (cap (neg x) n)
(* mk x p n is not ok, because order of keys might have changed!
OPT TODO: detect when this is ok *)
let trivially_disjoint x y = neg x == y
let compare x y = compare (id x) (id y)
let equal x y = x == y
let hash x = id x
let check x = ()
end
......@@ -24,6 +24,7 @@ sig
val trivially_disjoint : t -> t -> bool
end
module MakeOld(X : Custom.T) : S with type elem = X.t
module Make(X : Custom.T) : S with type elem = X.t
......@@ -392,7 +392,9 @@ end
let equal x y = Map.equal Y.equal x y
let check l = Map.check Y.check l
let dump ppf _ = Format.fprintf ppf "<SortedList.MakeMap>"
let dump ppf l =
List.iter (fun (x,y) ->
Format.fprintf ppf "(%a->%a)" X.dump x Y.dump y) l
let serialize t l =
Serialize.Put.list (Serialize.Put.pair X.serialize Y.serialize) t l
......
......@@ -259,8 +259,15 @@ struct
absent: bool
}
let dump ppf _ =
Format.fprintf ppf "<Types.Descr.t>"
let print_lst ppf =
List.iter (fun f -> f ppf; Format.fprintf ppf " |")
let dump ppf d =
Format.fprintf ppf "<types atoms(%a) times(%a) record(%a) xml(%a)>"
print_lst (Atoms.print d.atoms)
BoolPair.dump d.times
BoolRec.dump d.record
BoolPair.dump d.xml
let empty = {
hash = 0;
......@@ -375,7 +382,7 @@ end =
struct
type t = { id : int; comp_unit : CompUnit.t; mutable descr : Descr.t }
let check n = ()
let dump ppf n = failwith "Types.Node.dump"
let dump ppf n = Format.fprintf ppf "X%i" n.id
let hash x = x.id + 17 * x.comp_unit
let compare x y =
assert(x.id != y.id || x.comp_unit != y.comp_unit || x == y);
......@@ -857,7 +864,10 @@ let marks = ref []
let count_subtype = Stats.Counter.create "Subtyping internal loop"
let complex = ref 0
let rec slot d =
incr complex;
Stats.Counter.incr count_subtype;
if not ((Intervals.is_empty d.ints) &&
(Atoms.is_empty d.atoms) &&
......@@ -880,8 +890,8 @@ let rec slot d =
and check_times (left,right) s =
let rec aux accu1 accu2 right s = match right with
| (t1,t2)::right ->
let t1 = descr t1 and t2 = descr t2 in
| (n1,n2)::right ->
let t1 = descr n1 and t2 = descr n2 in
if trivially_disjoint accu1 t1 ||
trivially_disjoint accu2 t2 then (
aux accu1 accu2 right s )
......@@ -899,8 +909,8 @@ and check_times (left,right) s =
and check_xml (left,right) s =
let rec aux accu1 accu2 right s = match right with
| (t1,t2)::right ->
let t1 = descr t1 and t2 = descr t2 in
| (n1,n2)::right ->
let t1 = descr n1 and t2 = descr n2 in
if clearly_disjoint accu1 t1 ||
trivially_disjoint accu2 t2 then (
aux accu1 accu2 right s )
......@@ -983,6 +993,20 @@ let is_empty d =
if ClearlyEmpty.is_empty d then (Printf.eprintf "!\n"; true) else is_empty d
*)
(*
let is_empty d =
(* Format.fprintf Format.std_formatter "complex=%i@."
!complex; *)
if !complex = 0 then
(let r = is_empty d in
if !complex > 100 then
(let c = !complex in
Format.fprintf Format.std_formatter "is_empty (%i)@." c
(*Descr.dump (*!forward_print*) d*));
complex := 0; r)
else is_empty d
*)
let non_empty d =
not (is_empty d)
......
......@@ -29,11 +29,11 @@ the same as for OCaml (<tt>configure, make world, make install</tt>).
<ul>
<li><a
href="http://pauillac.inria.fr/~frisch/ocamlcduce/download/cduce-ocaml-0.0.1.tar.gz">Compiler,
version 0.0.1</a></li>
href="http://pauillac.inria.fr/~frisch/ocamlcduce/download/cduce-ocaml-0.0.2.tar.gz">Compiler,
version 0.0.2</a></li>
<li><a
href="http://pauillac.inria.fr/~frisch/ocamlcduce/download/xml-support-0.0.1.tar.gz">Support
library, version 0.0.1</a></li>
href="http://pauillac.inria.fr/~frisch/ocamlcduce/download/xml-support-0.0.2.tar.gz">Support
library, version 0.0.2</a></li>
</ul>
<p>
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment