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