Commit c0e146fa authored by Andrei Paskevich's avatar Andrei Paskevich

allow printers to produce "urgent output"

this is useful to declare on-the-fly a new sort which replaces
a complex type. Otherwise, the printer has to traverse any term
twice: first, to detect complex types, second, to print the term.
parent 9640fb2b
......@@ -51,49 +51,40 @@ type info = {
info_syn : syntax_map;
info_fmt : tptp_format;
info_srt : ty Mty.t ref;
info_urg : string list ref;
}
let complex_type = Wty.memoize 3 (fun ty ->
let s = Pp.string_of_wnl Pretty.print_ty ty in
create_tysymbol (id_fresh s) [] None)
let rec print_type info fmt ty = match ty.ty_node with
| Tyvar _ when info.info_fmt = TFF0 ->
unsupported "TFF0 does not support polymorphic types"
| Tyvar tv -> print_tvar fmt tv
| Tyapp (ts, tl) ->
begin match query_syntax info.info_syn ts.ts_name, tl with
| Some s, _ -> syntax_arguments s (print_type info) fmt tl
| None, [] -> print_symbol fmt ts.ts_name
| None, _ when info.info_fmt = TFF0 ->
print_type info fmt (Mty.find ty !(info.info_srt))
begin match Mty.find_opt ty !(info.info_srt) with
| Some ty -> print_type info fmt ty
| None ->
let ts = complex_type ty in let cty = ty_app ts [] in
let us = sprintf "@[<hov 2>tff(%s, type,@ %a:@ $tType).@]@\n@\n"
(id_unique pr_printer ts.ts_name) print_symbol ts.ts_name in
info.info_srt := Mty.add ty cty !(info.info_srt);
info.info_urg := us :: !(info.info_urg);
print_type info fmt cty
end
| None, tl ->
fprintf fmt "@[%a(%a)@]" print_symbol ts.ts_name
(print_list comma (print_type info)) tl
end
let complex_type = Wty.memoize 3 (fun ty ->
let s = Pp.string_of_wnl Pretty.print_ty ty in
create_tysymbol (id_fresh s) [] None)
let rec iter_complex_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "TFF0 does not support polymorphic types"
| Tyapp (_, []) -> ()
| Tyapp (ts, l) ->
begin match query_syntax info.info_syn ts.ts_name with
| Some _ -> List.iter (iter_complex_type info fmt) l
| None when Mty.mem ty !(info.info_srt) -> ()
| None ->
let ts = complex_type ty in
fprintf fmt "@[<hov 2>tff(%s, type,@ %a:@ $tType).@]@\n@\n"
(id_unique pr_printer ts.ts_name) print_symbol ts.ts_name;
info.info_srt := Mty.add ty (ty_app ts []) !(info.info_srt)
end
let iter_complex_type info fmt ty =
try iter_complex_type info fmt ty
let print_type info fmt ty = try print_type info fmt ty
with Unsupported s -> raise (UnsupportedType (ty,s))
let find_complex_type info fmt f = if info.info_fmt = TFF0 then
t_ty_fold (fun () ty -> iter_complex_type info fmt ty) () f
let iter_complex_type info fmt ty = if info.info_fmt = TFF0 then
iter_complex_type info fmt ty
let number_format = {
Number.long_int_support = true;
Number.extra_leading_zeros_support = false;
......@@ -209,8 +200,6 @@ let print_decl info fmt d = match d.d_node with
| Dparam _ when info.info_fmt = FOF -> ()
| Dparam ls when query_syntax info.info_syn ls.ls_name <> None -> ()
| Dparam ls ->
List.iter (iter_complex_type info fmt) ls.ls_args;
Opt.iter (iter_complex_type info fmt) ls.ls_value;
let print_type = print_type info in
let print_val fmt = function
| Some ty -> print_type fmt ty
......@@ -243,12 +232,10 @@ let print_decl info fmt d = match d.d_node with
"TPTP does not support inductive predicates, use eliminate_inductive"
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> ()
| Dprop (Paxiom, pr, f) ->
find_complex_type info fmt f;
let head = if info.info_fmt = FOF then "fof" else "tff" in
fprintf fmt "@[<hov 2>%s(%a, axiom,@ %a).@]@\n@\n"
head print_pr pr (print_fmla info) f
| Dprop (Pgoal, pr, f) ->
find_complex_type info fmt f;
let head = if info.info_fmt = FOF then "fof" else "tff" in
fprintf fmt "@[<hov 2>%s(%a, conjecture,@ %a).@]@\n"
head print_pr pr (print_fmla info) f
......@@ -256,9 +243,10 @@ let print_decl info fmt d = match d.d_node with
let print_decls fm =
let print_decl (sm,fm,ct) fmt d =
let info = {
info_syn = sm; info_fmt = fm; info_srt = ref ct } in
try print_decl info fmt d; (sm,fm,!(info.info_srt))
let info = { info_syn = sm; info_fmt = fm;
info_srt = ref ct; info_urg = ref [] } in
try print_decl info fmt d;
(sm,fm,!(info.info_srt)), !(info.info_urg)
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
......@@ -413,8 +401,11 @@ let print_dfg _env pr thpr _blacklist ?old:_ fmt task =
fprintf fmt
"name({**}). author({**}). status(unknown). description({**}).@\n";
fprintf fmt "end_of_list.@\n@\n";
let info = { info_syn = get_syntax_map task;
info_fmt = FOF; info_srt = ref Mty.empty } in
let info = {
info_syn = get_syntax_map task;
info_fmt = FOF;
info_urg = ref [];
info_srt = ref Mty.empty } in
let dl = Task.task_decls task in
let tl = List.filter (is_type info) dl in
let fl = List.filter (is_function info) dl in
......
......@@ -276,24 +276,24 @@ let on_syntax_map fn =
let sm = List.fold_left sm_add_pr sm spr in
fn sm)))
let sprint_tdecl (fn : 'a -> Format.formatter -> tdecl -> 'a) =
let sprint_tdecl (fn : 'a -> Format.formatter -> tdecl -> 'a * string list) =
let buf = Buffer.create 2048 in
let fmt = Format.formatter_of_buffer buf in
fun td (acc,strl) ->
Buffer.reset buf;
let acc = fn acc fmt td in
let acc, urg = fn acc fmt td in
Format.pp_print_flush fmt ();
acc, Buffer.contents buf :: strl
acc, Buffer.contents buf :: List.rev_append urg strl
let sprint_decl (fn : 'a -> Format.formatter -> decl -> 'a) =
let sprint_decl (fn : 'a -> Format.formatter -> decl -> 'a * string list) =
let buf = Buffer.create 2048 in
let fmt = Format.formatter_of_buffer buf in
fun td (acc,strl) -> match td.td_node with
| Decl d ->
Buffer.reset buf;
let acc = fn acc fmt d in
let acc, urg = fn acc fmt d in
Format.pp_print_flush fmt ();
acc, Buffer.contents buf :: strl
acc, Buffer.contents buf :: List.rev_append urg strl
| _ -> acc, strl
(** {2 exceptions to use in transformations and printers} *)
......
......@@ -75,11 +75,11 @@ val syntax_arguments_typed :
val on_syntax_map : (syntax_map -> 'a Trans.trans) -> 'a Trans.trans
val sprint_tdecl :
('a -> Format.formatter -> Theory.tdecl -> 'a) ->
('a -> Format.formatter -> Theory.tdecl -> 'a * string list) ->
Theory.tdecl -> 'a * string list -> 'a * string list
val sprint_decl :
('a -> Format.formatter -> Decl.decl -> 'a) ->
('a -> Format.formatter -> Decl.decl -> 'a * string list) ->
Theory.tdecl -> 'a * string list -> 'a * string list
(** {2 exceptions to use in transformations and printers} *)
......
......@@ -354,7 +354,7 @@ let check_typecasts acc = function
let print_decls =
let print_decl info fmt d =
try print_decl info fmt d; info
try print_decl info fmt d; info, []
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
......
......@@ -50,42 +50,35 @@ let print_ident fmt id =
type info = {
info_syn : syntax_map;
complex_type : ty Mty.t ref;
urg_output : string list ref;
}
(** type *)
let rec print_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "cvc3 : you must encode the polymorphism"
| Tyapp (ts, l) ->
begin match query_syntax info.info_syn ts.ts_name, l with
| Some s, _ -> syntax_arguments s (print_type info) fmt l
| None, [] -> fprintf fmt "%a" print_ident ts.ts_name
| None, _ -> print_type info fmt (Mty.find ty !(info.complex_type))
end
let complex_type = Wty.memoize 3 (fun ty ->
let s = Pp.string_of_wnl Pretty.print_ty ty in
create_tysymbol (id_fresh s) [] None)
let rec iter_complex_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "cvc3 : you must encode the polymorphism"
| Tyapp (_, []) -> ()
let rec print_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "cvc3: you must encode the polymorphism"
| Tyapp (ts, l) ->
begin match query_syntax info.info_syn ts.ts_name with
| Some _ -> List.iter (iter_complex_type info fmt) l
| None when Mty.mem ty !(info.complex_type) -> ()
| None ->
let ts = complex_type ty in
fprintf fmt "%a: TYPE;@\n@\n" print_ident ts.ts_name;
info.complex_type := Mty.add ty (ty_app ts []) !(info.complex_type)
begin match query_syntax info.info_syn ts.ts_name, l with
| Some s, _ -> syntax_arguments s (print_type info) fmt []
| None, [] -> fprintf fmt "%a" print_ident ts.ts_name
| None, _ ->
begin match Mty.find_opt ty !(info.complex_type) with
| Some ty -> print_type info fmt ty
| None ->
let ts = complex_type ty in let cty = ty_app ts [] in
let us = sprintf "%a: TYPE;@\n@\n" print_ident ts.ts_name in
info.complex_type := Mty.add ty cty !(info.complex_type);
info.urg_output := us :: !(info.urg_output);
print_type info fmt cty
end
end
let iter_complex_type info fmt ty =
try iter_complex_type info fmt ty
let print_type info fmt ty = try print_type info fmt ty
with Unsupported s -> raise (UnsupportedType (ty,s))
let find_complex_type info fmt f =
t_ty_fold (fun () ty -> iter_complex_type info fmt ty) () f
let print_type_value info fmt = function
| None -> fprintf fmt "BOOLEAN"
| Some ty -> print_type info fmt ty
......@@ -219,8 +212,6 @@ let print_lsargs info fmt = function
| l -> fprintf fmt "(%a) -> " (print_list comma (print_type info)) l
let print_param_decl info fmt ls =
List.iter (iter_complex_type info fmt) ls.ls_args;
Opt.iter (iter_complex_type info fmt) ls.ls_value;
fprintf fmt "@[<hov 2>%a: %a%a;@]@\n@\n"
print_ident ls.ls_name
(print_lsargs info) ls.ls_args
......@@ -231,10 +222,7 @@ let print_param_decl info fmt ls =
then print_param_decl info fmt ls
let print_logic_decl info fmt (ls,def) =
List.iter (iter_complex_type info fmt) ls.ls_args;
Opt.iter (iter_complex_type info fmt) ls.ls_value;
let vsl,expr = Decl.open_ls_defn def in
find_complex_type info fmt expr;
fprintf fmt "@[<hov 2>%a: %a%a = LAMBDA (%a): %a;@]@\n@\n"
print_ident ls.ls_name
(print_lsargs info) ls.ls_args
......@@ -260,11 +248,9 @@ let print_decl info fmt d = match d.d_node with
"cvc3 : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> ()
| Dprop (Paxiom, pr, f) ->
find_complex_type info fmt f;
fprintf fmt "@[<hov 2>%% %s@\nASSERT@ %a;@]@\n@\n"
pr.pr_name.id_string (print_fmla info) f
| Dprop (Pgoal, pr, f) ->
find_complex_type info fmt f;
fprintf fmt "@[QUERY@\n";
fprintf fmt "@[%% %a@]@\n" print_ident pr.pr_name;
(match pr.pr_name.id_loc with
......@@ -275,8 +261,8 @@ let print_decl info fmt d = match d.d_node with
let print_decls =
let print_decl (sm,ct) fmt d =
let info = {info_syn = sm; complex_type = ref ct} in
try print_decl info fmt d; (sm, !(info.complex_type))
let info = {info_syn = sm; complex_type = ref ct; urg_output = ref []} in
try print_decl info fmt d; (sm, !(info.complex_type)), !(info.urg_output)
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
......
......@@ -145,7 +145,7 @@ let print_decl info fmt d = match d.d_node with
let print_decls =
let print_decl sm fmt d =
try print_decl {info_syn = sm} fmt d; sm
try print_decl {info_syn = sm} fmt d; sm, []
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
......
......@@ -43,41 +43,35 @@ let print_var fmt {vs_name = id} =
type info = {
info_syn : syntax_map;
complex_type : ty Mty.t ref;
urg_output : string list ref;
}
let rec print_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "smtv1 : you must encode the polymorphism"
| Tyapp (ts, l) ->
begin match query_syntax info.info_syn ts.ts_name, l with
| Some s, _ -> syntax_arguments s (print_type info) fmt []
| None, [] -> fprintf fmt "%a" print_ident ts.ts_name
| None, _ -> print_type info fmt (Mty.find ty !(info.complex_type))
end
let complex_type = Wty.memoize 3 (fun ty ->
let s = Pp.string_of_wnl Pretty.print_ty ty in
create_tysymbol (id_fresh s) [] None)
let rec iter_complex_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "smtv1 : you must encode the polymorphism"
| Tyapp (_, []) -> ()
let rec print_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "smtv1: you must encode the polymorphism"
| Tyapp (ts, l) ->
begin match query_syntax info.info_syn ts.ts_name with
| Some _ -> List.iter (iter_complex_type info fmt) l
| None when Mty.mem ty !(info.complex_type) -> ()
| None ->
let ts = complex_type ty in
fprintf fmt ":extrasorts (%a)@\n@\n" print_ident ts.ts_name;
info.complex_type := Mty.add ty (ty_app ts []) !(info.complex_type)
begin match query_syntax info.info_syn ts.ts_name, l with
| Some s, _ -> syntax_arguments s (print_type info) fmt []
| None, [] -> fprintf fmt "%a" print_ident ts.ts_name
| None, _ ->
begin match Mty.find_opt ty !(info.complex_type) with
| Some ty -> print_type info fmt ty
| None ->
let ts = complex_type ty in let cty = ty_app ts [] in
let us = sprintf
":extrasorts (%a)@\n@\n" print_ident ts.ts_name in
info.complex_type := Mty.add ty cty !(info.complex_type);
info.urg_output := us :: !(info.urg_output);
print_type info fmt cty
end
end
let iter_complex_type info fmt ty =
try iter_complex_type info fmt ty
let print_type info fmt ty = try print_type info fmt ty
with Unsupported s -> raise (UnsupportedType (ty,s))
let find_complex_type info fmt f =
t_ty_fold (fun () ty -> iter_complex_type info fmt ty) () f
let rec print_term info fmt t = match t.t_node with
| Tconst c ->
let number_format = {
......@@ -194,11 +188,8 @@ let print_param_decl info fmt ls = match ls.ls_value with
(print_type info) value
let print_param_decl info fmt ls =
if not (Mid.mem ls.ls_name info.info_syn) then begin
List.iter (iter_complex_type info fmt) ls.ls_args;
Opt.iter (iter_complex_type info fmt) ls.ls_value;
print_param_decl info fmt ls
end
if not (Mid.mem ls.ls_name info.info_syn) then
print_param_decl info fmt ls
let print_decl info fmt d = match d.d_node with
| Dtype ts ->
......@@ -213,11 +204,9 @@ let print_decl info fmt d = match d.d_node with
"smtv1 : inductive definitions are not supported"
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> ()
| Dprop (Paxiom, pr, f) ->
find_complex_type info fmt f;
fprintf fmt "@[<hov 2>;; %s@\n:assumption@ %a@]@\n@\n"
pr.pr_name.id_string (print_fmla info) f
| Dprop (Pgoal, pr, f) ->
find_complex_type info fmt f;
fprintf fmt "@[:formula@\n";
fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
(match pr.pr_name.id_loc with
......@@ -228,8 +217,8 @@ let print_decl info fmt d = match d.d_node with
let print_decls =
let print_decl (sm,ct) fmt d =
let info = {info_syn = sm; complex_type = ref ct} in
try print_decl info fmt d; (sm, !(info.complex_type))
let info = {info_syn = sm; complex_type = ref ct; urg_output = ref []} in
try print_decl info fmt d; (sm, !(info.complex_type)), !(info.urg_output)
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
......
......@@ -270,7 +270,7 @@ let print_decl info fmt d = match d.d_node with
let print_decls =
let print_decl sm fmt d =
try print_decl {info_syn = sm} fmt d; sm
try print_decl {info_syn = sm} fmt d; sm, []
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
......
......@@ -379,8 +379,7 @@ let print_tdecl fmt td = match td.td_node with
let print_tdecls =
let print_tdecl sm fmt td =
info := {info_syn = sm};
print_tdecl fmt td; sm in
info := {info_syn = sm}; print_tdecl fmt td; sm, [] in
let print_tdecl = Printer.sprint_tdecl print_tdecl in
let print_tdecl task acc = print_tdecl task.Task.task_decl acc in
Discriminate.on_syntax_map (fun sm -> Trans.fold print_tdecl (sm,[]))
......
......@@ -55,42 +55,36 @@ let print_ident fmt id =
type info = {
info_syn : syntax_map;
complex_type : ty Mty.t ref;
urg_output : string list ref;
}
(** type *)
let rec print_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "yices: you must encode the polymorphism"
| Tyapp (ts, l) ->
begin match query_syntax info.info_syn ts.ts_name, l with
| Some s, _ -> syntax_arguments s (print_type info) fmt l
| None, [] -> fprintf fmt "%a" print_ident ts.ts_name
| None, _ -> print_type info fmt (Mty.find ty !(info.complex_type))
end
let complex_type = Wty.memoize 3 (fun ty ->
let s = Pp.string_of_wnl Pretty.print_ty ty in
create_tysymbol (id_fresh s) [] None)
let rec iter_complex_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "yices: you must encode the polymorphism"
| Tyapp (_, []) -> ()
let rec print_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "cvc3: you must encode the polymorphism"
| Tyapp (ts, l) ->
begin match query_syntax info.info_syn ts.ts_name with
| Some _ -> List.iter (iter_complex_type info fmt) l
| None when Mty.mem ty !(info.complex_type) -> ()
| None ->
let ts = complex_type ty in
fprintf fmt "(define-type %a)@\n@\n" print_ident ts.ts_name;
info.complex_type := Mty.add ty (ty_app ts []) !(info.complex_type)
begin match query_syntax info.info_syn ts.ts_name, l with
| Some s, _ -> syntax_arguments s (print_type info) fmt []
| None, [] -> fprintf fmt "%a" print_ident ts.ts_name
| None, _ ->
begin match Mty.find_opt ty !(info.complex_type) with
| Some ty -> print_type info fmt ty
| None ->
let ts = complex_type ty in let cty = ty_app ts [] in
let us = sprintf
"(define-type %a)@\n@\n" print_ident ts.ts_name in
info.complex_type := Mty.add ty cty !(info.complex_type);
info.urg_output := us :: !(info.urg_output);
print_type info fmt cty
end
end
let iter_complex_type info fmt ty =
try iter_complex_type info fmt ty
let print_type info fmt ty = try print_type info fmt ty
with Unsupported s -> raise (UnsupportedType (ty,s))
let find_complex_type info fmt f =
t_ty_fold (fun () ty -> iter_complex_type info fmt ty) () f
let print_type_value info fmt = function
| None -> fprintf fmt "bool"
| Some ty -> print_type info fmt ty
......@@ -235,8 +229,6 @@ let print_data_decl info fmt (ts, _ as d) =
print_data_decl info fmt d
let print_param_decl info fmt ls =
List.iter (iter_complex_type info fmt) ls.ls_args;
Opt.iter (iter_complex_type info fmt) ls.ls_value;
match ls.ls_args with
| [] ->
fprintf fmt "@[<hov 2>(define %a::%a)@]@\n@\n"
......@@ -265,11 +257,9 @@ let print_decl info fmt d = match d.d_node with
"yices: inductive definitions are not supported"
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> ()
| Dprop (Paxiom, pr, f) ->
find_complex_type info fmt f;
fprintf fmt "@[<hov 2>;; %s@\n(assert@ %a);@]@\n@\n"
pr.pr_name.id_string (print_fmla info) f
| Dprop (Pgoal, pr, f) ->
find_complex_type info fmt f;
fprintf fmt "@[(assert@\n";
fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
(match pr.pr_name.id_loc with
......@@ -280,8 +270,8 @@ let print_decl info fmt d = match d.d_node with
let print_decls =
let print_decl (sm,ct) fmt d =
let info = {info_syn = sm; complex_type = ref ct} in
try print_decl info fmt d; (sm, !(info.complex_type))
let info = {info_syn = sm; complex_type = ref ct; urg_output = ref []} in
try print_decl info fmt d; (sm, !(info.complex_type)), !(info.urg_output)
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc 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