%
%  Module translations
%    translates external and internal representation of operators
%    as well as the various representations of formulas:
%    internal (term), external (term), and printable (atom)
%
:- module(translations, [operator_translation/2,
			from_internal_to_external/2,
			from_external_to_internal/2,
			from_internal_to_printable/2,
			from_external_to_printable/2]).

:- ensure_loaded(external_operators).
:- ensure_loaded(internal_operators).

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

%
%  from_internal_to_external(+InternalFormula, -ExternalFormula)
%
from_internal_to_external(InternalFormula, ExternalFormula) :-
	operators_for_external_representation,
	to_external(InternalFormula, ExternalFormula),
	back_to_standard_representation_of_operators.

%
%  to_external(+InternalFormula, -ExternalFormula)
%
to_external(InternalFormula, ExternalFormula) :-
	InternalFormula =.. [InternalOperator, IntForm1, IntForm2],
	operator_translation(ExternalOperator, InternalOperator), !,
	to_external(IntForm1, ExtForm1),
	to_external(IntForm2, ExtForm2),
	ExternalFormula =.. [ExternalOperator, ExtForm1, ExtForm2].
to_external(InternalFormula, ExternalFormula) :-
	InternalFormula =.. [InternalOperator, IntForm],
	operator_translation(ExternalOperator, InternalOperator), !,
	to_external(IntForm, ExtForm),
	ExternalFormula =.. [ExternalOperator, ExtForm].
to_external(Formula, Formula).

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

%
%  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).

%
%  from_internal_to_printable(+InternalFormula, -PrintableFormula)
%    Converts formula in internal representation InternalFormula
%    to atom PrintableFormula, with correct spacing between symbols
%    and minimal number of parentheses
%
from_internal_to_printable(InternalFormula, PrintableFormula) :-
	operators_for_external_representation,
	from_internal_to_external(InternalFormula, ExternalFormula),
	from_external_to_printable(ExternalFormula, PrintableFormula),
	back_to_standard_representation_of_operators.

%
%  from_externall_to_printable(+ExternalFormula, -PrintableFormula)
%    Converts formula in external representation ExternalFormula
%    to atom PrintableFormula, with correct spacing between symbols
%    and minimal number of parentheses
%
from_external_to_printable(ExternalFormula, PrintableFormula) :-
	operators_for_external_representation,
	term_to_atom(ExternalFormula, Atom),
	back_to_standard_representation_of_operators,
        atom_codes(Atom, Codes),
	remove_spaces(Codes, Codes1),
	add_spaces(Codes1, Codes2),
	atom_codes(PrintableFormula, Codes2).

%
%  remove_spaces(+ListWithSpaces, -ListWithoutSpaces)
%    ListWithoutSpaces is ListWithSpaces with all spaces removed
%
remove_spaces([32| T], T1) :- !,     % 32 is the ASCII code for space
	remove_spaces(T, T1).
remove_spaces([H| T], [H| T1]) :- !,
	remove_spaces(T, T1).
remove_spaces([], []).

%
%  add_spaces(+ListWithoutSpaces, -ListWithSpaces)
%    ListWithSpaces is ListWithoutSpaces with spaces put
%    between binary operators
%
add_spaces([43| T], [32,43,32| T1]) :- !,              % space around +
	add_spaces(T, T1).
add_spaces([60,45,62| T], [32,60,45,62,32| T1]) :- !,  % space around <->
	add_spaces(T, T1).
add_spaces([45,62| T], [32,45,62,32| T1]) :- !,        % space around ->
	add_spaces(T, T1).
add_spaces([118| T], [32,118,32| T1]) :- !,            % space around v
	add_spaces(T, T1).
add_spaces([94| T], [32,94,32| T1]) :- !,              % space around ^
	add_spaces(T, T1).
add_spaces([H| T], [H| T1]) :-
	add_spaces(T, T1).
add_spaces([], []).