%%% Soundness of Evaluation under Continuations
%%% Author: Frank Pfenning

%{ Main Lemma:
   If   C :: K # (ev E) =>* (answer W)
   then for some V
        D :: eval E V
   and  C' :: K # (return V) =>* (answer W)
   where C' is a subderivation of C.

Proof: By complete induction on the structure of C.

Note that the fact that C' is a subderivation of C is not
represented in the implementation below.  This could be added
as a higher-level judgment on transformations.
}%

csd : K # (ev E) =>* (answer W)
       -> eval E V
       -> K # (return V) =>* (answer W)
       -> type.
%name csd CS.

% Natural Numbers
csd_z : csd (C' << st_z) (ev_z) C'.

csd_s : csd (C1 << st_s) (ev_s D1) C'
	 <- csd C1 D1 (C' << st_return).

csd_case_z : csd (C1 << st_case) (ev_case_z D2 D1) C'
	      <- csd C1 D1 (C2 << st_case1_z << st_return)
	      <- csd C2 D2 C'.

csd_case_s : csd (C1 << st_case) (ev_case_s D3 D1) C'
	      <- csd C1 D1 (C3 << st_case1_s << st_return)
	      <- csd C3 D3 C'.

% Pairs
csd_pair : csd (C1 << st_pair) (ev_pair D2 D1) C'
	    <- csd C1 D1 (C2 << st_pair1 << st_return)
	    <- csd C2 D2 (C' << st_return).

csd_fst : csd (C1 << st_fst) (ev_fst D1) C'
	   <- csd C1 D1 (C' << st_fst1 << st_return).

csd_snd : csd (C1 << st_snd) (ev_snd D1) C'
	   <- csd C1 D1 (C' << st_snd1 << st_return).

% Functions
csd_lam : csd (C' << st_lam) (ev_lam) C'.

csd_app : csd (C1 << st_app) (ev_app D3 D2 D1) C'
	   <- csd C1 D1 (C2 << st_app1 << st_return)
	   <- csd C2 D2 (C3 << st_app2 << st_return)
	   <- csd C3 D3 C'.

% Definitions
csd_letv : csd (C1 << st_letv) (ev_letv D2 D1) C'
	    <- csd C1 D1 (C2 << st_return)
	    <- csd C2 D2 C'.

csd_letn : csd (C1 << st_letn) (ev_letn D1) C'
	    <- csd C1 D1 C'.

% Recursion
csd_fix : csd (C1 << st_fix) (ev_fix D1) C'
	   <- csd C1 D1 C'.

% Values
csd_vl : csd (C' << st_vl) (ev_vl) C'.

% Return instruction are not possible since the initial state
% is of the form K # (ev E).

%{ Theorem:
   If  CE :: ceval E V
   then D :: eval E V.

Proof: By inversion on CE and appeal to the Main Lemma.
}%

ceval_sound : ceval E V -> eval E V -> type.

cevsd : ceval_sound (cev C) D
	 <- csd C D (stop << st_init).