2:- module(fol2bliksem,[fol2bliksem/2,
    3                       fol2bliksem/3]).    4
    5:- use_module(nutcracker(fol2tptp),[printArgs/2]).    6
    7
    8/* ========================================================================
    9   Translates formula to otter syntax on Stream
   10======================================================================== */
   11
   12fol2bliksem(Formula,Stream):-
   13   format(Stream,'~nAuto.~n~n',[]),
   14   printBliksemFormula(Stream,Formula).
   15
   16fol2bliksem(Axioms,Formula,Stream):-
   17   format(Stream,'~nAuto.~n~n',[]),
   18   printBliksemFormulas(Axioms,Stream),
   19   printBliksemFormula(Stream,Formula).
   20
   21
   22/* ========================================================================
   23   Print a Bliksem formula (introducing tab)
   24======================================================================== */
   25
   26printBliksemFormula(Stream,F):-
   27   \+ \+ ( numbervars(F,0,_),
   28           printBliksem(F,5,Stream) ),
   29   format(Stream,'.~n',[]).
   30
   31
   32/* ========================================================================
   33   Print a list of Bliksem formulas
   34======================================================================== */
   35
   36printBliksemFormulas([],_):- !.
   37
   38printBliksemFormulas([F|L],Stream):-
   39   printBliksemFormula(Stream,F),
   40   printBliksemFormulas(L,Stream).
   41
   42
   43/* ========================================================================
   44   Print Bliksem formulas
   45======================================================================== */
   46
   47printBliksem(some(X,Formula),Tab,Stream):- !,
   48   write(Stream,'(< '),
   49   write_term(Stream,X,[numbervars(true)]),
   50   write(Stream,' >'),
   51   printBliksem(Formula,Tab,Stream),
   52   write(Stream,')').
   53
   54printBliksem(all(X,Formula),Tab,Stream):- !,
   55   write(Stream,'([ '),
   56   write_term(Stream,X,[numbervars(true)]),
   57   write(Stream,' ]'),
   58   printBliksem(Formula,Tab,Stream),
   59   write(Stream,')').
   60
   61printBliksem(and(Phi,Psi),Tab,Stream):- !,
   62   write(Stream,'('),
   63   printBliksem(Phi,Tab,Stream), 
   64   format(Stream,' & ~n',[]),
   65   tab(Stream,Tab),
   66   NewTab is Tab + 5,
   67   printBliksem(Psi,NewTab,Stream),
   68   write(Stream,')').
   69
   70printBliksem(or(Phi,Psi),Tab,Stream):- !,
   71   write(Stream,'('),
   72   printBliksem(Phi,Tab,Stream),
   73   write(Stream,' | '),
   74   printBliksem(Psi,Tab,Stream),
   75   write(Stream,')').
   76
   77printBliksem(imp(Phi,Psi),Tab,Stream):- !,
   78   write(Stream,'('),  
   79   printBliksem(Phi,Tab,Stream),
   80   write(Stream,' -> '),
   81   printBliksem(Psi,Tab,Stream),
   82   write(Stream,')').
   83
   84printBliksem(bimp(Phi,Psi),Tab,Stream):- !,
   85   write(Stream,'('),  
   86   printBliksem(Phi,Tab,Stream),
   87   write(Stream,' <-> '),
   88   printBliksem(Psi,Tab,Stream),
   89   write(Stream,')').
   90
   91printBliksem(not(Phi),Tab,Stream):- !,
   92   write(Stream,'!'),
   93   printBliksem(Phi,Tab,Stream).
   94
   95printBliksem(eq(X,Y),_,Stream):- !,
   96   write(Stream,'( '),
   97   write_term(Stream,X,[numbervars(true)]),
   98   write(Stream,' = '),
   99   write_term(Stream,Y,[numbervars(true)]),
  100   write(Stream,' )').
  101
  102printBliksem(Pred,_,Stream):-
  103   nonvar(Pred),
  104   Pred =.. [Sym|Args],
  105   write(Stream,Sym),
  106   write(Stream,'('),
  107   printArgs(Args,Stream),
  108   write(Stream,')')