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 (* 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) -> 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) *) 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 (* Invariant: - no ``subsumption' *) 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) | 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 -> 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 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 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