tptp.ml 6.83 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    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.                  *)
(*                                                                        *)
(**************************************************************************)
Jean-Christophe Filliâtre's avatar
headers  
Jean-Christophe Filliâtre committed
19

20 21 22 23 24 25 26
open Format
open Pp
open Ident
open Ty
open Term
open Decl
open Task
27
open Printer
28 29

let ident_printer =
30
  (* let bls = ["and";" benchmark";" distinct";"exists";"false";"flet";"forall";
31 32 33 34 35
     "if then else";"iff";"implies";"ite";"let";"logic";"not";"or";
     "sat";"theory";"true";"unknown";"unsat";"xor";
     "assumption";"axioms";"defintion";"extensions";"formula";
     "funs";"extrafuns";"extrasorts";"extrapreds";"language";
     "notes";"preds";"sorts";"status";"theory";"Int";"Real";"Bool";
36 37 38
     "Array";"U";"select";"store"] in *)
  let bls = ["fof"; "axiom"; "conjecture"; "&"; "="; "!="; "!"; "|"; "=>"; 
      "~"; "?"; "itef"] in
39 40 41
  let san = sanitizer char_to_alpha char_to_alnumus in
  create_ident_printer bls ~sanitizer:san

42 43 44
let print_symbol fmt id =
  let san = String.uncapitalize in
  fprintf fmt "%s" (id_unique ~sanitizer:san ident_printer id)
45 46

let print_var fmt {vs_name = id} =
47 48
  let san = String.capitalize in
  fprintf fmt "%s" (id_unique ~sanitizer:san ident_printer id)
49

50
let forget_var v = forget_id ident_printer v.vs_name
51

52
type info = {
Andrei Paskevich's avatar
Andrei Paskevich committed
53
  info_syn : string Mid.t;
54 55 56 57
  info_rem : Sid.t;
}

let rec print_term info fmt t = match t.t_node with
58
  | Tbvar _ -> assert false
59 60
  | Tconst c -> fprintf fmt "'%a'"
      Pretty.print_const c
61
  | Tvar v -> print_var fmt v
62
  | Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
63
      | Some s -> syntax_arguments s (print_term info) fmt tl
64
      | None -> begin match tl with (* toto() is not accepted *)
65 66
          | [] -> fprintf fmt "@[%a@]" print_symbol ls.ls_name
          | _ -> fprintf fmt "@[%a(%a)@]"  print_symbol ls.ls_name
67
                (print_list comma (print_term info)) tl
68
          end
69 70
      end
  | Tlet (_,_) -> unsupportedTerm t
71
      "tptp : you must eliminate let"
72
  | Tif (f1,t1,t2) ->
73
      fprintf fmt "@[itef(%a,@ %a,@ %a)@]"
74
        (print_fmla info) f1 (print_term info) t1 (print_term info) t2
75 76 77 78 79
  | Tcase _ -> unsupportedTerm t
      "tptp : you must eliminate match"
  | Teps _ -> unsupportedTerm t
      "tptp : you must eliminate epsilon"

80
and print_fmla info fmt f = match f.f_node with
81
  | Fapp ({ ls_name = id }, []) ->
82
      print_symbol fmt id
83
  | Fapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
84
      | Some s -> syntax_arguments s (print_term info) fmt tl
85
      | None -> fprintf fmt "@[%a(%a)@]"
86
	      print_symbol ls.ls_name (print_list comma (print_term info)) tl
87
      end
88
  | Fquant (q, fq) ->
89
      let q = match q with Fforall -> "!" | Fexists -> "?" in
90 91
      let vl, _tl, f = f_open_quant fq in
      (* TODO trigger *)
92
      fprintf fmt "%s [%a] :@ %a" q (print_list comma print_var) vl (print_fmla info) f;
93 94
      List.iter forget_var vl
  | Fbinop (Fand, f1, f2) ->
95
      fprintf fmt "@[(%a@ & %a)@]" (print_fmla info) f1 (print_fmla info) f2
96
  | Fbinop (For, f1, f2) ->
97
      fprintf fmt "@[(%a@ | %a)@]" (print_fmla info) f1 (print_fmla info) f2
98
  | Fbinop (Fimplies, f1, f2) ->
99
      fprintf fmt "@[(%a@ => %a)@]"
100
        (print_fmla info) f1 (print_fmla info) f2
101
  | Fbinop (Fiff, f1, f2) ->
102
      fprintf fmt "@[(%a@ <=> %a)@]" (print_fmla info) f1 (print_fmla info) f2
103
  | Fnot f ->
104
      fprintf fmt "@[~@ (%a)@]" (print_fmla info) f
105
  | Ftrue ->
106
      fprintf fmt "$true"
107
  | Ffalse ->
108
      fprintf fmt "$false"
109 110
  | Fif (_,_,_) -> unsupportedFmla f "Fif not supported"
      (* fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
111
	(print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3 *)
112 113
  | Flet (_, _) -> unsupportedFmla f "Flet not supported"
      (* let v, f2 = f_open_bound tb in
114
      fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
115
        (print_term info) t1 (print_fmla info) f2;
116
      forget_var v *)
117 118 119
  | Fcase _ -> unsupportedFmla f
      "tptp : you must eliminate match"

120
and print_expr info fmt = e_apply (print_term info fmt) (print_fmla info fmt)
121

122
and print_triggers info fmt tl = print_list comma (print_expr info) fmt tl
123 124


125
let print_logic_decl _ _ (_,ld) = match ld with
126
  | None -> ()
127 128
  | Some _ -> unsupported "Predicate and function definition aren't supported"

129 130 131
let print_logic_decl info fmt d =
  if Sid.mem (fst d).ls_name info.info_rem then
    false else (print_logic_decl info fmt d; true)
132

133
let print_decl info fmt d = match d.d_node with
134
  | Dtype _ -> false
135
      (* print_list_opt newline (print_type_decl info) fmt dl *)
136
  | Dlogic dl ->
137
      print_list_opt newline (print_logic_decl info) fmt dl
138 139
  | Dind _ -> unsupportedDecl d
      "tptp : inductive definition are not supported"
140
  | Dprop (Paxiom, pr, _) when Sid.mem pr.pr_name info.info_rem -> false
141
  | Dprop (Paxiom, pr, f) ->
142
      fprintf fmt "@[<hov 2>fof(%s, axiom,@ %a).@]@\n"
143
        (id_unique ~sanitizer:String.uncapitalize ident_printer pr.pr_name)
144
        (print_fmla info) f; true
145
  | Dprop (Pgoal, pr, f) -> (* TODO : what is pr ? *)
146
      fprintf fmt "@[<hov 2>fof(%s, conjecture,@ %a ).@]@\n"
147
        (id_unique ~sanitizer:String.uncapitalize ident_printer pr.pr_name)
148
        (print_fmla info) f; true
149
      (* fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name; *)
150
  | Dprop ((Plemma|Pskip), _, _) -> assert false
151

152
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
153

Andrei Paskevich's avatar
Andrei Paskevich committed
154
let print_task pr thpr fmt task =
155 156 157
  print_prelude fmt pr;
  print_th_prelude task fmt thpr;
  let info = {
Andrei Paskevich's avatar
Andrei Paskevich committed
158
    info_syn = get_syntax_map task;
159 160
    info_rem = get_remove_set task }
  in
161
  let decls = Task.task_decls task in
162
  ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
163

164
let () = register_printer "tptp" 
165 166
  (fun pr thpr ?old fmt task ->
     ignore old;
167
     forget_all ident_printer;
Andrei Paskevich's avatar
Andrei Paskevich committed
168
     print_task pr thpr fmt task)
169