A simple type checker written in Prolog.

%esercizio di pdp07 typechecker

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


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

type(var(X), Env, Y) :- typenv(X,Env,Y).
type(fun(V,M),Env,arr(T,W)):- type(M,[ass(V,T)|Env],W).

% senza occur check
%type(app(X,Y), Env, T) :- type(X,Env,arr(U,T)), type(Y,Env,U).

% con occur check: controlla tipaggi ricorsivi
type(app(X,Y), Env, T) :- type(X,Env,arr(U1,T)), type(Y,Env,U2),
      unify_with_occurs_check(U1,U2).


type(cond(I,H,E), Env, T) :- type(I, Env, bool), type(H, Env, T), type(E, Env, T).
type(let(X,Y,Z), Env, T) :- type(Y, Env, U), type(Z,[ass(X,U)|Env],T).