/* Frege-Konverter: ein Prolog-Programm, das m.o.w. normale PL-Formeln */
/* in Begriffsschrift-Notation unwandelt. */
/* Christopher.von.Buelow@uni-konstanz.de */

frege(Formel)  :-
   normiere(Formel, NFormel),
   kuerze(NFormel, KFormel),
   del_all(usr),
   add_pic(line((10, 10), (10, 14))),
   male(10, 14, KFormel).
frege(b, Formel)  :-
   frege(Formel),
   beh_strich.
frege(uk, Formel)  :-
   normiere(Formel, NFormel),
   del_all(usr),
   add_pic(line((10, 10), (10, 14))),
   male(10, 14, NFormel).
frege(bu, Formel)  :-
   frege(uk, Formel),
   beh_strich.

beh_strich  :-
   add_pic(double(line((5, 9),(14, 9)))). 

/* normiere(Formel, NFormel) formt eine Formel so um, da§ */
/* sie an logischen Zeichen nur noch "->", "-" und "all" enthŠlt. */
normiere(P->Q, NP->NQ)  :-
   normiere(P, NP),
   normiere(Q, NQ).
normiere(P<->Q, -((NP->NQ)-> -(NQ->NP)))  :-
   normiere(P, NP),
   normiere(Q, NQ).
normiere(P&Q, -(NP-> -NQ))  :-
   normiere(P, NP),
   normiere(Q, NQ).
normiere(P v Q, -NP-> NQ)  :-
   normiere(P, NP),
   normiere(Q, NQ).
normiere(-P, -NP)  :-
   normiere(P, NP).
normiere(all(V, P), all(V, NP))  :-
   normiere(P, NP).
normiere(ex(V, P), -all(V, -NP))  :-
   normiere(P, NP).
normiere(P, P).

/* kuerze(Formel, KFormel) kŸrzt aus der Formel alle nebeneinander- */
/* liegenden Paare von Negationszeichen heraus. */
kuerze(P->Q, KP->KQ)  :-  kuerze(P, KP), kuerze(Q, KQ).
kuerze(-(-P), KP)  :-  kuerze(P, KP).
kuerze(-P, -KP)  :-  kuerze(P, KP).
kuerze(all(V, P), all(V, KP))  :-  kuerze(P, KP).
kuerze(P, P).

/* enden(Formel, Anzahl) zŠhlt die Enden  */
/* des Baumes, den die Formel darstellt. */
enden(P->Q, Enden)  :-
   !,
   enden(P, M),
   enden(Q, N),
   Enden is M+N.
enden(-P, Enden)  :-
   !,
   enden(P, Enden).
enden(all(V, P), Enden)  :-
   !,
   enden(P, Enden).
enden(_, 1).

/* breite(Formel, Breite) gibt die Breite des "Strichteils" des */
/* Begriffsschriftausdrucks an, in den die Formel umgewandelt wird. */
breite(P->Q, Breite)  :-
   breite(P, M),
   breite(Q, N),
   max(M, N, Max),
   Breite is Max+8.
breite(-P, Breite)  :-
   breite(P, M),
   Breite is M+8.
breite(all(V, P), Breite)  :-
   breite(P, M),
   Breite is M+20.
breite(_, 5).

/* max(M, N, Maximum_von_M_und_N) */
max(M, N, M)  :-  M>=N.
max(M, N, N)  :-  M<N.

/* male(Y, X, Formel) bringt den Begriffsschriftausdruck */
/* ins Bild, zu dem die Formel wird, und zwar ausgehend */
/* vom Punkt (Y, X) nach rechts unten sich ausbreitend. */
male(Y, X, P->Q)  :-
   X1 is X+4,
   breite(P->Q, B),
   breite(P, B1),
   breite(Q, B2),
   X2 is X+B-B2,
   X3 is X+B-B1,
   enden(Q, QEnden),
   Y1 is Y+12*QEnden,
   add_pic(line((Y, X), (Y, X2))),
   add_pic(line((Y, X1), (Y1, X1))),
   add_pic(line((Y1, X1), (Y1, X3))),
   male(Y, X2, Q),
   male(Y1, X3, P).
male(Y, X, -P)  :-
   X1 is X+4,
   X2 is X+8,
   Y1 is Y+5,
   add_pic(line((Y, X), (Y, X2))),
   add_pic(line((Y, X1), (Y1, X1))),
   male(Y, X2, P).
male(Y, X, all(V, P))  :-
   X1 is X+4,
   X2 is X+6,
   X3 is X+16,
   X4 is X+20,
   Y1 is Y-6,
   add_pic(line((Y, X), (Y, X1))),
   add_pic(line((Y, X3), (Y, X4))),
   add_pic(arc(Y1, X1, 12, 12, 90, 180)),
   add_pic(text('Times', 12, 0, Y, X2, V)),
   male(Y, X4, P).
male(Y, X, P)  :-
   X1 is X+5,
   X2 is X+9,
   Y1 is Y+4,
   add_pic(line((Y, X), (Y, X1))),
   pname(P, PName),
   add_pic(text('Times', 12, 0, Y1, X2, PName)).