\documentclass[a4paper]{article}

\usepackage{a4wide}
\usepackage{pifont}
\usepackage{semantic}
\usepackage{stmaryrd}

\newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}

\title{Continuationals semantics for \MATITA}
\author{Claudio Sacerdoti Coen \quad Enrico Tassi \quad Stefano Zacchiroli \\
\small Department of Computer Science, University of Bologna \\
\small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
\small \{\texttt{sacerdot}, \texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}

\newcommand{\MATHIT}[1]{\ensuremath{\mathit{#1}}}
\newcommand{\MATHTT}[1]{\ensuremath{\mathtt{#1}}}

\newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
\newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
\newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
\newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
\newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
\newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
\newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
\newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
\newcommand{\SKIP}{\MATHTT{skip}}
\newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}

\newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}}

\newcommand{\GOAL}{\MATHIT{goal}}
\newcommand{\SWITCH}{\MATHIT{switch}}
\newcommand{\LIST}{\MATHTT{list}}
\newcommand{\INT}{\MATHTT{int}}
\newcommand{\OPEN}{\MATHTT{Open}}
\newcommand{\CLOSED}{\MATHTT{Closed}}

\newcommand{\SEMOP}[1]{|[#1|]}
\newcommand{\TSEMOP}[1]{{}_t|[#1|]}
\newcommand{\SEM}[3][\xi]{\SEMOP{#2}_{{#1},{#3}}}
\newcommand{\ENTRY}[4]{\langle#1,#2,#3,#4\rangle}
\newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}}

\newcommand{\GIN}[1][1]{\ensuremath{[l_{#1};\cdots;l_n]}}

\newcommand{\ZEROPOS}{\MATHIT{zero\_pos}}
\newcommand{\INITPOS}{\MATHIT{init\_pos}}
\newcommand{\ISFRESH}{\MATHIT{is\_fresh}}
\newcommand{\FILTER}{\MATHIT{filter}}
\newcommand{\FILTEROPEN}{\MATHIT{filter\_open}}
\newcommand{\ISOPEN}{\MATHIT{is\_open}}
\newcommand{\DEEPCLOSE}{\MATHIT{deep\_close}}
\newcommand{\REMOVEGOALS}{\MATHIT{remove\_goals}}
\newcommand{\GOALS}{\MATHIT{goals}}

\newcommand{\BRANCHTAG}{\ensuremath{\mathtt{B}}}
\newcommand{\FOCUSTAG}{\ensuremath{\mathtt{F}}}

\newlength{\sidecondlen}
\setlength{\sidecondlen}{2cm}

\begin{document}
\maketitle

\section{Semantics}

\subsection{Language}

\[
\begin{array}{rcll}
 S & ::= & & \mbox{(\textbf{continuationals})}\\
   &     & \TACTIC{T} & \mbox{(tactic)}\\[2ex]
   &  |  & \DOT & \mbox{(dot)} \\
   &  |  & \SEMICOLON & \mbox{(semicolon)} \\
   &  |  & \BRANCH & \mbox{(branch)} \\
   &  |  & \SHIFT & \mbox{(shift)} \\
   &  |  & \POS{i} & \mbox{(relative positioning)} \\
   &  |  & \MERGE & \mbox{(merge)} \\[2ex]
   &  |  & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\
   &  |  & \UNFOCUS & \mbox{(unfocus)} \\[2ex]
   &  |  & S ~ S & \mbox{(sequential composition)} \\[2ex]
   T & : := & & \mbox{(\textbf{tactics})}\\
     &   & \SKIP & \mbox{(skip)} \\
     & | & \mathtt{reflexivity} & \\
     & | & \mathtt{apply}~t & \\
     & | & \dots &
\end{array}
\]

\subsection{Status}

\[
\begin{array}{rcll}
 \xi & & & \mbox{(proof status)} \\
 \mathit{goal} & & & \mbox{(proof goal)} \\[2ex]

 \SWITCH & = & \OPEN~\mathit{goal} ~ | ~ \CLOSED~\mathit{goal} & \\
 \mathit{locator} & = & \INT\times\SWITCH & \\
 \mathit{tag} & = & \BRANCHTAG ~ | ~ \FOCUSTAG \\[2ex]

 \Gamma & = & \mathit{locator}~\LIST & \mbox{(context)} \\
 \tau & = & \mathit{locator}~\LIST & \mbox{(todo)} \\
 \kappa & = & \mathit{locator}~\LIST & \mbox{(dot's future)} \\[2ex]

 \mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST
 \\[2ex]

 \mathit{status} & = & \xi\times\mathit{stack} \\
\end{array}
\]

\paragraph{Utilities}
\begin{itemize}
 \item $\ZEROPOS([g_1;\cdots;g_n]) =
  [\langle 0,\OPEN~g_1\rangle;\cdots;\langle 0,\OPEN~g_n\rangle]$
 \item $\INITPOS([\langle i_1,s_1\rangle;\cdots;\langle i_n,s_n\rangle]) =
  [\langle 1,\OPEN~s_1\rangle;\cdots;\langle n,\OPEN~s_n\rangle]$
 \item $\ISFRESH(s) =
  \left\{
  \begin{array}{ll}
   \mathit{true} & \mathrm{if} ~ s = \langle n, \OPEN~g\rangle\land n > 0 \\
   \mathit{false} & \mathrm{otherwise} \\
  \end{array}
  \right.$
 \item $\FILTEROPEN(\mathit{locs})=
  \left\{
  \begin{array}{ll}
   [] & \mathrm{if}~\mathit{locs} = [] \\
   \langle i,\OPEN~g\rangle :: \FILTEROPEN(\mathit{tl})
   & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} \\
   \FILTEROPEN(\mathit{tl})
   & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
  \end{array}
  \right.$
 \item $\REMOVEGOALS(G,\mathit{locs}) =
  \left\{
  \begin{array}{ll}
   [] & \mathrm{if}~\mathit{locs} = [] \\
   \REMOVEGOALS(G,\mathit{tl})
   & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl}
     \land g\in G\\
   hd :: \REMOVEGOALS(G,\mathit{tl})
   & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
  \end{array}
  \right.$
 \item $\DEEPCLOSE(G,S)$: (intuition) given a set of goals $G$ and a stack $S$
  it returns a new stack $S'$ identical to the given one with the exceptions
  that each locator whose goal is in $G$ is marked as closed in $\Gamma$ stack
  components and removed from $\tau$ and $\kappa$ components.
 \item $\GOALS(S)$: (inutition) return all goals appearing in whatever position
  on a given stack $S$.
\end{itemize}

\paragraph{Invariants}
\begin{itemize}
 \item $\forall~\mathrm{entry}~\ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s
  \in\tau\cup\kappa, \exists g, s = \OPEN~g$ (each locator on the stack in
  $\tau$ and $\kappa$ components has an \OPEN~switch).
 \item Unless \FOCUS{} is used the stack contains no duplicate goals.
\end{itemize}

\subsection{Semantics}

\[
\begin{array}{rcll}
 \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} &
  \mbox{(continuationals semantics)} \\
 \TSEMOP{\cdot} & : & T -> \xi -> \SWITCH ->
  \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tactics semantics)} \\
\end{array}
\]

\[
\begin{array}{rcl}
 \mathit{apply\_tac} & : & T -> \xi -> \GOAL ->
  \xi\times\GOAL~\LIST\times\GOAL~\LIST
\end{array}
\]

\[
\begin{array}{rlcc}
 \TSEM{T}{\xi}{\OPEN~g} & = & \mathit{apply\_tac}(T,\xi,n) & T\neq\SKIP\\
 \TSEM{\SKIP}{\xi}{\CLOSED~g} & = & \langle \xi, [], [g]\rangle &
\end{array}
\]

\[
\begin{array}{rcl}

 \SEM{\TACTIC{T}}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
 & =
 & \langle
   \xi_n,
   \ENTRY{\Gamma'}{\tau'}{\kappa'}{t}
%    \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t}
   :: \DEEPCLOSE(G^c_n,S)
   \rangle
 \\[1ex]
 \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~ n\geq 1}
 \\[1ex]
 \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
  \Gamma' = \ZEROPOS(G^o_n)
  \land \tau' = \REMOVEGOALS(G^c_n,\tau)
  \land \kappa' = \REMOVEGOALS(G^o_n,\kappa)
 }
 \\[1ex]
 \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
 \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
  & l_{i+1}\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
  & l_{i+1}\not\in G^c_i \\[1ex]
  & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{l_{i+1}} \\
 \end{array}
 \right.
 }
 \\[6ex]

 \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S}
 & =
 & \langle \xi, \ENTRY{l_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle
 \\[1ex]
 & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN \land n\geq 1
 \\[2ex]

 \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{l::\kappa}{t}::S}
 & =
 & \langle \xi, \ENTRY{[l]}{\tau}{\kappa}{t}::S \rangle
 \\[1ex]
 & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=[]
 \\[2ex]

 \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[1ex]

 \SEM{~\BRANCH~}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
 \quad 
 & =
 & \langle\xi, \ENTRY{[l_1']}{[]}{[]}{\BRANCHTAG}
   ::\ENTRY{[l_2';\cdots;l_n']}{\tau}{\kappa}{t}::S
 \\[1ex]
 & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[l_1';\cdots;l_n']
 \\[2ex]

 \SEM{~\SHIFT~}
  {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t'}
  ::S}
 & =
 & \langle
   \xi, \ENTRY{[l_1]}{\tau\cup\FILTEROPEN(\Gamma)}{[]}{\BRANCHTAG}
	::\ENTRY{\GIN[2]}{\tau'}{\kappa'}{t'}::S
   \rangle
 \\[1ex]
 & & \mathrm{where} ~ n\geq 1
 \\[2ex]

 \SEM{~\POS{i}~}
  {\ENTRY{[l]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
 & =
 & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
   ::\ENTRY{l :: (\Gamma'\setminus [l_i])}{\tau'}{\kappa'}{t'}::S \rangle
 \\[1ex]
 & & \mathrm{where} ~ \langle i,l'\rangle = l_i\in \Gamma'~\land~\ISFRESH(l)
 \\[2ex]

 \SEM{~\POS{i}~}
  {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}
  ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
 & =
 & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
 ::\ENTRY{\Gamma'\setminus [l_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S
   \rangle
 \\[1ex]
 & & \mathrm{where} ~ \langle i, l'\rangle = l_i\in \Gamma'
 \\[2ex]

 \SEM{~\MERGE~}
  {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}
  ::S}
 & =
 & \langle \xi,
   \ENTRY{\tau\cup\FILTEROPEN(\Gamma)\cup\Gamma'\cup\kappa}{\tau'}{\kappa'}{t'}
   :: S
   \rangle
 \\[2ex]

 \SEM{\FOCUS{g_1,\dots,g_n}}{S}
 & = 
 & \langle \xi, \ENTRY{[\OPEN~g_1;\cdots;\OPEN~g_n]}{[]}{[]}{\FOCUSTAG}
   ::\DEEPCLOSE(S)
   \rangle
 \\[1ex]
 & & \mathrm{where} ~
 \forall i=1,\dots,n,~g_i\in\GOALS(S)
 \\[2ex]

 \SEM{\UNFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S}
 & = 
 & \langle \xi, S\rangle \\[2ex]

\end{array}
\]

\end{document}

