#!/usr/bin/pl -q -t main -f

:- use_module('script_support').
:- use_module('../contrib/pl/swilib/pretty').

main :-
        main(before(_), linearize_proof(_), true).
		
proof_id(node(Id, _, _, _, _), Id) :- !.
proof_id(split(Id, _, _, _), Id) :- !.
proof_id(branch(Id, _, _), Id) :- !.
proof_id(ref(Id), Id) :- %nl,nl,write(Id),nl,nl,
	!.
proof_id(P, _) :-
	( nonvar(P) -> functor(P, F, N) ; true ),
	err('Bad proof term with functor: ~q/~q.', [F,N]).		
	
linearize_proof(szs_satisfiable) :-
	!,
	nl,
	write('SZS status Satisfiable'),
	nl,nl.
	
linearize_proof(szs_refutation_start) :-
	!,
	nl,
	write('SZS status Unsatisfiable'),
	nl,nl,
	write('SZS output start CNFRefutation'),
	nl,nl.
	
linearize_proof(szs_refutation_stop) :-
	!,
	nl,nl,
	write('SZS output stop CNFRefutation'),
	nl.

linearize_proof(szs_unfinished) :-
	!,
	nl,
	write('SZS status GaveUp'),
	nl.
	
linearize_proof(C) :- 
	extract_proof_terms([C]),	
	linearize_proof_terms([], ProofSteps),
	reverse(ProofSteps, ReversedProofSteps),	
	print_steps(ReversedProofSteps).

inference_input_write([]) :- !.
inference_input_write(L) :-
	write('('),
	write(L),
	write(')').
	

print_steps([]) :- !.
print_steps([(_, _, composed, _)|Rest]) :-
	!,
	print_steps(Rest).
print_steps([(Id, Clause, hyper(Clause), SubIds)|Rest]) :-
	!,
	write(Id),
	write(': (---)\t<- '),
	translate(hyper(a), TranslatedType),
	write(TranslatedType),
	inference_input_write(SubIds),
	nl,
	print_steps(Rest).
print_steps([(Id, Clause, Type, SubIds)|Rest]) :-
	write(Id),
	write(': ('),
	pp_clause_line(Clause),
	write(')\t<- '),
	translate(Type, TranslatedType),
	write(TranslatedType),
	inference_input_write(SubIds),
	nl,
	print_steps(Rest).
	
translate(hyper(_), 'hyperresolution/split'):-!.
translate(ref(_), 'reflexivity'):-!.
translate('sup-left'(_, _), 'superposition-left'):-!.
translate('unit-sup-right'(_, _), 'unit-superposition-right'):-!.
translate(input_clause, 'input([])'):-!.
translate(input_fact, 'input([])'):-!.
translate(X, X).	
	
proof_ids([],[]) :- !.
proof_ids([Proof|Rest], [ProofId|RestIds]) :-
		!,
		proof_id(Proof, ProofId),
		proof_ids(Rest, RestIds).
proof_ids(Proof,[ProofId]) :- 
	!,
	proof_id(Proof, ProofId).
	
extract_proof_terms([]) :- !.

extract_proof_terms([node(Id, Clause, Type, Sub1, Sub2)|ToDo]) :- 
	append(Sub1, Sub2, Sub),
	proof_ids(Sub, SubIds),
	append(Sub, ToDo, ToDoNext),	%write(ToDoNext),nl,
	assert(pt(Id, Clause, Type, SubIds)),
	extract_proof_terms(ToDoNext).
	
extract_proof_terms([ref(_Id)|ToDo]) :- %write(Id),nl,write(ToDo),nl,nl,
	extract_proof_terms(ToDo).
	
extract_proof_terms([split(Id, hyper(Clause), Sub1, Sub2)|ToDo]) :- 
	append(Sub1, Sub2, Sub),
	proof_ids(Sub, SubIds),
	append(Sub, ToDo, ToDoNext),
	assert(pt(Id, Clause, hyper(Clause), SubIds)),
	extract_proof_terms(ToDoNext).
	
extract_proof_terms([branch(Id, Clause, Sub)|ToDo]) :-	
	proof_ids(Sub, SubIds),			%write(Sub),
	append([Sub], ToDo, ToDoNext),	%write(ToDo),nl,
	assert(pt(Id, Clause, branch, SubIds)),
	extract_proof_terms(ToDoNext).
	
linearize_proof_terms(LinearizedSoFar, Linearized) :-
	pt(Id, Clause, Type, SubIds),
	all_done(SubIds),
	!,	%write(Id),nl,
	retract(pt(Id, Clause, Type, SubIds)),
	linearize_proof_terms([(Id, Clause, Type, SubIds)|LinearizedSoFar], Linearized).
	
linearize_proof_terms(Linearized, Linearized) :-
	not(pt(_, _, _, _)).
	
all_done([]) :- !.
all_done([Id|T]) :-
	not(pt(Id, _, _, _)),
	all_done(T).
	
	
before(Options) :-
	( extract_option_value('init=', Options, InitFile) ->
	  consult(InitFile)
	; true
	).

extract_option_value(Key, Options, Value) :-
	atom_length(Key, L),
	member(Option, Options),
	sub_atom(Option, 0, L, _, Key),
	!,
	sub_atom(Option, L, _, 0, Value).