:- ensure_loaded('../Evaluations/hilbert_proof.pl').
:- use_module('../Basis/translations.pl').
:- use_module('../Basis/external_operators.pl').

:- operators_for_external_representation.

%
%  test(+ExternalDeductions)
%
test(ExternalDeductions) :-
	change_representation(ExternalDeductions, InternalDeductions),
	proof(InternalDeductions).
%
%  change_representation(+ExternalDeductions, +InternalDeductions)
%
change_representation([],[]).
change_representation([(EForms, EForm)| ET], [(IForms, IForm)| IT]) :-
	from_external_to_internal(EForm, IForm),
	maplist(from_external_to_internal, EForms, IForms),
	change_representation(ET, IT).

t1 :- test([([forall x: (p(x) -> q(x)), forall x: p(x)], forall x: p(x)),
	    ([forall x: (p(x) -> q(x)), forall x: p(x)], forall x: p(x) -> p(a)),
	    ([forall x: (p(x) -> q(x)), forall x: p(x)], p(a)),
	    ([forall x: (p(x) -> q(x)), forall x: p(x)], forall x: (p(x) -> q(x))),
	    ([forall x: (p(x) -> q(x)), forall x: p(x)], forall x: (p(x) -> q(x)) -> p(a) -> q(a)),
	    ([forall x: (p(x) -> q(x)), forall x: p(x)], p(a) -> q(a)),
	    ([forall x: (p(x) -> q(x)), forall x: p(x)], q(a)),
	    ([forall x: (p(x) -> q(x)), forall x: p(x)], forall x: q(x)),
	    ([forall x: (p(x) -> q(x))], forall x: p(x) -> forall x: q(x)),
	    ([], forall x: (p(x) -> q(x)) -> forall x: p(x) -> forall x: q(x))]).

t2 :- test([([], forall x: p(x) -> p(a)),
	    ([], forall y: (forall x: p(x) -> p(y))),
	    ([], forall y: (forall x: p(x) -> p(y)) -> forall x: p(x) -> forall y: p(y)),
	    ([], forall x: p(x) -> forall y: p(y))]).


t3 :- test([([forall x: (p(x) -> q(x)), p(a)], p(a)),
	    ([forall x: (p(x) -> q(x)), p(a)], forall x: (p(x) -> q(x))),
	    ([forall x: (p(x) -> q(x)), p(a)], forall x: (p(x) -> q(x)) -> (p(a) -> q(a))),
	    ([forall x: (p(x) -> q(x)), p(a)], p(a) -> q(a)),
	    ([forall x: (p(x) -> q(x)), p(a)], q(a)),
	    ([forall x: (p(x) -> q(x)), p(a)], forall x: q(x)),
	    ([forall x: (p(x) -> q(x))], p(a) -> forall x: q(x)),
	    ([], forall x: (p(x) -> q(x)) -> p(a) -> forall x: q(x))]).