plugins/tptp/tptp_printer.ml

   1 (********************************************************************)
   2 (*                                                                  *)
   3 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
   4 (*  Copyright 2010-2024 --  Inria - CNRS - Paris-Saclay University  *)
   5 (*                                                                  *)
   6 (*  This software is distributed under the terms of the GNU Lesser  *)
   7 (*  General Public License version 2.1, with the special exception  *)
   8 (*  on linking described in file LICENSE.                           *)
   9 (*                                                                  *)
  10 (********************************************************************)
  11
  12 open Format
  13
  14 open Why3
  15 open Pp
  16 open Ident
  17 open Ty
  18 open Term
  19 open Decl
  20 open Printer
  21
  22 let bls = ["true";"false"]
  23
  24 let ident_printer =
  25   let san = sanitizer char_to_alpha char_to_alnumus in
  26   create_ident_printer bls ~sanitizer:san
  27
  28 let pr_printer =
  29   let san = sanitizer char_to_lalpha char_to_alnumus in
  30   create_ident_printer bls ~sanitizer:san
  31
  32 let print_symbol fmt id =
  33   let san = Strings.uncapitalize in
  34   pp_print_string fmt (id_unique ~sanitizer:san ident_printer id)
  35
  36 let print_tvar fmt {tv_name = id} =
  37   let san = Strings.capitalize in
  38   pp_print_string fmt (id_unique ~sanitizer:san ident_printer id)
  39
  40 let print_var fmt {vs_name = id} =
  41   let san = Strings.capitalize in
  42   pp_print_string fmt (id_unique ~sanitizer:san ident_printer id)
  43
  44 let print_pr fmt pr =
  45   pp_print_string fmt (id_unique pr_printer pr.pr_name)
  46
  47 let forget_var v = forget_id ident_printer v.vs_name
  48 let forget_tvar v = forget_id ident_printer v.tv_name
  49
  50 type tptp_format = FOF | TFF0 | TFF1
  51
  52 type tptp_number = TPTP | MetiTarski
  53
  54 type info = {
  55   info_syn : syntax_map;
  56   info_fmt : tptp_format;
  57   info_num : tptp_number;
  58   info_srt : ty Mty.t ref;
  59   info_urg : string list ref;
  60   info_rules : Decl.Spr.t;
  61 }
  62
  63 let complex_type = Wty.memoize 3 (fun ty ->
  64   let s = Pp.string_of_wnl Pretty.print_ty ty in
  65   create_tysymbol (id_fresh s) [] NoDef)
  66
  67 let rec print_type info fmt ty = match ty.ty_node with
  68   | Tyvar _ when info.info_fmt = TFF0 ->
  69       unsupported "TFF0 does not support polymorphic types"
  70   | Tyvar tv -> print_tvar fmt tv
  71   | Tyapp (ts, tl) ->
  72       begin match query_syntax info.info_syn ts.ts_name, tl with
  73       | Some s, _ -> syntax_arguments s (print_type info) fmt tl
  74       | None, [] -> print_symbol fmt ts.ts_name
  75       | None, _ when info.info_fmt = TFF0 ->
  76           begin match Mty.find_opt ty !(info.info_srt) with
  77           | Some ty -> print_type info fmt ty
  78           | None ->
  79               let ts = complex_type ty in let cty = ty_app ts [] in
  80               let us = Pp.sprintf "@[<hov 2>tff(%s, type,@ %a:@ $tType).@]@\n@\n"
  81                 (id_unique pr_printer ts.ts_name) print_symbol ts.ts_name in
  82               info.info_srt := Mty.add ty cty !(info.info_srt);
  83               info.info_urg := us :: !(info.info_urg);
  84               print_type info fmt cty
  85           end
  86       | None, tl ->
  87           fprintf fmt "@[%a(%a)@]" print_symbol ts.ts_name
  88             (print_list comma (print_type info)) tl
  89       end
  90
  91 let print_type info fmt ty = try print_type info fmt ty
  92   with Unsupported s -> raise (UnsupportedType (ty,s))
  93
  94 let number_format = {
  95     Number.long_int_support = `Default;
  96     Number.negative_int_support =
  97       `Custom (fun fmt f -> fprintf fmt "-%t" f);
  98     Number.dec_int_support = `Default;
  99     Number.hex_int_support = `Unsupported;
 100     Number.oct_int_support = `Unsupported;
 101     Number.bin_int_support = `Unsupported;
 102     Number.negative_real_support = `Default;
 103     Number.dec_real_support = `Default;
 104     Number.hex_real_support = `Unsupported;
 105     Number.frac_real_support =
 106       `Custom
 107         ((fun fmt i -> fprintf fmt "$to_real(%s)" i),
 108          (fun fmt i n -> fprintf fmt "$quotient($to_real(%s),$to_real(%s))" i n));
 109 }
 110
 111 let number_format_metitarski = {
 112     number_format with
 113     Number.frac_real_support =
 114       `Custom
 115         ((fun fmt i -> pp_print_string fmt i),
 116          (fun fmt i n -> fprintf fmt "(%s / %s)" i n));
 117   }
 118
 119 let print_const info fmt c =
 120   let supported = match info.info_num with
 121     | TPTP -> number_format
 122     | MetiTarski -> number_format_metitarski in
 123   Constant.(print supported unsupported_escape) fmt c
 124
 125 let rec print_app info fmt ls tl oty =
 126   match query_syntax info.info_syn ls.ls_name with
 127   | Some s -> syntax_arguments s (print_term info) fmt tl
 128   | None ->
 129       let sbs = ls_app_inst ls tl oty in
 130       if Mtv.is_empty sbs && tl = [] then
 131         print_symbol fmt ls.ls_name
 132       else begin
 133         let cm = if Mtv.is_empty sbs || tl = [] then "" else ", " in
 134         fprintf fmt "%a(%a%s%a)"
 135           print_symbol ls.ls_name
 136           (print_iter2 Mtv.iter comma nothing nothing (print_type info)) sbs
 137           cm
 138           (print_list comma (print_term info)) tl
 139       end
 140
 141 and print_term info fmt t = match t.t_node with
 142   | Tvar v ->
 143       print_var fmt v
 144   | Tapp (ls, tl) ->
 145       print_app info fmt ls tl t.t_ty
 146   | Tconst c ->
 147       print_const info fmt c
 148   | Tlet (t1,tb) ->
 149       let v,t2 = t_open_bound tb in
 150       fprintf fmt "$let_tt(%a@ =@ %a,@ %a)"
 151         print_symbol v.vs_name (print_term info) t1 (print_term info) t2;
 152       forget_var v
 153   | Tif (f1,t1,t2) ->
 154       fprintf fmt "$ite_t(%a,@ %a,@ %a)"
 155         (print_fmla info) f1 (print_term info) t1 (print_term info) t2
 156   | Tcase _ -> unsupportedTerm t
 157       "TPTP does not support pattern matching, use eliminate_algebraic"
 158   | Teps _ -> unsupportedTerm t
 159       "TPTP does not support epsilon-terms"
 160   | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
 161
 162 and print_fmla info fmt f = match f.t_node with
 163   | Tapp (ls, tl) ->
 164       print_app info fmt ls tl f.t_ty
 165   | Tbinop (op, f1, f2) ->
 166       let s = match op with
 167         | Tand -> "&" | Tor -> "|" | Timplies -> "=>" | Tiff -> "<=>" in
 168       fprintf fmt "(%a@ %s %a)" (print_fmla info) f1 s (print_fmla info) f2
 169   | Tnot f ->
 170       fprintf fmt "~@ %a" (print_fmla info) f
 171   | Ttrue ->
 172       pp_print_string fmt "$true"
 173   | Tfalse ->
 174       pp_print_string fmt "$false"
 175   | Tquant (q, fq) ->
 176       let q = match q with Tforall -> "!" | Texists -> "?" in
 177       let vl, _tl, f = t_open_quant fq in
 178       let print_vsty fmt vs =
 179         if info.info_fmt = FOF then print_var fmt vs
 180         else fprintf fmt "%a:@,%a" print_var vs (print_type info) vs.vs_ty in
 181       fprintf fmt "%s[%a]:@ %a" q
 182         (print_list comma print_vsty) vl (print_fmla info) f;
 183       List.iter forget_var vl
 184   | Tlet (t1,tb) ->
 185       let v,t2 = t_open_bound tb in
 186       fprintf fmt "$let_tf(%a@ =@ %a,@ %a)"
 187         print_symbol v.vs_name (print_term info) t1 (print_fmla info) t2;
 188       forget_var v
 189   | Tif (f1,t1,t2) ->
 190       fprintf fmt "$ite_f(%a,@ %a,@ %a)"
 191         (print_fmla info) f1 (print_fmla info) t1 (print_fmla info) t2
 192   | Tcase _ -> unsupportedTerm f
 193       "TPTP does not support pattern matching, use eliminate_algebraic"
 194   | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
 195
 196 let print_tvarg fmt tv = fprintf fmt "%a : $tType" print_tvar tv
 197 let print_tvargs fmt tvs = print_iter1 Stv.iter comma print_tvarg fmt tvs
 198
 199 let star fmt _ = fprintf fmt " *@ "
 200
 201 let print_fmla info fmt f =
 202   let tvs = t_ty_freevars Stv.empty f in
 203   if Stv.is_empty tvs then print_fmla info fmt f else
 204   fprintf fmt "![%a]:@ %a" print_tvargs tvs (print_fmla info) f;
 205   Stv.iter forget_tvar tvs
 206
 207 let print_decl info fmt d = match d.d_node with
 208   | Dtype _ when info.info_fmt = FOF -> ()
 209   | Dtype { ts_def = Alias _ } -> ()
 210   | Dtype { ts_args = _::_ } when info.info_fmt = TFF0 -> ()
 211   | Dtype ts when query_syntax info.info_syn ts.ts_name <> None -> ()
 212   | Dtype ts ->
 213       let print_arg fmt _ = pp_print_string fmt "$tType" in
 214       let print_sig fmt ts = match ts.ts_args with
 215         | [] -> pp_print_string fmt "$tType"
 216         | [_] -> fprintf fmt "$tType >@ $tType"
 217         | tl -> fprintf fmt "(%a) >@ $tType" (print_list star print_arg) tl
 218       in
 219       fprintf fmt "@[<hov 2>tff(%s, type,@ %a:@ %a).@]@\n@\n"
 220         (id_unique pr_printer ts.ts_name)
 221         print_symbol ts.ts_name print_sig ts
 222   | Dparam _ when info.info_fmt = FOF -> ()
 223   | Dparam ls when query_syntax info.info_syn ls.ls_name <> None -> ()
 224   | Dparam ls ->
 225       let print_type = print_type info in
 226       let print_val fmt = function
 227         | Some ty -> print_type fmt ty
 228         | None -> fprintf fmt "$o" in
 229       let print_sig fmt ls = match ls.ls_args with
 230         | [] -> print_val fmt ls.ls_value
 231         | [ty] -> fprintf fmt "%a >@ %a"
 232             print_type ty print_val ls.ls_value
 233         | tl -> fprintf fmt "(%a) >@ %a"
 234             (print_list star print_type) tl print_val ls.ls_value in
 235       let print_sig fmt ls =
 236         let tvs = List.fold_left ty_freevars Stv.empty ls.ls_args in
 237         let tvs = oty_freevars tvs ls.ls_value in
 238         if Stv.is_empty tvs then
 239           print_sig fmt ls
 240         else if ls.ls_args = [] then
 241           fprintf fmt "!>[%a]:@ %a" print_tvargs tvs print_sig ls
 242         else
 243           fprintf fmt "!>[%a]:@ (%a)" print_tvargs tvs print_sig ls;
 244         Stv.iter forget_tvar tvs
 245       in
 246       fprintf fmt "@[<hov 2>tff(%s, type,@ %a:@ %a).@]@\n@\n"
 247         (id_unique pr_printer ls.ls_name)
 248         print_symbol ls.ls_name print_sig ls
 249   | Ddata _ -> unsupportedDecl d
 250       "TPTP does not support algebraic datatypes, use eliminate_algebraic"
 251   | Dlogic _ -> unsupportedDecl d
 252       "Definitions are not supported, use eliminate_definition"
 253   | Dind _ -> unsupportedDecl d
 254       "TPTP does not support inductive predicates, use eliminate_inductive"
 255   | Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> ()
 256   | Dprop (Paxiom, pr, f) ->
 257 (*
 258     Format.eprintf "Dprop for %s: rewrite rules:" pr.pr_name.id_string;
 259     Spr.iter (fun pr -> Format.eprintf " %s" pr.pr_name.id_string) info.info_rules;
 260     Format.eprintf "@.";
 261 *)
 262     let annotation = if Spr.mem pr info.info_rules then ",rewrite" else "" in
 263     let head = if info.info_fmt = FOF then "fof" else "tff" in
 264     fprintf fmt "@[<hov 2>%s(%a, axiom,@ %a%s).@]@\n@\n"
 265       head print_pr pr (print_fmla info) f annotation
 266   | Dprop (Pgoal, pr, f) ->
 267       let head = if info.info_fmt = FOF then "fof" else "tff" in
 268       fprintf fmt "@[<hov 2>%s(%a, conjecture,@ %a).@]@\n"
 269         head print_pr pr (print_fmla info) f
 270   | Dprop (Plemma, _, _) -> assert false
 271
 272 let print_decls fm nm =
 273 (*
 274   Format.eprintf "rewrite rules:";
 275   Spr.iter (fun pr -> Format.eprintf " %s" pr.pr_name.id_string) rew_rules;
 276   Format.eprintf "@.";
 277 *)
 278   let print_decl (sm,fm,rr,ct) fmt d =
 279     let info = { info_syn = sm;
 280                  info_fmt = fm;
 281                  info_num = nm;
 282                  info_srt = ref ct;
 283                  info_urg = ref [];
 284                  info_rules = rr } in
 285     try print_decl info fmt d;
 286         (sm,fm,rr,!(info.info_srt)), !(info.info_urg)
 287     with Unsupported s -> raise (UnsupportedDecl (d,s)) in
 288   let print_decl = Printer.sprint_decl print_decl in
 289   let print_decl task acc = print_decl task.Task.task_decl acc in
 290   Discriminate.on_syntax_map (fun sm ->
 291   Trans.on_tagged_pr Compute.meta_rewrite (fun rr ->
 292     Trans.fold print_decl ((sm,fm,rr,Mty.empty),[])))
 293
 294 let print_task fm nm =
 295   let print_decls = print_decls fm nm in
 296   fun args ?old:_ fmt task ->
 297     (* In trans-based p-printing [forget_all] is a no-no *)
 298     (* forget_all ident_printer; *)
 299     print_prelude fmt args.prelude;
 300     print_th_prelude task fmt args.th_prelude;
 301     let rec print = function
 302       | x :: r -> print r; Pp.string fmt x
 303       | [] -> () in
 304     print (snd (Trans.apply print_decls task));
 305     pp_print_flush fmt ()
 306
 307 let () =
 308   register_printer "tptp-tff0" (print_task TFF0 TPTP) ~desc:"TPTP TFF0 format";
 309   register_printer "tptp-tff1" (print_task TFF1 TPTP) ~desc:"TPTP TFF1 format";
 310   register_printer "tptp-fof"  (print_task FOF  TPTP) ~desc:"TPTP FOF format"
 311
 312 let () =
 313   register_printer "metitarski" (print_task FOF MetiTarski)
 314     ~desc:"MetiTarski TPTP format"
 315
 316 (** DFG input format for SPASS >= 3.8
 317     (with the help of Daniel Wand)
 318
 319     TODO:
 320     - type arguments for polymorphic functions and predicates
 321     - data types
 322   *)
 323
 324 let is_type info d = match d.d_node with
 325   | Dtype ts -> query_syntax info.info_syn ts.ts_name = None
 326   | Ddata _ -> unsupportedDecl d "no data types"
 327   | _ -> false
 328 let is_function info d = match d.d_node with
 329   | Dparam ls ->
 330       ls.ls_value <> None && query_syntax info.info_syn ls.ls_name = None
 331   | _ -> false
 332 let is_predicate info d = match d.d_node with
 333   | Dparam ls ->
 334       ls.ls_value = None &&  query_syntax info.info_syn ls.ls_name = None
 335   | _ -> false
 336
 337 let ls_arity fmt d = match d.d_node with
 338   | Dparam ls ->
 339       let ntv = Stv.cardinal (ls_ty_freevars ls) in
 340       let na = List.length ls.ls_args in
 341       if ntv = 0 then fprintf fmt "(%a, %d)" print_symbol ls.ls_name na
 342       else fprintf fmt "(%a, %d+%d)" print_symbol ls.ls_name ntv na
 343   | _ -> assert false
 344 let type_arity fmt d = match d.d_node with
 345   | Dtype ts ->
 346       let ntv = List.length ts.ts_args in
 347       if ntv = 0 then print_symbol fmt ts.ts_name
 348       else fprintf fmt "(%a, %d)" print_symbol ts.ts_name ntv
 349   | _ -> assert false
 350
 351 let ls_type kind info fmt d = match d.d_node with
 352   | Dparam ls ->
 353       fprintf fmt "%s(@[%a" kind print_symbol ls.ls_name;
 354       let tvs = ls_ty_freevars ls in
 355       if not (Stv.is_empty tvs) then
 356         fprintf fmt ", [%a]" (print_list comma print_tvar) (Stv.elements tvs);
 357       begin match ls.ls_value, ls.ls_args with
 358         | None, [] -> ()
 359         | None, _ ->
 360             fprintf fmt ", %a" (print_list comma (print_type info)) ls.ls_args
 361         | Some ty, [] -> fprintf fmt ", %a" (print_type info) ty
 362         | Some ty, _ ->
 363             fprintf fmt ", (%a) %a" (print_list comma (print_type info))
 364               ls.ls_args (print_type info) ty
 365       end;
 366       fprintf fmt "@]).@\n";
 367       Stv.iter forget_tvar tvs
 368   | _ -> assert false
 369
 370 let rec print_app info fmt ls tl oty =
 371   match query_syntax info.info_syn ls.ls_name with
 372   | Some s -> syntax_arguments s (print_term info) fmt tl
 373   | None ->
 374       print_symbol fmt ls.ls_name;
 375       let sbs = ls_app_inst ls tl oty in
 376       if not (Mtv.is_empty sbs) then
 377         fprintf fmt "<%a>"
 378           (print_iter2 Mtv.iter comma nothing nothing (print_type info)) sbs;
 379       if tl <> [] then
 380         fprintf fmt "(%a)"
 381           (print_list comma (print_term info)) tl
 382
 383 and print_term info fmt t = match t.t_node with
 384   | Tvar v ->
 385       print_var fmt v
 386   | Tapp (ls, tl) ->
 387       print_app info fmt ls tl t.t_ty
 388   | Tconst c ->
 389       Constant.(print number_format unsupported_escape) fmt c
 390   | Tlet _ -> unsupportedTerm t
 391       "DFG does not support let, use eliminate_let"
 392   | Tif _ -> unsupportedTerm t
 393       "DFG does not support if, use eliminate_if"
 394   | Tcase _ -> unsupportedTerm t
 395       "TPTP does not support pattern matching, use eliminate_algebraic"
 396   | Teps _ -> unsupportedTerm t
 397       "TPTP does not support epsilon-terms"
 398   | Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
 399
 400 let rec print_fmla info fmt f = match f.t_node with
 401   | Tapp (ls, tl) ->
 402       print_app info fmt ls tl f.t_ty
 403   | Tbinop (op, f1, f2) ->
 404       let s = match op with
 405         | Tand -> "and" | Tor -> "or"
 406         | Timplies -> "implies" | Tiff -> "equiv" in
 407       fprintf fmt "%s(%a,@ %a)" s (print_fmla info) f1 (print_fmla info) f2
 408   | Tnot f ->
 409       fprintf fmt "not(%a)" (print_fmla info) f
 410   | Ttrue ->
 411       pp_print_string fmt "true"
 412   | Tfalse ->
 413       pp_print_string fmt "false"
 414   | Tquant (q, fq) ->
 415       let q = match q with Tforall -> "forall" | Texists -> "exists" in
 416       let vl, _tl, f = t_open_quant fq in
 417       let print_vsty fmt vs =
 418         fprintf fmt "%a:@,%a" print_var vs (print_type info) vs.vs_ty in
 419       fprintf fmt "%s([%a],@ %a)" q
 420         (print_list comma print_vsty) vl (print_fmla info) f;
 421       List.iter forget_var vl
 422   | Tlet _ -> unsupportedTerm f
 423       "DFG does not support let, use eliminate_let"
 424   | Tif _ -> unsupportedTerm f
 425       "DFG does not support if, use eliminate_if"
 426   | Tcase _ -> unsupportedTerm f
 427       "DFG does not support pattern matching, use eliminate_algebraic"
 428   | Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
 429
 430 let print_axiom info fmt d = match d.d_node with
 431   | Dprop (Paxiom, pr, _) when Mid.mem pr.pr_name info.info_syn -> ()
 432   | Dprop (Paxiom, pr, f) ->
 433       fprintf fmt "@[<hov 2>formula(%a, %a).@]@\n"
 434         (print_fmla info) f print_pr pr
 435   | _ -> ()
 436
 437 let print_dfg args ?old:_ fmt task =
 438   forget_all ident_printer;
 439   forget_all pr_printer;
 440   fprintf fmt "@[begin_problem(why3).@\n@\n";
 441   print_prelude fmt args.prelude;
 442   print_th_prelude task fmt args.th_prelude;
 443   fprintf fmt "list_of_descriptions.@\n";
 444   fprintf fmt
 445     "name({**}). author({**}). status(unknown). description({**}).@\n";
 446   fprintf fmt "end_of_list.@\n@\n";
 447   let info = {
 448     info_syn = get_syntax_map task;
 449     info_fmt = FOF;
 450     info_num = TPTP;
 451     info_urg = ref [];
 452     info_srt = ref Mty.empty ;
 453     info_rules = Spr.empty;
 454   } in
 455   let dl = Task.task_decls task in
 456   let tl = List.filter (is_type info) dl in
 457   let fl = List.filter (is_function info) dl in
 458   let pl = List.filter (is_predicate info) dl in
 459   (* arities *)
 460   fprintf fmt "list_of_symbols.@\n";
 461   fprintf fmt "functions [@[%a@]].@\n" (print_list comma ls_arity) fl;
 462   fprintf fmt "predicates [@[%a@]].@\n" (print_list comma ls_arity) pl;
 463   fprintf fmt "sorts [@[%a@]].@\n" (print_list comma type_arity) tl;
 464   fprintf fmt "end_of_list.@\n@\n";
 465   (* types *)
 466   fprintf fmt "list_of_declarations.@\n";
 467   List.iter (ls_type "function" info fmt) fl;
 468   List.iter (ls_type "predicate" info fmt) pl;
 469   fprintf fmt "end_of_list.@\n@\n";
 470
 471   fprintf fmt "list_of_formulae(axioms).@\n";
 472   List.iter (print_axiom info fmt) dl;
 473   fprintf fmt "end_of_list.@\n@\n";
 474   fprintf fmt "list_of_formulae(conjectures).@\n";
 475
 476   let f = Task.task_goal_fmla task in
 477   fprintf fmt "@[<hov 2>formula(%a, %a)@].@\n" (print_fmla info) f
 478     print_pr (Task.task_goal task);
 479   fprintf fmt "end_of_list.@\n@\n";
 480   fprintf fmt "end_problem.@\n"
 481
 482 let () =
 483   register_printer "dfg" print_dfg ~desc:"First-order monomorphic DFG format"