Just retab (many lines changed for nothing)

1 files changed, 114 insertions, 114 deletions

diff --git a/abstract/interpret.ml b/abstract/interpret.ml
index 5f03775..c599a76 100644
--- a/abstract/interpret.ml
+++ b/abstract/interpret.ml
@@ -4,94 +4,94 @@ open Util
 
 module Make (E : ENVIRONMENT_DOMAIN) = struct
 
-	let neg (e, l) =
-		(AST_unary(AST_NOT, (e, l))), l
+    let neg (e, l) =
+        (AST_unary(AST_NOT, (e, l))), l
 
-	let binop op (e, l) e2 =
-		(AST_binary (op, (e,l), e2)), l
-	let m1 (e, l) =
-		binop AST_MINUS (e, l) (AST_int_const("1", l), l)
-	let p1 (e, l) =
-		binop AST_PLUS (e, l) (AST_int_const("1", l), l)
+    let binop op (e, l) e2 =
+        (AST_binary (op, (e,l), e2)), l
+    let m1 (e, l) =
+        binop AST_MINUS (e, l) (AST_int_const("1", l), l)
+    let p1 (e, l) =
+        binop AST_PLUS (e, l) (AST_int_const("1", l), l)
 
     let bottom_with_vars =
         List.fold_left E.addvar E.bottom
 
-	let rec condition cond env =
-		begin match fst cond with
-		| AST_binary (AST_LESS_EQUAL, e1, e2) ->
-			E.compare_leq env e1 e2
-		| AST_binary (AST_EQUAL, e1, e2) ->
+    let rec condition cond env =
+        begin match fst cond with
+        | AST_binary (AST_LESS_EQUAL, e1, e2) ->
+            E.compare_leq env e1 e2
+        | AST_binary (AST_EQUAL, e1, e2) ->
             E.compare_eq env e1 e2
-		| AST_binary (AST_AND, e1, e2) ->
-			E.meet (condition e1 env) (condition e2 env)
-		| AST_binary (AST_OR, e1, e2) ->
-			E.join (condition e1 env) (condition e2 env)
+        | AST_binary (AST_AND, e1, e2) ->
+            E.meet (condition e1 env) (condition e2 env)
+        | AST_binary (AST_OR, e1, e2) ->
+            E.join (condition e1 env) (condition e2 env)
 
-		(* transformations : remove not *)
-		| AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) ->
-			condition cond env
-		| AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) ->
-			condition
-				(AST_binary(AST_OR, neg e1, neg e2), x) env
-		| AST_unary (AST_NOT, (AST_binary(AST_OR, e1, e2), x)) ->
-			condition
-				(AST_binary(AST_AND, neg e1, neg e2), x) env
+        (* transformations : remove not *)
+        | AST_unary (AST_NOT, (AST_unary(AST_NOT, cond), x)) ->
+            condition cond env
+        | AST_unary (AST_NOT, (AST_binary(AST_AND, e1, e2), x)) ->
+            condition
+                (AST_binary(AST_OR, neg e1, neg e2), x) env
+        | AST_unary (AST_NOT, (AST_binary(AST_OR, e1, e2), x)) ->
+            condition
+                (AST_binary(AST_AND, neg e1, neg e2), x) env
 
-		| AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) ->
-			let op2 = match op with
-			| AST_LESS_EQUAL -> AST_GREATER
-			| AST_LESS -> AST_GREATER_EQUAL
-			| AST_GREATER_EQUAL -> AST_LESS
-			| AST_GREATER -> AST_LESS_EQUAL
-			| AST_EQUAL -> AST_NOT_EQUAL
-			| AST_NOT_EQUAL -> AST_EQUAL
-			| _ -> assert false
-			in
-			condition (binop op2 e1 e2) env
-		
-		(* transformations : encode everything with leq *)
-		| AST_binary(AST_LESS, e1, e2) ->
-			condition
-				(binop AST_AND (binop AST_LESS_EQUAL e1 (m1 e2))
-							   (binop AST_LESS_EQUAL (p1 e1) e2))
-				env
-		| AST_binary (AST_GREATER_EQUAL, e1, e2) ->
-			condition
-				(binop AST_LESS_EQUAL e2 e1)
-				env
-		| AST_binary (AST_GREATER, e1, e2) ->
-			condition
-				(binop AST_LESS e2 e1)
-				env
-		| AST_binary (AST_NOT_EQUAL, e1, e2) ->
-			condition
-				(binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1))
-				env
+        | AST_unary (AST_NOT, (AST_binary(op, e1, e2), x)) ->
+            let op2 = match op with
+            | AST_LESS_EQUAL -> AST_GREATER
+            | AST_LESS -> AST_GREATER_EQUAL
+            | AST_GREATER_EQUAL -> AST_LESS
+            | AST_GREATER -> AST_LESS_EQUAL
+            | AST_EQUAL -> AST_NOT_EQUAL
+            | AST_NOT_EQUAL -> AST_EQUAL
+            | _ -> assert false
+            in
+            condition (binop op2 e1 e2) env
+        
+        (* transformations : encode everything with leq *)
+        | AST_binary(AST_LESS, e1, e2) ->
+            condition
+                (binop AST_AND (binop AST_LESS_EQUAL e1 (m1 e2))
+                               (binop AST_LESS_EQUAL (p1 e1) e2))
+                env
+        | AST_binary (AST_GREATER_EQUAL, e1, e2) ->
+            condition
+                (binop AST_LESS_EQUAL e2 e1)
+                env
+        | AST_binary (AST_GREATER, e1, e2) ->
+            condition
+                (binop AST_LESS e2 e1)
+                env
+        | AST_binary (AST_NOT_EQUAL, e1, e2) ->
+            condition
+                (binop AST_OR (binop AST_LESS e1 e2) (binop AST_LESS e2 e1))
+                env
 
-		| _ -> env
-		end
+        | _ -> env
+        end
 
-	let rec interp_stmt env stat =
-		begin match fst stat with
-		| AST_block b ->
-			(* remember to remove vars that have gone out of scope at the end *)
-			let prevars = E.vars env in
-			let env2 = List.fold_left interp_stmt env b in
-			let postvars = E.vars env2 in
-			let rmvars = List.filter (fun x -> not (List.mem x prevars)) postvars in
-			List.fold_left E.rmvar env2 rmvars
-		| AST_assign ((id, _), exp) ->
-			E.assign env id exp
-		| AST_if (cond, tb, None) ->
-			E.join
-				(interp_stmt (condition cond env) tb)
-				(condition (neg cond) env)
-		| AST_if (cond, tb, Some eb) ->
-			let e1 = (interp_stmt (condition cond env) tb) in
-			let e2 = (interp_stmt (condition (neg cond) env) eb) in
-			E.join e1 e2
-		| AST_while (cond, body) ->
+    let rec interp_stmt env stat =
+        begin match fst stat with
+        | AST_block b ->
+            (* remember to remove vars that have gone out of scope at the end *)
+            let prevars = E.vars env in
+            let env2 = List.fold_left interp_stmt env b in
+            let postvars = E.vars env2 in
+            let rmvars = List.filter (fun x -> not (List.mem x prevars)) postvars in
+            List.fold_left E.rmvar env2 rmvars
+        | AST_assign ((id, _), exp) ->
+            E.assign env id exp
+        | AST_if (cond, tb, None) ->
+            E.join
+                (interp_stmt (condition cond env) tb)
+                (condition (neg cond) env)
+        | AST_if (cond, tb, Some eb) ->
+            let e1 = (interp_stmt (condition cond env) tb) in
+            let e2 = (interp_stmt (condition (neg cond) env) eb) in
+            E.join e1 e2
+        | AST_while (cond, body) ->
             (* loop unrolling *)
             let rec unroll u = function
                 | 0 -> u, bottom_with_vars (E.vars env)
@@ -118,40 +118,40 @@ module Make (E : ENVIRONMENT_DOMAIN) = struct
             let x = iter 0 env in
             let y = fix fsharp x in     (* decreasing iteration *)
             E.join (condition (neg cond) y) u_u
-		| AST_HALT -> bottom_with_vars (E.vars env)
-		| AST_assert cond ->
-			if not
-				(E.is_bot (condition (neg cond) env))
-			then begin
-				Format.printf "%s: ERROR: assertion failure@."
-					(Abstract_syntax_printer.string_of_extent (snd stat));
-			end;
-			condition cond env
-		| AST_print items ->
-			Format.printf "%s: %s@."
-				(Abstract_syntax_printer.string_of_extent (snd stat))
-				(E.var_str env (List.map fst items));
-			env
-		| AST_local ((ty, _), vars) ->
-			List.fold_left
-				(fun env ((id, _), init) ->
-					let env2 = E.addvar env id in
-					match init with
-					| Some e -> E.assign env2 id e
-					| None -> env2)
-				env
-				vars
-		| _ -> assert false (* not implemented *)
-		end
-	
-	let interpret prog =
-		let result = List.fold_left
-			(fun env x -> match x with
-				| AST_stat st -> interp_stmt env st
-				| _ -> env)
-			E.init
-			(fst prog)
-		in
-			Format.printf "Output: %s@."
-				(E.var_str result (E.vars result))
+        | AST_HALT -> bottom_with_vars (E.vars env)
+        | AST_assert cond ->
+            if not
+                (E.is_bot (condition (neg cond) env))
+            then begin
+                Format.printf "%s: ERROR: assertion failure@."
+                    (Abstract_syntax_printer.string_of_extent (snd stat));
+            end;
+            condition cond env
+        | AST_print items ->
+            Format.printf "%s: %s@."
+                (Abstract_syntax_printer.string_of_extent (snd stat))
+                (E.var_str env (List.map fst items));
+            env
+        | AST_local ((ty, _), vars) ->
+            List.fold_left
+                (fun env ((id, _), init) ->
+                    let env2 = E.addvar env id in
+                    match init with
+                    | Some e -> E.assign env2 id e
+                    | None -> env2)
+                env
+                vars
+        | _ -> assert false (* not implemented *)
+        end
+    
+    let interpret prog =
+        let result = List.fold_left
+            (fun env x -> match x with
+                | AST_stat st -> interp_stmt env st
+                | _ -> env)
+            E.init
+            (fst prog)
+        in
+            Format.printf "Output: %s@."
+                (E.var_str result (E.vars result))
 end