Just retab (many lines changed for nothing)

1 files changed, 115 insertions, 115 deletions

diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml
index 98f4daf..b63f8a9 100644
--- a/abstract/intervals_domain.ml
+++ b/abstract/intervals_domain.ml
@@ -1,122 +1,122 @@
 open Value_domain
 
 module Intervals : VALUE_DOMAIN = struct
-  type bound = Int of Z.t | PInf | MInf
-
-  type t = Itv of bound * bound | Bot
-
-  (* utilities *)
-  let bound_leq a b =   (* a <= b ? *)
-    match a, b with
-    | MInf, _ | _, PInf -> true
-    | Int a, Int b -> Z.leq a b
-    | x, y -> x = y
-
-  let bound_add a b =
-    match a, b with
-    | MInf, Int a | Int a, MInf -> MInf
-    | PInf, Int a | Int a, PInf -> PInf
-    | MInf, MInf -> MInf
-    | PInf, PInf -> PInf
-    | Int a, Int b -> Int (Z.add a b)
-    | _ -> assert false
-  let bound_mul a b =
-    match a, b with
-    | PInf, Int(x) | Int(x), PInf ->
-      if x > Z.zero then PInf
-      else if x < Z.zero then MInf
-      else Int Z.zero
-    | MInf, Int(x) | Int(x), MInf ->
-      if x < Z.zero then PInf
-      else if x > Z.zero then MInf
-      else Int Z.zero
-    | Int(x), Int(y) -> Int(Z.mul x y)
-    | MInf, PInf | PInf, MInf -> MInf
-    | MInf, MInf | PInf, PInf -> PInf
-
-  let bound_min a b = match a, b with
-    | MInf, _ | _, MInf -> MInf
-    | Int a, Int b -> Int (min a b)
-    | Int a, PInf -> Int a
-    | PInf, Int a -> Int a
-    | PInf, PInf -> PInf
-  let bound_max a b = match a, b with
-    | PInf, _ | _, PInf -> PInf
-    | Int a, Int b -> Int (max a b)
-    | Int a, MInf | MInf, Int a -> Int a
-    | MInf, MInf -> MInf
-
-  let bound_neg = function
-    | PInf -> MInf
-    | MInf -> PInf
-    | Int i -> Int (Z.neg i)
-
-  (* implementation *)
-  let top = Itv(MInf, PInf)
-  let bottom = Bot
-  let const i = Itv(Int i, Int i)
-  let rand i j =
+    type bound = Int of Z.t | PInf | MInf
+
+    type t = Itv of bound * bound | Bot
+
+    (* utilities *)
+    let bound_leq a b =   (* a <= b ? *)
+        match a, b with
+        | MInf, _ | _, PInf -> true
+        | Int a, Int b -> Z.leq a b
+        | x, y -> x = y
+
+    let bound_add a b =
+        match a, b with
+        | MInf, Int a | Int a, MInf -> MInf
+        | PInf, Int a | Int a, PInf -> PInf
+        | MInf, MInf -> MInf
+        | PInf, PInf -> PInf
+        | Int a, Int b -> Int (Z.add a b)
+        | _ -> assert false
+    let bound_mul a b =
+        match a, b with
+        | PInf, Int(x) | Int(x), PInf ->
+            if x > Z.zero then PInf
+            else if x < Z.zero then MInf
+            else Int Z.zero
+        | MInf, Int(x) | Int(x), MInf ->
+            if x < Z.zero then PInf
+            else if x > Z.zero then MInf
+            else Int Z.zero
+        | Int(x), Int(y) -> Int(Z.mul x y)
+        | MInf, PInf | PInf, MInf -> MInf
+        | MInf, MInf | PInf, PInf -> PInf
+
+    let bound_min a b = match a, b with
+        | MInf, _ | _, MInf -> MInf
+        | Int a, Int b -> Int (min a b)
+        | Int a, PInf -> Int a
+        | PInf, Int a -> Int a
+        | PInf, PInf -> PInf
+    let bound_max a b = match a, b with
+        | PInf, _ | _, PInf -> PInf
+        | Int a, Int b -> Int (max a b)
+        | Int a, MInf | MInf, Int a -> Int a
+        | MInf, MInf -> MInf
+
+    let bound_neg = function
+        | PInf -> MInf
+        | MInf -> PInf
+        | Int i -> Int (Z.neg i)
+
+    (* implementation *)
+    let top = Itv(MInf, PInf)
+    let bottom = Bot
+    let const i = Itv(Int i, Int i)
+    let rand i j =
     if Z.leq i j then Itv(Int i, Int j) else Bot
 
-  let subset a b = match a, b with
-    | Bot, _ -> true
-    | _, Bot -> false
-    | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b
-
-  let join a b = match a, b with
-    | Bot, x | x, Bot -> x
-    | Itv(a, b), Itv(c, d) -> Itv(bound_min a c, bound_max b d)
-
-  let meet a b = match a, b with
-    | Bot, x | x, Bot -> Bot
-    | Itv(a, b), Itv(c, d) ->
-      let u, v = bound_max a c, bound_min b d in
-      if bound_leq u v
-        then Itv(u, v)
-        else Bot
-
-  let widen a b = match a, b with
-    | x, Bot | Bot, x -> x
-    | Itv(a, b), Itv(c, d) ->
-      Itv(
-        (if not (bound_leq a c) then MInf else a),
-        (if not (bound_leq d b) then PInf else b))
-
-  let neg = function
-    | Bot -> Bot
-    | Itv(a, b) -> Itv(bound_neg b, bound_neg a)
-  let add a b = match a, b with
-    | Bot, _ | _, Bot -> Bot
-    | Itv(a, b), Itv(c, d) -> Itv(bound_add a c, bound_add b d)
-  let sub a b = match a, b with
-    | Bot, _ | _, Bot -> Bot
-    | Itv(a, b), Itv(c, d) -> Itv(bound_add a (bound_neg d), bound_add b (bound_neg c))
-  let mul a b = match a, b with
-    | Bot, _ | _, Bot -> Bot
-    | Itv(a, b), Itv(c, d) ->
-        Itv(
-          (bound_min (bound_min (bound_mul a c) (bound_mul a d))
-                     (bound_min (bound_mul b c) (bound_mul b d))),
-          (bound_max (bound_max (bound_mul a c) (bound_mul a d))
-                     (bound_max (bound_mul b c) (bound_mul b d))))
-      
-
-  let div a b = top (* TODO *)
-  let rem a b = top (* TODO *)
-
-  let leq a b = match a, b with
-    | Bot, _ | _, Bot -> Bot, Bot
-    | Itv(a, b), Itv(c, d) ->
-      if not (bound_leq a d)
-        then Bot, Bot
-        else Itv(a, bound_min b d), Itv(bound_max a c, d)
-
-  let bound_str = function
-    | MInf -> "-oo"
-    | PInf -> "+oo"
-    | Int i -> Z.to_string i
-  let to_string = function
-    | Bot -> "bot"
-    | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]"
+    let subset a b = match a, b with
+        | Bot, _ -> true
+        | _, Bot -> false
+        | Itv(a, b), Itv(c, d) -> bound_leq a c && bound_leq d b
+
+    let join a b = match a, b with
+        | Bot, x | x, Bot -> x
+        | Itv(a, b), Itv(c, d) -> Itv(bound_min a c, bound_max b d)
+
+    let meet a b = match a, b with
+        | Bot, x | x, Bot -> Bot
+        | Itv(a, b), Itv(c, d) ->
+            let u, v = bound_max a c, bound_min b d in
+            if bound_leq u v
+            then Itv(u, v)
+            else Bot
+
+    let widen a b = match a, b with
+        | x, Bot | Bot, x -> x
+        | Itv(a, b), Itv(c, d) ->
+            Itv(
+            (if not (bound_leq a c) then MInf else a),
+            (if not (bound_leq d b) then PInf else b))
+
+    let neg = function
+        | Bot -> Bot
+        | Itv(a, b) -> Itv(bound_neg b, bound_neg a)
+    let add a b = match a, b with
+        | Bot, _ | _, Bot -> Bot
+        | Itv(a, b), Itv(c, d) -> Itv(bound_add a c, bound_add b d)
+    let sub a b = match a, b with
+        | Bot, _ | _, Bot -> Bot
+        | Itv(a, b), Itv(c, d) -> Itv(bound_add a (bound_neg d), bound_add b (bound_neg c))
+    let mul a b = match a, b with
+        | Bot, _ | _, Bot -> Bot
+        | Itv(a, b), Itv(c, d) ->
+            Itv(
+                (bound_min (bound_min (bound_mul a c) (bound_mul a d))
+                            (bound_min (bound_mul b c) (bound_mul b d))),
+                (bound_max (bound_max (bound_mul a c) (bound_mul a d))
+                            (bound_max (bound_mul b c) (bound_mul b d))))
+        
+
+    let div a b = top (* TODO *)
+    let rem a b = top (* TODO *)
+
+    let leq a b = match a, b with
+        | Bot, _ | _, Bot -> Bot, Bot
+        | Itv(a, b), Itv(c, d) ->
+            if not (bound_leq a d)
+            then Bot, Bot
+            else Itv(a, bound_min b d), Itv(bound_max a c, d)
+
+    let bound_str = function
+        | MInf -> "-oo"
+        | PInf -> "+oo"
+        | Int i -> Z.to_string i
+    let to_string = function
+        | Bot -> "bot"
+        | Itv(a, b) -> "[" ^ (bound_str a) ^ ";" ^ (bound_str b) ^ "]"
 
 end