%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% Definition 13 : Control-stack substitution
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

cstack_substE : (ccont -> cexp) -> (ccont -> cstack) -> (ccont -> cexp) 
                -> type.

cstack_substC : (ccont -> ccont) -> (ccont -> cstack) -> (ccont -> ccont) 
                -> type.
%mode cstack_substE +E +Phi -E'.
%mode cstack_substC +C +Phi -C'.

csubst_cret : cstack_substE ([k:ccont]cret (C k) T) Phi 
                            ([k:ccont]cret (C' k) T)
              <- cstack_substC C Phi C'.

csubst_capp : cstack_substE ([k:ccont]capp T0 T1 (C k)) Phi 
                            ([k:ccont]capp T0 T1 (C' k))
              <- cstack_substC C Phi C'. 

csubst_vlam : cstack_substC ([k:ccont]vlam [v:ctriv]E v k) Phi 
                            ([k:ccont]vlam [v:ctriv]E' v k)
              <- {v:ctriv}cstack_substE (E v) Phi (E' v).

csubst_k_init : cstack_substC ([k:ccont]k) ([k:ccont]cdot)
                              ([k:ccont]k).

csubst_k_vlam : cstack_substC ([k:ccont]k) 
                              ([k:ccont]((Phi k) ; (vlam [v:ctriv]E v k))) 
                              ([k:ccont]vlam [v:ctriv]E' v k)
                <- {v:ctriv}cstack_substE (E v) Phi (E' v).

% does this require a multiset extension? -fp
%{
%terminates [(Phi1 Phi2) (E C)]
 (cstack_substE E Phi1 _)
 (cstack_substC C Phi2 _).
}%