An algorithm for type-checking dependent types

dependent.pl

% An algorithm for type-checking dependent types

:- op(650,xfy,$).
:- op(900,xfy,[=>,->,⇓]).
:- op(920,xfx,[⊢]).
failwith(A,L) :- format(A,L),halt.

% Syntax

id(Id)               :- atom(Id).                      % Identify
exp(Id)              :- id(Id).                        % Variable
exp(E$E1)            :- exp(E),exp(E1).                % Application
exp(λ(Id->E))        :- id(Id),exp(E).                 % Lambda Abstraction
exp(let(Id=E:E1);E2) :- id(Id),exp(E),exp(E1),exp(E2). % Let Expression
exp(π(Id:E->E1))     :- id(Id),exp(E),exp(E1).         % Pi Abstraction
exp(*).                                                % Type
val(p(I))  :- integer(I).                              % Generalization
val(V1$V2) :- val(V1),val(V2).                         % Application
val(*).                                                % Type
val(C/E)   :- env(C),exp(E).                           % Closure
env(C)     :- maplist(env1, C).                        % Environment
env1(Id=V) :- id(Id), val(V).

% Evaluation

app(C/λ(X->E)$V = E_) :- !, [X=V|C] ⊢ E ⇓ E_.
app(        U$V = U$V).

U$V ⇓ E_ :- U ⇓ U_, V ⇓ V_, app(U_$V_ = E_).
C/E ⇓ E_ :- C ⊢ E ⇓ E_.
V   ⇓ V.

C ⊢ X               ⇓ E   :- atom(X), member(X=E,C).
C ⊢ E1$E2           ⇓ E   :- C ⊢ E1 ⇓ E1_, C ⊢ E2 ⇓ E2_, app(E1_$E2_ = E).
C ⊢ (let(X=E1:_);E3)⇓ E   :- C ⊢ E1 ⇓ E1_, [X=E1_|C] ⊢ E3 ⇓ E.
_ ⊢ *               ⇓ * .
C ⊢ E               ⇓ C/E.

% Equality

K ⊢ U            = U2              :- U ⇓ U_, U2 ⇓ U2_, K ⊢ U_ == U2_.
_ ⊢ *           == * .
K ⊢ T$W         == T2$W2           :- K ⊢ T = T2, K ⊢ W = W2.
_ ⊢ p(K1)       == p(K1).
K ⊢ C/λ(X->E)   == C2/λ(X2->E2)    :- K1 is K+1,
                                       K1 ⊢ [X=p(K)|C]/E = [X2=p(K)|C2]/E2.
K ⊢ C/π(X:A->B) == C2/π(X2:A2->B2) :- K1 is K+1,K ⊢ C/A = C2/A2,
                                       K1 ⊢ [X=p(K)|C]/B = [X2=p(K)|C2]/B2.

% Type checking

P/Γ ⊢ λ(X->N)         => V :- V ⇓ C/π(Y:A->B), length(P,K),
                               [X=p(K)|P]/[X:C/A|Γ] ⊢ N => [Y=p(K)|C]/B.
P/Γ ⊢ π(X:A->B)       => V :- V ⇓ *, P/Γ ⊢ A => *, length(P,K),
                               [X=p(K)|P]/[X:P/A|Γ] ⊢ B => * .
P/Γ ⊢ (let(X=E:T);E3) => V :- P/Γ ⊢ T => *, P ⊢ E ⇓ E_, P ⊢ T ⇓ T_,
                               [X=E_|P]/[X:T_|Γ] ⊢ E3 => V.
P/Γ ⊢ E               => V :- P/Γ⊢E->T, length(P,K), K ⊢ T = V.

% Type inference

_/Γ ⊢ Id    -> T            :- atom(Id), member(Id:T,Γ).
P/Γ ⊢ E1$E2 -> [X=P/E2|C]/B :- P/Γ ⊢ E1 -> T1, T1 ⇓ C/π(X:A->B),
                                P/Γ ⊢ E2 => C/A.
_/_ ⊢ *     -> * .

test(M : A) :- exp(M), exp(A), []/[] ⊢ A => *, []/[] ⊢ M => []/A.

:- test(λ(a->λ(x->x)):π(a : * -> π(x : a -> a))).
:- halt.