2:- module(fol2otter,[fol2otter/2,
    3                     fol2otter/3,
    4                     fol2mace/2,
    5                     fol2mace/3]).    6
    7:- use_module(nutcracker(fol2tptp),[printArgs/2]).    8
    9
   10/*========================================================================
   11   Translates formula to Otter syntax on Stream
   12========================================================================*/
   13
   14fol2otter(Formula,Stream):-
   15   headerOtter(Stream),
   16   printOtterFormula(Formula,Stream),
   17   footerOtter(Stream).
   18
   19fol2otter(Axioms,Formula,Stream):-
   20   headerOtter(Stream),
   21   printOtterFormulas(Axioms,Stream),
   22   printOtterFormula(Formula,Stream),
   23   footerOtter(Stream).
   24
   25
   26/*========================================================================
   27   Header and Footer OTTER
   28========================================================================*/
   29
   30headerOtter(Stream):- 
   31   format(Stream,'set(auto).~n~n',[]),
   32   format(Stream,'assign(max_seconds,100).~n~n',[]),
   33   format(Stream,'clear(print_proofs).~n~n',[]),
   34   format(Stream,'set(prolog_style_variables).~n~n',[]),
   35   format(Stream,'formula_list(usable).~n~n',[]).
   36
   37footerOtter(Stream):-
   38   format(Stream,'~nend_of_list.~n',[]).
   39
   40
   41/*========================================================================
   42   Translates formula to MACE syntax on Stream
   43========================================================================*/
   44
   45fol2mace(Formula,Stream):- 
   46   headerMace(Stream),
   47   printOtterFormula(Formula,Stream),
   48   footerMace(Stream).
   49
   50fol2mace(Axioms,Formula,Stream):- 
   51   headerMace(Stream),
   52   printOtterFormulas(Axioms,Stream),
   53   printOtterFormula(Formula,Stream),
   54   footerMace(Stream).
   55
   56
   57/*========================================================================
   58   Header and footer MACE
   59========================================================================*/
   60
   61headerMace(Stream):-
   62   format(Stream,'set(auto).~n~n',[]),
   63   format(Stream,'clear(print_proofs).~n~n',[]),
   64   format(Stream,'set(prolog_style_variables).~n~n',[]),
   65   format(Stream,'formula_list(usable).~n~n',[]).
   66
   67footerMace(Stream):-
   68   format(Stream,'~nend_of_list.~n',[]).
   69
   70
   71/*========================================================================
   72   Print an Otter formula (introducing tab)
   73========================================================================*/
   74
   75printOtterFormula(F,Stream):-
   76   \+ \+ ( numbervars(F,0,_),
   77           printOtter(F,5,Stream) ),
   78   format(Stream,'.~n',[]).
   79
   80
   81/*========================================================================
   82   Print a set of Otter formulas
   83========================================================================*/
   84
   85printOtterFormulas([],_).
   86
   87printOtterFormulas([F|L],Stream):-
   88   printOtterFormula(F,Stream),
   89   printOtterFormulas(L,Stream).
   90
   91
   92/*========================================================================
   93   Print Otter formulas
   94========================================================================*/
   95
   96printOtter(some(X,Formula),Tab,Stream):- !, 
   97   write(Stream,'(exists '),
   98   write_term(Stream,X,[numbervars(true)]),
   99   write(Stream,' '),
  100   printOtter(Formula,Tab,Stream),
  101   write(Stream,')').
  102
  103printOtter(all(X,Formula),Tab,Stream):- !,
  104   write(Stream,'(all '),
  105   write_term(Stream,X,[numbervars(true)]),   
  106   write(Stream,' '),
  107   printOtter(Formula,Tab,Stream),
  108   write(Stream,')').
  109
  110printOtter(and(Phi,Psi),Tab,Stream):- !,
  111   write(Stream,'('),
  112   printOtter(Phi,Tab,Stream), 
  113   format(Stream,' & ~n',[]),
  114   tab(Stream,Tab),
  115   NewTab is Tab + 5,
  116   printOtter(Psi,NewTab,Stream),
  117   write(Stream,')').
  118
  119printOtter(or(Phi,Psi),Tab,Stream):- !,
  120   write(Stream,'('),
  121   printOtter(Phi,Tab,Stream),
  122   write(Stream,' | '),
  123   printOtter(Psi,Tab,Stream),
  124   write(Stream,')').
  125
  126printOtter(imp(Phi,Psi),Tab,Stream):- !,
  127   write(Stream,'('),  
  128   printOtter(Phi,Tab,Stream),
  129   write(Stream,' -> '),
  130   printOtter(Psi,Tab,Stream),
  131   write(Stream,')').
  132
  133printOtter(bimp(Phi,Psi),Tab,Stream):- !,
  134   write(Stream,'('),  
  135   printOtter(Phi,Tab,Stream),
  136   write(Stream,' <-> '),
  137   printOtter(Psi,Tab,Stream),
  138   write(Stream,')').
  139
  140printOtter(not(Phi),Tab,Stream):- !,
  141   write(Stream,'-('),
  142   printOtter(Phi,Tab,Stream),
  143   write(Stream,')').
  144
  145printOtter(eq(X,Y),_,Stream):- !,
  146   write(Stream,'('),  
  147   write_term(Stream,X,[numbervars(true)]),
  148   write(Stream,' = '),
  149   write_term(Stream,Y,[numbervars(true)]),
  150   write(Stream,')').
  151
  152printOtter(Pred,_,Stream):-
  153   nonvar(Pred),
  154   Pred =.. [Sym|Args],
  155   write(Stream,Sym),
  156   write(Stream,'('),
  157   printArgs(Args,Stream),
  158   write(Stream,')')