%%% Mini-ML Natural Semantics
%%% Version with separate category of values
%%% Author: Frank Pfenning, based on [Michaylov & Pfenning 92]

eval : exp -> val -> type.  %name eval D.

% Natural Numbers
ev_z       : eval z z*.
ev_s       : eval (s E) (s* V)
	      <- eval E V.
ev_case_z  : eval (case E1 E2 E3) V
	      <- eval E1 z*
	      <- eval E2 V.
ev_case_s  : eval (case E1 E2 E3) V
	      <- eval E1 (s* V1')
	      <- eval (E3 V1') V.

% Pairs
ev_pair : eval (pair E1 E2) (pair* V1 V2)
	     <- eval E1 V1
	     <- eval E2 V2.
ev_fst  : eval (fst E) V1
	     <- eval E (pair* V1 V2).
ev_snd  : eval (snd E) V2
	     <- eval E (pair* V1 V2).

% Functions
ev_lam  : eval (lam E) (lam* E).
ev_app  : eval (app E1 E2) V
	    <- eval E1 (lam* E1')
	    <- eval E2 V2
	    <- eval (E1' V2) V.

% Definitions
ev_letv : eval (letv E1 E2) V
	     <- eval E1 V1
	     <- eval (E2 V1) V.
ev_letn : eval (letn E1 E2) V
	     <- eval (E2 E1) V.

% Recursion
ev_fix  : eval (fix E) V
	     <- eval (E (fix E)) V.

% Values
ev_vl : eval (vl V) V.