/*  Degree and Rank Calculation Program - Exercise 2.9.4

  Propositional operators are: neg, and, or, imp, revimp,
    uparrow, downarrow, notimp and notrevimp.
*/

?-op(140, fy, neg).
?-op(160, xfy, [and, or, imp, revimp, uparrow, downarrow,
    notimp, notrevimp]).


/*  analyse(Z, X, Y) :- X and Y are the subformulas of Z.
*/

analyse(X and Y, X, Y).
analyse(X or Y, X, Y).
analyse(X imp Y, X, Y).
analyse(X revimp Y, X, Y).
analyse(X uparrow Y, X, Y).
analyse(X downarrow Y, X, Y).
analyse(X notimp Y, X, Y).
analyse(X notrevimp Y, X, Y).


/*  components(X, Y, Z) :- Y and Z are the components
      of the formula X, as defined in the alpha and
      beta table.
*/

components(X and Y, X, Y).
components(neg(X and Y), neg X, neg Y).
components(X or Y, X, Y).
components(neg(X or Y), neg X, neg Y).
components(X imp Y, neg X, Y).
components(neg(X imp Y), X, neg Y).
components(X revimp Y, X, neg Y).
components(neg(X revimp Y), neg X, Y).
components(X uparrow Y, neg X, neg Y).
components(neg(X uparrow Y), X, Y).
components(X downarrow Y, neg X, neg Y).
components(neg(X downarrow Y), X, Y).
components(X notimp Y, X, neg Y).
components(neg(X notimp Y), neg X, Y).
components(X notrevimp Y, neg X, Y).
components(neg(X notrevimp Y), X, neg Y).


/*  degree(F, D) :- D is the degree of the formula F.
*/

degree(neg Formula, Deg) :-
  degree(Formula, Degf),
  Deg is Degf + 1.

degree(Formula, Deg) :-
  analyse(Formula, X, Y),
  degree(X, Degx),
  degree(Y, Degy),
  Deg is Degx + Degy + 1.

degree(_, 0).


/*  rank(F, R) :- R is the rank of the formula F.
*/

rank(neg false, 1).

rank(neg true, 1).

rank(neg neg Z, Rank) :-
  rank(Z, Rankz),
  Rank is Rankz + 1.

rank(Formula, Rank) :-
  components(Formula, X, Y),
  rank(X, Rankx),
  rank(Y, Ranky),
  Rank is Rankx + Ranky + 1.

rank(_, 0).