Commit e12dddfd authored by Andrei Paskevich's avatar Andrei Paskevich

simplify the prelude printing API

parent d1a720d7
......@@ -325,9 +325,12 @@ let get_transform drv = drv.drv_transform
let get_printer drv = drv.drv_printer
let get_env drv = drv.drv_env
let print_prelude drv task fmt =
let print_prelude_list fmt prel =
let pr_pr s () = fprintf fmt "%s@\n" s in
List.fold_right pr_pr drv.drv_prelude ();
List.fold_right pr_pr prel ()
let print_prelude drv task fmt =
print_prelude_list fmt drv.drv_prelude;
let seen = Hid.create 17 in
let rec print_prel th_name th =
if Hid.mem seen th_name then () else begin
......@@ -337,12 +340,24 @@ let print_prelude drv task fmt =
try Mid.find th_name drv.drv_thprelude
with Not_found -> []
in
List.fold_right pr_pr prel ()
print_prelude_list fmt prel
end
in
Mid.iter print_prel (task_used task);
fprintf fmt "@."
let print_full_prelude dq = print_prelude dq.query_driver
let print_global_prelude dq fmt =
print_prelude_list fmt dq.query_driver.drv_prelude
let print_theory_prelude dq th_name fmt =
let prel =
try Mid.find th_name dq.query_driver.drv_thprelude
with Not_found -> []
in
print_prelude_list fmt prel
let filename_regexp = Str.regexp "%\\(.\\)"
let get_filename drv input_file theory_name goal_name =
......
......@@ -42,7 +42,7 @@ type driver_query
val driver_query : driver -> task -> driver_query
val query_syntax : driver_query -> ident -> string option
val query_syntax : driver_query -> ident -> string option
val query_remove : driver_query -> ident -> bool
val query_tags : driver_query -> ident -> Sstr.t
val query_clone : driver_query -> Theory.clone_map
......@@ -50,6 +50,10 @@ val query_driver : driver_query -> driver
val query_env : driver_query -> env
val query_tag : driver_query -> int
val print_global_prelude : driver_query -> formatter -> unit
val print_theory_prelude : driver_query -> ident -> formatter -> unit
val print_full_prelude : driver_query -> task -> formatter -> unit
(** {2 use a driver} *)
val get_env : driver -> env
......@@ -59,8 +63,6 @@ val get_transform : driver -> string list
(** file_of_task input_file theory_name task *)
val file_of_task : driver -> string -> string -> task -> string
val print_prelude : driver -> task -> formatter -> unit
val call_on_buffer :
?debug : bool ->
command : string ->
......
......@@ -201,6 +201,7 @@ let print_decl drv fmt d = match d.d_node with
let print_decl drv fmt = catch_unsupportedDeclaration (print_decl drv fmt)
let print_task drv fmt task =
Driver.print_full_prelude drv task fmt;
let decls = Task.task_decls task in
ignore (print_list_opt (add_flush newline2) (print_decl drv) fmt decls)
......@@ -210,7 +211,6 @@ let () = register_printer "alt-ergo"
print_task drv fmt task)
let print_goal drv fmt (id, f, task) =
Driver.print_prelude (Driver.query_driver drv) task fmt;
print_task drv fmt task;
fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id (print_fmla drv) f
......@@ -327,7 +327,7 @@ let print_decls drv fmt dl =
let print_task drv fmt task =
forget_all ();
Driver.print_prelude (Driver.query_driver drv) task fmt;
Driver.print_full_prelude drv task fmt;
print_decls drv fmt (Task.task_decls task)
let () = Register.register_printer "coq" print_task
......
......@@ -195,7 +195,7 @@ let print_task drv fmt task =
fprintf fmt "(benchmark toto@\n"
(*print_ident (Task.task_goal task).pr_name*);
fprintf fmt " :status unknown@\n";
Driver.print_prelude (Driver.query_driver drv) task fmt;
Driver.print_full_prelude drv task fmt;
let decls = Task.task_decls task in
ignore (print_list_opt (add_flush newline2) (print_decl drv) fmt decls);
fprintf fmt "@\n)@."
......
......@@ -329,7 +329,7 @@ let print_decls drv fmt dl =
let print_task drv fmt task =
forget_all ();
Driver.print_prelude (Driver.query_driver drv) task fmt;
Driver.print_full_prelude drv task fmt;
print_decls drv fmt (Task.task_decls task)
let () = Register.register_printer "why3" print_task
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment