%% -*- prolog -*-

%% Type Inference

%% target of inference:
%%  - simple "expression" language
%%  - represent using Prolog terms
%%  - representation resembles compiler internal data structure: i.e., no sugar

%% E ::= constNum(n)
%%     | call(E, E)   %% only unary functions (use currying for ...)
%%     | prim(Op)     %% primitive ("basis") function, Op is an atom
%%     | is(E, T)     %% identity w/ type assertion
%%     | var(V)       %% V is an atom
%%     | lambda(V, E) %% lambda expression, formal parameter is V

%% T ::= atom         %% basis type (like "int", or "num")
%%     | '->'(T,T)    %% function from T (left) to T (righthand)

%% check(E) is true when E type checks.
check(E) :- oftype(E, _, []).

%% oftype(Expr, Type, Env) says Expr has type Type in the context of
%% types of local variable given by Env.  E.g., Env=[[x,num],[f,'->'(num,num)]].
oftype(constNum(_), num, _).

oftype(prim(exp), '->'(num,num), _).
oftype(prim('+'), '->'(num,'->'(num,num)), _).

oftype(var(V), T, Env) :- member([V,T1], Env), !, T=T1.

oftype(call(F, Arg), Range, Env) :-
	oftype(F,'->'(Domain, Range), Env),
	oftype(Arg, Domain, Env).

oftype(lambda(V, Body), '->'(Domain, Range), Env) :-
	oftype(Body, Range, [[V, Domain], Env]).

oftype(is(E, T), T, Env) :- oftype(E, T, Env).

% | ?- check(lambda(x, call(prim('+'), is(var(x), T)))).
% T = num
% yes
