:- ensure_loaded('../Basis/internal_operators.pl').
:- ensure_loaded('../Basis/truth_tables.pl').
:- use_module('../Basis/translations.pl').

%
%  create_tt(+Formula) creates the truth table for Formula
%    - get_atoms gets a list Atoms of the atoms in Formula
%    - generate_valuation creates a valuation for the Atoms
%    (i.e., a list of pairs (Atom,TruthValue) where
%    Atom is a propositional symbol and TruthValue is the value assigned to it)
%    - truth_value computes the truth value of a formula under a valuation
%    - write_tt_line print a line of the truth table 
%    - fail is used to generate all valuations on backtracking
%
create_tt(Formula) :-
	get_atoms(Formula, Atoms),
	from_internal_to_printable(Formula, PrintableFormula),
	write_tt_title(PrintableFormula, Atoms),
	atom_length(PrintableFormula, Length),
	generate_valuation(Atoms, Valuation),
	truth_value(Formula, Valuation, TruthValues),
	write_tt_line(Length, Valuation, TruthValues),
	fail.
create_tt(_).

%
%  get_atoms(+Formula, -SortedAtoms)
%
get_atoms(Formula, SortedAtoms) :-
	get_atoms1(Formula, UnsortedAtoms),
	sort(UnsortedAtoms, SortedAtoms).

%
%  get_atoms1(+Formula, -Atoms)
%
get_atoms1(Formula, Atoms) :-
	Formula =.. [_, Form], !,
	get_atoms1(Form, Atoms).
get_atoms1(Formula, Atoms) :-
	Formula =.. [_, Form1, Form2], !,
	get_atoms1(Form1, Atoms1),
	get_atoms1(Form2, Atoms2),
	union(Atoms1, Atoms2, Atoms).
get_atoms1(Atom, [Atom]).

%
%  generate_valuation(+Atoms, -Valuation)
%    for each atom Atom in the list Atoms,
%    generate a pair, first (Atom,t) and upon backtracking (Atom,f)
%
generate_valuation([Atom| Atoms], [(Atom, t)| TruthValues]) :-
	generate_valuation(Atoms, TruthValues).
generate_valuation([Atom| Atoms], [(Atom, f)| TruthValues]) :-
	generate_valuation(Atoms, TruthValues).
generate_valuation([], []).

%
%  truth_value(+Formula, +Valuation, -TruthValue)
%
truth_value(neg A, Valuation, TruthValue) :-
	truth_value(A, Valuation, TruthValueA),
	negation(TruthValueA, TruthValue).
truth_value(A or  B, Valuation, TruthValue) :-
	truth_value(A, Valuation, TruthValueA),
	truth_value(B, Valuation, TruthValueB),
	binary_operation(or,  TruthValueA, TruthValueB, TruthValue).
truth_value(A and B, Valuation, TruthValue) :-
	truth_value(A, Valuation, TruthValueA),
	truth_value(B, Valuation, TruthValueB),
	binary_operation(and, TruthValueA, TruthValueB, TruthValue).
truth_value(A imp B, Valuation, TruthValue) :-
	truth_value(A, Valuation, TruthValueA),
	truth_value(B, Valuation, TruthValueB),
	binary_operation(imp, TruthValueA, TruthValueB, TruthValue).
truth_value(A eqv B, Valuation, TruthValue) :-
	truth_value(A, Valuation, TruthValueA),
	truth_value(B, Valuation, TruthValueB),
	binary_operation(eqv, TruthValueA, TruthValueB, TruthValue).
truth_value(A xor B, Valuation, TruthValue) :-
	truth_value(A, Valuation, TruthValueA),
	truth_value(B, Valuation, TruthValueB),
	binary_operation(xor, TruthValueA, TruthValueB, TruthValue).
truth_value(A, Valuation, TruthValue) :-
	member((A, TruthValue), Valuation).


%
%  write_tt_title(+Formula, +Atoms)
%    write the truth table title: Formula and Atoms
%
write_tt_title(Formula, Atoms) :-
	writef('%w  ', [Formula]),
	write_tt_title1(Atoms).

%
%  write_tt_title(+Formula, +Atoms)
%
write_tt_title1([Atom| Atoms]) :-
	writef('%w  ', [Atom]),
	write_tt_title1(Atoms).
write_tt_title1([]) :-
	writeln('value ').

%
%  write_tt_line(+Length, +Valuation, +TruthValue)
%    Length us length of formula, and is used for indenting
%
write_tt_line(Length, Valuation, TruthValue) :-
	tab(Length),
	write('  '),
	write_valuation(Valuation),
	writef('  %w\n', [TruthValue]).

%
%  write_valuation(+TruthValues)
%
write_valuation([]).        
write_valuation([(_,TruthValue)| TruthValues]) :-
  writef('%w  ', [TruthValue]),
  write_valuation(TruthValues).