viewcvs.cgi/types/intervals.ml

open Big_int

type v = big_int
let print_v ppf i = Format.fprintf ppf "%s" (string_of_big_int i)
let vcompare = compare_big_int
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 vhash = num_digits_big_int 
(* improve this *)

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