:- set_prolog_flag(verbose,silent).
:- prompt(_, '').
:- use_module(library(readutil)).

:- set_prolog_flag(occurs_check,true).
:- op(500,xfy,$).

% STLC type system specification

type(C,var(X),      T1) :- first(X:T,C), instantiate(T,T1).                            
type(C,lam(X,E),A -> B) :- type([X:mono(A)|C],E,B).                             
type(C,X $ Y,        B) :- type(C,X,A -> B), type(C,Y,A).                               
type(C,let(X=E0,E1), T) :- type(C,E0,A), type([X:poly(C,A)|C],E1,T).

instantiate(poly(C,T),T1) :- copy_term(t(C,T),t(C,T1)).                         
instantiate(mono(T),T).

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,
	halt.

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,
	type_and_print([],let(id=lam(x,var(x)),var(id)$var(id)),_), nl,
	true.

:- main.