Commit f321c02d authored by Pietro Abate's avatar Pietro Abate
Browse files

[r2003-03-22 21:56:53 by cvscast] Empty log message

Original author: cvscast
Date: 2003-03-22 21:57:06+00:00
parent 5c81c7c7
type 'a obj = { id : int; mutable v : 'a }
type 'a t =
| True
| False
| Split of 'a obj * 'a t * 'a t * 'a t
let rec equal a b =
(a == b) ||
match (a,b) with
| Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) ->
(x1.id = x2.id) && (equal p1 p2) & (equal i1 i2) &&
(equal n1 n2)
| _ -> false
let rec compare a b =
if (a == b) then 0
else match (a,b) with
| Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) ->
if x1.id < x2.id then -1
else if x1.id > x2.id then 1
else let c = compare p1 p2 in if c <> 0 then c
else let c = compare i1 i2 in if c <> 0 then c
else compare n1 n2
| True,_ -> -1
| _, True -> 1
| False,_ -> -1
| _,False -> 1
let rec hash = function
| True -> 1
| False -> 2
| Split (x, p,i,n) ->
x.id + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
let rec iter f = function
| Split (x, p,i,n) -> f x.v; iter f p; iter f i; iter f n
| _ -> ()
module type ARG =
sig
type 'a t
val dump: Format.formatter -> 'a t -> unit
val equal: 'a t -> 'a t -> bool
val hash: 'a t -> int
val compare: 'a t -> 'a t -> int
end
module type S =
sig
type 'a elem
type 'a t
val dump: Format.formatter -> 'a t -> unit
val equal : 'a t -> 'a t -> bool
val compare: 'a t -> 'a t -> int
val hash: 'a t -> int
val get: 'a t -> ('a elem list * 'a elem list) list
val empty : 'a t
val full : 'a t
val cup : 'a t -> 'a t -> 'a t
val cap : 'a t -> 'a t -> 'a t
val diff : 'a t -> 'a t -> 'a t
val atom : 'a elem -> 'a t
val iter: ('a elem-> unit) -> 'a t -> unit
val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b)
-> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
atom:('a elem -> 'b) -> 'a t -> 'b
val print: string -> (Format.formatter -> 'a elem -> unit) -> 'a t ->
(Format.formatter -> unit) list
end
module Make(X : ARG) =
struct
type 'a elem = 'a X.t
type 'a t =
| True
| False
| Split of int * 'a elem * 'a t * 'a t * 'a t
let rec equal a b =
(a == b) ||
match (a,b) with
| Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
(h1 == h2) &&
(X.equal x1 x2) && (equal p1 p2) & (equal i1 i2) &&
(equal n1 n2)
| _ -> false
let rec compare a b =
if (a == b) then 0
else match (a,b) with
| Split (h1,x1, p1,i1,n1), Split (h2,x2, p2,i2,n2) ->
if h1 < h2 then -1 else if h1 > h2 then 1
else let c = X.compare x1 x2 in if c <> 0 then c
else let c = compare p1 p2 in if c <> 0 then c
else let c = compare i1 i2 in if c <> 0 then c
else compare n1 n2
| True,_ -> -1
| _, True -> 1
| False,_ -> -1
| _,False -> 1
(* TODO: precompute hash value for Split node to have fast equality... *)
(*
let rec print f ppf = function
| True -> Format.fprintf ppf "True"
| False -> Format.fprintf ppf "False"
| Split (x, p,i,n) ->
Format.fprintf ppf "%a(@[%a,%a,%a@])"
f x.v (print f) p (print f) i (print f) n
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
| Split(h, _,_,_,_) -> h
let compute_hash x p i n =
(X.hash x) + 17 * (hash p) + 257 * (hash i) + 16637 * (hash n)
let atom x =
let h = X.hash x + 17 in (* partial evaluation of compute_hash... *)
Split (h, x,True,False,False)
let rec iter f = function
| Split (_, x, p,i,n) -> f x; iter f p; iter f i; iter f n
| _ -> ()
(* TODO: precompute hash value for Split node to have fast equality... *)
let rec dump ppf = function
| True -> Format.fprintf ppf "+"
| False -> Format.fprintf ppf "-"
| Split (_,x, p,i,n) ->
Format.fprintf ppf "%a(@[%a,%a,%a@])"
X.dump x dump p dump i dump n
let rec print f ppf = function
| True -> Format.fprintf ppf "Any"
| False -> Format.fprintf ppf "Empty"
| Split (x, p,i, n) ->
(* Format.fprintf ppf "{%i}" x.id; *)
let flag = ref false in
let b () = if !flag then Format.fprintf ppf " | " else flag := true in
(match p with
| True -> b(); Format.fprintf ppf "%a" f x.v
| False -> ()
| _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x.v (print f) p );
(match i with
| True -> assert false;
| False -> ()
| _ -> b(); print f ppf i);
(match n with
| True -> b (); Format.fprintf ppf "@[~%a@]" f x.v
| False -> ()
| _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x.v (print f) n)
let rec dump ppf = function
| True -> Format.fprintf ppf "True"
| False -> Format.fprintf ppf "False"
| Split (x, p,i,n) ->
Format.fprintf ppf "%i(@[%a,%a,%a@])"
x.id dump p dump i dump n
let rec dnf accu pos neg = function
| True -> (pos,neg) :: accu
| False -> accu
| Split (x, p,i,n) ->
let accu = dnf accu (x.v::pos) neg p in
let accu = dnf accu pos (x.v::neg) n in
let accu = dnf accu pos neg i in
accu
let dnf x = dnf [] [] [] x
let compute ~empty ~any ~cup ~cap ~diff ~atom b =
let rec aux = function
| True -> any
| False -> empty
| Split(x, p,i,n) ->
let p = cap (atom x.v) (aux p)
and i = aux i
and n = diff (aux p) (atom x.v) in
cup (cup p i) n
in
aux b
let rec print f ppf = function
| True -> Format.fprintf ppf "Any"
| False -> Format.fprintf ppf "Empty"
| Split (_, x, p,i, n) ->
let flag = ref false in
let b () = if !flag then Format.fprintf ppf " | " else flag := true in
(match p with
| True -> b(); Format.fprintf ppf "%a" f x
| False -> ()
| _ -> b (); Format.fprintf ppf "%a & @[(%a)@]" f x (print f) p );
(match i with
| True -> assert false;
| False -> ()
| _ -> b(); print f ppf i);
(match n with
| True -> b (); Format.fprintf ppf "@[~%a@]" f x
| False -> ()
| _ -> b (); Format.fprintf ppf "@[~%a@] & @[(%a)@]" f x (print f) n)
let print a f = function
| True -> [ fun ppf -> Format.fprintf ppf "%s" a ]
| False -> []
| c -> [ fun ppf -> print f ppf c ]
let rec get accu pos neg = function
| True -> (pos,neg) :: accu
| False -> accu
| Split (_,x, p,i,n) ->
let accu = get accu (x::pos) neg p in
let accu = get accu pos (x::neg) n in
let accu = get accu pos neg i in
accu
let get x = get [] [] [] x
let compute ~empty ~full ~cup ~cap ~diff ~atom b =
let rec aux = function
| True -> full
| False -> empty
| Split(_,x, p,i,n) ->
let p = cap (atom x) (aux p)
and i = aux i
and n = diff (aux p) (atom x) in
cup (cup p i) n
in
aux b
(* Invariant: correct hash value *)
let split x pos ign neg =
Split (compute_hash x pos ign neg, x, pos, ign, neg)
let empty = False
let full = True
(* Invariants:
Split (x, pos,ign,neg) ==> (ign <> True);
(pos <> False or neg <> False)
Other meaningful invariant that could be enforced:
- pos <> neg
- no ``subsumption'' --> DONE (cf below)
*)
let split x pos ign neg =
if ign = True then True
else if (pos = False) && (neg = False) then ign
else Split (x, pos, ign, neg)
let split x pos ign neg =
if ign = True then True
else if (pos = False) && (neg = False) then ign
else split x pos ign neg
let ( !! ) x = Split (x, True, False, False)
let empty = False
let any = True
let rec simplify a l =
(* Format.fprintf Format.std_formatter "simplify %a <=" dump a;
List.iter (fun b -> Format.fprintf Format.std_formatter " %a" dump b) l;
Format.fprintf Format.std_formatter "@\n";
(* Invariant:
- no ``subsumption'
*)
if (a = False) then False else simpl_aux1 a [] l
and simpl_aux1 a accu = function
let rec simplify a l =
if (a = False) then False else simpl_aux1 a [] l
and simpl_aux1 a accu = function
| [] ->
if accu = [] then a else
(match a with
| True -> True
| False -> assert false
| Split (x,p,i,n) -> simpl_aux2 x p i n [] [] [] accu)
(match a with
| True -> True
| False -> assert false
| Split (_,x,p,i,n) -> simpl_aux2 x p i n [] [] [] accu)
| False :: l -> simpl_aux1 a accu l
| True :: l -> False
| b :: l -> if a == b then False else simpl_aux1 a (b::accu) l
and simpl_aux2 x p i n ap ai an = function
| [] -> split x (simplify p ap) (simplify i ai) (simplify n an)
| (Split (x2,p2,i2,n2) as b) :: l ->
if x2.id < x.id then
simpl_aux3 x p i n ap ai an l i2
else if x.id < x2.id then
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
| _ -> assert false
and simpl_aux3 x p i n ap ai an l = function
| False -> simpl_aux2 x p i n ap ai an l
| True -> assert false
| Split (x2,p2,i2,n2) as b ->
if x2.id < x.id then
simpl_aux3 x p i n ap ai an l i2
else if x.id < x2.id then
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])
let rec ( ++ ) a b =
if a == b then a
else match (a,b) with
| True, _ | _, True -> True
| False, a | a, False -> a
| Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) ->
if x1.id = x2.id then
split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2)
else if x1.id < x2.id then
split x1 p1 (i1 ++ b) n1
else
split x2 p2 (i2 ++ a) n2
(* TODO: optimize the cup with 3 arguments ? *)
let rec ( ** ) a b =
if a == b then a
else match (a,b) with
| True, a | a, True -> a
| False, _ | _, False -> False
| Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) ->
if x1.id = x2.id then
split x1
((p1 ** p2) ++ (p1 ** i2) ++ (p2 ** i1))
(i1 ** i2)
((n1 ** n2) ++ (n1 ** i2) ++ (n2 ** i1))
else if x1.id < x2.id then
split x1 (p1 ** b) (i1 ** b) (n1 ** b)
and simpl_aux2 x p i n ap ai an = function
| [] -> split x (simplify p ap) (simplify i ai) (simplify n an)
| (Split (_,x2,p2,i2,n2) as b) :: l ->
let c = X.compare x2 x in
if c < 0 then
simpl_aux3 x p i n ap ai an l i2
else if c > 0 then
simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
else
split x2 (p2 ** a) (i2 ** a) (n2 ** a)
let rec ( // ) a b =
if a == b then False
else match (a,b) with
| False,_ | _, True -> False
| a, False -> a
| True, Split (x2, p2,i2,n2) ->
let i = True // i2 in
split x2 (i // p2) False (i // n2)
| Split (x1, p1,i1,n1), Split (x2, p2,i2,n2) ->
if x1.id = x2.id then
let i = i1 // i2 in
split x1
((p1 // p2 // i2) ++ (i // p2))
False
((n1 // n2 // i2) ++ (i // n2))
else if x1.id < x2.id then
split x1 (p1 // b) (i1 // b) (n1 // b)
simpl_aux2 x p i n (p2 :: i2 :: ap) (i2 :: ai) (n2 :: i2 :: an) l
| _ -> assert false
and simpl_aux3 x p i n ap ai an l = function
| False -> simpl_aux2 x p i n ap ai an l
| True -> assert false
| Split (_,x2,p2,i2,n2) as b ->
let c = X.compare x2 x in
if c < 0 then
simpl_aux3 x p i n ap ai an l i2
else if c > 0 then
simpl_aux2 x p i n (b :: ap) (b :: ai) (b :: an) l
else
let i = a // i2 in
split x2 (i // p2) False (i // n2)
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])
let rec ( ++ ) a b =
if a == b then a
else match (a,b) with
| True, _ | _, True -> True
| False, a | a, False -> a
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
split x1 (p1 ++ p2) (i1 ++ i2) (n1 ++ n2)
else if c < 0 then
split x1 p1 (i1 ++ b) n1
else
split x2 p2 (i2 ++ a) n2
(* Pseudo-Invariant:
- pos <> neg
*)
let split x pos ign neg =
if equal pos neg then (neg ++ ign) else split x pos ign neg
(* seems better not to make ++ and this split mutually recursive;
is the invariant still inforced ? *)
let rec ( ** ) a b =
if a == b then a
else match (a,b) with
| True, a | a, True -> a
| False, _ | _, False -> False
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
(* split x1
(p1 ** (p2 ++ i2) ++ (p2 ** i1))
(i1 ** i2)
(n1 ** (n2 ++ i2) ++ (n2 ** i1))
*)
split x1
((p1 ++ i1) ** (p2 ++ i2))
False
((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 neg = function
| True -> False
| False -> True
(* | Split (_,x, p,i,False) -> split x False (neg (i ++ p)) (neg i)
| Split (_,x, False,i,n) -> split x (neg i) (neg (i ++ n)) False
| Split (_,x, p,False,n) -> split x (neg p) (neg (p ++ n)) (neg n) *)
| Split (_,x, p,i,n) -> split x (neg (i ++ p)) False (neg (i ++ n))
let rec ( // ) a b =
if a == b then False
else match (a,b) with
| False,_ | _, True -> False
| a, False -> a
| True, b -> neg b
| Split (_,x1, p1,i1,n1), Split (_,x2, p2,i2,n2) ->
let c = X.compare x1 x2 in
if c = 0 then
split x1
((p1 ++ i1) // (p2 ++ i2))
False
((n1 ++ i1) // (n2 ++ i2))
else if c < 0 then
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))
let cup = ( ++ )
let cap = ( ** )
let diff = ( // )
let diff x y =
(* 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
end
type 'a obj = { id : int; mutable v : 'a }
module type ARG =
sig
type 'a t
val dump: Format.formatter -> 'a t -> unit
type 'a t (* = True | False | Split of 'a obj * 'a t * 'a t * 'a t *)
val equal: 'a t -> 'a t -> bool
val hash: 'a t -> int
val compare: 'a t -> 'a t -> int
end
val equal : 'a t -> 'a t -> bool
val compare: 'a t -> 'a t -> int
val hash: 'a t -> int
module type S =
sig
type 'a elem
type 'a t
val iter: ('a -> unit) -> ('a t -> unit)
val dump: Format.formatter -> 'a t -> unit
val print :
(Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
val dump : Format.formatter -> 'a t -> unit
val equal : 'a t -> 'a t -> bool
val compare: 'a t -> 'a t -> int
val hash: 'a t -> int
val dnf : 'a t -> ('a list * 'a list) list
val get: 'a t -> ('a elem list * 'a elem list) list
val compute: empty:'b -> any:'b -> cup:('b -> 'b -> 'b)
-> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
atom:('a -> 'b) -> 'a t -> 'b
val empty : 'a t
val full : 'a t
val cup : 'a t -> 'a t -> 'a t
val cap : 'a t -> 'a t -> 'a t
val diff : 'a t -> 'a t -> 'a t
val atom : 'a elem -> 'a t
val empty : 'a t
val any : 'a t
val ( !! ) : 'a obj -> 'a t
val ( ++ ) : 'a t -> 'a t -> 'a t
val ( ** ) : 'a t -> 'a t -> 'a t
val ( // ) : 'a t -> 'a t -> 'a t
val iter: ('a elem-> unit) -> 'a t -> unit
val compute: empty:'b -> full:'b -> cup:('b -> 'b -> 'b)
-> cap:('b -> 'b -> 'b) -> diff:('b -> 'b -> 'b) ->
atom:('a elem -> 'b) -> 'a t -> 'b
val print: string -> (Format.formatter -> 'a elem -> unit) -> 'a t ->
(Format.formatter -> unit) list
end
module Make(X : ARG) : S with type 'a elem = 'a X.t
......@@ -463,7 +463,6 @@ let fun do_table (X_table -> String) _ -> raise "<table> nothandled";;
do_tbodies
*)
match load_xml "tst_html2latex.xml" with
| x & X_html -> print (do_html x)
| _ -> raise "Input file is not XHTML !";;
......
......@@ -3,6 +3,7 @@ type v = AtomPool.t
let value = AtomPool.value
let mk = AtomPool.mk
let vcompare = AtomPool.compare
let vhash = AtomPool.hash
module SList = SortedList.Make_transp(SortedList.Lift(AtomPool))
type t = Finite of unit SList.t | Cofinite of unit SList.t
......
......@@ -3,6 +3,7 @@ val value: v -> string
val mk: string -> v
val print_v: Format.formatter -> v -> unit
val vcompare: v -> v -> int
val vhash: v -> int
type t
......
......@@ -26,6 +26,8 @@ let print_v_in_string ppf c =
let vcompare (v1:int) v2 =
if v1 = v2 then 0 else if v1 < v2 then -1 else 1
let vhash i = i
type t = (v * v) list
......
......@@ -6,6 +6,7 @@ val to_char: v -> char
val print_v : Format.formatter -> v -> unit
val print_v_in_string : Format.formatter -> v -> unit