inst_bidi.m

:- module inst_bidi.

:- interface.

:- type nat ---> zero ; suc(nat).

:- type ty ---> base ; ty -> ty.
:- type ctx ---> nil ; ctx << ty.

% Fully typed (post-elaboration) terms store enough type information to
% reconstruct the type of the term in constant time.
% For example, `lam(S, A, B)` represents a lambda-abstraction with type
% `A -> B`.
:- type tm_chk --->
    emb(tm_syn, ty) ; lam(tm_chk, ty, ty).
:- type tm_syn --->
    ann(ty, tm_chk) ; var(nat, ty) ; app(tm_syn, tm_chk, ty, ty).

% Untyped (pre-elaboration) terms have all information that is going to be
% generated by elaboration represented as free unification variables.
:- inst untyped_chk for tm_chk/0
    --->    emb(untyped_syn, free)
    ;       lam(untyped_chk, free, free).
:- inst untyped_syn for tm_syn/0
    --->    ann(ground, untyped_chk)
    ;       var(ground, free)
    ;       app(untyped_syn, untyped_chk, free, free).
% Elaboration fills in all the missing information of subjects.
:- mode subj_chk == untyped_chk >> ground.
:- mode subj_syn == untyped_syn >> ground.

:- pred lookup(ctx::in, nat::in, ty::out) is semidet.

:- pred syn(ctx::in, tm_syn::subj_syn, ty::out) is semidet.
:- pred chk(ctx::in, ty::in, tm_chk::subj_chk) is semidet.

:- implementation.

lookup(_ << A, zero, A).
lookup(Ga << _, suc(N), A) :- lookup(Ga, N, A).

chk(Ga, A, emb(E, B)) :- syn(Ga, E, B), A = B.
chk(Ga, A -> B, lam(S, A, B)) :- chk(Ga << A, B, S).
syn(Ga, ann(A, S), A) :- chk(Ga, A, S).
syn(Ga, var(N, A), A) :- lookup(Ga, N, A).
syn(Ga, app(E, S, A, B), B) :- syn(Ga, E, A -> B), chk(Ga, A, S).