%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%% Definition 3 + 6 + Figure 5 : Var-validity of cps terms
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

stack : type.

dot : stack.
,   : stack -> ctriv -> stack.             %infix left 10 , .
% moved from lemma9.elf Thu Mar 10 20:45:28 2005 -fp
& : stack -> stack -> stack. %infix left 10 & .

vvalR : croot -> type.                     %name vvalR VVR.
vvalE : stack -> cexp -> type.             
vvalT : stack -> ctriv -> stack -> type.   
vvalC : stack -> ccont -> type.            
vvalK : stack -> (ctriv -> cexp) -> type.            

%mode vvalR +R.
%mode vvalE +Xi +E.
%mode vvalT +Xi +T -Xi'.
%mode vvalC +Xi +C.
%mode vvalK +Xi +K.

vval_klam : vvalR (klam E)
            <- ({k:ccont}vvalC dot k -> vvalE dot (E k)).

vval_capp : vvalE Xi (capp T0 T1 C)
            <- vvalT Xi T1 Xi1
            <- vvalT Xi1 T0 Xi0
            <- vvalC Xi0 C.

vval_cret : vvalE Xi (cret C T)
            <- vvalT Xi T Xi'
            <- vvalC Xi' C.

vval_xlam : vvalT Xi (xlam R) Xi
            <- ({x:ctriv}({Xi':stack}vvalT Xi' x Xi') -> vvalR (R x)).

vval_vlam : vvalC Xi (vlam E)
            <- ({v:ctriv}({Xi':stack}vvalT (Xi' , v) v Xi') 
                -> vvalE (Xi , v) (E v)).

vval_kappa : vvalK Xi Kappa
             <- ({v:ctriv}({Xi':stack}vvalT (Xi' , v) v Xi') 
                -> vvalE (Xi , v) (Kappa v))
             <- ({t:ctriv}({Xi':stack}vvalT Xi' t Xi') 
                -> vvalE Xi (Kappa t)).      

%name vvalE VVE. 
%name vvalT VVT.
%name vvalC VVC.
%name vvalK VVK.

%terminates (R E T C)
  (vvalR R)
  (vvalE _ E)
  (vvalT _ T _)
  (vvalC _ C).
%terminates K (vvalK _ K).