diff options
| -rw-r--r-- | Makefile | 10 | ||||
| -rw-r--r-- | abstract/formula.ml | 24 | ||||
| -rw-r--r-- | abstract/formula_printer.ml | 56 | ||||
| -rw-r--r-- | frontend/ast_printer.ml | 3 | ||||
| -rw-r--r-- | interpret/data.ml | 6 | ||||
| -rw-r--r-- | interpret/interpret.ml (renamed from interpret/interpret2.ml) | 2 | ||||
| -rw-r--r-- | main.ml | 71 |
7 files changed, 123 insertions, 49 deletions
@@ -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) @@ -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) -> |