Add AST for logical formula.

7 files changed, 123 insertions, 49 deletions

diff --git a/Makefile b/Makefile
index 62245ae..681b651 100644
--- a/Makefile
+++ b/Makefile
@@ -1,17 +1,18 @@
 .PHONY: clean
 
 BIN=analyze
-SRCDIRS=libs,frontend,interpret
+SRCDIRS=libs,frontend,interpret,abstract
 
 SRC= 	main.ml \
 		frontend/ast.ml \
 		frontend/parser.mly \
 		frontend/lexer.mll \
 		frontend/ast_printer.ml \
-		interpret/data.ml \
+		abstract/formula.ml \
+		abstract/formula_printer.ml \
 		interpret/bad_interpret.ml \
 		interpret/interface.ml \
-		interpret/interpret2.ml \
+		interpret/interpret.ml \
 		interpret/rename.ml
 
 all: $(BIN)
@@ -23,4 +24,5 @@ $(BIN): $(SRC)
 	mv main.native $(BIN)
 
 clean:
-	rm -rf _build
+	rm $(BIN)
+	ocamlbuild -clean
diff --git a/abstract/formula.ml b/abstract/formula.ml
new file mode 100644
index 0000000..389000c
--- /dev/null
+++ b/abstract/formula.ml
@@ -0,0 +1,24 @@
+open Ast
+
+(* AST for logical formulas *)
+
+type num_expr =
+  (* constants *)
+  | NIntConst of int
+  | NRealConst of float
+  (* operators *)
+  | NBinary of binary_op * num_expr * num_expr
+  | NUnary of unary_op * num_expr
+  (* identifier *)
+  | NIdent of id
+
+type bool_expr =
+  (* constants *)
+  | BConst of bool
+  (* operators from numeric values to boolean values *)
+  | BRel of binary_rel_op * num_expr * num_expr
+  (* boolean operators *)
+  | BAnd of bool_expr * bool_expr
+  | BOr of bool_expr * bool_expr
+  | BNot of bool_expr
+
diff --git a/abstract/formula_printer.ml b/abstract/formula_printer.ml
new file mode 100644
index 0000000..7e626f0
--- /dev/null
+++ b/abstract/formula_printer.ml
@@ -0,0 +1,56 @@
+open Formula
+open Ast_printer
+
+let ne_prec = function
+  | NUnary(op, _) -> unary_precedence
+  | NBinary(op, _, _) -> binary_op_precedence op
+  | _ -> 100
+
+let be_prec = function
+  | BRel(op, _, _) -> binary_rel_precedence op
+  | BAnd _ -> binary_bool_precedence AST_AND
+  | BOr _ -> binary_bool_precedence AST_OR
+  | BNot _ -> unary_precedence
+  | _ -> 100
+
+
+let print_lh fmt pf fa a fe e =
+  if fa a < fe e
+    then Format.fprintf fmt "@[<2>(%a)@]" pf a
+    else Format.fprintf fmt "%a" pf a
+let print_rh fmt pf fb b fe e =
+  if fb b < fe e
+    then Format.fprintf fmt "@[<2>(%a)@]" pf b
+    else Format.fprintf fmt "%a" pf b
+
+let rec print_num_expr fmt e = match e with
+  | NIntConst i -> Format.fprintf fmt "%d" i
+  | NRealConst f -> Format.fprintf fmt "%f" f
+  | NIdent id -> Format.fprintf fmt "%s" id
+  | NBinary(op, a, b) ->
+    print_lh fmt print_num_expr ne_prec a ne_prec e;
+    Format.fprintf fmt "@ %s@ " (string_of_binary_op op);
+    print_rh fmt print_num_expr ne_prec b ne_prec e
+  | NUnary(op, a) ->
+    Format.pp_print_string fmt (string_of_unary_op op);
+    print_rh fmt print_num_expr ne_prec a ne_prec e
+
+let rec print_bool_expr fmt e = match e with
+  | BConst b -> Format.fprintf fmt "%s" (if b then "true" else "false")
+  | BRel(op, a, b) ->
+    print_lh fmt print_num_expr ne_prec a be_prec e;
+    Format.fprintf fmt "@ %s@ " (string_of_binary_rel op);
+    print_rh fmt print_num_expr ne_prec b be_prec e
+  | BAnd (a, b) ->
+    print_lh fmt print_bool_expr be_prec a be_prec e;
+    Format.fprintf fmt "@ /\\@ ";
+    print_rh fmt print_bool_expr be_prec b be_prec e
+  | BOr (a, b) ->
+    print_lh fmt print_bool_expr be_prec a be_prec e;
+    Format.fprintf fmt "@ \\/@ ";
+    print_rh fmt print_bool_expr be_prec b be_prec e
+  | BNot (a) ->
+    Format.pp_print_string fmt "!";
+    print_rh fmt print_bool_expr be_prec a be_prec e
+
+let print_expr = print_bool_expr
diff --git a/frontend/ast_printer.ml b/frontend/ast_printer.ml
index 08f4fb4..b6dcdbc 100644
--- a/frontend/ast_printer.ml
+++ b/frontend/ast_printer.ml
@@ -44,6 +44,7 @@ let string_of_binary_bool = function
   | AST_OR -> "or"
 
 
+let unary_precedence = 99
 let binary_op_precedence = function
   | AST_MUL| AST_DIV| AST_MOD-> 51
   | AST_PLUS  | AST_MINUS -> 50
@@ -57,7 +58,7 @@ let arrow_precedence = 20
 let if_precedence = 10
 
 let expr_precedence = function
-  | AST_unary (_, _) | AST_pre(_, _) | AST_not(_) -> 99
+  | AST_unary (_, _) | AST_pre(_, _) | AST_not(_) -> unary_precedence
   | AST_binary(op, _, _) -> binary_op_precedence op
   | AST_binary_rel(r, _, _) -> binary_rel_precedence r
   | AST_binary_bool(r, _, _) -> binary_bool_precedence r
diff --git a/interpret/data.ml b/interpret/data.ml
deleted file mode 100644
index 1d91e93..0000000
--- a/interpret/data.ml
+++ /dev/null
@@ -1,6 +0,0 @@
-(* Data structures for representing the state of a system *)
-
-open Util
-open Ast
-open Ast_util
-
diff --git a/interpret/interpret2.ml b/interpret/interpret.ml
index d6f7731..063dad0 100644
--- a/interpret/interpret2.ml
+++ b/interpret/interpret.ml
@@ -350,6 +350,7 @@ module I : INTERPRET = struct
       let save = VarMap.add (node^"/"^prefix^"init") (VBool init) save in
 
       let save_expr save e =
+        (* Save pre expressions *)
         let save = List.fold_left
           (fun save (id, expr) ->
             let n = node^"/"^prefix^id in
@@ -365,6 +366,7 @@ module I : INTERPRET = struct
               with Not_found -> save
           )
           save (extract_pre e) in
+        (* Save recursively in sub instances of nodes *)
         let save = List.fold_left
           (fun save (n, eqs, _) ->
             aux (node^"/"^n, "", eqs) save)
diff --git a/main.ml b/main.ml
index bd67cb4..61755e3 100644
--- a/main.ml
+++ b/main.ml
@@ -1,6 +1,6 @@
 open Ast
 
-module Interpret = Interpret2.I
+module Interpret = Interpret.I
 
 (* command line options *)
 let dump = ref false
@@ -18,6 +18,36 @@ let options = [
     "--test", Arg.Set test, "Simple testing.";
 ]
 
+let do_test_interpret prog verbose =
+    let s0 = Interpret.init_state prog "test" in
+    if verbose then begin
+      Format.printf "Init state:@.";
+      Interpret.print_state Format.std_formatter s0;
+    end;
+    let rec it i st =
+      let next_st, out =
+        Interpret.step st
+        ["i", Interpret.int_value i]
+      in
+      if verbose then begin
+        Format.printf "@.> Step %d:@." i;
+        Interpret.print_state Format.std_formatter st;
+        Format.printf "Outputs:@.";
+        List.iter
+          (fun (k, v) -> Format.printf "%s = %s@."
+              k (Interpret.str_repr_of_val v))
+            out;
+      end else begin
+        Format.printf "%d. %s %s %s@." i 
+          (Interpret.str_repr_of_val (List.assoc "a" out))
+          (Interpret.str_repr_of_val (List.assoc "b" out))
+          (Interpret.str_repr_of_val (List.assoc "c" out));
+      end;
+      if not (Interpret.as_bool (List.assoc "exit" out)) then
+        it (i+1) next_st
+    in
+    it 0 s0
+
 let () =
     Arg.parse options (fun f -> ifile := f) usage;
 
@@ -33,44 +63,9 @@ let () =
       let prog = Rename.rename_prog prog in
       if !dumprn then Ast_printer.print_prog Format.std_formatter prog;
 
-      if !vtest then begin
-        let s0 = Interpret.init_state prog "test" in
-        Format.printf "Init state:@.";
-        Interpret.print_state Format.std_formatter s0;
-        let rec it i st =
-          let next_st, out =
-            Interpret.step st
-            ["i", Interpret.int_value i]
-          in
-          Format.printf "@.> Step %d:@." i;
-          Interpret.print_state Format.std_formatter st;
-          Format.printf "Outputs:@.";
-          List.iter
-            (fun (k, v) -> Format.printf "%s = %s@."
-                k (Interpret.str_repr_of_val v))
-              out;
-          if not (Interpret.as_bool (List.assoc "exit" out)) then
-            it (i+1) next_st
-        in
-        it 0 s0
-      end;
+      if !vtest then do_test_interpret prog true
+      else if !test then do_test_interpret prog false;
 
-      if !test then begin
-        let s0 = Interpret.init_state prog "test" in
-        let rec it i st =
-          let next_st, outputs =
-            Interpret.step st
-            ["i", Interpret.int_value i]
-          in
-          Format.printf "%d. %s %s %s@." i 
-            (Interpret.str_repr_of_val (List.assoc "a" outputs))
-            (Interpret.str_repr_of_val (List.assoc "b" outputs))
-            (Interpret.str_repr_of_val (List.assoc "c" outputs));
-          if not (Interpret.as_bool (List.assoc "exit" outputs)) then
-            it (i+1) next_st
-        in
-        it 0 s0
-      end
     with
     | Util.NoLocError e -> Format.eprintf "Error: %s@." e
     | Util.LocError(l, e) ->