open Util open Ast open Formula open Ast_printer (* Just a pretty-printer, nothing to see here *) let string_of_binary_rel = function | AST_EQ -> "=" | AST_NE -> "≠" | AST_LT -> "<" | AST_LE -> "≤" | AST_GT -> ">" | AST_GE -> "≥" let ne_prec = function | NUnary _ -> unary_precedence | NBinary(op, _, _, _) -> binary_op_precedence op | _ -> 100 let be_prec = function | BTernary _ -> 10 | 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 "@[(%a)@]" pf a else Format.fprintf fmt "@[%a@]" pf a let print_ah fmt pf fa a fe e = if fa a <= fe e then Format.fprintf fmt "@[(%a)@]" pf a else Format.fprintf fmt "@[%a@]" pf a let print_id fmt id = let re = Str.regexp "/" in Format.fprintf fmt "%s" (Str.global_replace re "·" id) 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 -> print_id fmt id | NBinary(op, a, b, is_real) -> print_ch fmt print_num_expr ne_prec a ne_prec e; Format.fprintf fmt "@ %s%s " (string_of_binary_op op) (if is_real then "." else ""); print_ah fmt print_num_expr ne_prec b ne_prec e | NUnary(op, a, is_real) -> Format.fprintf fmt "%s%s " (string_of_unary_op op) (if is_real then "." else ""); print_ah fmt print_num_expr ne_prec a ne_prec e (* Enumeated expressions *) let print_enum_expr fmt = function | EIdent id -> print_id fmt id | EItem x -> Format.fprintf fmt "%s" x let str_of_enum_op = function | E_EQ -> "≡" | E_NE -> "≢" let print_econs fmt (op, a, b) = Format.fprintf fmt "%a %s %a" print_id a (str_of_enum_op op) print_enum_expr b (* 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") | BEnumCons c -> print_econs fmt c | BRel(op, a, b, is_real) -> print_ch fmt print_num_expr ne_prec a be_prec e; Format.fprintf fmt "@ %s%s " (string_of_binary_rel op) (if is_real then "." else ""); 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 "@[(%a)@]" print_bool_expr a else Format.fprintf fmt "@[%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 "@[(%a)@]" print_bool_expr b else Format.fprintf fmt "@[%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 | BTernary(c, a, b) -> print_ah fmt print_bool_expr be_prec c be_prec e; Format.fprintf fmt "@ ? "; print_ah fmt print_bool_expr be_prec a be_prec e; Format.fprintf fmt "@ : "; print_ah 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 "@[%a@]" print_bool_expr e (* Print constraint list form of formula *) let print_cons_sg fmt sg = let sg_str = match sg with | CONS_EQ -> "=" | CONS_NE -> "≠" | CONS_GT -> ">" | CONS_GE -> "≥" in Format.fprintf fmt "%s" sg_str let print_cons fmt (eq, sg) = Format.fprintf fmt "@[%a %a 0@]" print_num_expr eq print_cons_sg sg let rec print_conslist fmt (econs, cons, e) = let c = (List.map (fun x -> Left x) econs) @ (List.map (fun y -> Right y) cons) in let f fmt = function | Left x -> Format.fprintf fmt "@[%a@]" print_econs x | Right x -> Format.fprintf fmt "@[%a@]" print_cons x in let rec aux = function | [] -> false | [a] -> f fmt a; true | p::q -> f fmt p; Format.fprintf fmt "@ ∧ "; aux q in match e with | CLTrue -> Format.fprintf fmt "@[("; ignore (aux c); Format.fprintf fmt ")@]" | CLFalse -> Format.fprintf fmt "false" | _ -> Format.fprintf fmt "@[("; if aux c 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 "@[(%a@ ∨ %a)@]" print_conslist a print_conslist b | CLAnd(a, b) -> Format.fprintf fmt "%a@ ∧ %a" print_conslist_expr a print_conslist_expr b