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

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

example(Clauses) :-
	writeln('================================================================================'),
	maplist(portray_clause,Clauses),
	writeln('--------------------------------------------------------------------------------'),
	genConstraints(Clauses),
	write_types,
	writeln('================================================================================'),
	nl, nl.

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
	, 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))
	]).	

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

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

genClauseConstraints(Cl) :-
	Cl = (H :- B),
	genHeadAtomConstraints(H),
	genBodyConstraints(B).

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

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

genAtomConstraints(X = Y) :- !,
	unify(X,Y).
genAtomConstraints(X) :-
 	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).


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

:- constraints
	signature/1,
	normal_subseteq/2,
	depends_on/2,
	call_instance/1,
	subtype/3.

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).

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

depends_on_copy @
depends_on(X,Y) \ depends_on(X,Y) <=> true.


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

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) <=>
	A = B.

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

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

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

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

axiom_5_3 @
depends_on(X,Y), subtype(A,X,ID), subtype(A,Y,ID),
	normal_subseteq(X,_)
	==> X \== Y |
	X = Y.


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

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

constraints 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,
	write_type_declarations/0,
	write_type_declaration/1,
	write_signatures/0.

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.

assemble_full_names, alpha_type(T), type_name(T,N) ==>
	fullname(T,N).
assemble_full_names, regular_type(T) ==>
	assemble_full_name(T).

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

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).
regular_type(T), type_name(T,Name) \ assemble_full_name(T) 
	<=>
		fullname(T,Name).
regular_type(T), subtype(T,OT,ID), type_name(OT,Name), alphas_top_type(OT,Alphas)  \ assemble_full_name(T) 
	<=>
		instance_names(Alphas,ID,InstanceNames),
		FName =.. [Name|InstanceNames],
		fullname(T,FName).
regular_type(T), subtype(T,OT,_ID) \ 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 = [].

subtype(T,OT,ID) \ instance_names([OT|OTs],ID,List) <=> List = [N|Ns], fullname(T,N), instance_names(OTs,ID,Ns).
instance_names([],_,List) <=> List = [].

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) ==>
	write(N),
	write(' ---> '),
	write_functors(Fs),
	nl.

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

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

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

write_type_declarations <=> nl, write_signatures.

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

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