intervals.ml 4.34 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
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 =
12
  (l1 == l2) ||
13
14
15
16
17
18
19
20
21
22
23
24
  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
25
    | ([], []) -> true
26
27
28
29
30
31
32
33
34
35
36
    | _ -> 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
37

38
let empty = []
39
40
41
let any = [Any]

let atom a b =
42
  if le_big_int a b then [Bounded (a,b)] else empty
43
44


45
let rec iadd_left l b = match l with
46
47
48
49
50
  | [] -> [Left b]
  | (Bounded (a1,_) | Right a1) :: _
      when (lt_big_int b (pred_big_int a1)) -> 
      Left b :: l
  | Bounded (_,b1) :: l' -> 
51
      iadd_left l' (max_big_int b b1)
52
53
  | Left b1 :: _ when le_big_int b b1-> l
  | Left _ :: l' ->
54
      iadd_left l' b
55
  | _ -> any
56

57
let rec iadd_bounded l a b = match l with
58
  | [] -> 
59
60
61
62
63
64
      [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) -> 
65
      i'::(iadd_bounded l' a b)
66
  | Bounded (a1,b1) :: l' -> 
67
      iadd_bounded l' (min_big_int a a1) (max_big_int b b1)
68
  | Left b1 :: l' ->
69
      iadd_left l' b
70
  | Right a1 :: _ -> [Right (min_big_int a a1)]
71
72
  | Any :: _ -> any

73
let rec iadd_right l a = match l with
74
75
76
  | [] -> [Right a]
  | ((Bounded (_,b1) | Left b1) as i') :: l' 
      when (lt_big_int (succ_big_int b1) a) -> 
77
      i'::(iadd_right l' a)
78
79
80
81
  | (Bounded (a1,_) | Right a1) :: _ -> 
      [Right (min_big_int a a1)]
  | _ -> any

82
83
84
85
let iadd l = function
  | Bounded (a,b) -> iadd_bounded l a b
  | Left b -> iadd_left l b
  | Right a -> iadd_right l a
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
  | 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
102
103

let cup i1 i2 =
104
  List.fold_left iadd i1 i2
105
106
107
108
109
110
111

let cap i1 i2 =
  neg (cup (neg i1) (neg i2))

let diff i1 i2 =
  neg (cup (neg i1) i2)

112
let is_empty = function [] -> true | _ -> false
113

114

115
(* TODO: can optimize this to stop running through the list earlier *)
116
let contains n =
117
118
119
120
121
122
  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)
	      )
123
124

let sample = function
125
126
127
  | (Left x | Right x | Bounded (x,_)) :: _ -> x
  | Any :: _ -> zero_big_int
  | [] -> raise Not_found
128
129
130
131
  

let print =
  List.map 
132
133
134
135
    (fun x ppf -> match x with
       | Any ->
	   Format.fprintf ppf "Int"
       | Left b -> 
136
	   Format.fprintf ppf "*--%s" 
137
138
	     (string_of_big_int b)
       | Right a -> 
139
	   Format.fprintf ppf "%s--*" 
140
141
142
143
144
145
146
147
	     (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)
148
    )
149
150


151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
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
175
176
177
178
179
180
181
182
183
184
185
186

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)