diff --git a/lib/drivers/alt_ergo.drv b/lib/drivers/alt_ergo.drv index 1f8ce9ffb1642451150db9b34933ee3f33dc6fe3..bbd02a605c2a06c912c42d7eae8012206d6771a3 100644 --- a/lib/drivers/alt_ergo.drv +++ b/lib/drivers/alt_ergo.drv @@ -37,8 +37,15 @@ theory prelude.Int syntax logic (_>=_) "(%1 >= %2)" syntax logic (_> _) "(%1 > %2)" - remove prop Mul_comm remove prop One_neutral + remove prop Add_assoc + remove prop Add_comm + remove prop Zero_neutral + remove prop Neg + remove prop Mul_comm + remove prop Mul_assoc + remove prop Mul_distr + end theory algebra.AC diff --git a/src/output/alt_ergo.ml b/src/output/alt_ergo.ml index 2d881fc0a44783daab6834dcb8a1396d7e48a91e..85aacd88d607f130d5652c324af7c496f8d3ffa6 100644 --- a/src/output/alt_ergo.ml +++ b/src/output/alt_ergo.ml @@ -139,9 +139,8 @@ let print_type_decl drv fmt = function | ts, Tabstract -> begin match Driver.query_ident drv ts.ts_name with - | Driver.Remove -> () - | Driver.Syntax _ -> () - | Driver.Tag s -> fprintf fmt "type %a" print_ident ts.ts_name + | Driver.Remove | Driver.Syntax _ -> false + | Driver.Tag _ -> fprintf fmt "type %a" print_ident ts.ts_name; true end | _, Talgebraic _ -> assert false @@ -152,8 +151,7 @@ let print_logic_decl drv ctxt fmt = function | Lfunction (ls, None) -> begin match Driver.query_ident drv ls.ls_name with - | Driver.Remove -> () - | Driver.Syntax _ -> () + | Driver.Remove | Driver.Syntax _ -> false | Driver.Tag s -> let sac = if Snm.mem "AC" s then "ac " else "" in let tyl = ls.ls_args in @@ -161,7 +159,8 @@ let print_logic_decl drv ctxt fmt = function fprintf fmt "@[<hov 2>logic %s%a : %a -> %a@]@\n" sac print_ident ls.ls_name - (print_list comma (print_type drv)) tyl (print_type drv) ty + (print_list comma (print_type drv)) tyl (print_type drv) ty; + true end | Lfunction (ls, Some defn) -> let id = ls.ls_name in @@ -169,45 +168,45 @@ let print_logic_decl drv ctxt fmt = function let ty = match ls.ls_value with None -> assert false | Some ty -> ty in fprintf fmt "@[<hov 2>function %a(%a) : %a =@ %a@]@\n" print_ident id (print_list comma (print_logic_binder drv)) vl (print_type drv) ty (print_term drv) t; - List.iter forget_var vl + List.iter forget_var vl;true | Lpredicate (ls, None) -> begin match Driver.query_ident drv ls.ls_name with - | Driver.Remove -> () - | Driver.Syntax _ -> () + | Driver.Remove | Driver.Syntax _ -> false | Driver.Tag s -> let sac = if Snm.mem "AC" s then "ac " else "" in fprintf fmt "@[<hov 2>logic %s%a : %a -> prop@]" sac - print_ident ls.ls_name (print_list comma (print_type drv)) ls.ls_args + print_ident ls.ls_name (print_list comma (print_type drv)) ls.ls_args; + true end | Lpredicate (ls, Some fd) -> let _,vl,f = open_ps_defn fd in fprintf fmt "@[<hov 2>predicate %a(%a) = %a@]" print_ident ls.ls_name - (print_list comma (print_logic_binder drv)) vl (print_fmla drv) f + (print_list comma (print_logic_binder drv)) vl (print_fmla drv) f; + true let print_decl drv ctxt fmt d = match d.d_node with | Dtype dl -> - print_list newline (print_type_decl drv) fmt dl + print_list_opt newline (print_type_decl drv) fmt dl | Dlogic dl -> - print_list newline (print_logic_decl drv ctxt) fmt dl + print_list_opt newline (print_logic_decl drv ctxt) fmt dl | Dind _ -> assert false (* TODO *) | Dprop (Paxiom, pr) when - Driver.query_ident drv pr.pr_name = Driver.Remove -> () + Driver.query_ident drv pr.pr_name = Driver.Remove -> false | Dprop (Paxiom, pr) -> fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n" - print_ident pr.pr_name (print_fmla drv) pr.pr_fmla + print_ident pr.pr_name (print_fmla drv) pr.pr_fmla; true | Dprop (Pgoal, pr) -> fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n" - print_ident pr.pr_name (print_fmla drv) pr.pr_fmla + print_ident pr.pr_name (print_fmla drv) pr.pr_fmla; true | Dprop (Plemma, _) -> assert false - | Duse _ | Dclone _ -> - () + | Duse _ | Dclone _ -> false let print_context drv fmt ctxt = let decls = Context.get_decls ctxt in - print_list newline2 (print_decl drv ctxt) fmt decls + ignore (print_list_opt newline2 (print_decl drv ctxt) fmt decls) let () = Driver.register_printer "alt-ergo" print_context diff --git a/src/output/driver.ml b/src/output/driver.ml index 0534fa23ddfab22b81ab9b5882b7c7ed592decb2..baf7412633a29dcb1bc1ed48362162f000d93377 100644 --- a/src/output/driver.ml +++ b/src/output/driver.ml @@ -28,9 +28,6 @@ open Ident (* From global_substitute of str *) open Str -let string_after s n fmt = pp_print_string fmt - (String.sub s n (String.length s - n)) - let opt_search_forward re s pos = try Some(search_forward re s pos) with Not_found -> None @@ -38,11 +35,11 @@ let global_substitute expr repl_fun text fmt = let rec replace start last_was_empty = let startpos = if last_was_empty then start + 1 else start in if startpos > String.length text then - string_after text start fmt + pp_print_string fmt (string_after text start) else match opt_search_forward expr text startpos with | None -> - string_after text start fmt + pp_print_string fmt (string_after text start) | Some pos -> let end_pos = match_end() in pp_print_string fmt (String.sub text start (pos-start)); diff --git a/src/util/pp.ml b/src/util/pp.ml index be4321281a0e5f3c8aab39ca5a70de845adb03cd..087e6993896385716065fd40bc70dfbec6338b77 100644 --- a/src/util/pp.ml +++ b/src/util/pp.ml @@ -125,3 +125,13 @@ let print_in_file ?(margin=78) p f = close_out cout + +(* With optional separation *) +let rec print_list_opt sep print fmt = function + | [] -> false + | [x] -> print fmt x + | x :: r -> + let notempty1 = print fmt x in + if notempty1 then sep fmt (); + let notempty2 = print_list_opt sep print fmt r in + notempty1 || notempty2 diff --git a/src/util/pp.mli b/src/util/pp.mli index fa80250edd33ccc7a8214d6f1656b4bf2d9e89a2..e78a8aebe92b2306a6150420ec8fd07667bba973 100644 --- a/src/util/pp.mli +++ b/src/util/pp.mli @@ -93,3 +93,8 @@ val open_file_and_formatter : ?margin:int -> string -> out_channel * formatter val close_file_and_formatter : out_channel * formatter -> unit val print_in_file_no_close : ?margin:int -> (Format.formatter -> unit) -> string -> out_channel val print_in_file : ?margin:int -> (Format.formatter -> unit) -> string -> unit + + +val print_list_opt : + (formatter -> unit -> unit) -> + (formatter -> 'a -> bool) -> formatter -> 'a list -> bool