intervals.ml

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)