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

Invoke this with:

# parse "+ 3 5";;
type(app(app(bfun(+),num(3)),num(5)), _, T)

type(app(app(bfun(-),num(3)),num(5)), _, T)

type(app(app(bfun(*),num(3)),num(5)), _, T)



# parse " let a=5 in (+a 6)";;
type(let(var(a),num(5),app(app(bfun(+),var(a)),num(6))), _, T)

# parse "if (= 5 3) then 4 else 5";;
type(cond(app(app(bfun(=),num(5)),num(3)),num(4),num(5)), _, T)

# parse "if (> 5 3) then 4 else 5";;
type(cond(app(app(bfun(>),num(5)),num(3)),num(4),num(5)), _, T)

# prova per occur check: (!x. x x)
type(fun(x,app(var(x),var(x))), _, T).