/* Γ ⊢ M@N : ρ */
/* ⊢(Γ,:(M,ρ)) */
/* i = λ(x,x), k = λ(x,λ(y,x)), s = λ(x,λ(y,λ(z,x@z@(y@z)))) */
/* x@y = @(x,y) */
/* α ⇒ β ⇒ α */
:- set_prolog_flag(occurs_check, true).
:- op(160, fx, ⊢).
:- op(150, xfx, ⊢).
:- op(140, xfx, :).
:- op(120, xfy, ⇒).
:- op(100, yfx, @).

/*

  ?- [] ⊢ term : X
  X = ....
  false -> ако няма тип

*/

i(λ(x,x)).
k(λ(x,λ(y,x))).
s(λ(x,λ(y,λ(z,x@z@(y@z))))).
f(λ(x,λ(y,x@(y@x)))).
ω(λ(x,x@x)).

/* Γ ⊢ M : T */
/* Γ е списък от типови съждения */
Γ ⊢ X : T            :- member(X : T, Γ).
Γ ⊢ λ(X, M) : Ρ ⇒ Σ :- [ X : Ρ | Γ ] ⊢ M : Σ.
Γ ⊢ M @ N : Σ        :- Γ ⊢ M : Ρ ⇒ Σ, Γ ⊢ N : Ρ.

⊢ M : T  :- [] ⊢ M : T.