%% Programming Assignment 7: Type Inference in Prolog

type_of(Expr,T) :-
  not_implemented.

%% Some tests here are adapted from PLAI.
%% Adapt the rest of the tests from PLAI, and write your own.
:- begin_tests(basic).
test(num_literals) :-
  setof(T, type_of(num(0),T), [A]), A==t_num,
  not(type_of(num(foo),_)).
test(bool_literals) :-
  setof(T, type_of(bool(t),T), [A]), A==t_bool,
  not(type_of(bool(foo),_)).
test(fun_const) :-
  setof(T, type_of(fun(x,num(0)),T), [t_fun(A,B)]), var(A), B==t_num.
:- end_tests(basic).

%% This test exposes a bug in the PLAI code, which you should fix.
:- begin_tests(plai_bug).
test(env_shadowing) :-
  setof(T, type([bind(v,t_num),bind(v,t_bool)],id(v),T), [A]), A==t_num.
:- end_tests(plai_bug).

%% The following tests won't even terminate until the previous test passes.
:- begin_tests(more_interesting).
test(fun_if) :-
  setof(T, type_of(fun(x,if(id(x),id(x),id(x))),T),
        [t_fun(A,B)]), A==t_bool, B==t_bool.
test(fun_identity) :-
  setof(T, type_of(fun(x,id(x)),T), [t_fun(A,B)]), var(A), var(B), A==B.
test(with_shadowed) :-
  setof(T, type_of(with(x,bool(t),with(x,num(0),id(x))),T), [A]), A==t_num.
test(rec_curried_mult) :-
  setof(T,
        type_of(rec(mult, fun(x, fun(y,
                            if(app(id(is_zero),id(y)), num(0),
                               add(id(x),
                                   app(app(id(mult),id(x)),
                                       add(id(y),num(-1))))))),
                    id(mult)),
                T),
        [t_fun(A,t_fun(B,C))]), A==t_num, B==t_num, C==t_num.
:- end_tests(more_interesting).