Type Checker per CoreML in Prolog -- Con typing del Let like ML

/*
Type checker per coreML.
*/


% Regole per l'ambiente.

typenv(X, [ass(X,Y)|_], Y).
typenv(X, [_|Env],Y) :- typenv(X,Env,Y).


% REGOLE PER IL TIPO DELLE VARIE ESPRESSIONI.

% Constanti e operatori.

type(int(_),_,integer).
type(bool(_),_,boolean).
type(bfun(+),_,arr(integer,(arr(integer, integer)))).
type(bfun(-),_,arr(integer,(arr(integer, integer)))).
type(bfun(*),_,arr(integer,(arr(integer, integer)))).
type(bfun(/),_,arr(integer,(arr(integer, integer)))).
type(bfun(=),_,arr(integer,(arr(integer, boolean)))).
type(bfun(>),_,arr(integer,(arr(integer, boolean)))).
type(bfun(<),_,arr(integer,(arr(integer, boolean)))).


%Variabili.
type(var(V),Env,T) :- typenv(V,Env,T).


%Funzione.
type(fun(X,M),Env, arr(T1,T2)) :- type(M,[ass(X,T1)|Env],T2).


%Applicazione, senza occur_check.
%type(app(M1,M2),Env,T) :- type(M1,Env,arr(U,T)), type(M2,Env,U).


%Applicazione, con occur_check.
type(app(M1,M2),Env,T) :- type(M1,Env,arr(U1,T)), type(M2,Env,U2),unify_with_occurs_check(U1,U2).


%Condizionale.
type(cond(M1,M2,M3),Env,T) :- type(M1,Env, boolean), type(M2,Env,T), type(M3,Env,T).


%let normale.
%type(let(X,M1,M2),Env,T2) :- type(M1,Env,T), type(M2,[ass(X,T)|Env],T2).

%let like ML.
type(let(X,M1,M2),Env,T1) :- sub(X,M1,M2,M3), type(M3,Env,T1).



%SOSTITUZIONE

%Per le variabili.
sub(X,_,var(Y),var(Y)) :- X\==Y,!.
sub(X,NEW,var(X),NEW).

%Per le funzioni.
sub(X,NEW,fun(Y,C),fun(Y,C1)) :- X\==Y,! , sub(X,NEW,C,C1).
sub(X,_,fun(X,C),fun(X,C)).


%Per il Let.
sub(X,NEW,let(Y,M1,M2),let(Y,M1S,M2S)) :- X\==Y, !, sub(X,NEW,M1,M1S), sub(X,NEW,M2,M2S).
sub(X,NEW,let(X,M1,M2),let(X,M1S,M2)) :- sub(X,NEW,M1,M1S).

%Per l'applicazione.
sub(X,NEW,app(M1,M2),app(M1S,M2S)) :- sub(X,NEW,M1,M1S), sub(X,NEW,M2,M2S).

%Per il Condizionale.
sub(X,NEW,cond(M1,M2,M3),cond(M1S,M2S,M3S)) :- sub(X,NEW,M1,M1S), sub(X,NEW,M2,M2S), sub(X,NEW,M3,M3S).

%Per il bfun.
sub(_,_,bfun(Y),bfun(Y)).

%Per gli interi.
sub(_,_,int(Y), int(Y)).

%Per i booleani.
sub(_,_, bool(Y), bool(Y)).