-\section{Foo}
-
-\subsection{Language}
-
-\[
-\begin{array}{rcll}
- C & ::= & & \mbox{(\textbf{continuationals})} \\
- & & \DOT & \mbox{(dot)} \\
- & | & C ~ \SEMICOLON ~ C & \mbox{(semicolon)} \\
- & | & \BRANCH & \mbox{(branch)} \\
- & | & \SHIFT & \mbox{(shift)} \\
- & | & \MERGE & \mbox{(merge)} \\
- & | & \GOTO{n}{C} & \mbox{(goto)} \\
- & | & \TACTICAL{T} & \mbox{(tactical)} \\[2ex]
-
- T & ::= & & \mbox{(\textbf{tacticals})} \\
- & & \APPLY{tac} & \mbox{(tactic application)} \\
- & | & \SKIP & \mbox{(closed goal skipping)} \\
-\end{array}
-\]
-
-\subsection{Status}
-
-\[
-\begin{array}{rcll}
- \mathit{status} & = & \xi\times\Gamma\times\tau\times\kappa & \\
- \xi & & & \mbox{(metasenv)} \\
- \Gamma & = & \GOALSWITCH~\LIST~\STACK & \mbox{(context)} \\
- \GOALSWITCH & = & \OPEN{n} \quad | \quad \CLOSED{n} & \\
- \tau & = & \GOAL~\LIST~\STACK & \mbox{(todo)} \\
- \kappa & = & \GOAL~\LIST~\STACK & \mbox{(dot continuations)} \\
-\end{array}
-\]
-
-\subsection{Semantics}
-
-\[
-\begin{array}{rcll}
- \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} &
- \mbox{(continuationals semantics)} \\
- \TSEMOP{\cdot} & : & T -> \xi -> \GOALSWITCH ->
- \GOAL~\LIST \times \GOAL~\LIST & \mbox{(tacticals semantics)} \\
-\end{array}
-\]
-
-\[
-\begin{array}{rcl}
- \mathit{apply\_tac} & : & \mathit{tac} -> \xi -> \GOAL ->
- \GOAL~\LIST\times\GOAL~\LIST \\
- \mathit{map\_open} & : & \GOAL~\LIST -> \GOALSWITCH~\LIST \\
- \mathit{filter\_open} & : & \GOALSWITCH~\LIST -> \GOAL~\LIST \\
- \mathit{deep\_close} & :
- & \GOAL~\LIST -> \GOALSWITCH~\LIST~\STACK -> \GOALSWITCH~\LIST~\STACK \\
- \cup & : & \alpha~\LIST -> \alpha~\LIST -> \alpha~\LIST\\
- \setminus & : & \alpha~\LIST -> \alpha~\LIST -> \alpha~\LIST\\
-\end{array}
-\]
-
-\[
-\begin{array}{rlcc}
- \TSEM{\APPLY{tac}}{\xi}{\OPEN{n}} & =
- & \mathit{apply\_tac}(\mathit{tac},\xi,n) & \\
- \TSEM{\SKIP}{\xi}{\CLOSED{n}} & = & \langle [], [n]\rangle & \\
-\end{array}
-\]
-
-\[
-\begin{array}{rcl}
- \SEM{\TACTICAL{T}}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
- & =
- & \langle\xi_n,\MAPOPEN{G^O_n}::\DEEPCLOSE{G^C_n,\Gamma},\tau,\kappa\rangle
- \\[1ex]
-
- \multicolumn{3}{l}{\hspace{2em}
- \left\{
- \begin{array}{rcll}
- \langle\xi_0, G^O_0, G^C_0\rangle & = & \langle\xi, [], []\rangle \\
- \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle
- & =
- & \langle\xi_i, G^O_i, G^C_i\rangle
- & g_i\in G^C_i \\
- \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle
- & =
- & \langle\xi, (G^O_i\setminus G^C)\cup G^O, G^C_i\cup G^C\rangle
- & g_i\not\in G^C_i \\
- & & \mathit{where} ~ \langle\xi,G^O,G^C\rangle=\TSEM{T}{\xi_i}{g_{i+1}}
- \\
- \end{array}
- \right.
- }
- \\[2ex]
-
- \SEM{C_1 ~ \SEMICOLON ~ C_2}{\xi}{\Gamma}{\tau}{\kappa}
- & =
- & \SEM{C_2}{\xi'}{\Gamma'}{\tau'}{\kappa'}
- \\[1ex]
-
- & & \mathit{where} ~
- \langle\xi',\Gamma',\tau',\kappa',\rangle =
- \SEM{C_1}{\xi}{\Gamma}{\tau}{\kappa}
- \\[2ex]
-
- \SEM{~\DOT~}{\xi}{(g::G)::\Gamma}{\tau}{K::\kappa}
- & =
- & \langle\xi, [g]::\Gamma, \tau,
- (\FILTEROPEN{G}\cup K)::\kappa\rangle
- \\[2ex]
-
- \SEM{~\DOT~}{\xi}{[]::\Gamma}{\tau}{(n::N)::\kappa}
- & =
- & \langle\xi, [\OPEN{n}]::\Gamma, \tau, N::\kappa\rangle
- \\[2ex]
-
- \SEM{~\BRANCH~}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
- & =
- & \langle\xi, [g_1]::[g_2;\dots;g_n]::\Gamma, []::\tau, []::\kappa\rangle
- \\[2ex]
-
- \SEM{~\SHIFT~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
- & =
- & \langle\xi,
- [g_i]::[g_{i+1};\dots;g_n]::\Gamma,
- (T\cup\FILTEROPEN{G}\cup K)::\tau,
- []::\kappa\rangle
- \\[2ex]
-
- \SEM{~\MERGE~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
- & =
- & \langle\xi,
- (T\cup G\cup[g_i;\dots;g_n]\cup\MAPOPEN{K})::\Gamma,
- \tau,
- \kappa\rangle
- \\[2ex]
-
- \SEM{\GOTO{n}{C}}{\xi}{\Gamma}{\tau}{\kappa}
- & =
- & \langle\xi',\Gamma',\tau\setminus[n],\kappa\setminus[n]\rangle
- \\[1ex]
-
- & & \mathit{where} ~
- \langle \xi', []::\Gamma', []::\tau, []::\kappa\rangle
- = \SEM{C}{\xi}{[\OPEN{n}]::\Gamma}{[]::\tau}{[]::\kappa}
- \\[2ex]
-
-\end{array}
-\]