Commit 85f7543f by Pietro Abate

### [r2003-04-02 12:34:22 by cvscast] Empty log message

```Original author: cvscast
Date: 2003-04-02 12:34:22+00:00```
 ... ... @@ -36,6 +36,8 @@ sig val print: string -> (Format.formatter -> 'a elem -> unit) -> 'a t -> (Format.formatter -> unit) list val trivially_disjoint: 'a t -> 'a t -> bool end module Make(X : ARG) = ... ... @@ -74,13 +76,6 @@ struct | _,False -> 1 (* let rec hash = function | True -> 1 | False -> 2 | Split (x, p,i,n) -> (X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n) *) let rec hash = function | True -> 1 | False -> 0 ... ... @@ -180,6 +175,7 @@ struct - no ``subsumption' *) (* let rec simplify a b = if equal a b then False else match (a,b) with ... ... @@ -204,7 +200,9 @@ struct if (p1 != p1') || (n1 != n1') || (i1 != i1') then split x1 p1' i1' n1' else a (* *) let rec simplify a l = if (a = False) then False else simpl_aux1 a [] l and simpl_aux1 a accu = function ... ... @@ -239,10 +237,12 @@ struct simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l else simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l *) let split x p i n = split x (simplify p i) i (simplify n i) split x (simplify p [i]) i (simplify n [i]) let rec ( ++ ) a b = (* if equal a b then a *) ... ... @@ -270,8 +270,8 @@ struct is the invariant still inforced ? *) let rec ( ** ) a b = (* if equal a b then a *) if a == b then a (* if equal a b then a *) if a == b then a else match (a,b) with | True, a | a, True -> a | False, _ | _, False -> False ... ... @@ -281,17 +281,36 @@ struct (* split x1 (p1 ** (p2 ++ i2) ++ (p2 ** i1)) (i1 ** i2) (n1 ** (n2 ++ i2) ++ (n2 ** i1)) *) (n1 ** (n2 ++ i2) ++ (n2 ** i1)) *) split x1 ((p1 ++ i1) ** (p2 ++ i2)) False ((n1 ++ i1) ** (n2 ++ i2)) ((n1 ++ i1) ** (n2 ++ i2)) else if c < 0 then split x1 (p1 ** b) (i1 ** b) (n1 ** b) else split x2 (p2 ** a) (i2 ** a) (n2 ** a) let rec trivially_disjoint a b = if a == b then a = False else match (a,b) with | True, a | a, True -> a = False | False, _ | _, False -> true | Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) -> let c = X.compare x1 x2 in if c = 0 then (* try expanding -> p1 p2; p1 i2; i1 p2; i1 i2 ... *) trivially_disjoint (p1 ++ i1) (p2 ++ i2) && trivially_disjoint (n1 ++ i1) (n2 ++ i2) else if c < 0 then trivially_disjoint p1 b && trivially_disjoint i1 b && trivially_disjoint n1 b else trivially_disjoint p2 a && trivially_disjoint i2 a && trivially_disjoint n2 a let rec neg = function | True -> False | False -> True ... ... @@ -301,8 +320,8 @@ struct | Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n)) let rec ( // ) a b = (* if equal a b then False *) if a == b then False (* if equal a b then False *) if a == b then False else match (a,b) with | False,_ | _, True -> False | a, False -> a ... ... @@ -315,7 +334,7 @@ struct False ((n1 ++ i1) // (n2 ++ i2)) else if c < 0 then split x1 (p1 // b) (i1 // b) (n1 // b) split x1 (p1 // b) (i1 // b) (n1 // b) (* split x1 ((p1 ++ i1)// b) False ((n1 ++i1) // b) *) else split x2 (a // (i2 ++ p2)) False (a // (i2 ++ n2)) ... ... @@ -325,9 +344,17 @@ struct let cap = ( ** ) let diff = ( // ) (* let diff x y = (* let d = diff x y in let d = diff x y in Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX\\Z = %a@\n" dump x dump y dump d; *) diff x y dump x dump y dump d; d let cap x y = let d = cap x y in Format.fprintf Format.std_formatter "X = %a@\nY = %a@\nX**Z = %a@\n" dump x dump y dump d; d *) end
 ... ... @@ -13,6 +13,7 @@ sig type 'a elem type 'a t val dump: Format.formatter -> 'a t -> unit val equal : 'a t -> 'a t -> bool ... ... @@ -36,6 +37,8 @@ sig val print: string -> (Format.formatter -> 'a elem -> unit) -> 'a t -> (Format.formatter -> unit) list val trivially_disjoint : 'a t -> 'a t -> bool end module Make(X : ARG) : S with type 'a elem = 'a X.t
 ... ... @@ -132,6 +132,7 @@ let fun do_table (Xtable -> String) _ -> raise " nothandled";; do_tbodies *) match load_xml "tst_html2latex.xml" with | x & Xhtml -> print (do_html x) | _ -> raise "Input file is not XHTML !";; ... ...
 ... ... @@ -38,6 +38,14 @@ let contains x = function | Finite s -> SList.mem s x | Cofinite s -> not (SList.mem s x) let disjoint s t = match (s,t) with | (Finite s, Finite t) -> SList.disjoint s t | (Finite s, Cofinite t) -> SList.subset s t | (Cofinite s, Finite t) -> SList.subset t s | (Cofinite s, Cofinite t) -> false let is_empty = function | Finite [] -> true | _ -> false ... ...
 ... ... @@ -21,6 +21,7 @@ val diff : t -> t -> t val atom : v -> t val contains : v -> t -> bool val disjoint : t -> t -> bool val is_empty : t -> bool val is_atom : t -> v option val sample : t -> v ... ...
 ... ... @@ -30,7 +30,8 @@ sig val print: string -> (Format.formatter -> 'a elem -> unit) -> 'a t -> (Format.formatter -> unit) list val trivially_disjoint : 'a t -> 'a t -> bool val check: 'a t -> unit end ... ... @@ -195,6 +196,8 @@ let print any f = ) ) let trivially_disjoint a b = cap a b = [] let check b = () (* SSList.check b; ... ...
 ... ... @@ -39,6 +39,7 @@ sig (Format.formatter -> unit) list val trivially_disjoint : 'a t -> 'a t -> bool val check: 'a t -> unit end ... ...
 ... ... @@ -83,6 +83,15 @@ let diff i1 i2 = neg (cup (neg i1) i2) let is_empty i = i = [] let rec disjoint (a : t) b = match (a,b) with | [],_ | _,[] -> true | (xa,ya)::a', (xb,yb)::b' -> if xa = xb then false else if xa < xb then (ya < xb) && (disjoint a' b) else (yb < xa) && (disjoint a b') let contains n = List.exists (fun (a,b) -> (n>=a) && (n<=b)) let sample = function ... ...
 ... ... @@ -21,7 +21,7 @@ val diff : t -> t -> t val char_class : v -> v -> t val atom : v -> t val disjoint : t -> t -> bool val is_empty : t -> bool val contains : v -> t -> bool val sample : t -> v ... ...
 open Big_int (* Hack to compute hash value for bigints *) let hash_nat x = Nat.nth_digit_nat x 0 let hash_bigint (sign,nat) = sign * 17 + hash_nat nat type v = big_int let print_v ppf i = Format.fprintf ppf "%s" (string_of_big_int i) let vcompare = compare_big_int let vhash = num_digits_big_int (* improve this *) let vhash x = hash_bigint (Obj.magic x) (* num_digits_big_int x *) (* improve this *) let mk = big_int_of_string let vadd = add_big_int let vmult = mult_big_int ... ... @@ -128,6 +133,25 @@ let diff i1 i2 = let is_empty = function [] -> true | _ -> false let rec disjoint a b = match (a,b) with | [],_ | _,[] -> true | Any::_,_ | _,Any::_ -> false | Left _::_, Left _::_ -> false | Right _::_, Right _::_ -> false | Left x :: a, Bounded (y,_) :: _ -> (lt_big_int x y) && (disjoint a b) | Bounded (y,_) :: _, Left x :: b -> (lt_big_int x y) && (disjoint a b) | Left x :: _, Right y :: _ -> lt_big_int x y | Right y :: _, Left x :: _ -> lt_big_int x y | Right y :: _, Bounded (_,x) :: _ -> lt_big_int x y | Bounded (_,x) :: _, Right y :: _ -> lt_big_int x y | Bounded (xa,ya) :: a', Bounded (xb,yb) :: b' -> let c = compare_big_int xa xb in if c = 0 then false else if c < 0 then (lt_big_int ya xb) && (disjoint a' b) else (lt_big_int yb xa) && (disjoint a b') (* TODO: can optimize this to stop running through the list earlier *) let contains n = ... ... @@ -211,10 +235,11 @@ let dump s i = let diff i1 i2 = let ppf = Format.std_formatter in Format.fprintf ppf "Intervals.diff."; Format.fprintf ppf "Intervals.diff:"; dump "i1" i1; dump "i2" i2; dump "~i1|i2" (cup (neg i1) i2); dump "i1-i2" (diff i1 i2); Format.fprintf ppf "@\n"; diff i1 i2 *)
 ... ... @@ -28,6 +28,7 @@ val left : v -> t val right : v -> t val atom : v -> t val disjoint : t -> t -> bool val is_empty : t -> bool val contains : v -> t -> bool val sample : t -> v ... ...
 ... ... @@ -12,6 +12,7 @@ end type 'a bool = ('a list * 'a list) list (* module Make(X1 : S)(X2 : S) = struct type t = (X1.t * X2.t) list ... ... @@ -59,17 +60,18 @@ struct let line res (p,n) = let (d1,d2) = bigcap p in if not ((X1.is_empty d1) || (X2.is_empty d2)) then (let resid = ref d1 in (let resid = ref X1.empty in List.iter (fun (t1,t2) -> let t1 = X1.cap d1 t1 in if not (X1.is_empty t1) then (resid := X1.diff !resid t1; (resid := X1.cup !resid t1; let t2 = X2.diff d2 t2 in if not (X2.is_empty t2) then add res t1 t2 !res ) ) (normal n); if not (X1.is_empty !resid) then add res !resid d2 !res) let d1 = X1.diff d1 !resid in if not (X1.is_empty d1) then add res d1 d2 !res) let boolean_normal x = let res = ref (Obj.magic 0) in ... ... @@ -94,3 +96,71 @@ struct if X1.is_empty (X1.cap t1 restr) then accu else X2.cup accu t2) X2.empty end *) module Make(X1 : S)(X2 : S) = struct type t = (X1.t * X2.t) list (* Possible optimizations: - check whether t1 or t2 is empty initially - check s1 = t1 (structural equility) *) let rec add root t1 t2 = function | [] -> (t1,t2) :: root | (s1,s2) :: rem -> let i = X1.cap t1 s1 in if X1.is_empty i then add ((s1,s2)::root) t1 t2 rem else ( let root = (i, X2.cup t2 s2) :: root in let k = X1.diff s1 t1 in let root = if not (X1.is_empty k) then (k, s2) :: root else root in let j = X1.diff t1 s1 in if not (X1.is_empty j) then add root j t2 rem else root ) let normal x = List.fold_left (fun accu (t1,t2) -> add [] t1 t2 accu) [] x let rec bigcap_aux t1 t2 = function | (s1,s2)::rem -> bigcap_aux (X1.cap t1 s1) (X2.cap t2 s2) rem | [] -> (t1,t2) let bigcap = bigcap_aux X1.any X2.any (* optimize: one knows that the t1 are pairwise disjoint ... *) let line accu (p,n) = let (d1,d2) = bigcap p in if not ((X1.is_empty d1) || (X2.is_empty d2)) then (let resid = ref X1.empty in let accu = List.fold_left (fun accu (t1,t2) -> let i = X1.cap d1 t1 in if not (X1.is_empty i) then (resid := X1.cup !resid t1; let t2 = X2.diff d2 t2 in if not (X2.is_empty t2) then add [] i t2 accu else accu ) else accu ) accu (normal n) in let d1 = X1.diff d1 !resid in if not (X1.is_empty d1) then add [] d1 d2 accu else accu) else accu let boolean_normal x = List.fold_left line [] x let boolean x = List.fold_left (fun accu x -> (line [] x) @ accu) [] x let pi1 = List.fold_left (fun accu (t1,t2) -> X1.cup accu t1) X1.empty let pi2 = List.fold_left (fun accu (t1,t2) -> X2.cup accu t2) X2.empty let pi2_restricted restr = List.fold_left (fun accu (t1,t2) -> if X1.is_empty (X1.cap t1 restr) then accu else X2.cup accu t2) X2.empty end
 ... ... @@ -206,6 +206,7 @@ module Normal : sig nrecord: record; } val dummy: t val compare_nf: t -> t -> int val any_basic: Types.descr ... ... @@ -360,6 +361,7 @@ struct | Some l -> RecLabel (l,NLineProd.empty) | None -> RecNolabel (None,None)) } let dummy = nempty None let ncup nf1 nf2 = ... ... @@ -745,6 +747,12 @@ struct let cur_id = State.ref "Patterns.cur_id" 0 (* TODO: save dispatchers ? *) module NfMap = Map.Make( struct type t = Normal.t let compare = Normal.compare_nf end) module DispMap = Map.Make( struct type t = Types.descr * Normal.t array ... ... @@ -881,15 +889,31 @@ struct ) LabelPool.dummy_max !accu in let lab = if lab= LabelPool.dummy_max then None else Some lab in let accu = List.map (fun (ty,pl,i,info) -> let p = Normal.normal lab ty pl in (p,[i, p.Normal.ncatchv, info])) !accu in (* eliminate this generic comparison *) let sorted = Array.of_list (SortedMap.from_list SortedList.cup accu) in let infos = Array.map snd sorted in let disp = dispatcher t (Array.map fst sorted) lab in let pats = ref NfMap.empty in let nb_p = ref 0 in List.iter (fun (ty,pl,i,info) -> let p = Normal.normal lab ty pl in let x = (i, p.Normal.ncatchv, info) in try let s = NfMap.find p !pats in s := x :: !s with Not_found -> pats := NfMap.add p (ref [x]) !pats; incr nb_p ) !accu; let infos = Array.make !nb_p [] in let ps = Array.make !nb_p Normal.dummy in let count = ref 0 in NfMap.iter (fun p l -> let i = !count in infos.(i) <- !l; ps.(i) <- p; count := succ i) !pats; assert( !nb_p = !count ); let disp = dispatcher t ps lab in let result (t,_,m) = let selected = Array.create (Array.length pl) [] in let add r (i, ncv, inf) = selected.(i) <- (r,ncv,inf) :: selected.(i) in ... ... @@ -1170,7 +1194,7 @@ struct let lab = if lab= LabelPool.dummy_max then None else Some lab in let pl = Array.of_list (List.map (fun p -> Normal.normal lab Types.Record.any_or_absent [p]) pl) in (List.map (fun p -> Normal.normal lab (*t*) Types.Record.any_or_absent [p]) pl) in show ppf t pl lab; Format.fprintf ppf "# compiled dispatchers: %i@\n" !cur_id ... ...
 ... ... @@ -225,6 +225,16 @@ let hash_descr a = let accu = if a.absent then accu+5 else accu in accu (* TODO: optimize disjoint check for boolean combinations *) let trivially_disjoint a b = (Chars.disjoint a.chars b.chars) && (Intervals.disjoint a.ints b.ints) && (Atoms.disjoint a.atoms b.atoms) && (BoolPair.trivially_disjoint a.times b.times) && (BoolPair.trivially_disjoint a.xml b.xml) && (BoolPair.trivially_disjoint a.arrow b.arrow) && (BoolRec.trivially_disjoint a.record b.record) module Descr = struct ... ... @@ -372,6 +382,7 @@ let set s = s.notify <- Nothing; raise NotEmpty let count_slot = ref 0 let rec big_conj f l n = match l with | [] -> set n ... ... @@ -396,12 +407,17 @@ and slot d = (not d.absent)) then slot_not_empty else try DescrHash.find memo d with Not_found -> (* incr count_slot; Printf.eprintf "%i;" !count_slot; *) (* Format.fprintf Format.std_formatter "Empty:%a@\n" !print_descr d; *) let s = { status = Maybe; active = false; notify = Nothing } in DescrHash.add memo d s; (try iter_s s check_times (BoolPair.get d.times); iter_s s check_times (BoolPair.get d.xml); (* Format.fprintf Format.std_formatter "check_times_bool:@[%a@]@\n" BoolPair.dump d.times; *) (* check_times_bool any any d.times s; *) iter_s s check_times (BoolPair.get d.times); iter_s s check_times (BoolPair.get d.xml); iter_s s check_arrow (BoolPair.get d.arrow); iter_s s check_record (get_record d.record); if s.active then marks := s :: !marks else s.status <- Empty; ... ... @@ -414,27 +430,61 @@ and check_times (left,right) s = flush stderr; *) let rec aux accu1 accu2 right s = match right with | (t1,t2)::right -> if trivially_empty (cap_t accu1 t1) || trivially_empty (cap_t accu2 t2) then ( let t1 = descr t1 and t2 = descr t2 in if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then ( aux accu1 accu2 right s ) else ( let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 right) s; let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s let accu1' = diff accu1 t1 in guard accu1' (aux accu1' accu2 right) s; let accu2' = diff accu2 t2 in guard accu2' (aux accu1 accu2' right) s (* let accu1 = cap accu1 t1 in (* TODO: approximation of cap ... *) let accu2' = diff accu2 t2 in guard accu1 (guard accu2' (aux accu1 accu2' right)) s *) ) | [] -> set s in (* if List.length right > 6 then ( Printf.eprintf "HEURISTIC\n"; flush stderr; let (accu1,accu2) = cap_product left in (* if List.length right > 6 then ( Printf.eprintf "HEURISTIC\n"; flush stderr; let (n1,n2) = cup_product right in let n1 = diff accu1 n1 and n2 = diff accu2 n2 in guard n1 set s; guard n2 set s; Printf.eprintf "HEURISTIC failed\n"; flush stderr; ); *) let (accu1,accu2) = cap_product left in Printf.eprintf "HEURISTIC failed\n"; flush stderr; ); *) guard accu1 (guard accu2 (aux accu1 accu2 right)) s (* and check_times_bool accu1 accu2 b s = match b with | BoolPair.True -> guard accu1 (guard accu2 set) s | BoolPair.False -> () | BoolPair.Split (_, (t1,t2), p,i,n) -> check_times_bool accu1 accu2 i s; let t1 = descr t1 and t2 = descr t2 in if (trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2) then check_times_bool accu1 accu2 n s else ( if p <> BoolPair.False then (let accu1 = cap accu1 t1 and accu2 = cap accu2 t2 in if not (trivially_empty accu1 || trivially_empty accu2) then check_times_bool accu1 accu2 p s); if n <> BoolPair.False then (let accu1' = diff accu1 t1 in check_times_bool accu1' accu2 n s; let accu2' = diff accu2 t2 in check_times_bool accu1 accu2' n s) ) *) and check_arrow (left,right) s = let single_right (s1,s2) s = let rec aux accu1 accu2 left s = match left with ... ... @@ -453,10 +503,9 @@ and check_record (labels,(oleft,left),rights) s = | [] -> set s | (oright,right)::rights -> let next = (oleft && (not oright)) || (* ggg... why ??? check this line *) (oleft && (not oright)) || exists (Array.length left) (fun i -> trivially_empty (cap left.(i) right.(i)))