2:- module(fol2tptp,[fol2tptp/2,
    3                    fol2tptp/3,
    4                    fol2tptpNew/2,
    5                    fol2tptpNew/3,
    6                    fol2tptpOld/2,
    7                    fol2tptpOld/3,
    8                    printArgs/2]).    9
   10:- use_module(semlib(errors),[warning/2]).   11
   12
   13/* ========================================================================
   14   Select TPTP syntax style (default: New style)
   15======================================================================== */
   16
   17fol2tptp(Conjecture,Stream):- fol2tptpNew(Conjecture,Stream).
   18fol2tptp(Axioms,Conjecture,Stream):- fol2tptpNew(Axioms,Conjecture,Stream).
   19
   20
   21/* ========================================================================
   22   Translates formula to TPTP syntax on Stream (new style TPTP)
   23======================================================================== */
   24
   25fol2tptpNew(Formula,Stream):- 
   26   write(Stream,'fof(nutcracker,conjecture,'),
   27   \+ \+ ( numbervars(Formula,0,_),printTPTP(Formula,Stream) ),
   28   write(Stream,').'),
   29   nl(Stream).
   30
   31
   32/* ========================================================================
   33   Translates axioms+formula to TPTP syntax on Stream (new style TPTP)
   34======================================================================== */
   35
   36fol2tptpNew([],Formula,Stream):- !,
   37   fol2tptpNew(Formula,Stream).
   38
   39fol2tptpNew([Axiom|L],Formula,Stream):- 
   40   write(Stream,'fof(nutcracker,axiom,'),
   41   \+ \+ ( numbervars(Axiom,0,_),printTPTP(Axiom,Stream) ),
   42   write(Stream,').'), nl(Stream),
   43   fol2tptpNew(L,Formula,Stream).
   44
   45
   46/* ========================================================================
   47   Translates formula to TPTP syntax on Stream (old style TPTP)
   48======================================================================== */
   49
   50fol2tptpOld(Formula,Stream):-
   51   write(Stream,'input_formula(nutcracker,conjecture,'),
   52   \+ \+ ( numbervars(Formula,0,_),printTPTP(Formula,Stream) ),
   53   write(Stream,').'),
   54   nl(Stream).
   55
   56
   57/* ========================================================================
   58   Translates axioms+formula to TPTP syntax on Stream (old style TPTP)
   59======================================================================== */
   60
   61fol2tptpOld([],Formula,Stream):- !,
   62   fol2tptpOld(Formula,Stream).
   63
   64fol2tptpOld([Axiom|L],Formula,Stream):- 
   65   write(Stream,'input_formula(nutcracker,axiom,'),
   66   \+ \+ ( numbervars(Axiom,0,_),printTPTP(Axiom,Stream) ),
   67   write(Stream,').'), nl(Stream),
   68   fol2tptpOld(L,Formula,Stream).
   69
   70
   71/* ========================================================================
   72   Print TPTP formulas
   73======================================================================== */
   74
   75printTPTP(some(X,Formula),Stream):- !,
   76   write(Stream,'(? ['),
   77   write_term(Stream,X,[numbervars(true)]),
   78   write(Stream,']: '),
   79   printTPTP(Formula,Stream),
   80   write(Stream,')').
   81
   82printTPTP(all(X,Formula),Stream):- !,
   83   write(Stream,'(! ['),
   84   write_term(Stream,X,[numbervars(true)]),
   85   write(Stream,']: '),
   86   printTPTP(Formula,Stream),
   87   write(Stream,')').
   88
   89printTPTP(and(Phi,Psi),Stream):- !,
   90   write(Stream,'('),
   91   printTPTP(Phi,Stream), 
   92   write(Stream,' & '), 
   93   printTPTP(Psi,Stream), 
   94   write(Stream,')').
   95
   96printTPTP(or(Phi,Psi),Stream):- !,
   97   write(Stream,'('),
   98   printTPTP(Phi,Stream), 
   99   write(Stream,' | '),
  100   printTPTP(Psi,Stream), 
  101   write(Stream,')').
  102
  103printTPTP(imp(Phi,Psi),Stream):- !,
  104   write(Stream,'('),
  105   printTPTP(Phi,Stream), 
  106   write(Stream,' => '),
  107   printTPTP(Psi,Stream), 
  108   write(Stream,')').
  109
  110printTPTP(bimp(Phi,Psi),Stream):- !,
  111   write(Stream,'('),
  112   printTPTP(Phi,Stream), 
  113   write(Stream,' <=> '),
  114   printTPTP(Psi,Stream), 
  115   write(Stream,')').
  116
  117printTPTP(not(Phi),Stream):- !,
  118   write(Stream,'~ '),
  119   printTPTP(Phi,Stream).
  120
  121printTPTP(eq(X,Y),Stream):- !,
  122   write_term(Stream,X=Y,[numbervars(true)]).
  123
  124printTPTP(Pred,Stream):-
  125   nonvar(Pred),
  126   Pred =.. [Sym|Args],
  127   write(Stream,Sym),
  128   write(Stream,'('),
  129   printArgs(Args,Stream),
  130   write(Stream,')').
  131
  132
  133/* ========================================================================
  134   Print arguments
  135======================================================================== */
  136
  137printArgs([X],Stream):- !,
  138   printArg(Stream,X).
  139
  140printArgs([X|L],Stream):- 
  141   printArg(Stream,X),
  142   write(Stream,','),
  143   printArgs(L,Stream).
  144
  145
  146/* ========================================================================
  147   Print argument
  148======================================================================== */
  149
  150printArg(Stream,X):- 
  151   functor(X,'$VAR',1), !,
  152   write_term(Stream,X,[numbervars(true)]).
  153
  154printArg(Stream,X):- 
  155   warning('term expexted, found formula: ~p',X),
  156   write_term(Stream,X,[numbervars(true)])