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 compare l1 l2 =
  match (l1,l2) with
    | [], [] -> 0
    | [],_ -> -1
    | _,[] -> 1
    | Bounded (a1,b1) :: l1, Bounded (a2,b2) :: l2 ->
        let c = vcompare a1 a2 in if c <> 0 then c 
        else let c = vcompare b1 b2 in if c <> 0 then c
        else compare l1 l2
    | Bounded (_,_) :: _, _ -> -1
    | _, Bounded (_,_) :: _ -> 1

    | Left a1 :: l1, Left a2 :: l2 ->
        let c = vcompare a1 a2 in if c <> 0 then c 
        else compare l1 l2
    | Left _ :: _, _ -> -1
    | _, Left _ :: _ -> 1

    | Right a1 :: l1, Right a2 :: l2 ->
        let c = vcompare a1 a2 in if c <> 0 then c 
        else compare l1 l2
    | Right _ :: _, _ -> -1
    | _, Right _ :: _ -> 1

    | Any :: _, Any :: _ -> 0


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