% propositions A,B ::= and(A,B) | imp(A,B) | ...
% checkable terms M,N ::= pair(M,N) | fun(X,M) | R | ...
% synth terms R ::= fst R | snd R | app(R,M) | X | ...
% context O ::= tp(X,A).O | nil

% check(+O, +M, +A)
% synth(+O, +R, -A)

check(O, pair(M, N), and(A, B)) :- check(O, M, A),
                                   check(O, N, B).
check(O, fun(X, M), imp(A, B)) :- check([tp(X, A)|O], M, B).
check(O, R, A) :- synth(O, R, B),
                  unify_with_occurs_check(A, B).

synth(O, fst(R), A) :- synth(O, R, and(B, C)), A = B.
synth(O, snd(R), A) :- synth(O, R, and(B, C)), A = C.
synth(O, app(R, M), B) :- synth(O, R, imp(A, C)),
                          check(O, M, A),
                          B = C.
synth([tp(X, A)|O], X, B) :- unify_with_occurs_check(A, B).
synth([tp(Y, B)|O], X, A) :- synth(O, X, A),
                             X \= Y.
