intervals.ml 4.34 KB
 Pietro Abate committed Oct 05, 2007 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 = `````` Pietro Abate committed Oct 05, 2007 12 `````` (l1 == l2) || `````` Pietro Abate committed Oct 05, 2007 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 `````` Pietro Abate committed Oct 05, 2007 25 `````` | ([], []) -> true `````` Pietro Abate committed Oct 05, 2007 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 `````` Pietro Abate committed Jul 10, 2007 37 `````` `````` Pietro Abate committed Jul 10, 2007 38 ``````let empty = [] `````` Pietro Abate committed Oct 05, 2007 39 40 41 ``````let any = [Any] let atom a b = `````` Pietro Abate committed Oct 05, 2007 42 `````` if le_big_int a b then [Bounded (a,b)] else empty `````` Pietro Abate committed Oct 05, 2007 43 44 `````` `````` Pietro Abate committed Oct 05, 2007 45 ``````let rec iadd_left l b = match l with `````` Pietro Abate committed Oct 05, 2007 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' -> `````` Pietro Abate committed Oct 05, 2007 51 `````` iadd_left l' (max_big_int b b1) `````` Pietro Abate committed Oct 05, 2007 52 53 `````` | Left b1 :: _ when le_big_int b b1-> l | Left _ :: l' -> `````` Pietro Abate committed Oct 05, 2007 54 `````` iadd_left l' b `````` Pietro Abate committed Oct 05, 2007 55 `````` | _ -> any `````` Pietro Abate committed Jul 10, 2007 56 `````` `````` Pietro Abate committed Oct 05, 2007 57 ``````let rec iadd_bounded l a b = match l with `````` Pietro Abate committed Jul 10, 2007 58 `````` | [] -> `````` Pietro Abate committed Oct 05, 2007 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) -> `````` Pietro Abate committed Oct 05, 2007 65 `````` i'::(iadd_bounded l' a b) `````` Pietro Abate committed Oct 05, 2007 66 `````` | Bounded (a1,b1) :: l' -> `````` Pietro Abate committed Oct 05, 2007 67 `````` iadd_bounded l' (min_big_int a a1) (max_big_int b b1) `````` Pietro Abate committed Oct 05, 2007 68 `````` | Left b1 :: l' -> `````` Pietro Abate committed Oct 05, 2007 69 `````` iadd_left l' b `````` Pietro Abate committed Oct 05, 2007 70 `````` | Right a1 :: _ -> [Right (min_big_int a a1)] `````` Pietro Abate committed Oct 05, 2007 71 72 `````` | Any :: _ -> any `````` Pietro Abate committed Oct 05, 2007 73 ``````let rec iadd_right l a = match l with `````` Pietro Abate committed Oct 05, 2007 74 75 76 `````` | [] -> [Right a] | ((Bounded (_,b1) | Left b1) as i') :: l' when (lt_big_int (succ_big_int b1) a) -> `````` Pietro Abate committed Oct 05, 2007 77 `````` i'::(iadd_right l' a) `````` Pietro Abate committed Oct 05, 2007 78 79 80 81 `````` | (Bounded (a1,_) | Right a1) :: _ -> [Right (min_big_int a a1)] | _ -> any `````` Pietro Abate committed Oct 05, 2007 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 `````` Pietro Abate committed Oct 05, 2007 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 `````` Pietro Abate committed Jul 10, 2007 102 103 `````` let cup i1 i2 = `````` Pietro Abate committed Oct 05, 2007 104 `````` List.fold_left iadd i1 i2 `````` Pietro Abate committed Jul 10, 2007 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) `````` Pietro Abate committed Oct 05, 2007 112 ``````let is_empty = function [] -> true | _ -> false `````` Pietro Abate committed Jul 10, 2007 113 `````` `````` Pietro Abate committed Jul 10, 2007 114 `````` `````` Pietro Abate committed Oct 05, 2007 115 ``````(* TODO: can optimize this to stop running through the list earlier *) `````` Pietro Abate committed Jul 10, 2007 116 ``````let contains n = `````` Pietro Abate committed Oct 05, 2007 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) ) `````` Pietro Abate committed Jul 10, 2007 123 124 `````` let sample = function `````` Pietro Abate committed Oct 05, 2007 125 126 127 `````` | (Left x | Right x | Bounded (x,_)) :: _ -> x | Any :: _ -> zero_big_int | [] -> raise Not_found `````` Pietro Abate committed Jul 10, 2007 128 129 130 131 `````` let print = List.map `````` Pietro Abate committed Oct 05, 2007 132 133 134 135 `````` (fun x ppf -> match x with | Any -> Format.fprintf ppf "Int" | Left b -> `````` Pietro Abate committed Oct 05, 2007 136 `````` Format.fprintf ppf "*--%s" `````` Pietro Abate committed Oct 05, 2007 137 138 `````` (string_of_big_int b) | Right a -> `````` Pietro Abate committed Oct 05, 2007 139 `````` Format.fprintf ppf "%s--*" `````` Pietro Abate committed Oct 05, 2007 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) `````` Pietro Abate committed Jul 10, 2007 148 `````` ) `````` Pietro Abate committed Oct 05, 2007 149 150 `````` `````` Pietro Abate committed Oct 05, 2007 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 `````` Pietro Abate committed Oct 05, 2007 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)``````