open Big_int type interval = | Bounded of big_int * big_int | Left of big_int | Right of big_int | Any type t = interval list let rec equal l1 l2 = (l1 == l2) || match (l1,l2) with | (Bounded (a1,b1) :: l1, Bounded (a2,b2) :: l2) -> (eq_big_int a1 a2) && (eq_big_int b1 b2) && (equal l1 l2) | (Left b1 :: l1, Left b2 :: l2) -> (eq_big_int b1 b2) && (equal l1 l2) | (Right a1 :: l1, Right a2 :: l2) -> (eq_big_int a1 a2) && (equal l1 l2) | (Any :: _, Any :: _) -> true | ([], []) -> true | _ -> false let hash = function | Bounded (a,b) :: _ -> 1 + 2 * (num_digits_big_int a) + 3 * (num_digits_big_int b) | Left b :: _ -> 3 * num_digits_big_int b | Right a :: _ -> 2 * (num_digits_big_int a) | Any :: _ -> 1234 | [] -> 0 let empty = [] let any = [Any] let atom a b = if le_big_int a b then [Bounded (a,b)] else empty let rec iadd_left l b = match l with | [] -> [Left b] | (Bounded (a1,_) | Right a1) :: _ when (lt_big_int b (pred_big_int a1)) -> Left b :: l | Bounded (_,b1) :: l' -> iadd_left l' (max_big_int b b1) | Left b1 :: _ when le_big_int b b1-> l | Left _ :: l' -> iadd_left l' b | _ -> any let rec iadd_bounded l a b = match l with | [] -> [Bounded (a,b)] | (Bounded (a1,_) | Right a1) :: _ when (lt_big_int b (pred_big_int a1)) -> Bounded (a,b) :: l | ((Bounded (_,b1) | Left b1) as i') :: l' when (lt_big_int (succ_big_int b1) a) -> i'::(iadd_bounded l' a b) | Bounded (a1,b1) :: l' -> iadd_bounded l' (min_big_int a a1) (max_big_int b b1) | Left b1 :: l' -> iadd_left l' b | Right a1 :: _ -> [Right (min_big_int a a1)] | Any :: _ -> any let rec iadd_right l a = match l with | [] -> [Right a] | ((Bounded (_,b1) | Left b1) as i') :: l' when (lt_big_int (succ_big_int b1) a) -> i'::(iadd_right l' a) | (Bounded (a1,_) | Right a1) :: _ -> [Right (min_big_int a a1)] | _ -> any let iadd l = function | Bounded (a,b) -> iadd_bounded l a b | Left b -> iadd_left l b | Right a -> iadd_right l a | Any -> any let rec neg' start l = match l with | [] -> [Right start] | Bounded (a,b) :: l' -> Bounded (start, pred_big_int a) :: (neg' (succ_big_int b) l') | Right a :: l' -> [Bounded (start, pred_big_int a)] | _ -> assert false let neg = function | Any :: _ -> [] | [] -> any | Left b :: l -> neg' (succ_big_int b) l | Right a :: _ -> [Left (pred_big_int a)] | Bounded (a,b) :: l -> Left (pred_big_int a) :: neg' (succ_big_int b) l let cup i1 i2 = List.fold_left iadd i1 i2 let cap i1 i2 = neg (cup (neg i1) (neg i2)) let diff i1 i2 = neg (cup (neg i1) i2) let is_empty = function [] -> true | _ -> false (* TODO: can optimize this to stop running through the list earlier *) let contains n = List.exists (function | Any -> true | Left b -> le_big_int n b | Right a -> le_big_int a n | Bounded (a,b) -> (le_big_int a n) && (le_big_int n b) ) let sample = function | (Left x | Right x | Bounded (x,_)) :: _ -> x | Any :: _ -> zero_big_int | [] -> raise Not_found let print = List.map (fun x ppf -> match x with | Any -> Format.fprintf ppf "Int" | Left b -> Format.fprintf ppf "*--%s" (string_of_big_int b) | Right a -> Format.fprintf ppf "%s--*" (string_of_big_int a) | Bounded (a,b) when eq_big_int a b -> Format.fprintf ppf "%s" (string_of_big_int a) | Bounded (a,b) -> Format.fprintf ppf "%s--%s" (string_of_big_int a) (string_of_big_int b) ) let (+) = add_big_int let add_inter i1 i2 = match (i1,i2) with | Bounded (a1,b1), Bounded (a2,b2) -> Bounded (a1+a2, b1+b2) | Bounded (_,b1), Left b2 | Left b1, Bounded (_,b2) | Left b1, Left b2 -> Left (b1+b2) | Bounded (a1,_), Right a2 | Right a1, Bounded (a2,_) | Right a1, Right a2 -> Right (a1+a2) | _ -> Any (* Optimize this ... *) let add l1 l2 = List.fold_left (fun accu i1 -> List.fold_left (fun accu i2 -> iadd accu (add_inter i1 i2)) accu l2 ) empty l1 let negat = List.rev_map (function | Bounded (i,j) -> Bounded (minus_big_int j, minus_big_int i) | Left i -> Right (minus_big_int i) | Right j -> Left (minus_big_int j) | Any -> Any ) let sub l1 l2 = add l1 (negat l2)