:- op(650, xfy, eqv).	 % equivalence
:- op(640, xfy, imp).    % implication
:- op(630, xfy, or).     % binary disjunction
:- op(620, xfy, and).    % binary conjunction
:- op(610, fy, or_set).  % unary disjunction
:- op(610, fy, and_set). % unary conjunction
:- op(610, fy, neg).	 % negation

%
% Question 4
%

%
%                    STANDARDIZING FORMULAS
%


%
%  standardize(+Formula, -StandardFormula)
%    StandardFormula is a formula built from negation only applied to atoms,
%    and disjunction and conjunction applied to (possibly empty) sets of formulas;
%    Formula is a formula defined from negation, binary disjunction,
%    conjunction, implication and logical equivalence, and unary disjunction
%    and conjunction as allowed in StandardFormula;
%    Formula is to be viewed as an abbreviation of Standardformula
%

% A v B
standardize(A or B, or_set Formulas) :-
	standardize(A, AFormula),
	standardize(B, BFormula),
	sort([AFormula, BFormula], Formulas).

% A ^ B
% YOU MUST WRITE THIS RULE

% \/ { Forms }
standardize(or_set Forms, or_set Formulas) :-
	maplist(standardize, Forms, StandardForms),
	sort(StandardForms, Formulas).

% /\ { Forms }
% YOU MUST WRITE THIS RULE

% A <-> B
% YOU MUST WRITE THIS RULE

% A -> B
% YOU MUST WRITE THIS RULE

% ~ ~ A
standardize(neg neg A, Formula) :-
	standardize(A, Formula).

% ~ \/ { Forms }
standardize(neg or_set Forms, and_set Formulas) :-
        maplist(negate, Forms, NegatedForms),
        maplist(standardize, NegatedForms, NegatedFormulas),
        sort(NegatedFormulas, Formulas).


%
%    SEVERAL MORE RULES FOR NEGATION ARE REQUIRED
%                 WHICH YOU MUST WRITE
%


%
% This rule works with the above four rules
%
%            ***** BUT *****
%
%     YOU WILL NEED TO MODIFY THIS RULE!
%
standardize(Formula, Formula) :-
  Formula \= _ or _,
  Formula \= or_set _,
  Formula \= neg neg _,
  Formula \= neg or_set _.


%
%  negate(+Formula, - NegatedFormula)
%
negate(Formula, neg Formula).

%
%  YOUR CODE WILL BE TESTED WITH THE FOLLOWING PREDICATE:
%

standardize_test(ExternalFormula) :-
        from_external_to_internal(ExternalFormula, InternalFormula),
        standardize(InternalFormula, Formula),
        write_formula(Formula).

%
%   Question 5
%

%
%                  EXTENDING SEMANTIC TABLEAU
%

%
%                    YOU MUST WRITE CODE HERE
%
% You must write:
%
%   create_tableau/2
%
% as per the comments below.  You may find it useful to 
% also write extend_tableau and call extend_tableau from 
% create_tableau.
%

%  A construction of semantic tableaux for the language
%    of negation only applied to atomic formulas,
%    and disjunction and conjunction applied to
%    (possibly empty) finite sets of formulas

%
%  create_tableau(+Formula, -Tableau)
%    Tableau is a pair of the form
%    (ListOfFormulas, ListOfSubtableaux),
%    where ListOfFormulas is initialized to [Formula];
%    the tableau is constructed by instantiating the logical
%    variable for ListOfSubtableaux
%

%
%  extend_tableau(+(ListOfFormulas, ListOfSubtableaux))
%    1. check for a pair of contradicatory formulas (branch is closed)
%    2. check if Formulas contains only literals (branch is open)
%    3. if possible, find a conjunction in some member of ListOfFormulas;
%       either the conjunction is over the empty set and the branch is open,
%       or the conjuncts are added to ListOfFormulas to make up the root
%       of ListOfSubtableaux
%    4. otherwise find a disjunction in some member of ListOfFormulas;
%       either the disjunction is over the empty set and the branch is closed,
%       or each disjunct is added to ListOfFormulas to make up the root
%       of as many members of ListOfSubtableaux
%

write_tableau(Tableau) :-
        write_tableau(0, Tableau).

%
%  write_tableau(+Indent, +Tableau)
%    Write Tableau, indenting each level of the tree by indent spaces
%    SubTableux are indented by an additional four spaces
%

write_tableau(Indent, (Formulas, [closed])) :- !,
	nl, tab(Indent),
	write_flat_formula_list(Formulas),
	write('   Closed').
write_tableau(Indent, (Formulas, [open])) :-
	nl, tab(Indent),
	write_flat_formula_list(Formulas),
	write('   Open').
write_tableau(Indent, (Formulas, SubTableaux)) :-
	nl, tab(Indent),
	write_flat_formula_list(Formulas),
	NewIndent is Indent + 4,
	checklist(write_tableau(NewIndent), SubTableaux).

%
%  YOUR CODE WILL BE TESTED WITH THE FOLLOWING PREDICATE:
%

tableau_test(ExternalFormula) :-
        from_external_to_internal(ExternalFormula, Formula),
        standardize(Formula, StandardFormula),
        create_tableau(StandardFormula, Tableau),
        write_tableau(Tableau).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
%      You do NOT need to modify anything below this line
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% external/internal operators -

operators_for_external_representation :-
	op(650, xfy, <->),   % equivalence
	op(640, xfy, ->),    % implication
        op(630, xfy, v),     % binary disjunction
        op(620, xfy, ^),     % binary conjunction
	op(610, fy, \/),     % unary disjunction
	op(610, fy, /\),     % unary conjunction
	op(610, fy, ~).      % negation

back_to_standard_representation_of_operators :-
	op(1050, xfy, ->),
	op(900, fy, ~),
	op(500, yfx, \/),
	op(500, yfx, /\),
        op(200, xfy, ^).



%
%  input_output
%    translates external representation to internal representation
%    (changing the names of operators);
%    writes formulas and lists of formulas with or without indenting
%    of subformulas
%

:- operators_for_external_representation.

%
%  operator_translation(?External, ?Internal)
%
operator_translation(<->, eqv).
operator_translation(->, imp).
operator_translation(v, or).
operator_translation(^, and).

%
%  from_external_to_internal(+ExternalFormula, -InternalFormula)
%
from_external_to_internal(ExternalFormula, InternalFormula) :-
	to_internal(ExternalFormula, InternalFormula),
	back_to_standard_representation_of_operators.

%
%  to_internal(+ExternalFormula, -InternalFormula)
%
to_internal(\/ ExternalFormulas, or_set InternalFormulas) :- !,
	maplist(to_internal, ExternalFormulas, InternalFormulas).
to_internal(/\ ExternalFormulas, and_set InternalFormulas) :- !,
	maplist(to_internal, ExternalFormulas, InternalFormulas).
to_internal(~ ExternalFormula, neg InternalFormula) :- !,
	to_internal(ExternalFormula, InternalFormula).
to_internal(ExternalFormula, InternalFormula) :-
        ExternalFormula =.. [ExternalOperator, ExtForm1, ExtForm2],
        operator_translation(ExternalOperator, InternalOperator), !,
        to_internal(ExtForm1, IntForm1),
        to_internal(ExtForm2, IntForm2),
        InternalFormula =.. [InternalOperator, IntForm1, IntForm2].
to_internal(ExternalFormula, InternalFormula) :-
        ExternalFormula =.. [ExternalOperator, ExtForm],
        operator_translation(ExternalOperator, InternalOperator), !,
        to_internal(ExtForm, IntForm),
        InternalFormula =.. [InternalOperator, IntForm].
to_internal(Formula, Formula).

%
%  write_formula(+Formula)
%    writes Formula indending sets of disjuncts and sets of conjuncts
%    that contain at least one disjunction or one conjunction, plus
%    another formula
%
write_formula(Formula) :-
	write_formula(0, Formula), nl.

%
%  write_formula(+Indent, +Formula)
%    writes Formula indending sets of disjuncts and sets of conjuncts
%    that contain at least one disjunction or one conjunction, plus
%    another formula, with Indent as indentation value
%
write_formula(N, or_set Formulas) :- !,
	write('\\/ ['),
	write_formulas(N, Formulas),
	write(']').
write_formula(N, and_set Formulas) :- !,
	write('/\\ ['),
	write_formulas(N, Formulas),
	write(']').
write_formula(_, neg Formula) :- !,
	write('~'),
	write(Formula).
write_formula(_, Formula) :-
	write(Formula).

%
%  write_formulas(+Indent, +Formulas)
%
write_formulas(N, [Formula| Formulas]) :-
	select(or_set _, [Formula |Formulas], [_ |_]), !,
	N1 is N + 4,
	write_formula(N1, Formula),
	write_formulas1(N1, Formulas).
write_formulas(N, [Formula| Formulas]) :-
	select(and_set _, [Formula |Formulas], [_ |_]), !,
	N1 is N + 4,
	write_formula(N1, Formula),
	write_formulas1(N1, Formulas).
write_formulas(N, [or_set List]) :- !,
	write_formula(N, or_set List).
write_formulas(N, [and_set List]) :- !,
	write_formula(N, and_set List).
write_formulas(_, Formulas) :-
	write_formula_list(Formulas).

%
%  write_formulas1(+Indent, +Formulas)
%
write_formulas1(N, [Formula| Formulas]) :-
	writeln(', '),
	tab(N),
	write_formula(N, Formula),
	write_formulas1(N, Formulas).
write_formulas1(_, []).

%
%  write_formula_list(+Formulas)
%
write_formula_list([neg Formula1, Formula2| Formulas]) :- !,
        writef('~%w, ', [Formula1]),
        write_formula_list([Formula2| Formulas]).
write_formula_list([Formula1, Formula2| Formulas]) :- !,
        writef('%w, ', [Formula1]),
        write_formula_list([Formula2| Formulas]).
write_formula_list([neg Formula]) :- !,
        writef('~%w ', [Formula]).
write_formula_list([Formula]) :-
        write(Formula).
write_formula_list([]).

%
%  write_flat_formula(+Formula)
%    writes Formula on one line
%
write_flat_formula(or_set Formulas) :- !,
	write('\\/ ['),
	write_flat_formula_list(Formulas),
	write(']').
write_flat_formula(and_set Formulas) :- !,
	write('/\\ ['),
	write_flat_formula_list(Formulas),
	write(']').
write_flat_formula(neg Formula) :- !,
	write('~'),
	write(Formula).
write_flat_formula(Formula) :-
	write(Formula).

%
%  write_flat_formula_list(+ListOfFormulas)
%
write_flat_formula_list([Formula1, Formula2| Formulas]) :- !,
	write_flat_formula(Formula1),
	write(', '),
        write_flat_formula_list([Formula2| Formulas]).
write_flat_formula_list([Formula]) :-
        write_flat_formula(Formula).
write_flat_formula_list([]).