SWI-Prolog-repl

[1]  ?- eval(add(tInt(1), tInt(2)), R).
R = tInt(1+2).

[1]  ?- eval(let(T, =, add(tInt(1), tInt(2))), R).
T = tInt(1+2),
R = tVoid.

[1]  ?- eval(let(T, =, add(T2, tInt(2))), R).
T = tInt(_8418+2),
T2 = tInt(_8418),
R = tVoid.

type-inference.pro

% ===================== Types =====================

type(tAny).
type(tVoid).
type(tInt(_)).
type(tFloat(_)).
type(tString(S)) :- string(S).
type(tList(T)) :- type(T).
type(tDict(K, V)) :- type(K), type(V).
type(tTuple(T1)) :- type(T1).
type(tTuple(T1, T2)) :- type(T1), type(T2).
type(tTuple(T1, T2, T3)) :- type(T1), type(T2), type(T3).
type(tError(_, _)).


% ===================== Utilities =====================

error(Expr, Msg, Err) :- type(Err) = type(tError(Expr, Msg)).
% error(Expr, Msg, Err) :- type(Err) = type(tError(Expr, Msg)); true.
error_string(Expr, Expected, Got, Err) :-
  stringify(Expected, E),
  stringify(Got, G),
  concat_atom(["expected ", E, " but got ", G], Atom),
  atom_string(Atom, Msg),
  error(Expr, Msg, Err).

stringify(S1, S2) :-
  string(S1),
  S2 = S1.
stringify(T, S) :-
  type(T),
  type_name(T, S).
stringify(V, S) :-
  term_string(V, S).
stringify(L, S) :-
  is_list(L),
  stringify(L, "", S).
stringify([V|Rest], S, Result) :-
  (string(V); type(V)),
  stringify(V, VS),
  concat_atom([S, VS], "", Added),
  stringify(Rest, Added, Result).
stringify([], S, Result) :- Result = S.

% for variable (e.g. type_name(T, N))
type_name(unknown, N) :- N = "Unknown", !.
type_name(tAny, N) :- N = "Any", !.
type_name(tVoid, N) :- N = "Void", !.
type_name(tInt(_), N) :- N = "Int", !.
type_name(tFloat(_), N) :- N = "Float", !.
type_name(tString(_), N) :- N = "String", !.
type_name(tList(T), N) :-
  type_name(T, TN),
  concat_atom(["List<", TN, ">"], "", N),
  !.
type_name(tDict(K, V), N) :-
  type_name(K, KName),
  type_name(V, VName),
  concat_atom(["Dict<", KName, ", ", VName, ">"], "", N),
  !.
type_name(tTuple(T1), N) :-
  type_name(T1, T1Name),
  concat_atom(["[", T1Name, "]"], "", N),
  !.
type_name(tTuple(T1, T2), N) :-
  type_name(T1, T1Name),
  type_name(T2, T2Name),
  concat_atom(["[", T1Name, ", ", T2Name, "]"], "", N),
  !.
type_name(tTuple(T1, T2, T3), N) :-
  type_name(T1, T1Name),
  type_name(T2, T2Name),
  type_name(T3, T3Name),
  concat_atom(["[", T1Name, ", ", T2Name, ", ", T3Name, "]"], "", N),
  !.
% for wrong type (e.g. type_name("foo", N))
type_name(S, N) :-
  string(S),
  N = S,
  !.
% for wrong type (e.g. type_name(foo, N))
type_name(Atom, N) :- atom_string(Atom, N).

eval(E, E) :- type(E).

% ===================== Syntax =====================

eval(let(_, =, E2), tError(Expr, Msg)) :- eval(E2, R), R = tError(Expr, Msg), !.
eval(let(E1, =, E2), tVoid) :- eval(E2, R2), E1 = R2, !.
eval(let(E1, =, E2), R) :-
  Expr = let(E1, =, E2),
  error_string(Expr, "same types", "different types", R),
  !.

% ===================== Binary operators =====================

eval(add(tInt(A), tInt(B)), tInt(A + B)) :- !.
eval(add(tFloat(A), tFloat(B)), tFloat(A + B)) :- !.
eval(add(tList(T), tList(T)), tList(R)) :- eval(T, R), !.
eval(add(E1, E2), R) :-
  Expr = add(E1, E2),
  error_string(Expr, [tInt(_), ",", tFloat(_), ",", tList(tAny)], [E1, " and ", E2], R).