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

%
%  proof(+Deductions)
%
proof(Deductions) :- proof(Deductions, 1, []).

%
%  proof(+Deductions, +Line, +CheckedDeductions)
%    Deductions and CheckDeductions are lists of pairs of the form
%    (Assumptions, Formula);
%    Line is equal to the length of CheckedDeductions + 1,
%    and the first member of Deductions is meant to generate
%    the Line'th line of the proof to be checked 
proof([], _, _).
proof([Deduction| Deductions], Line, CheckedDeductions) :-
	justify(Deduction, Line, CheckedDeductions), !,
	NextLine is Line + 1,
	proof(Deductions, NextLine, [Deduction| CheckedDeductions]).
proof([Deduction| _], Line, _) :-
	write_proof_line(Line, Deduction, ['cannot be justified']).


%
%  justify(+Deduction, +Line, +CheckedDeductions)
%    If successful, Deduction will become Line's line of the proof;
%    it will be justified as an axiom, or as an assumption,
%    or on the basis of the deduction rule, or on the basis of modus ponens
%
justify(Deduction, Line, _) :-
	Deduction = (_, Formula),
	axiom(Formula, N),
	write_proof_line(Line, Deduction,  ['Axiom ', N]).
justify(Deduction, Line, _) :-
	Deduction = (Assumptions, Formula),
	member(Formula, Assumptions),
	write_proof_line(Line, Deduction, ['Assumption']).
justify(Deduction, Line, CheckedDeductions) :-
	Deduction = (Assumptions, A imp B),
	nth1(L, CheckedDeductions, (AssumptionsSupportingB, B)),
	select(A, AssumptionsSupportingB, Assumptions),
	LineOfBInProof is Line - L,
	write_proof_line(Line, Deduction, ['Deduction ', LineOfBInProof]).
justify(Deduction, Line, CheckedDeductions) :-
	Deduction = (_, B),
	nth1(L1, CheckedDeductions, (_, A imp B)),
	nth1(L2, CheckedDeductions, (_, A)),
	LineOfAImpliesBInProof is Line - L1,
	LineOfAInProof is Line - L2,
	write_proof_line(Line, Deduction,
		    ['Modus Ponens ', LineOfAImpliesBInProof, ',', LineOfAInProof]).

%
%  axiom(+Formula, -N)
%    Formula is by convention defined as the N'th axiom
%
axiom(A imp _ imp A, 1).
axiom((A imp B imp C) imp ((A imp B) imp A imp C), 2).
axiom((neg B imp neg A) imp A imp B, 3).

%
%  write_proof_line(+Line, +Deduction, +Reason)
%    Deduction is the Line'th line of the proof for Justification
%
write_proof_line(Line, Deduction, Justification) :-
	writef('%3r. ', [Line]),
	Deduction = (Assumptions, Formula),
	print_assumptions(Assumptions),
	write('|- '),
	from_internal_to_printable(Formula, PrintableFormula),
	write(PrintableFormula),
	line_position(user_output, Position),
	Spaces = 60 - Position,
	tab(Spaces),
	checklist(write, Justification),
	nl.

%
%  print_assumptions(+Assumptions)
%
print_assumptions([]) :- !.
print_assumptions(Assumptions) :-
	maplist(from_internal_to_printable, Assumptions,Printable),
	write_formula_list(Printable),
	write(' ').