Commit 08c5987e authored by Andrei Paskevich's avatar Andrei Paskevich

merge TPTP printer into the tptp plugin

parent 97518e86
......@@ -260,11 +260,11 @@ PLUGGENERATED = plugins/tptp/tptp_lexer.ml \
plugins/tptp/tptp_parser.ml plugins/tptp/tptp_parser.mli
PLUG_PARSER = genequlin
PLUG_PRINTER = tptp_fof tptp_tff
PLUG_PRINTER =
PLUG_TRANSFORM =
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer
PLUG_TPTP = tptp_ast tptp_parser tptp_typing tptp_lexer tptp_printer
PLUGINS = genequlin tptp_fof tptp_tff tptp
PLUGINS = genequlin tptp
TPTPMODULES = $(addprefix plugins/tptp/, $(PLUG_TPTP))
......
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2012 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Format
open Why3
open Pp
open Ident
open Ty
open Term
open Decl
open Task
open Printer
let ident_printer =
let bls = ["fof"; "axiom"; "conjecture"; "itef"] in
let san = sanitizer char_to_alpha char_to_alnumus in
create_ident_printer bls ~sanitizer:san
let print_symbol fmt id =
let san = String.uncapitalize in
fprintf fmt "%s" (id_unique ~sanitizer:san ident_printer id)
let print_var fmt {vs_name = id} =
let san = String.capitalize in
fprintf fmt "%s" (id_unique ~sanitizer:san ident_printer id)
let forget_var v = forget_id ident_printer v.vs_name
type info = {
info_syn : syntax_map;
}
let rec print_term info fmt t = match t.t_node with
| Tvar v -> print_var fmt v
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments s (print_term info) fmt tl
| None -> begin match tl with (* toto() is not accepted *)
| [] -> fprintf fmt "@[%a@]" print_symbol ls.ls_name
| _ -> fprintf fmt "@[%a(%a)@]" print_symbol ls.ls_name
(print_list comma (print_term info)) tl
end
end
| Tconst _ -> unsupportedTerm t
"tptp : you must eliminate constants"
| Tlet (_,_) -> unsupportedTerm t
"tptp : you must eliminate let"
| Tif (f1,t1,t2) ->
fprintf fmt "@[itef(%a,@ %a,@ %a)@]"
(print_fmla info) f1 (print_term info) t1 (print_term info) t2
| Tcase _ -> unsupportedTerm t
"tptp : you must eliminate match"
| Teps _ -> unsupportedTerm t
"tptp : you must eliminate epsilon"
| Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
and print_fmla info fmt f = match f.t_node with
| Tapp ({ ls_name = id }, []) ->
print_symbol fmt id
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments s (print_term info) fmt tl
| None -> fprintf fmt "@[%a(%a)@]"
print_symbol ls.ls_name (print_list comma (print_term info)) tl
end
| Tquant (q, fq) ->
let q = match q with Tforall -> "!" | Texists -> "?" in
let vl, _tl, f = t_open_quant fq in
fprintf fmt "%s [%a] :@ %a" q (print_list comma print_var) vl (print_fmla info) f;
List.iter forget_var vl
| Tbinop (Tand, f1, f2) ->
fprintf fmt "@[(%a@ & %a)@]" (print_fmla info) f1 (print_fmla info) f2
| Tbinop (Tor, f1, f2) ->
fprintf fmt "@[(%a@ | %a)@]" (print_fmla info) f1 (print_fmla info) f2
| Tbinop (Timplies, f1, f2) ->
fprintf fmt "@[(%a@ => %a)@]"
(print_fmla info) f1 (print_fmla info) f2
| Tbinop (Tiff, f1, f2) ->
fprintf fmt "@[(%a@ <=> %a)@]" (print_fmla info) f1 (print_fmla info) f2
| Tnot f ->
fprintf fmt "@[~@ (%a)@]" (print_fmla info) f
| Ttrue ->
fprintf fmt "$true"
| Tfalse ->
fprintf fmt "$false"
| Tif (_,_,_) -> unsupportedTerm f "Tif not supported"
(* fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
(print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3 *)
| Tlet (_, _) -> unsupportedTerm f "Tlet not supported"
(* let v, f2 = t_open_bound tb in
fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
(print_term info) t1 (print_fmla info) f2;
forget_var v *)
| Tcase _ -> unsupportedTerm f
"tptp : you must eliminate match"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
let print_decl info fmt d = match d.d_node with
| Dtype _ | Dparam _ -> false
(* print_list_opt newline (print_type_decl info) fmt dl *)
| Ddata _ -> unsupportedDecl d
"Algebraic datatypes are not supported"
| Dlogic _ -> unsupportedDecl d
"Predicate and function definition aren't supported"
| Dind _ -> unsupportedDecl d
"tptp : inductive definition are not supported"
| Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> false
| Dprop (Paxiom, pr, f) ->
fprintf fmt "@[<hov 2>fof(%s, axiom,@ %a).@]@\n"
(id_unique ~sanitizer:String.uncapitalize ident_printer pr.pr_name)
(print_fmla info) f; true
| Dprop (Pgoal, pr, f) -> (* TODO : what is pr ? *)
fprintf fmt "@[<hov 2>fof(%s, conjecture,@ %a ).@]@\n"
(id_unique ~sanitizer:String.uncapitalize ident_printer pr.pr_name)
(print_fmla info) f; true
(* fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name; *)
| Dprop ((Plemma|Pskip), _, _) -> assert false
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
let print_task pr thpr fmt task =
print_prelude fmt pr;
print_th_prelude task fmt thpr;
let info = {
info_syn = get_syntax_map task }
in
ignore (print_list_opt (add_flush newline2)
(print_decl info) fmt (Task.task_decls task))
let () = register_printer "tptp-fof"
(fun _env pr thpr ?old:_ fmt task ->
forget_all ident_printer;
print_task pr thpr fmt task)
(**************************************************************************)
(* *)
(* Copyright (C) 2010-2012 *)
(* François Bobot *)
(* Jean-Christophe Filliâtre *)
(* Claude Marché *)
(* Guillaume Melquiond *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(** a printer targeting simply typed first-order logic tptp syntax *)
......@@ -57,6 +57,7 @@ let forget_tvar v = forget_id ident_printer v.tv_name
type info = {
info_syn : syntax_map;
info_fof : bool;
}
let rec print_type info fmt ty = match ty.ty_node with
......@@ -93,16 +94,16 @@ and print_term info fmt t = match t.t_node with
print_app info fmt ls tl t.t_ty
| Tconst c ->
let number_format = {
Print_number.long_int_support = true;
Print_number.dec_int_support = Print_number.Number_default;
Print_number.hex_int_support = Print_number.Number_unsupported;
Print_number.oct_int_support = Print_number.Number_unsupported;
Print_number.bin_int_support = Print_number.Number_unsupported;
Print_number.def_int_support = Print_number.Number_unsupported;
Print_number.dec_real_support = Print_number.Number_default;
Print_number.hex_real_support = Print_number.Number_unsupported;
Print_number.frac_real_support = Print_number.Number_unsupported;
Print_number.def_real_support = Print_number.Number_unsupported;
Print_number.long_int_support = true;
Print_number.dec_int_support = Print_number.Number_default;
Print_number.hex_int_support = Print_number.Number_unsupported;
Print_number.oct_int_support = Print_number.Number_unsupported;
Print_number.bin_int_support = Print_number.Number_unsupported;
Print_number.def_int_support = Print_number.Number_unsupported;
Print_number.dec_real_support = Print_number.Number_default;
Print_number.hex_real_support = Print_number.Number_unsupported;
Print_number.frac_real_support = Print_number.Number_unsupported;
Print_number.def_real_support = Print_number.Number_unsupported;
} in
Print_number.print number_format fmt c
| Tlet (t1,tb) ->
......@@ -122,15 +123,10 @@ and print_term info fmt t = match t.t_node with
and print_fmla info fmt f = match f.t_node with
| Tapp (ls, tl) ->
print_app info fmt ls tl f.t_ty
| Tbinop (Tand, f1, f2) ->
fprintf fmt "(%a@ & %a)" (print_fmla info) f1 (print_fmla info) f2
| Tbinop (Tor, f1, f2) ->
fprintf fmt "(%a@ | %a)" (print_fmla info) f1 (print_fmla info) f2
| Tbinop (Timplies, f1, f2) ->
fprintf fmt "(%a@ => %a)"
(print_fmla info) f1 (print_fmla info) f2
| Tbinop (Tiff, f1, f2) ->
fprintf fmt "(%a@ <=> %a)" (print_fmla info) f1 (print_fmla info) f2
| Tbinop (op, f1, f2) ->
let s = match op with
| Tand -> "&" | Tor -> "|" | Timplies -> "=>" | Tiff -> "<=>" in
fprintf fmt "(%a@ %s %a)" (print_fmla info) f1 s (print_fmla info) f2
| Tnot f ->
fprintf fmt "~@ (%a)" (print_fmla info) f
| Ttrue ->
......@@ -141,8 +137,8 @@ and print_fmla info fmt f = match f.t_node with
let q = match q with Tforall -> "!" | Texists -> "?" in
let vl, _tl, f = t_open_quant fq in
let print_vsty fmt vs =
fprintf fmt "%a:@,%a" print_var vs (print_type info) vs.vs_ty
in
if info.info_fof then fprintf fmt "%a" print_var vs
else fprintf fmt "%a:@,%a" print_var vs (print_type info) vs.vs_ty in
fprintf fmt "%s[%a]:@ %a" q
(print_list comma print_vsty) vl (print_fmla info) f;
List.iter forget_var vl
......@@ -170,6 +166,7 @@ let print_fmla info fmt f =
Stv.iter forget_tvar tvs
let print_decl info fmt d = match d.d_node with
| Dtype _ when info.info_fof -> ()
| Dtype { ts_def = Some _ } -> ()
| Dtype ts when query_syntax info.info_syn ts.ts_name <> None -> ()
| Dtype ts ->
......@@ -182,6 +179,7 @@ let print_decl info fmt d = match d.d_node with
fprintf fmt "@[<hov 2>tff(%s, type,@ %a:@ %a).@]@\n@\n"
(id_unique pr_printer ts.ts_name)
print_symbol ts.ts_name print_sig ts
| Dparam _ when info.info_fof -> ()
| Dparam ls when query_syntax info.info_syn ls.ls_name <> None -> ()
| Dparam ls ->
let print_type = print_type info in
......@@ -216,22 +214,25 @@ 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) ->
fprintf fmt "@[<hov 2>tff(%a, axiom,@ %a).@]@\n@\n"
print_pr pr (print_fmla info) f
let head = if info.info_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) ->
fprintf fmt "@[<hov 2>tff(%a, conjecture,@ %a).@]@\n"
print_pr pr (print_fmla info) f
let head = if info.info_fof then "fof" else "tff" in
fprintf fmt "@[<hov 2>%s(%a, conjecture,@ %a).@]@\n"
head print_pr pr (print_fmla info) f
| Dprop ((Plemma|Pskip), _, _) -> assert false
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
let print_task _env pr thpr ?old:_ fmt task =
let print_task fof _env pr thpr ?old:_ fmt task =
forget_all ident_printer;
forget_all pr_printer;
print_prelude fmt pr;
print_th_prelude task fmt thpr;
let info = { info_syn = get_syntax_map task } in
let info = { info_syn = get_syntax_map task; info_fof = fof } in
fprintf fmt "@[%a@]@."
(print_list nothing (print_decl info)) (Task.task_decls task)
let () = register_printer "tptp-tff" print_task
let () = register_printer "tptp-tff" (print_task false)
let () = register_printer "tptp-fof" (print_task true)
......@@ -18,4 +18,3 @@
(* *)
(**************************************************************************)
(** a printer targeting first-order logic tptp syntax *)
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