open Ast
open Formula
open Ast_printer

let string_of_binary_rel = function
  | AST_EQ -> "="
  | AST_NE -> "≠"
  | AST_LT -> "<"
  | AST_LE -> "≤"
  | AST_GT -> ">"
  | AST_GE -> "≥"

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 is_or = function
  | BOr _ -> true
  | _ -> false
let is_and = function
  | BAnd _ -> true
  | _ -> false


let print_ch fmt pf fa a fe e =
  if fa a < fe e
    then Format.fprintf fmt "@[<hv 2>(%a)@]" pf a
    else Format.fprintf fmt "@[<hv 2>%a@]" pf a
let print_ah fmt pf fa a fe e =
  if fa a <= fe e
    then Format.fprintf fmt "@[<hv 2>(%a)@]" pf a
    else Format.fprintf fmt "@[<hv 2>%a@]" pf a

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 ->
    let re = Str.regexp "/" in
    Format.fprintf fmt "%s" (Str.global_replace re "·" id)
  | NBinary(op, a, b) ->
    print_ch fmt print_num_expr ne_prec a ne_prec e;
    Format.fprintf fmt "@ %s " (string_of_binary_op op);
    print_ah fmt print_num_expr ne_prec b ne_prec e
  | NUnary(op, a) ->
    Format.fprintf fmt "%s " (string_of_unary_op op);
    print_ah fmt print_num_expr ne_prec a ne_prec e

(* Print boolean form of formula *)

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_ch fmt print_num_expr ne_prec a be_prec e;
    Format.fprintf fmt "@ %s " (string_of_binary_rel op);
    print_ch fmt print_num_expr ne_prec b be_prec e
  | BAnd (a, b) ->

    if is_and a then
      Format.fprintf fmt "%a" print_bool_expr a
    else
      if be_prec a < be_prec e || is_or a
        then Format.fprintf fmt "@[<hv 2>(%a)@]" print_bool_expr a
        else Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr a;
    Format.fprintf fmt "@ ∧ ";
    if is_and b then
        Format.fprintf fmt "%a" print_bool_expr b
    else
      if be_prec b < be_prec e || is_or b
        then Format.fprintf fmt "@[<hv 2>(%a)@]" print_bool_expr b
        else Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr b

  | BOr (a, b) ->
    print_ch fmt print_bool_expr be_prec a be_prec e;
    Format.fprintf fmt "@ ∨ ";
    print_ch fmt print_bool_expr be_prec b be_prec e
  | BNot (a) ->
    Format.pp_print_string fmt "¬";
    print_ch fmt print_bool_expr be_prec a be_prec e

let print_expr fmt e =
  Format.fprintf fmt "@[<hv 2>%a@]" print_bool_expr e


(* Print constraint list form of formula *)

let print_cons fmt (eq, sg) =
  let sg_str = match sg with
  | CONS_EQ -> "="
  | CONS_NE -> "≠"
  | CONS_GT -> ">"
  | CONS_GE -> "≥"
  in
  Format.fprintf fmt "@[<hv 2>%a %s 0@]"
    print_num_expr eq sg_str

let rec print_conslist fmt (cons, e) =
  let rec aux = function
    | [] -> false
    | [a] ->
      Format.fprintf fmt "@[<hv 2>%a@]" print_cons a; true
    | p::q ->
      Format.fprintf fmt "@[<hv 2>%a@]" print_cons p;
      Format.fprintf fmt "@ ∧ ";
      aux q
  in
  match e with
  | CLTrue ->
    Format.fprintf fmt "@[<hv 2>(";
    ignore (aux cons);
    Format.fprintf fmt ")@]"
  | CLFalse -> 
    Format.fprintf fmt "false"
  | _ ->
    Format.fprintf fmt "@[<hv 2>(";
    if aux cons then Format.fprintf fmt "@ ∧ ";
    print_conslist_expr fmt e;
    Format.fprintf fmt ")@]"

and print_conslist_expr fmt = function
  | CLTrue -> Format.fprintf fmt "true"
  | CLFalse -> Format.fprintf fmt "false"
  | CLOr(a, b) ->
    Format.fprintf fmt "@[<hv 2>(%a@ ∨ %a)@]"
        print_conslist a
        print_conslist b
  | CLAnd(a, b) ->
    Format.fprintf fmt "%a@ ∧ %a"
        print_conslist_expr a
        print_conslist_expr b