% Note: There are some problems with this type system... :P

:- discontiguous(type/2).
:- discontiguous(convert/2).
:- style_check(-singleton).

/* implict conversions */
subtype(X, T2) :- type(X, T1), distinct(convert(T1, T2)).
convert(T, T).

/* function */
type(apply(F, X), TY) :- subtype(F, TX -> TY), subtype(X, TX). % application
convert(A1 -> B1, A2 -> B2) :- convert(A2, A1), convert(B1, B2).
%type(lambda(X, Y), T -> V) :- var(X), subtype(Y, V), distinct(type(X, T)). Doesn't work :<

/* basic combinators */
type(id, T -> T).
type(const, T -> V -> T).
type(fatal_error, string -> T). % can be used anywhere since crashes

/* bool */
type(true, bool).
type(false, bool).
type(not(X), bool) :- subtype(X, bool).
type(and(X, Y), bool) :- subtype(X, bool), subtype(Y, bool).
type(or(X, Y), bool) :- subtype(X, bool), subtype(Y, bool).
type(xor(X, Y), bool) :- subtype(X, bool), subtype(Y, bool).
type(if_then_else(X, Y, N), T) :- subtype(X, bool), subtype(Y, T), subtype(N, T).

/* int */
type(X, int) :- distinct(integer(X)). % built-in integer literal
type(X + Y, int) :- subtype(X, int), subtype(Y, int).
type(X - Y, int) :- subtype(X, int), subtype(Y, int).
type(X * Y, int) :- subtype(X, int), subtype(Y, int).
type(X / Y, int) :- subtype(X, int), subtype(Y, int).
type(square, int -> int).

/* big_int */
type(X, big_int) :- distinct(integer(X)). % built-in integer literal
type(X + Y, big_int) :- subtype(X, big_int), subtype(Y, big_int).
type(X - Y, big_int) :- subtype(X, big_int), subtype(Y, big_int).
type(X * Y, big_int) :- subtype(X, big_int), subtype(Y, big_int).
type(X / Y, big_int) :- subtype(X, big_int), subtype(Y, big_int).
convert(int, big_int).

/* float */
type(X, float) :- distinct(float(X)).
type(X, float) :- distinct(integer(X)).
type(X + Y, float) :- subtype(X, float), subtype(Y, float).
type(X - Y, float) :- subtype(X, float), subtype(Y, float).
type(X * Y, float) :- subtype(X, float), subtype(Y, float).
type(X / Y, float) :- subtype(X, float), subtype(Y, float).

/* list */
type([X|XS], apply(list, T)) :- subtype(X, T), subtype(XS, apply(list, T)).
type([], apply(list, _)).
type(X + Y, apply(list, T))  :- type(X, apply(list, T)), type(Y, apply(list, T)).
type(cons(X, Y), apply(list, T)) :- type(X, T), type(Y, apply(list, T)).

/* string */
type(X, string) :- distinct(string(X)). % built-in string literal
type(reverse(X), string) :- subtype(X, string).
type(char_at(X, I), char) :- subtype(X, string), subtype(I, int).
convert(string, apply(list, char)).
convert(apply(list, char), string).

/* optional */
type(apply(some, X), apply(optional, T)) :- type(X, T).
type(none, apply(optional, _)).

/* functor */
conform(list, functor).
conform(optional, functor).
type(map, (T1 -> T2) -> apply(F1, T1) -> apply(F2, T2)) :- conform(F1, functor), conform(F2, functor).