%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Constraint-based Type Inference with Polymorphic Recursion 
% for \Lambda^{+}, % the \lambda-calculus extended with recursive definitions.
%
% author	Tom Schrijvers
% copyright	K.U.Leuven, 2005-2006
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
:- use_module(library(lists)).

:- use_module(library(chr)).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Example

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

example(Defs) :-
	writeln('================================================================================'),
	writeln(Defs),
	writeln('--------------------------------------------------------------------------------'),
	( type(Defs,abs(X,var(X)),_) ->
		write_types,
		write_defs
	;
		writeln('No well-typing!')
	),
	writeln('================================================================================'),
	nl,nl.

program([ f = abs(_X,name(f)) ]).
program([ i = abs(X,var(X))
        , k = abs(A,abs(_B,var(A)))
	, g = abs(V,app(app(name(k),app(name(g),name(i))),app(name(g),name(k))))
        ]).
	

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

type(Definitions,Expression,Type) :-
	type_defs(Definitions),
	type_expr(Expression,Type).

type_defs([]).
type_defs([N = E|Defs]) :-
	type_name(N,T),
	annotate(def(N),T,_),
	type_expr(E,Type),
	T = Type,
	type_defs(Defs).

type_expr(var(V),V) :- annotate(var(V),V,_).
type_expr(name(N),T) :-
	type_name(N,_),
	instance(T,N),
	annotate(name(N),T,_).
type_expr(abs(V,E),AT) :-
	type_expr(var(V),VT),
	type_expr(E,T),
	arrow_type(AT,VT,T),
	annotate(abs(V,E),AT,_).
type_expr(app(E1,E2),T3) :-
	type_expr(E1,T1),
	type_expr(E2,T2),
	arrow_type(T1,T2,T3),
	annotate(app(E1,E2),T3,_).

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

constraints
	type_name/2,
	arrow_type/3,
	instance/2,
	depends_on/2,
	subtype/3,
	annotate/3.

name @
type_name(N,Type) \ instance(CallType,N) <=>
	subtype(CallType,Type,_ID).

unique_name_type @
type_name(N,T1) \ type_name(N,T2) <=>
	T1 = T2.

axiom_4_1 @
arrow_type(T1,T2,T3) \ arrow_type(T4,T2,T3) <=>
	T1 = T4.

axiom_4_2 @
arrow_type(T1,T2,T3) \ arrow_type(T1,T4,T5) <=>
	T2 = T4, T3 = T5.

axiom_4_8 @
depends_on(X,X), arrow_type(X,_,_) <=> fail.

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

axiom_4_6 @
arrow_type(T1,T2,T3) ==>
	depends_on(T1,T2),
	depends_on(T1,T3).

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 @
arrow_type(Y,T1,T2) , subtype(X,Y,ID) ==>
	arrow_type(X,T3,T4),
	subtype(T3,T1,ID), subtype(T4,T2,ID).
 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Code for printing the types

annotate(E,T,N1) \ annotate(E,T,N2) <=>
	N1 = N2.

constraints 
	write_types/0,
	write_type/2,
	write_defs/0.

:- nb_setval(alphaname,1).

write_types, annotate(_,T,TN) ==> write_type(T,TN).
write_types <=> true.

arrow_type(T,T1,T1), annotate(_,T1,T1N) \ write_type(T,TN) <=>
	TN = (T1N -> T1N).
arrow_type(T,T1,T2), annotate(_,T1,T1N), annotate(_,T2,T2N) \ write_type(T,TN) <=>
	TN = (T1N -> T2N).

write_type(_,TN) <=> var(TN) | 
	nb_getval(alphaname,I),
	J is I + 1,
	nb_setval(alphaname,J),
	atom_concat('phi',I,Name),
	TN = Name.
write_type(_,_) <=> true.

write_defs, annotate(def(N),_,Name) ==> write(N), write(' : '), writeln(Name).

write_defs <=> true.