Commit 6b8c6a97 authored by Andrei Paskevich's avatar Andrei Paskevich

Printer: gather printer arguments in a single record type

Submitted by Johannes Kanig
parent 170ce1dc
......@@ -255,11 +255,11 @@ let print_decls fm =
let print_task fm =
let print_decls = print_decls fm in
fun _env pr thpr _blacklist ?old:_ fmt task ->
fun args ?old:_ fmt task ->
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
print_prelude fmt pr;
print_th_prelude task fmt thpr;
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
......@@ -391,12 +391,12 @@ let print_axiom info fmt d = match d.d_node with
(print_fmla info) f print_pr pr
| _ -> ()
let print_dfg _env pr thpr _blacklist ?old:_ fmt task =
let print_dfg args ?old:_ fmt task =
forget_all ident_printer;
forget_all pr_printer;
fprintf fmt "@[begin_problem(why3).@\n@\n";
print_prelude fmt pr;
print_th_prelude task fmt thpr;
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
fprintf fmt "list_of_descriptions.@\n";
fprintf fmt
"name({**}). author({**}). status(unknown). description({**}).@\n";
......
......@@ -28,8 +28,14 @@ type blacklist = string list
type 'a pp = formatter -> 'a -> unit
type printer =
Env.env -> prelude -> prelude_map -> blacklist -> ?old:in_channel -> task pp
type printer_args = {
env : Env.env;
prelude : prelude;
th_prelude : prelude_map;
blacklist : blacklist;
}
type printer = printer_args -> ?old:in_channel -> task pp
type reg_printer = Pp.formatted * printer
......@@ -51,7 +57,7 @@ let list_printers () =
let () = register_printer
~desc:"Dummy@ printer@ with@ no@ output@ (used@ for@ debugging)." "(null)"
(fun _ _ _ _ ?old:_ _ _ -> ())
(fun _ ?old:_ _ _ -> ())
(** Syntax substitutions *)
......
......@@ -24,8 +24,14 @@ type blacklist = string list
type 'a pp = Format.formatter -> 'a -> unit
type printer =
Env.env -> prelude -> prelude_map -> blacklist -> ?old:in_channel -> task pp
type printer_args = {
env : Env.env;
prelude : prelude;
th_prelude : prelude_map;
blacklist : blacklist;
}
type printer = printer_args -> ?old:in_channel -> task pp
val register_printer : desc:Pp.formatted -> string -> printer -> unit
......
......@@ -281,10 +281,11 @@ let print_task_prepared ?old drv fmt task =
| None -> raise NoPrinter
| Some p -> p
in
let printer =
lookup_printer p drv.drv_env drv.drv_prelude drv.drv_thprelude
drv.drv_blacklist
in
let printer = lookup_printer p
{ Printer.env = drv.drv_env;
prelude = drv.drv_prelude;
th_prelude = drv.drv_thprelude;
blacklist = drv.drv_blacklist } in
fprintf fmt "@[%a@]@?" (printer ?old) task
let print_task ?old drv fmt task =
......
......@@ -377,11 +377,11 @@ let print_decls =
} in
Trans.fold print_decl (info,[]))))))
let print_task _env pr thpr _blacklist ?old:_ fmt task =
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
print_prelude fmt pr;
print_th_prelude task fmt thpr;
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
......
......@@ -962,11 +962,11 @@ let print_decl ~old info fmt d =
let print_decls ~old info fmt dl =
fprintf fmt "@\n@[<hov>%a@\n@]" (print_list nothing (print_decl ~old info)) dl
let print_task env pr thpr _blacklist realize ?old fmt task =
let print_task printer_args realize ?old fmt task =
(* eprintf "Task:%a@.@." Pretty.print_task task; *)
forget_all ();
print_prelude fmt pr;
print_th_prelude task fmt thpr;
print_prelude fmt printer_args.prelude;
print_th_prelude task fmt printer_args.th_prelude;
(* find theories that are both used and realized from metas *)
let realized_theories =
Task.on_meta meta_realized_theory (fun mid args ->
......@@ -976,7 +976,7 @@ let print_task env pr thpr _blacklist realize ?old fmt task =
let f,id =
let l = Strings.rev_split s1 '.' in
List.rev (List.tl l), List.hd l in
let th = Env.find_theory env f id in
let th = Env.find_theory printer_args.env f id in
Mid.add th.Theory.th_name (th, if s2 = "" then s1 else s2) mid
| _ -> assert false
) Mid.empty task in
......@@ -1017,11 +1017,11 @@ let print_task env pr thpr _blacklist realize ?old fmt task =
print_decls ~old info fmt local_decls;
output_remaining fmt !old
let print_task_full env pr thpr blacklist ?old fmt task =
print_task env pr thpr blacklist false ?old fmt task
let print_task_full args ?old fmt task =
print_task args false ?old fmt task
let print_task_real env pr thpr blacklist ?old fmt task =
print_task env pr thpr blacklist true ?old fmt task
let print_task_real args ?old fmt task =
print_task args true ?old fmt task
let () = register_printer "coq" print_task_full
~desc:"Printer@ for@ the@ Coq@ proof@ assistant@ \
......
......@@ -269,11 +269,11 @@ let print_decls =
Discriminate.on_syntax_map (fun sm ->
Trans.fold print_decl ((sm,Mty.empty),[]))
let print_task _env pr thpr _blacklist ?old:_ fmt task =
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
print_prelude fmt pr;
print_th_prelude task fmt thpr;
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
......
......@@ -433,11 +433,11 @@ let print_goal info fmt g =
fprintf fmt "# (no goal at all ??)@\n";
fprintf fmt "1 in [0,0]@\n"
let print_task env pr thpr _blacklist ?old:_ fmt task =
let print_task args ?old:_ fmt task =
forget_all ident_printer;
let info = get_info env task in
print_prelude fmt pr;
print_th_prelude task fmt thpr;
let info = get_info args.env task in
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
let equations,hyps,goal =
List.fold_left (prepare info (Hid.create 17)) ([],[],Goal_none) (Task.task_decls task)
in
......
......@@ -514,12 +514,12 @@ let print_goal info fmt g =
fprintf fmt "False@\n"
let print_task env pr thpr _blacklist ?old:_ fmt task =
let print_task args ?old:_ fmt task =
forget_all ident_printer;
let info = get_info env task in
print_prelude fmt (List.append pr ["$MaxExtraPrecision = 256;
let info = get_info args.env task in
print_prelude fmt (List.append args.prelude ["$MaxExtraPrecision = 256;
ClearAll[vcWhy,varsWhy,resWhy];"]);
print_th_prelude task fmt thpr;
print_th_prelude task fmt args.th_prelude;
let params,funs,preds,eqs,hyps,goal,types =
List.fold_left (prepare info (Hid.create 17)) ([],[],[],[],[],Goal_none,[])
(Task.task_decls task)
......
......@@ -815,10 +815,10 @@ let init_printer th =
Sid.iter (fun id -> ignore (id_unique pr id)) th.Theory.th_local;
pr
let print_task env pr thpr _blacklist realize ?old fmt task =
let print_task printer_args realize ?old fmt task =
forget_all ();
print_prelude fmt pr;
print_th_prelude task fmt thpr;
print_prelude fmt printer_args.prelude;
print_th_prelude task fmt printer_args.th_prelude;
(* find theories that are both used and realized from metas *)
let realized_theories =
Task.on_meta meta_realized_theory (fun mid args ->
......@@ -827,7 +827,7 @@ let print_task env pr thpr _blacklist realize ?old fmt task =
let f,id =
let l = Strings.rev_split s1 '.' in
List.rev (List.tl l), List.hd l in
let th = Env.find_theory env f id in
let th = Env.find_theory printer_args.env f id in
Mid.add th.Theory.th_name
(th, (f, if s2 = "" then String.concat "." f else s2)) mid
| _ -> assert false
......@@ -898,11 +898,11 @@ let print_task env pr thpr _blacklist realize ?old fmt task =
output_remaining fmt !old;
fprintf fmt "@]@\nEND %s@\n@]" thname
let print_task_full env pr thpr blacklist ?old fmt task =
print_task env pr thpr blacklist false ?old fmt task
let print_task_full args ?old fmt task =
print_task args false ?old fmt task
let print_task_real env pr thpr blacklist ?old fmt task =
print_task env pr thpr blacklist true ?old fmt task
let print_task_real args ?old fmt task =
print_task args true ?old fmt task
let () = register_printer "pvs" print_task_full
~desc:"Printer@ for@ the@ PVS@ proof@ assistant@ \
......
......@@ -151,11 +151,11 @@ let print_decls =
let print_decl task acc = print_decl task.Task.task_decl acc in
Discriminate.on_syntax_map (fun sm -> Trans.fold print_decl (sm,[]))
let print_task _env pr thpr _blacklist ?old:_ fmt task =
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
print_prelude fmt pr;
print_th_prelude task fmt thpr;
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
......
......@@ -225,13 +225,13 @@ let print_decls =
Discriminate.on_syntax_map (fun sm ->
Trans.fold print_decl ((sm,Mty.empty),[]))
let print_task _env pr thpr _blacklist ?old:_ fmt task =
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
fprintf fmt "(benchmark why3@\n";
fprintf fmt " :status unknown@\n";
print_prelude fmt pr;
print_th_prelude task fmt thpr;
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
......
......@@ -276,11 +276,11 @@ let print_decls =
let print_decl task acc = print_decl task.Task.task_decl acc in
Discriminate.on_syntax_map (fun sm -> Trans.fold print_decl (sm,[]))
let print_task _env pr thpr _blacklist ?old:_ fmt task =
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
print_prelude fmt pr;
print_th_prelude task fmt thpr;
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
......
......@@ -384,12 +384,12 @@ let print_tdecls =
let print_tdecl task acc = print_tdecl task.Task.task_decl acc in
Discriminate.on_syntax_map (fun sm -> Trans.fold print_tdecl (sm,[]))
let print_task _env pr thpr _blacklist ?old:_ fmt task =
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] IST STRENG VERBOTEN *)
(* forget_all (); *)
print_prelude fmt pr;
print_prelude fmt args.prelude;
fprintf fmt "theory Task@\n";
print_th_prelude task fmt thpr;
print_th_prelude task fmt args.th_prelude;
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
......
......@@ -278,11 +278,11 @@ let print_decls =
Discriminate.on_syntax_map (fun sm ->
Trans.fold print_decl ((sm,Mty.empty),[]))
let print_task _env pr thpr _blacklist ?old:_ fmt task =
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
print_prelude fmt pr;
print_th_prelude task fmt thpr;
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
......
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