%% -*- 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

%% 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, T).

oftype(constNum(_), num).
oftype(prim(exp), '->'(num,num)).
oftype(prim('+'), '->'(num,'->'(num,num))).
oftype(call(F, Arg), Range) :- oftype(F,'->'(Domain, Range)), oftype(Arg, Domain).
oftype(is(E, T), T) :- oftype(E, T).

% | ?- check(is(call(prim(O), constNum(2)), T)).  

% O = exp
% T = num ? ;

% O = +
% T = num->num

% | ?- check(is(call(E, constNum(2)), T)).
% ...
