%!TEX root = ../Main.tex
\section{Joint Evaluation Contexts}

\begin{itemize}
\item   We use @exp_ctx_run@ with contexts lists in progress with data constructors, but then need the joint form when converting big step to small step evaluation
\end{itemize}

\begin{small}
\begin{code}
Inductive exp_ctx : (exp -> exp) -> Prop :=
 | XcTop  :  exp_ctx  (fun x => x)

 | XcApp1 :  forall x2
          ,  exp_ctx  (fun xx => XApp xx x2)

 | XcApp2 :  forall v1
          ,  value v1
          -> exp_ctx  (fun xx => XApp v1 xx)
 ...
 | XcCon  :  forall  dc ts C
          ,  exps_ctx wnfX C 
          -> exp_ctx  (fun xx => XCon dc ts (C xx))
\end{code}
\end{small}

\begin{small}
\begin{code}
Inductive exps_ctx {exp : Type} (Val : exp -> Prop) 
                 : (exp -> list exp) -> Prop :=
 | XscHead
   :  forall xs
   ,  exps_ctx Val (fun xx => xx :: xs)

 | XscCons
   :  forall v C
   ,  Val v
   -> exps_ctx Val C
   -> exps_ctx Val (fun xx => v :: C xx).
\end{code}
\end{small}
