--- /dev/null
+\documentclass[a4paper,draft]{article}
+
+\usepackage{a4wide}
+\usepackage{pifont}
+\usepackage{semantic}
+\usepackage{stmaryrd}
+
+\newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
+
+\title{Continuationals semantics for \MATITA}
+\author{Enrico Tassi \qquad Stefano Zacchiroli \\
+\small Department of Computer Science, University of Bologna \\
+\small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
+\small \{\texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}
+
+\newcommand{\DOT}{\mbox{\textbf{.}}}
+\newcommand{\SEMICOLON}{\mbox{\textbf{;}}}
+\newcommand{\BRANCH}{\mbox{\textbf{[}}}
+\newcommand{\SHIFT}{\mbox{\textbf{\textbar}}}
+\newcommand{\MERGE}{\mbox{\textbf{]}}}
+\newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}}
+\newcommand{\SKIP}{\ensuremath{\mathtt{skip}}}
+\newcommand{\TACTICAL}[1]{\ensuremath{\mathtt{tactical}~\mathit{#1}}}
+\newcommand{\GOTO}[2]{\ensuremath{\mathtt{goal} ~ #1 ~ #2}}
+
+\newcommand{\GOAL}{\ensuremath{\mathit{goal}}}
+\newcommand{\GOALSWITCH}{\ensuremath{\mathit{goal\_switch}}}
+\newcommand{\LIST}{\ensuremath{\mathtt{list}}}
+\newcommand{\STACK}{\ensuremath{\mathtt{stack}}}
+\newcommand{\OPEN}[1]{\ensuremath{\mathtt{Open}~#1}}
+\newcommand{\CLOSED}[1]{\ensuremath{\mathtt{Closed}~#1}}
+
+\newcommand{\SEMOP}[1]{|[#1|]}
+\newcommand{\TSEMOP}[1]{{}_t|[#1|]}
+\newcommand{\SEM}[5]{\SEMOP{#1}_{#2,#3,#4,#5}}
+\newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}}
+
+\newcommand{\FUN}[2]{\ensuremath{\mathit{#1}(#2)}}
+\newcommand{\FILTEROPEN}[1]{\FUN{filter\_open}{#1}}
+\newcommand{\MAPOPEN}[1]{\FUN{map\_open}{#1}}
+\newcommand{\DEEPCLOSE}[1]{\FUN{deep\_close}{#1}}
+
+\begin{document}
+\maketitle
+
+\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{g} \quad | \quad \CLOSED{g} & \\
+ \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{g}} & =
+ & \mathit{apply\_tac}(\mathit{tac},\xi,g) & \\
+ \TSEM{\SKIP}{\xi}{\CLOSED{g}} & = & \langle [], [g]\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}{(g::G)::\kappa}
+ & =
+ & \langle\xi, [g]::\Gamma, \tau, G::\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{g}{C}}{\xi}{\Gamma}{\tau}{\kappa}
+ & =
+ & \langle\xi',\Gamma',\tau\setminus[g],\kappa\setminus[g]\rangle
+ \\[1ex]
+
+ & & \mathit{where} ~
+ \langle \xi', []::\Gamma', []::\tau, []::\kappa\rangle
+ = \SEM{C}{\xi}{[g]::\Gamma}{[]::\tau}{[]::\kappa}
+ \\[2ex]
+
+\end{array}
+\]
+
+\end{document}
+
projects / helm.git / blobdiff