%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Constraint-based Type Inference with Polymorphic Recursion 
% for Prolog
%
% author	Tom Schrijvers
% copyright	K.U.Leuven, 2005-2006
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- use_module(library(chr)).
:- use_module(library(lists)).


%:- chr_option(inplace_updates,on).
%:- chr_option(suspension_reuse,on).
%:- chr_option(reduced_garbage,off).
%:- chr_option(suspension_reuse_profiling,on).

%write2(F) :- write(F).
%nl2 :- nl.
write2(_) :- !.
nl2 :- !.

 apply_rule(_).
%apply_rule(Name) :- writeln(Name).


main :-
	main(100).	% 100 times for more accurate time measurements

main(N) :-
	measure(loop(N), bogusloop(N), Ufib,GBfib,_) ->
        statistics,
	format('~d ~d (~d)',[N,Ufib,GBfib]),nl,
        fail.
	

loop(N) :-
	( N =< 0 ->
		true
	;
		( example, fail ; true),
		M is N - 1,
		loop(M)
	).

bogusloop(N) :-
	( N =< 0 ->
		true
	;
		( true, fail ; true),
		M is N - 1,
		bogusloop(M)
	).




%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Example
example :- program(Prog), example(Prog), fail.
example.


example(Clauses) :-
%	writeln('================================================================================'),
%	maplist(portray_clause,Clauses),
%	writeln('--------------------------------------------------------------------------------'),
	topological_sccs(Clauses,SCCs),
	genConstraints(Clauses,SCCs),
	% chr_show_store(user),
	write_types.
%	writeln('================================================================================'),
%	nl, nl.


program([
		fl([],[],0) :- true
	,	fl([A|B],C,s(D)) :- (append(A,E,C), fl(B,E,D))
	,	append([],F,F) :- true
	,	append([G|H],I,[G|J]) :- append(H,I,J)  
]).


program([
		p([A]) :- true
	,	p([s(s(X)),Y|Xs]) :- (p([X,Y|Xs]), p([s(s(s(s(Y))))|Xs]))
	,	p([0|Bs]) :- p(Bs)
	]).


program([
		flat([],[]) :- true
	,	flat([[]|T],R) :- flat(T,R)
	,	flat([[A|B]|C],[A|D]) :- flat([B|C],D)
	]).

program([ append(nil,L2,L3) :- L2 = L3
	, append(cons(X,Xs),Ys,cons(X,Zs)) :- append(Xs,Ys,Zs)
	]).	
program([ append(nil,L2,L3) :- L2 = L3
	]).	
program([ append(cons(X,Xs),Ys,cons(X,Zs)) :- append(Xs,Ys,Zs)
	]).	
program([ p(a,a,a) :- true
 	, query(X) :- p(X,X,X)
 	]).
program([ append(nil,L2,L3) :- L2 = L3
	, append(cons(X,Xs),Ys,cons(X,Zs)) :- append(Xs,Ys,Zs)
	, reverse(nil,nil) :- true
	, reverse(cons(A,As),Bs) :- (reverse(As,Cs),append(Cs,cons(A,nil),Bs))
	]).	
program([ p(a(b,_),a(_,c)) :- true
	, query(X) :- p(X,X)
	]).
program([ p(a,a) :- true
	, query(X) :- p(X,X)
	]).
program([p(X,Y) :- p(Y,X)]).
program([   
		(a(X) :- b(X)),
                (a(Y) :- c(Y)),
                (c(s) :- true),
                (b(Z) :- a(f(Z))),
                (b(t) :- true)
	]).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Constraint Inference

genConstraints([],_).
genConstraints([Clause|Rest],SCCs) :-
	genClauseConstraints(Clause,SCCs),
	genConstraints(Rest,SCCs).

genClauseConstraints(Cl,SCCs) :-
	Cl = (H :- B),
	genHeadAtomConstraints(H),
	functor(H,F,A),
	once((member(_-List,SCCs), member(F/A,List))),	
	% writeln(F/A-List),
	genBodyConstraints(B,List).

genHeadAtomConstraints(X) :-
	functor(X,F,A),
	functor(Sig,F,A),
	signature(Sig),
	unify(X,Sig).

genBodyConstraints(true,_) :- !.
genBodyConstraints((B1,B2),SCC) :- !,
	genBodyConstraints(B1,SCC),
	genBodyConstraints(B2,SCC).
genBodyConstraints(B,SCC) :-
	genAtomConstraints(B,SCC).

genAtomConstraints(X = Y,_) :- !,
	unify(X,Y).
genAtomConstraints(X,SCC) :-
 	functor(X,F,A),
	functor(Sig,F,A),
	signature(Sig), % ensure that there is a signature
 	functor(Copy,F,A),
%  	call_instance(Copy),
%  	unify(Copy,X).
%	( memberchk(F/A,SCC) ->
%		unify(Sig,X)
%	;
	 	functor(Copy,F,A),
	 	call_instance(Copy),
	 	unify(Copy,X)
%	).
.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Constraint Axioms

:- chr_constraint
	signature/1,
	depends_on/2,
	normal_subseteq/2,
	call_instance/1,
	% lub/3,
	subtype/3,
	termtype/1,
	root/2,
	artificial_type/1.

%option(debug,off).
%option(optimize,full).

unify(X,Y) :- 
	( var(X) -> 
		( var(Y) -> 
			X = Y
		;
			chr_subseteq(X,Y)
		)
	; nonvar(Y) ->
		functor(X,F,A),
		functor(Y,F,A),
		X =.. [_|XArgs],
		Y =.. [_|YArgs],
		unify_list(XArgs,YArgs)	
	;
		unify(Y,X)
	).

unify_list([],[]).
unify_list([X|Xs],[Y|Ys]) :-
	unify(X,Y),
	unify_list(Xs,Ys).

call_constraint_inference @
signature(Signature) \ call_instance(Call) <=>
	functor(Call,F,A),
	functor(Signature,F,A)
	|
	Call      =.. [_|CallArgs],
	Signature =.. [_|SignatureArgs],
	subtypes(CallArgs,SignatureArgs,_ID).

subtypes([],[],_).
subtypes([X|Xs],[Y|Ys],ID) :-
	subtype(X,Y,ID),
	subtypes(Xs,Ys,ID).

chr_subseteq(X,Term) :-
	functor(Term,F,A),
	functor(T,F,A),
	unify(T,Term),
	normal_subseteq(X,T).
%- SET SEMANTICS ---------------------------------------------------------------
depends_on_copy @
depends_on(X,Y) \ depends_on(X,Y) <=> true.

signature_copy @
signature(Sig1) \ signature(Sig2) <=>
	functor(Sig1,F,A),
	functor(Sig2,F,A)
	|
	Sig1 = Sig2.

axiom_5_1 @
normal_subseteq(X,T1) \ normal_subseteq(X,T2) <=>
	functor(T1,F,A),
	functor(T2,F,A)
	|
	T1 = T2.

termtype(X) \ termtype(X) <=> 
	apply_rule(termtype_setsemantics),
	true.

%-------------------------------------------------------------------------------
root(X,_) \ root(X,_) <=> true.

termtype(X) ==>
	% writeln('- introduce new root -----------------------------------------------------------'),
	% chr_show_store(user),
	apply_rule(infer_root),
	root(X,X).

subtype(X,Y,_), root(Y,Z) \ root(X,X) 
	<=>
		X \== Z
	|
		apply_rule(propagate_root),
		% writeln('- upgrading root --------------------------------------------------------'),
		% writeln((subtype(X,Y,_), root(Y,Z) \ root(X,X) <=> root(X,Z))),
		root(X,Z).

root(Y,Z) \ root(X,Y) 
	<=>
		Y \== Z
	|
		apply_rule(update_root),
		% format('- propagate root down ----------------------------------------------------------\n'),
		% writeln((root(Y,Z) \ root(X,Y) <=> root(X,Z))),
		% chr_show_store(user),
		root(X,Z).
axiom_4_6 @
normal_subseteq(X,T) ==>
	T =.. [_|Args],
	depends_on_args(Args,X).

depends_on_args([],_).
depends_on_args([X|Xs],Y) :-
	depends_on(Y,X),
	depends_on_args(Xs,Y).

axiom_4_4 @
subtype(A,X,ID) \ subtype(B,X,ID) <=>
	apply_rule(propate_eq_down),
	A = B.

axiom_4_9 @
depends_on(X,Y), subtype(Y,X,_) <=>
	apply_rule(dependson_subtype_cycle:(depends_on(X,Y), subtype(Y,X,_))),
	X = Y.

axiom_4_7 @
depends_on(X,Y), depends_on(Y,Z) ==> 
	apply_rule(depends_on_transitive),
	depends_on(X,Z).

axiom_4_3 @
normal_subseteq(Y,Term) , subtype(X,Y,ID) ==>
	apply_rule(propate_functor_down),
	functor(Term,F,A),
	functor(Copy,F,A),
	chr_subseteq(X,Copy),
	Copy =.. [_|CopyArgs],
	Term =.. [_|TermArgs],
	subtypes(CopyArgs,TermArgs,ID).

subtype(X,Y,_), subtype(Y,X,_) <=>
	apply_rule(subtype_cycle),
	X = Y.

depends_on(A,A), subtype(A,X,I), subtype(A,Y,J), depends_on(X,Y), normal_subseteq(X,_)
	==> X \== Y |
	X = Y.

% axiom_5_3 @
% depends_on(X,Y), subtype(A,X,ID), subtype(A,Y,ID),
% 	normal_subseteq(X,_)
% 	==> X \== Y |
% 	apply_rule(propagte_eq_up),
% 	X = Y.
% 
% depends_on(A,B), depends_on(B,A), subtype(A,X,I), subtype(B,Y,I),
% 	subtype(A,Y,J), subtype(B,X,J),
% 	normal_subseteq(X,_)
% 	==> X \== Y | apply_rule(propagte_eq_up2),
% 	X = Y.

axiom_5_2 @
termtype(Y), subtype(X,Y,_), normal_subseteq(X,Term) ==>
	apply_rule(propate_functor_up),
	functor(Term,F,A),
	functor(Copy,F,A),
	chr_subseteq(Y,Copy).

normal_subseteq(X,_) 
	==>
		apply_rule(infer_termtype),
		termtype(X).

subtype(S,T1,_), subtype(S,T2,_), artificial_type(R1), root(T1,R1) \ root(T2,R2) 
	<=>
		R1 \== R2 
	|
		apply_rule(multi_subtype),
		root(R2,R1),
		subtype(R2,R1,_).	

subtype(S,T1,_), subtype(S,T2,_) \ root(T1,R1), root(T2,R2) 
	<=>
		R1 \== R2 
	|
		apply_rule(multi_subtype),
		artificial_type(T),
		termtype(T),
		root(R1,T),
		root(R2,T),
		subtype(R1,T,_),
		subtype(R2,T,_).	

normal_subseteq(T1,Term1), normal_subseteq(T2,Term2), root(T1,T1), root(T2,T2), artificial_type(T1)
	==>
		functor(Term1,F,A),
		functor(Term2,F,A)
	|
		apply_rule(unique_functors_a),
		subtype(T2,T1,_).	

% [optional] monomorhpic functor
normal_subseteq(T1,Term1), normal_subseteq(T2,Term2), root(T1,T1), root(T2,T2)
	==>
		functor(Term1,F,A),
		functor(Term2,F,A)
	|
		apply_rule(unique_functors),
		artificial_type(T),
		subtype(T1,T,_),
		subtype(T2,T,_),	
		termtype(T).
		

% subtype(X,A,_), subtype(X,B,_) ==>
% 	lub(C,A,B).
% 
% lub(C,X,X) <=>
% 	C = X.
% 
% lub(C,A,B) \ lub(D,A,B) <=> C = D.
% lub(C,A,B) \ lub(D,B,A) <=> C = D.
% 
% lub(C,A,B) ==>
% 	subtype(A,C,_),
% 	subtype(B,C,_).
% 
% lub(C,A,B), normal_subseteq(A,T1), normal_subseteq(B,T2) ==>
% 	functor(T1,F,N),
% 	functor(T2,F,N)
% 	|
% 	functor(T3,F,N),
% 	T1 =.. [_|Args1],
% 	T2 =.. [_|Args2],
% 	T3 =.. [_|Args3],
% 	normal_subseteq(C,T3),
% 	lub_args(Args1,Args2,Args3).
% 
% lub_args([],[],[]).
% lub_args([X|Xs],[Y|Ys],[Z|Zs]) :-
% 	lub(Z,X,Y),
% 	lub_args(Xs,Ys,Zs).


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Code for printing types

:- nb_setval(typename,1).
:- nb_setval(alphaname,1).

:- chr_constraint write_types/0, functors/0, functors/2, alpha_type/1, regular_type/1, name_top_types, name_top_type/1, type_name/2,
	alphas_top_type/1,
	alphas_top_type/2,
	name_alpha_types/0,
	assemble_full_names/0,
	assemble_full_name/1,
	fullname/2,
	get_fullname/2,
	alpha_names/2,
	instance_names/3,
	instance_names/5,
	write_type_declarations/0,
	write_type_declaration/1,
	write_signatures/0,
	enable_trans_subtype/0,
	trans_subtype/2,
	regular_top/2.

%----------------------------------------------------------------------
write_types ==> enable_trans_subtype.

enable_trans_subtype, subtype(T,PT,_) ==>
	trans_subtype(T,PT).

enable_trans_subtype <=> true.

trans_subtype(X,X) <=> true.
trans_subtype(X,Y) \ trans_subtype(X,Y) <=> true.
trans_subtype(X,Y), trans_subtype(Y,Z) ==> trans_subtype(X,Z).
%----------------------------------------------------------------------


signature(S), write_types ==>
	term_variables(S,Vars),
	init_types(Vars).
normal_subseteq(T,F), write_types ==>
	term_variables(T-F,Vars),
	init_types(Vars).

init_types([]).
init_types([T|Ts]) :-
	alpha_type(T),
	init_types(Ts).

write_types ==> functors.

functors, normal_subseteq(T,F) ==> functors(T,[F]).
functors(T,L1), functors(T,L2) <=> append(L1,L2,L3), functors(T,L3).
functors <=>
	name_top_types.

alpha_type(T) \ alpha_type(T) <=> true.
regular_type(T) \ alpha_type(T) <=> true.
regular_type(T) \ regular_type(T) <=> true.

functors(T,_L) \ alpha_type(T) <=> regular_type(T).

name_top_types, regular_type(T) ==>
	name_top_type(T).

name_top_types <=> name_alpha_types.

subtype(T,OT,_), regular_type(OT) \ name_top_type(T) <=>
	OT \== T | true.
name_top_type(T) ==>
	nb_getval(typename,I),
	J is I + 1,
	nb_setval(typename,J),
	atom_concat(type,I,Name),
	type_name(T,Name).

name_top_type(T) <=> alphas_top_type(T).

alphas_top_type(T1), alpha_type(T2), depends_on(T1,T2) ==>
	alphas_top_type(T1,[T2]).
alphas_top_type(_) <=> true.

alphas_top_type(T,L1), alphas_top_type(T,L2) <=>
	append(L1,L2,L3), alphas_top_type(T,L3).	

name_alpha_types, alpha_type(T) ==> 
	nb_getval(alphaname,I),
	J is I + 1,
	nb_setval(alphaname,J),
	atom_concat('Alpha',I,Name),
	type_name(T,Name).

name_alpha_types <=> assemble_full_names.

% A. alpha type
assemble_full_names, alpha_type(T), type_name(T,N) ==>
	fullname(T,N).

% B. regular type
assemble_full_names, regular_type(T) ==>
	assemble_full_name(T).

fullname(T,N1) \ fullname(T,N2) <=> N1 = N2.


%-------------------------------------------------------------------------------
regular_type(T), trans_subtype(T,PT), regular_type(PT) ==>
	regular_top(T,PT).

regular_top(T,PT) \ regular_top(T,PT) <=> true.
regular_top(T,PT1), trans_subtype(PT2,PT1) \ regular_top(T,PT2) <=> true.
%-------------------------------------------------------------------------------

% B.1 type itself is a top type
%	a) has type parameters
regular_type(T), type_name(T,Name), alphas_top_type(T,Alphas) \ assemble_full_name(T) 
	<=>
		alpha_names(Alphas,AlphaNames),
		FName =.. [Name|AlphaNames],
		fullname(T,FName).
%	b) has no type parameters
regular_type(T), type_name(T,Name) \ assemble_full_name(T) 
	<=>
		fullname(T,Name).

% B.2 type is not a top type
%	a) has a regular top type parent
%		i) that has type parameters
regular_type(T), regular_top(T,PT), type_name(PT,Name), alphas_top_type(PT,Alphas)  \ assemble_full_name(T) 
	<=>
		length(Alphas,Length),
		length(InstanceNames,Length),
		instance_names(Alphas,T,InstanceNames),
		FName =.. [Name|InstanceNames],
		fullname(T,FName).
	% regular_type(T), subtype(T,OT,ID), alpha_type(OT), type_name(OT,Name), alphas_top_type(OT,Alphas)  \ assemble_full_name(T) 
	% 	<=>
	% 		instance_names(Alphas,ID,InstanceNames),
	% 		FName =.. [Name|InstanceNames],
	% 		fullname(T,FName).

%		ii) that has no type parameters
regular_type(T), regular_top(T,PT), type_name(PT,Name) \ assemble_full_name(T) 
	<=>
		% get_fullname(PT,Name),
		fullname(T,Name).
	% regular_type(T), subtype(T,OT,_ID), alpha_type(OT) \ assemble_full_name(T) 
	% 	<=>
	% 		get_fullname(OT,Name),
	% 		fullname(T,Name).

fullname(T,N) \ alpha_names([T|Ts],List) <=> List = [N|R], alpha_names(Ts,R).
alpha_names([],List) <=> List = [].

% TODO: fix such that nested dependencies (e.g list(list(T))) are properly dealt with
depends_on(BT,T), trans_subtype(T,OT) \ instance_names([OT|OTs],BT,List) <=>  BT \== T | instance_names(T,OT,OTs,BT,List).
instance_names([],_,List) <=> List = [].

depends_on(BT,T2), depends_on(T2,T1), trans_subtype(T2,OT) \ instance_names(T1,OT,OTs,BT,List) <=> T2 \== T1, T2 \== BT | instance_names(T2,OT,OTs,BT,List).
instance_names(T,OT,OTs,BT,List) <=> List = [N|Ns], fullname(T,N), instance_names(OTs,BT,Ns).

assemble_full_names <=> write_type_declarations.

fullname(T,Name) \ get_fullname(T,N) <=> N = Name.

write_type_declarations, regular_type(T) ==> write_type_declaration(T).

subtype(T,OT,_), regular_type(OT) \ write_type_declaration(T) <=> OT \== T | true.

write_type_declaration(T), functors(T,Fs), fullname(T,N) ==>
	write2(N),
	write2(' ---> '),
	write_functors(Fs),
	nl2.

write_functors([F|Fs]) :-
	write_functor(F),
	write_functors_(Fs).

write_functors_([F|Fs]) :-
	write2(' ; '),
	write_functor(F),
	write_functors_(Fs).
write_functors_([]) :- write2('.').

write_functor(Term) :-
	Term =.. [F|Args],
	get_fullnames(Args,Names),
	Copy =.. [F|Names], 
	write2(Copy).

write_type_declarations <=> nl2, write_signatures.

write_signatures, signature(Sig) ==>
	Sig =.. [F|Args],
	get_fullnames(Args,Names),
	SigTerm =.. [F|Names],
	write2(':- pred '),
	write2(SigTerm),
	write2('.'),nl2.	
	
write_signatures <=> true.

get_fullnames([],[]).
get_fullnames([T|Ts],[N|Ns]) :-
	get_fullname(T,N),
	get_fullnames(Ts,Ns).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
suite :-
	test_file(File),	
	write('==================='),nl,
	write(File),nl,
	write('==================='),nl,
	readprog(File,_,Clauses),
	time(example(Clauses)),
	fail.
suite.

process(File) :-
	readprog(File,_,Clauses),
	time(example(Clauses)).

test_file('Tests/append.pl').
test_file('Tests/frev.pl').
test_file('Tests/pq.pl').
test_file('Tests/rev.pl').
test_file('Tests/trans.pl').
test_file('Tests/qsort.pl').
test_file('Tests/combinednorm.pl').
test_file('Tests/dnf.pl').

readprog(F, Preds,Clauses) :-
	open(F,read,Stream),
	readprog1(Stream, UPreds, Clauses),
	sort(UPreds,Preds),
	close(Stream).
readprog1(Stream,UPreds,Clauses) :-
	read_clause(Stream,Clause),
	( Clause == end_of_file ->
		UPreds = [],
		Clauses = []
	; 
		( Clause = (H :- B) ->
			true
	 	;
			H = Clause,
			B = true
		),
		functor(H,F,A),
		UPreds = [F/A|UPredsT],
		Clauses = [(H:-B)|ClausesT],
		readprog1(Stream,UPredsT,ClausesT)
	).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
topological_sccs(Clauses,SCCs) :-
	dependency_graph(Clauses),
	get_sccs(USCCs),
	clear_scc,
	sort(USCCs,SCCs).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Compute SCC

:- chr_constraint
	scc_predicate(+,?),
	scc_predicates(?,+),
	calls(+,+),
	calls_closure(+,+),
	scc_lt(?,?),
	scc_number(?,+int),
	number_sccs,
	get_sccs(?),
	clear_scc
	.

clear_scc \ scc_predicate(_,_) <=> true.
clear_scc \ scc_predicates(_,_) <=> true.
clear_scc \ calls(_,_) <=> true.
clear_scc \ calls_closure(_,_) <=> true.
clear_scc \ scc_lt(_,_) <=> true.
clear_scc \ scc_number(_,_) <=> true.

clear_scc <=> true.

calls(P,Q) \ calls(P,Q) <=> true.

calls(P,Q) ==> calls_closure(P,Q).

calls_closure(P,P) <=> true.
calls_closure(P,Q) \ calls_closure(P,Q) <=> true.
calls_closure(P,Q), calls_closure(Q,R) ==> calls_closure(P,R).

scc_predicate(P,SCC1) \ scc_predicate(P,SCC2) <=> SCC1 = SCC2.

scc_predicate(P,SCCP), scc_predicate(Q,SCCQ),
	calls_closure(P,Q), calls_closure(Q,P)
	==>
		SCCP = SCCQ.

scc_predicate(P,SCCP), scc_predicate(Q,SCCQ), calls(P,Q)
	==>
		scc_lt(SCCQ,SCCP).

scc_lt(SCC,SCC) <=> true.
scc_lt(SCC1,SCC2) \ scc_lt(SCC1,SCC2) <=> true.

number_sccs, scc_predicate(P,SCC) ==>
	scc_number(SCC,1).
number_sccs <=> true.

scc_number(SCC,N) \ scc_number(SCC,M) <=> N >= M | true.
scc_number(SCC1,N), scc_lt(SCC1,SCC2) ==>
	M is N + 1, scc_number(SCC2,M).

scc_predicate(P,SCC) ==> scc_predicates(SCC,[P]).
scc_predicates(SCC,P1), scc_predicates(SCC,P2)
	<=> append(P1,P2,P), scc_predicates(SCC,P).

get_sccs(List), scc_number(SCC,N), scc_predicates(SCC,P)
	<=>
		List = [N-P|Tail],
		get_sccs(Tail).
get_sccs(List) <=> List = [].

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

dependency_graph_from_file(File) :-
	readfile(File,Clauses),
	dependency_graph(Clauses).

dependency_graph(Clauses) :-
	findall(C, ( member(C,Clauses), C \= (:- _) , C \= (?- _)), Cs),
	track_dependencies(Cs),
	number_sccs.

track_dependencies([]).
track_dependencies([C|Cs]) :-
	hb(C,H,B),
	extract_predicates(B,Ps,[]),
	functor(H,F,A),
	scc_predicate(F/A,_SCC),
	calls_predicates(Ps,F/A),
	track_dependencies(Cs).

calls_predicates([],FA).
calls_predicates([P|Ps],FA) :-
	calls(FA,P),
	calls_predicates(Ps,FA).

hb(C,H,B) :-
	( C = (H :- B) ->
		true
	;
		C = H,
		B = true
	).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
extract_predicates(!,L,L) :- ! .
extract_predicates(_ < _,L,L) :- ! .
extract_predicates(_ = _,L,L) :- ! .
extract_predicates(_ =.. _ ,L,L) :- ! .
extract_predicates(_ =:= _,L,L) :- ! .
extract_predicates(_ == _,L,L) :- ! .
extract_predicates(_ > _,L,L) :- ! .
extract_predicates(_ \= _,L,L) :- ! .
extract_predicates(_ \== _,L,L) :- ! .
extract_predicates(_ is _,L,L) :- ! .
extract_predicates(arg(_,_,_),L,L) :- ! .
extract_predicates(atom_concat(_,_,_),L,L) :- ! .
extract_predicates(atomic(_),L,L) :- ! .
extract_predicates(b_getval(_,_),L,L) :- ! .
extract_predicates(call(_),L,L) :- ! .
extract_predicates(compound(_),L,L) :- ! .
extract_predicates(copy_term(_,_),L,L) :- ! .
extract_predicates(del_attr(_,_),L,L) :- ! .
extract_predicates(fail,L,L) :- ! .
extract_predicates(functor(_,_,_),L,L) :- ! .
extract_predicates(get_attr(_,_,_),L,L) :- ! .
extract_predicates(length(_,_),L,L) :- ! .
extract_predicates(nb_setval(_,_),L,L) :- ! .
extract_predicates(nl,L,L) :- ! .
extract_predicates(nonvar(_),L,L) :- ! .
extract_predicates(once(G),L,T) :- !,
	( nonvar(G) ->
		extract_predicates(G,L,T)
	;
		L = T
	).
extract_predicates(op(_,_,_),L,L) :- ! .
extract_predicates(prolog_flag(_,_),L,L) :- ! .
extract_predicates(prolog_flag(_,_,_),L,L) :- ! .
extract_predicates(put_attr(_,_,_),L,L) :- ! .
extract_predicates(read(_),L,L) :- ! .
extract_predicates(see(_),L,L) :- ! .
extract_predicates(seen,L,L) :- ! .
extract_predicates(setarg(_,_,_),L,L) :- ! .
extract_predicates(tell(_),L,L) :- ! .
extract_predicates(term_variables(_,_),L,L) :- ! .
extract_predicates(told,L,L) :- ! .
extract_predicates(true,L,L) :- ! .
extract_predicates(var(_),L,L) :- ! .
extract_predicates(write(_),L,L) :- ! .
extract_predicates((G1,G2),L,T) :- ! ,
	extract_predicates(G1,L,T1),
	extract_predicates(G2,T1,T).
extract_predicates((G1->G2),L,T) :- !,
	extract_predicates(G1,L,T1),
	extract_predicates(G2,T1,T).
extract_predicates((G1;G2),L,T) :- !,
	extract_predicates(G1,L,T1),
	extract_predicates(G2,T1,T).
extract_predicates(\+ G, L, T) :- !,
	extract_predicates(G, L, T).
extract_predicates(findall(_,G,_),L,T) :- !,
	extract_predicates(G,L,T).
extract_predicates(bagof(_,G,_),L,T) :- !,
	extract_predicates(G,L,T).
extract_predicates(_^G,L,T) :- !,
	extract_predicates(G,L,T).
extract_predicates(_:Call,L,T) :- !,
	extract_predicates(Call,L,T).
extract_predicates(Call,L,T) :-
	( var(Call) ->
		L = T
	;
		functor(Call,F,A),
		L = [F/A|T]
	).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%
%% File Reading

readfile(File,Declarations) :-
	see(File),
	readcontent(Declarations),
	seen.

readcontent(C) :-
	read(X),
	( X = (:- op(Prec,Fix,Op)) ->
		op(Prec,Fix,Op)
	;
		true
	),
	( X == end_of_file ->
		C = []
	;
		C = [X | Xs],
		readcontent(Xs)
	).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

measure(G,_,Time,GTime,swi) :-
	cputime(X),	gctime(Y),
	call(G),
	cputime(Now),	gctime(NowG),
	GTime is NowG-Y,
	Time is Now-X-GTime.
cputime(Time) :- statistics(runtime, [Time,_]).
gctime(Time) :- statistics(garbage_collection, [_,_,Time]).