hm.pl

has_type(G,abs(V,E),arr(T1,T2)) :- has_type([[V,T1]|G],E,T2).
has_type(G,let(I,V,E),T2) :- has_type(G,V,T1), has_type([[I,T1]|G],E,T2).
has_type(G,app(E1,E2),T2) :- has_type(G,E1,arr(T1,T2)), has_type(G,E2,T1).
has_type(G,if(C,V1,V2),T) :- has_type(C,bool), has_type(G,V1,T), has_type(G,V2,T).
has_type(G,I,T) :- atom(I), append(_,[[I,T]|_],G).
has_type([],X,bool) :- X = true ; X = false.
has_type(Tm,Ty) :- has_type([],Tm,Ty).

subst(I,V,I,V).
subst(I,V,app(T1,T2),app(T12,T22)) :- subst(I,V,T1,T12), subst(I,V,T2,T22).
subst(I,V,abs(J,E),abs(J,E2)) :- \+ I = J, subst(I,V,E,E2).
subst(I,Vi,let(J,Vj,E),let(J,Vj2,E2)) :-
    \+ I = J, subst(I,Vi,Vj,Vj2), subst(I,Vi,E,E2).

subst(I,V,if(C,V1,V2),if(C2,V12,V22)) :-
    subst(I,V,C,C2), subst(I,V,V1,V12), subst(I,V,V2,V22).

subst(_,_,E,E).

eval(app(abs(I,E),V),Z2) :- subst(I,V,E,Z1), !, eval(Z1,Z2).
eval(app(T1,T2),Z2) :- eval(T1,T12), !, eval(app(T12,T2),Z2).
eval(let(I,V,E),Z2) :- subst(I,V,E,E2), !, eval(E2,Z2).
eval(if(true,V,_),Z) :- eval(V,Z), !.
eval(if(false,_,V),Z) :- eval(V,Z), !.
eval(if(C,V1,V2),Z) :- eval(C,C2), !, eval(if(C2,V1,V2),Z).
eval(abs(I,E),abs(I,E)).
eval(X,X) :- atom(X), !. %% Symbolic!

check_and_eval(E) :- has_type(E,_), eval(E,X), !, print(X).
check_and_eval(E,X) :- has_type(E,_), eval(E,X), !.