inferJud1(empty,diamante).
inferJud1(add(type(X,k(Y)),G),diamante):- 
	\+ inDomG(X,G),kappa(Y).

inferJud2(G,k(X)):-
	inferJud1(G,diamante),kappa(X).
inferJud2(G,freccia(A,B)):-
	inferJud2(G,A),inferJud2(G,B).

infer(G,type(X,A)):-
	inG(type(X,A),G).
infer(G,type(abs(X,A,M),freccia(A,B))):-
	infer(add(type(X,A),G),type(M,B)).
infer(G,type(app(M,N),B)):-
	infer(G,type(M,freccia(A,B))), 
	infer(G,type(N,A)).

/* ambiente gamma*/
inDomG(X,add(type(X,_),_)).
inDomG(_,empty):-false.
inDomG(X,add(type(_,_),Z)):-
	inDomG(X,Z).

inG(type(X,A),add(type(X,A),_)).
inG(type(X,A),add(type(_,_),Z)):-
	inG(type(X,A),Z).
	
/* tipi base: insieme kappa */
kappa(int).
kappa(char).

/* un goal: abs(x,k(int),abs(y,k(char),x)) ha tipo? */
/* infer(empty,type(abs(x,k(int),x),X)) */
/* infer(G,type(x,int)) */	
/* 
una sessione:

| ?- infer(empty,type(abs(x,freccia(A,B),abs(y,k(char),app(x,y))),T)).

A = k(char)
T = freccia(freccia(k(char),B),freccia(k(char),B)) ? ;

no
*/

