module poplmark-2a.

% Subtyping (Declarative version)

sub S top.

sub T T.

sub S T :- sub S Q, sub Q T.

sub (arrow S1 S2) (arrow T1 T2) :- sub T1 S1, sub S2 T2.

sub (all S1 (x\ S2 x)) (all T1 (x\ T2 x)) :-
    sub T1 S1,
    pi x\ (sub x T1 => sub (S2 x) (T2 x)).


% Typing

of (abs T1 E) (arrow T1 T2) :-
    pi x\ of x T1 => of (E x) T2.

of (app E1 E2) T12 :-
    of E1 (arrow T11 T12), of E2 T11.

of (tabs T1 E) (all T1 T2) :-
    pi x\ sub x T1 => of (E x) (T2 x).

of (tapp E T2) (T12 T2) :-
    of E (all T11 T12), sub T2 T11.

of E T :- of E S, sub S T.


% Small step evaluation

value (abs T E).
value (tabs T E).

step (app (abs T E1) V2) (E1 V2) :- value V2.

step (tapp (tabs T1 E) T2) (E T2).

step (app E1 E2) (app E1' E2) :- step E1 E1'.

step (app V1 E2) (app V1 E2') :- value V1, step E2 E2'.

step (tapp E T) (tapp E' T) :- step E E'.