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

Original author: afrisch
Date: 2005-05-05 22:43:43+00:00

misc/bool.ml

@@ -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

misc/bool.mli

@@ -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
 
 

types/sortedList.ml

@@ -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

types/types.ml

@@ -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)
 

web/ocaml.xml

@@ -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>