viewcvs.cgi/types/intervals.ml

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 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
let vsub = sub_big_int
let vdiv = div_big_int
let vmod  = mod_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 rec hash accu = function
  | Bounded (a,b) :: rem  ->
      hash (1 + 2 * (vhash a) + 3 * (vhash b) + 17 * accu) rem
  | Left b :: rem ->
      hash (3 * vhash b + 17 * accu) rem
  | Right a :: _ ->
      2 * (vhash a) + 17 * accu
  | Any :: _ -> 17 * accu + 1234
  | [] -> accu + 3

let empty = []
let any = [Any]

let bounded a b =
  if le_big_int a b then [Bounded (a,b)] else empty

let left a = [Left a]
let right a = [Right a]
let atom a = bounded a a


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' (max_big_int b b1)
  | 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

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 =
  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)

(*
let dump s i =
  let ppf = Format.std_formatter in
  Format.fprintf ppf "%s = [ " s;
  List.iter (fun x -> x ppf; Format.fprintf ppf " ") (print i);  
  Format.fprintf ppf "] "

let diff i1 i2 =
  let ppf = Format.std_formatter in
  Format.fprintf ppf "Intervals.diff:";
  dump "i1" i1;
  dump "i2" i2; 
  dump "i1-i2" (diff i1 i2); 
  Format.fprintf ppf "@\n";
  diff i1 i2

*)
1	abate	15	open Big_int
2	abate	1
3	abate	281	(* Hack to compute hash value for bigints *)
4			let hash_nat x = Nat.nth_digit_nat x 0
5			let hash_bigint (sign,nat) = sign * 17 + hash_nat nat
6
7	abate	222	type v = big_int
8			let print_v ppf i = Format.fprintf ppf "%s" (string_of_big_int i)
9	abate	237	let vcompare = compare_big_int
10	abate	281	let vhash x = hash_bigint (Obj.magic x)
11			(* num_digits_big_int x ) ( improve this *)
12	abate	222	let mk = big_int_of_string
13			let vadd = add_big_int
14			let vmult = mult_big_int
15			let vsub = sub_big_int
16			let vdiv = div_big_int
17			let vmod = mod_big_int
18
19
20	abate	15	type interval =
21			\| Bounded of big_int * big_int
22			\| Left of big_int
23			\| Right of big_int
24			\| Any
25
26			type t = interval list
27
28	abate	263
29	abate	15	let rec equal l1 l2 =
30	abate	16	(l1 == l2) \|\|
31	abate	15	match (l1,l2) with
32			\| (Bounded (a1,b1) :: l1, Bounded (a2,b2) :: l2) ->
33			(eq_big_int a1 a2) &&
34			(eq_big_int b1 b2) &&
35			(equal l1 l2)
36			\| (Left b1 :: l1, Left b2 :: l2) ->
37			(eq_big_int b1 b2) &&
38			(equal l1 l2)
39			\| (Right a1 :: l1, Right a2 :: l2) ->
40			(eq_big_int a1 a2) &&
41			(equal l1 l2)
42			\| (Any :: _, Any :: _) -> true
43	abate	16	\| ([], []) -> true
44	abate	15	\| _ -> false
45
46	abate	222	let rec hash accu = function
47			\| Bounded (a,b) :: rem ->
48			hash (1 + 2 * (vhash a) + 3 * (vhash b) + 17 * accu) rem
49			\| Left b :: rem ->
50			hash (3 * vhash b + 17 * accu) rem
51	abate	15	\| Right a :: _ ->
52	abate	222	2 * (vhash a) + 17 * accu
53			\| Any :: _ -> 17 * accu + 1234
54			\| [] -> accu + 3
55	abate	15
56	abate	1	let empty = []
57	abate	15	let any = [Any]
58	abate	1
59	abate	52	let bounded a b =
60	abate	16	if le_big_int a b then [Bounded (a,b)] else empty
61	abate	15
62	abate	52	let left a = [Left a]
63			let right a = [Right a]
64			let atom a = bounded a a
65	abate	15
66	abate	52
67	abate	16	let rec iadd_left l b = match l with
68	abate	15	\| [] -> [Left b]
69			\| (Bounded (a1,_) \| Right a1) :: _
70			when (lt_big_int b (pred_big_int a1)) ->
71			Left b :: l
72			\| Bounded (_,b1) :: l' ->
73	abate	16	iadd_left l' (max_big_int b b1)
74	abate	15	\| Left b1 :: _ when le_big_int b b1-> l
75			\| Left _ :: l' ->
76	abate	16	iadd_left l' b
77	abate	15	\| _ -> any
78
79	abate	16	let rec iadd_bounded l a b = match l with
80	abate	1	\| [] ->
81	abate	15	[Bounded (a,b)]
82			\| (Bounded (a1,_) \| Right a1) :: _
83			when (lt_big_int b (pred_big_int a1)) ->
84			Bounded (a,b) :: l
85			\| ((Bounded (_,b1) \| Left b1) as i') :: l'
86			when (lt_big_int (succ_big_int b1) a) ->
87	abate	16	i'::(iadd_bounded l' a b)
88	abate	15	\| Bounded (a1,b1) :: l' ->
89	abate	16	iadd_bounded l' (min_big_int a a1) (max_big_int b b1)
90	abate	15	\| Left b1 :: l' ->
91	abate	263	iadd_left l' (max_big_int b b1)
92	abate	43	\| Right a1 :: _ -> [Right (min_big_int a a1)]
93	abate	15	\| Any :: _ -> any
94	abate	1
95	abate	16	let rec iadd_right l a = match l with
96	abate	15	\| [] -> [Right a]
97			\| ((Bounded (_,b1) \| Left b1) as i') :: l'
98			when (lt_big_int (succ_big_int b1) a) ->
99	abate	16	i'::(iadd_right l' a)
100	abate	15	\| (Bounded (a1,_) \| Right a1) :: _ ->
101			[Right (min_big_int a a1)]
102			\| _ -> any
103	abate	1
104	abate	16	let iadd l = function
105			\| Bounded (a,b) -> iadd_bounded l a b
106			\| Left b -> iadd_left l b
107			\| Right a -> iadd_right l a
108	abate	15	\| Any -> any
109	abate	1
110	abate	15	let rec neg' start l = match l with
111			\| [] -> [Right start]
112			\| Bounded (a,b) :: l' ->
113			Bounded (start, pred_big_int a) :: (neg' (succ_big_int b) l')
114			\| Right a :: l' ->
115			[Bounded (start, pred_big_int a)]
116			\| _ -> assert false
117
118			let neg = function
119			\| Any :: _ -> []
120			\| [] -> any
121			\| Left b :: l -> neg' (succ_big_int b) l
122			\| Right a :: _ -> [Left (pred_big_int a)]
123			\| Bounded (a,b) :: l -> Left (pred_big_int a) :: neg' (succ_big_int b) l
124
125	abate	1	let cup i1 i2 =
126	abate	16	List.fold_left iadd i1 i2
127	abate	1
128			let cap i1 i2 =
129			neg (cup (neg i1) (neg i2))
130
131			let diff i1 i2 =
132			neg (cup (neg i1) i2)
133
134	abate	16	let is_empty = function [] -> true \| _ -> false
135	abate	1
136	abate	281	let rec disjoint a b =
137			match (a,b) with
138			\| [],_ \| _,[] -> true
139			\| Any::_,_ \| _,Any::_ -> false
140			\| Left _::_, Left _::_ -> false
141			\| Right _::_, Right _::_ -> false
142			\| Left x :: a, Bounded (y,_) :: _ -> (lt_big_int x y) && (disjoint a b)
143			\| Bounded (y,_) :: _, Left x :: b -> (lt_big_int x y) && (disjoint a b)
144			\| Left x :: _, Right y :: _ -> lt_big_int x y
145			\| Right y :: _, Left x :: _ -> lt_big_int x y
146			\| Right y :: _, Bounded (_,x) :: _ -> lt_big_int x y
147			\| Bounded (_,x) :: _, Right y :: _ -> lt_big_int x y
148			\| Bounded (xa,ya) :: a', Bounded (xb,yb) :: b' ->
149			let c = compare_big_int xa xb in
150			if c = 0 then false
151			else
152			if c < 0 then (lt_big_int ya xb) && (disjoint a' b)
153			else (lt_big_int yb xa) && (disjoint a b')
154	abate	1
155	abate	281
156	abate	15	(* TODO: can optimize this to stop running through the list earlier *)
157	abate	1	let contains n =
158	abate	15	List.exists (function
159			\| Any -> true
160			\| Left b -> le_big_int n b
161			\| Right a -> le_big_int a n
162			\| Bounded (a,b) -> (le_big_int a n) && (le_big_int n b)
163			)
164	abate	1
165			let sample = function
166	abate	15	\| (Left x \| Right x \| Bounded (x,_)) :: _ -> x
167			\| Any :: _ -> zero_big_int
168			\| [] -> raise Not_found
169	abate	1
170
171			let print =
172			List.map
173	abate	15	(fun x ppf -> match x with
174			\| Any ->
175			Format.fprintf ppf "Int"
176			\| Left b ->
177	abate	16	Format.fprintf ppf "*--%s"
178	abate	15	(string_of_big_int b)
179			\| Right a ->
180	abate	16	Format.fprintf ppf "%s--*"
181	abate	15	(string_of_big_int a)
182			\| Bounded (a,b) when eq_big_int a b ->
183			Format.fprintf ppf "%s"
184			(string_of_big_int a)
185			\| Bounded (a,b) ->
186			Format.fprintf ppf "%s--%s"
187			(string_of_big_int a)
188			(string_of_big_int b)
189	abate	1	)
190	abate	15
191
192	abate	16	let (+) = add_big_int
193
194
195			let add_inter i1 i2 =
196			match (i1,i2) with
197			\| Bounded (a1,b1), Bounded (a2,b2) -> Bounded (a1+a2, b1+b2)
198			\| Bounded (_,b1), Left b2
199			\| Left b1, Bounded (_,b2)
200			\| Left b1, Left b2 -> Left (b1+b2)
201			\| Bounded (a1,_), Right a2
202			\| Right a1, Bounded (a2,_)
203			\| Right a1, Right a2 -> Right (a1+a2)
204			\| _ -> Any
205
206
207			(* Optimize this ... *)
208			let add l1 l2 =
209			List.fold_left
210			(fun accu i1 ->
211			List.fold_left
212			(fun accu i2 -> iadd accu (add_inter i1 i2))
213			accu l2
214
215			) empty l1
216	abate	51
217			let negat =
218			List.rev_map
219			(function
220			\| Bounded (i,j) -> Bounded (minus_big_int j, minus_big_int i)
221			\| Left i -> Right (minus_big_int i)
222			\| Right j -> Left (minus_big_int j)
223			\| Any -> Any
224			)
225
226			let sub l1 l2 =
227			add l1 (negat l2)
228	abate	263
229			(*
230			let dump s i =
231			let ppf = Format.std_formatter in
232			Format.fprintf ppf "%s = [ " s;
233			List.iter (fun x -> x ppf; Format.fprintf ppf " ") (print i);
234			Format.fprintf ppf "] "
235
236			let diff i1 i2 =
237			let ppf = Format.std_formatter in
238	abate	281	Format.fprintf ppf "Intervals.diff:";
239	abate	263	dump "i1" i1;
240			dump "i2" i2;
241	abate	281	dump "i1-i2" (diff i1 i2);
242	abate	263	Format.fprintf ppf "@\n";
243			diff i1 i2
244	abate	281
245	abate	263	*)