:- 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([(EForms, EForm)| ET], [(IForms, IForm)| IT]) :-
	from_external_to_internal(EForm, IForm),
	maplist(from_external_to_internal, EForms, IForms),
	change_representation(ET, IT).
change_representation([],[]).

t1 :- test([([], (p -> (p -> p) -> p) -> ((p -> p -> p) -> (p -> p))),
	    ([], p -> (p -> p) -> p),
            ([], (p -> p -> p) -> p -> p),
            ([], p -> p -> p),
            ([], p->p)]).

t2 :- test([([p -> q, q -> r, p], p),
	  ([p -> q, q -> r, p], p -> q),
	  ([p -> q, q -> r, p], q),
	  ([p -> q, q -> r, p], q -> r),
	  ([p -> q, q -> r, p], r),
	  ([p -> q, q -> r], p -> r),
	  ([p -> q], (q -> r) -> p -> r),
	  ([], (p -> q) -> ((q -> r) -> p -> r))]).

t3 :- test([([~p, p], ~p -> ~q -> ~p),
	  ([~p, p], ~p),
	  ([~p, p], ~q -> ~p),
	  ([~p, p], (~q -> ~p) -> p -> q),
	  ([~p, p], p -> q),
	  ([~p, p], p),
	  ([~p, p], q),
	  ([~p], p -> q),
	  ([], ~p -> p -> q)]).