2 files changed, 80 insertions, 0 deletions
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