first usable version of tptp printer

drivers/tptp.drv

@@ -21,6 +21,8 @@ transformation "eliminate_algebraic"
 transformation "eliminate_if"
 transformation "eliminate_let"
 
+(* TODO : transformation to eliminate types *)
+
 
 theory BuiltIn
   syntax type int "Int"
@@ -36,3 +38,5 @@ mode: why
 compile-command: "unset LANG; make -C .. bench"
 End:
 *)
+(* vim:syntax=ocaml
+*)

src/printer/tptp.ml

@@ -26,13 +26,15 @@ open Decl
 open Task
 
 let ident_printer =
-  let bls = ["and";" benchmark";" distinct";"exists";"false";"flet";"forall";
+  (* let bls = ["and";" benchmark";" distinct";"exists";"false";"flet";"forall";
      "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";
-     "Array";"U";"select";"store"] in
+     "Array";"U";"select";"store"] in *)
+  let bls = ["fof"; "axiom"; "conjecture"; "&"; "="; "!="; "!"; "|"; "=>"; 
+      "~"; "?"; "itef"] in
   let san = sanitizer char_to_alpha char_to_alnumus in
   create_ident_printer bls ~sanitizer:san
 
@@ -42,7 +44,7 @@ let print_ident fmt id =
 let forget_var v = forget_id ident_printer v.vs_name
 
 let print_var fmt {vs_name = id} =
-  let sanitize n = "?" ^ n in
+  let sanitize n = String.capitalize n in
   let n = id_unique ident_printer ~sanitizer:sanitize id in
   fprintf fmt "%s" n
 
@@ -54,6 +56,7 @@ let rec print_type drv fmt ty = match ty.ty_node with
       | None -> fprintf fmt "%a%a" (print_tyapp drv) tl print_ident ts.ts_name
     end
 
+(* TODO : remove *)
 and print_tyapp drv fmt = function
   | [] -> ()
   | [ty] -> fprintf fmt "%a " (print_type drv) ty
@@ -63,17 +66,15 @@ let print_type drv fmt = catch_unsupportedType (print_type drv fmt)
 
 let rec print_term drv fmt t = match t.t_node with
   | Tbvar _ -> assert false
-  | Tconst c ->
-      Pretty.print_const fmt c
+  | Tconst c -> fprintf fmt "'%a'"
+      Pretty.print_const c
   | Tvar v -> print_var fmt v
   | Tapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
       | Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
-      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
-          | [] -> fprintf fmt "@[%a@]" print_ident ls.ls_name
-          | _ -> fprintf fmt "@[(%a %a)@]"
-	      print_ident ls.ls_name (print_list space (print_term drv)) tl
-        end end
-  | Tlet (t1, tb) -> unsupportedTerm t
+      | None ->fprintf fmt "@[%a(%a)@]"
+	      print_ident ls.ls_name (print_list comma (print_term drv)) tl
+      end
+  | Tlet (_,_) -> unsupportedTerm t
       "tptp : you must eliminate let"
   | Tif (f1,t1,t2) ->
       fprintf fmt "@[itef(%a@, %a@, %a)@]"
@@ -88,46 +89,43 @@ and print_fmla drv fmt f = match f.f_node with
       print_ident fmt id
   | Fapp (ls, tl) -> begin match Driver.query_syntax drv ls.ls_name with
       | Some s -> Driver.syntax_arguments s (print_term drv) fmt tl
-      | None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
-          | [] -> fprintf fmt "%a" print_ident ls.ls_name
-          | _ -> fprintf fmt "(%a %a)"
-	      print_ident ls.ls_name (print_list space (print_term drv)) tl
-        end end
+      | None -> fprintf fmt "%a(%a)"
+	      print_ident ls.ls_name (print_list comma (print_term drv)) tl
+      end
   | Fquant (q, fq) ->
-      let q = match q with Fforall -> "forall" | Fexists -> "exists" in
+      let q = match q with Fforall -> "!" | Fexists -> "?" in
       let vl, _tl, f = f_open_quant fq in
       (* TODO trigger *)
       let rec forall fmt = function
         | [] -> print_fmla drv fmt f
         | v::l ->
-	    fprintf fmt "@[(%s (%a %a)@ %a)@]" q print_var v
-              (print_type drv) v.vs_ty forall l
+	    fprintf fmt "@[(%s [%a]@ : (%a))@]" q print_var v forall l
       in
       forall fmt vl;
       List.iter forget_var vl
   | Fbinop (Fand, f1, f2) ->
-      fprintf fmt "@[(and@ %a %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
+      fprintf fmt "@[(%a &@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
   | Fbinop (For, f1, f2) ->
-      fprintf fmt "@[(or@ %a %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
+      fprintf fmt "@[(%a |@ %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
   | Fbinop (Fimplies, f1, f2) ->
-      fprintf fmt "@[(implies@ %a %a)@]"
+      fprintf fmt "@[(%a =>@ %a)@]"
         (print_fmla drv) f1 (print_fmla drv) f2
   | Fbinop (Fiff, f1, f2) ->
-      fprintf fmt "@[(iff@ %a %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
+      fprintf fmt "@[(%a <=> %a)@]" (print_fmla drv) f1 (print_fmla drv) f2
   | Fnot f ->
-      fprintf fmt "@[(not@ %a)@]" (print_fmla drv) f
+      fprintf fmt "@[(~@ %a)@]" (print_fmla drv) f
   | Ftrue ->
       fprintf fmt "true"
   | Ffalse ->
       fprintf fmt "false"
-  | Fif (f1, f2, f3) ->
-      fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
-	(print_fmla drv) f1 (print_fmla drv) f2 (print_fmla drv) f3
-  | Flet (t1, tb) ->
-      let v, f2 = f_open_bound tb in
+  | Fif (_,_,_) -> unsupportedFmla f "Fif not supported"
+      (* fprintf fmt "@[(if_then_else %a@ %a@ %a)@]"
+	(print_fmla drv) f1 (print_fmla drv) f2 (print_fmla drv) f3 *)
+  | Flet (_, _) -> unsupportedFmla f "Flet not supported"
+      (* let v, f2 = f_open_bound tb in
       fprintf fmt "@[(let (%a %a)@ %a)@]" print_var v
         (print_term drv) t1 (print_fmla drv) f2;
-      forget_var v
+      forget_var v *)
   | Fcase _ -> unsupportedFmla f
       "tptp : you must eliminate match"
 
@@ -147,18 +145,7 @@ let print_type_decl drv fmt = function
   | _, Talgebraic _ -> unsupported "tptp : algebraic type are not supported"
 
 let print_logic_decl drv fmt (ls,ld) = match ld with
-  | None ->
-      begin match ls.ls_value with
-        | None ->
-            fprintf fmt "@[<hov 2>:extrapreds ((%a %a))@]@\n"
-              print_ident ls.ls_name
-              (print_list space (print_type drv)) ls.ls_args
-        | Some value ->
-            fprintf fmt "@[<hov 2>:extrafuns ((%a %a %a))@]@\n"
-              print_ident ls.ls_name
-              (print_list space (print_type drv)) ls.ls_args
-              (print_type drv) value
-      end
+  | None -> ()
   | Some _ -> unsupported "Predicate and function definition aren't supported"
 
 let print_logic_decl drv fmt d =
@@ -174,28 +161,20 @@ let print_decl drv fmt d = match d.d_node with
       "tptp : inductive definition are not supported"
   | Dprop (Paxiom, pr, _) when Driver.query_remove drv pr.pr_name -> false
   | Dprop (Paxiom, _pr, f) ->
-      fprintf fmt "@[<hov 2>:assumption@ %a@]@\n"
-        (print_fmla drv) f; true
-  | Dprop (Pgoal, pr, f) ->
-      fprintf fmt "@[:formula@\n";
-      fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
-      (match id_from_user pr.pr_name with
-        | None -> ()
-        | Some loc -> fprintf fmt " @[;; %a@]@\n"
-            Loc.gen_report_position loc);
-      fprintf fmt "  @[(not@ %a)@]" (print_fmla drv) f;true
+      fprintf fmt "fof(%s, axiom,@ %a).\n"
+         (string_unique ident_printer "axiom") (print_fmla drv) f; true
+  | Dprop (Pgoal, pr, f) -> (* TODO : what is pr ? *)
+      fprintf fmt "fof(%s, conjecture,@ %a ).\n"
+        (string_unique ident_printer "goal") (print_fmla drv) f; true
+      (* fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name; *)
   | Dprop (Plemma, _, _) -> assert false
 
 let print_decl drv fmt = catch_unsupportedDecl (print_decl drv fmt)
 
 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_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)@."
+  ignore (print_list_opt (add_flush newline2) (print_decl drv) fmt decls)
 
 let () = register_printer "tptp"
   (fun drv fmt task ->

src/printer/tptp.mli

@@ -17,3 +17,4 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** a printer targeting first-order logic tptp syntax *)