Pure Type Systems type checker in Prolog

They ( http://people.cs.uu.nl/andres/LambdaPi/index.html http://augustss.blogspot.com/2007/10/simpler-easier-in-recent-paper-simply.html ) said it was easy but actually it's very hard, of course these posts are very helpful though. My other reference is the book Lectures on the Curry-Howard Isomorphism (Studies in Logic and Foundations of Mathematics - Vol 149).

Assuming this doesn't have any bugs, does it..?

:- op(1200, xfx, :=).
:- op(150, xfx, ⊢).
:- op(140, xfx, :).
:- op(100, yfx, $).


sort(★).
sort(▢).

axiom(★,▢).

rule(★,★,★). % λ→
rule(★,▢,▢). % λP
rule(▢,★,★). % λ2
rule(▢,▢,▢). % λω


unfold(Term, TermU) :- unfold([],Term,TermU).
unfold(_, Sort, Sort) :- sort(Sort).
unfold(Γ, Ident, Value) :- member(Ident, Γ) -> Ident = Value ; ( Ident := ValueD ), unfold(ValueD, Value).
unfold(Γ, λ(Var:Type,Body), λ(Var:TypeU,BodyU)) :- unfold(Γ, Type, TypeU), unfold([Var|Γ], Body, BodyU).
unfold(Γ, π(Var:Type,Body), π(Var:TypeU,BodyU)) :- unfold(Γ, Type, TypeU), unfold([Var|Γ], Body, BodyU).
unfold(Γ, U $ V, P $ Q) :- unfold(Γ, U, P), unfold(Γ, V, Q).

alpha(X,Y) :- alpha([],X,Y).
alpha(_,Id,Id) :- !.
alpha(Γ,Var1,Var2) :- member(Var1=Var2,Γ).
alpha(Γ,λ(Var1:Type1,Body1), λ(Var2:Type2,Body2)) :- alpha(Γ,Type1,Type2), alpha([Var1=Var2|Γ],Body1,Body2).
alpha(Γ,π(Var1:Type1,Body1), π(Var2:Type2,Body2)) :- alpha(Γ,Type1,Type2), alpha([Var1=Var2|Γ],Body1,Body2).
alpha(Γ,U $ V,P $ Q) :- alpha(Γ,U,P), alpha(Γ,V,Q).

subst(X->Y,X,Y) :- !.
subst(_->_,Var,Var) :- atomic(Var).
subst(X->Y,λ(X:Type1,Body),λ(X:Type2,Body)) :- !, subst(X->Y,Type1,Type2).
subst(X->Y,λ(Z:Type1,Body1),λ(Z:Type2,Body2)) :- subst(X->Y,Type1,Type2), subst(X->Y,Body1,Body2).
subst(X->Y,π(X:Type1,Body),π(X:Type2,Body)) :- !, subst(X->Y,Type1,Type2).
subst(X->Y,π(Z:Type1,Body1),π(Z:Type2,Body2)) :- subst(X->Y,Type1,Type2), subst(X->Y,Body1,Body2).
subst(X->Y,U $ V,P $ Q) :- subst(X->Y,U,P), subst(X->Y,V,Q).

eval(λ(U:_,B) $ V, BetaVal) :- !, subst(U->V,B,Beta), eval(Beta,BetaVal).
eval(X $ Y, XY) :- !, eval(X,Xv), eval(Xv $ Y,XY).
eval(Value, Value).


type(Term, Type) :- unfold(Term,TermU), [] ⊢ TermU : Type.
hasType(Term, Type) :- type(Term, Type1), unfold(Type,TypeU), eval(TypeU, Type2), alpha(Type1,Type2).

_ ⊢ S1 : S2 :- axiom(S1,S2).
Γ ⊢ I : T :- once(member(I:T, Γ)).
Γ ⊢ λ(A:T,B) : π(A:Tv,C) :- Γ ⊢ T : S1, sort(S1), eval(T,Tv), [A:Tv|Γ] ⊢ B : C. %%, /* sanity checks: */ Γ ⊢ π(A:Tv,C) : S2, sort(S2).
Γ ⊢ π(A:T,B) : S :- Γ ⊢ T : S1, [A:T|Γ] ⊢ B : S2, rule(S1,S2,S).
Γ ⊢ P $ Q : T :- Γ ⊢ P : π(X:U,B), Γ ⊢ Q : V, alpha(U,V), eval(λ(X:U,B) $ Q,T).



id := λ(t:★, λ(x:t, x)).
idTy := π(x:★, π(e:x, x)).

const := λ(s:★, λ(t:★, λ(u:s, λ(v:t, u)))).
constTy := π(u:★, π(v:★, π(g0:u, π(g1:v, u)))).

%%bool := π(a:★, a -> a -> a).
bool := π(a:★, π(g1:a, π(g2:a, a))).
true := λ(a:★, λ(x:a, λ(y:a, x))).
false := λ(a:★, λ(x:a, λ(y:a, y))).

%%nat := π(u:★, u -> (u -> u) -> u).
nat := π(u:★, π(g1:u, π(g2:π(g3:u, u), u))).
zero := λ(a:★, λ(x:a, λ(f:π(g:a, a), x))).
%%succ := λ(n:nat, λ(a:★, λ(x:a, λ(f:(a -> a), f $ (n $ a $ x $ f))))).
succ := λ(n:nat, λ(a:★, λ(x:a, λ(f:π(g:a, a), f $ (n $ a $ x $ f))))).

add := λ(m:nat, λ(n:nat, m $ nat $ n $ succ)).

eq := λ(a:★, λ(x:a, λ(y:a,
       λ(p:π(x:a, ★), π(g:p$x, p$y))))).

%%eq(a:★, x:a, y:a) := λ(p:π(x:a, ★), π(g:p$x, p$y)).