:- prompt(_, '').
:- use_module(library(readutil)).
% STLC type system specification
type
(C
,var(X
), T
) :- first
(X
:T
,C
).type(C,lam(X,E),A -> B) :- type([X:A|C], E, B).
type(C,X $ Y, B) :- type(C,X,A -> B), type(C,Y,A).
first(K:V,[K1:V1|_]) :- K = K1, V=V1.
first(K:V,[K1:_|Xs]) :- K\==K1, first(K:V, Xs). % no cut but use var cmp
main:-
process,
type_and_print(C,E,T) :- type(C,E,T), print(E : T).
process:-
/* your code goes here */
type_and_print
([],lam
(x
,var(x
)),_
), nl, type_and_print
([],lam
(x
,lam
(y
,var(y
)$var
(x
))),_
), nl,
:- main.
Oi0gc2V0X3Byb2xvZ19mbGFnKHZlcmJvc2Usc2lsZW50KS4KOi0gcHJvbXB0KF8sICcnKS4KOi0gdXNlX21vZHVsZShsaWJyYXJ5KHJlYWR1dGlsKSkuCgo6LSBzZXRfcHJvbG9nX2ZsYWcob2NjdXJzX2NoZWNrLHRydWUpLgo6LSBvcCg1MDAseGZ5LCQpLgoKJSBTVExDIHR5cGUgc3lzdGVtIHNwZWNpZmljYXRpb24KCnR5cGUoQyx2YXIoWCksICAgICAgIFQpIDotIGZpcnN0KFg6VCxDKS4KdHlwZShDLGxhbShYLEUpLEEgLT4gQikgOi0gdHlwZShbWDpBfENdLCBFLCAgQikuCnR5cGUoQyxYICQgWSwgICAgICAgIEIpIDotIHR5cGUoQyxYLEEgLT4gQiksIHR5cGUoQyxZLEEpLgoKZmlyc3QoSzpWLFtLMTpWMXxfXSkgOi0gSyA9IEsxLCBWPVYxLgpmaXJzdChLOlYsW0sxOl98WHNdKSA6LSBLXD09SzEsIGZpcnN0KEs6ViwgWHMpLiAlIG5vIGN1dCBidXQgdXNlIHZhciBjbXAKCm1haW46LQoJcHJvY2VzcywKCWhhbHQuCgp0eXBlX2FuZF9wcmludChDLEUsVCkgOi0gdHlwZShDLEUsVCksIHByaW50KEUgOiBUKS4KCnByb2Nlc3M6LQogICAgLyogeW91ciBjb2RlIGdvZXMgaGVyZSAqLwoJdHlwZV9hbmRfcHJpbnQoW10sbGFtKHgsdmFyKHgpKSxfKSwgbmwsCgl0eXBlX2FuZF9wcmludChbXSxsYW0oeCxsYW0oeSx2YXIoeSkkdmFyKHgpKSksXyksIG5sLAoJdHJ1ZS4KCjotIG1haW4u