helm/ocaml/tactics/doc/main.tex

   1 \documentclass[a4paper,draft]{article}
   2
   3 \usepackage{a4wide}
   4 \usepackage{pifont}
   5 \usepackage{semantic}
   6 \usepackage{stmaryrd}
   7
   8 \newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}}
   9
  10 \title{Continuationals semantics for \MATITA}
  11 \author{Claudio Sacerdoti Coen \quad Enrico Tassi \quad Stefano Zacchiroli \\
  12 \small Department of Computer Science, University of Bologna \\
  13 \small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
  14 \small \{\texttt{sacerdot}, \texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}}
  15
  16 \newcommand{\MATHIT}[1]{\ensuremath{\mathit{#1}}}
  17 \newcommand{\MATHTT}[1]{\ensuremath{\mathtt{#1}}}
  18
  19 \newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
  20 \newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
  21 \newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
  22 \newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
  23 \newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
  24 \newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
  25 \newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
  26 \newcommand{\ENDFOCUS}{\ensuremath{\mathtt{unfocus}}}
  27 \newcommand{\SKIP}{\MATHTT{skip}}
  28 \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
  29
  30 \newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}}
  31
  32 \newcommand{\GOAL}{\MATHIT{goal}}
  33 \newcommand{\SWITCH}{\MATHIT{switch}}
  34 \newcommand{\LIST}{\MATHTT{list}}
  35 \newcommand{\INT}{\MATHTT{int}}
  36 \newcommand{\OPEN}{\MATHTT{Open}}
  37 \newcommand{\CLOSED}{\MATHTT{Closed}}
  38
  39 \newcommand{\SEMOP}[1]{|[#1|]}
  40 \newcommand{\TSEMOP}[1]{{}_t|[#1|]}
  41 \newcommand{\SEM}[3][\xi]{\SEMOP{#2}_{{#1},{#3}}}
  42 \newcommand{\ENTRY}[4]{\langle#1,#2,#3,#4\rangle}
  43 \newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}}
  44
  45 \newcommand{\GIN}[1][1]{\ensuremath{[s_{#1};\cdots;s_n]}}
  46
  47 \newcommand{\ZEROPOS}{\MATHIT{zero\_pos}}
  48 \newcommand{\INITPOS}{\MATHIT{init\_pos}}
  49 \newcommand{\ISFRESH}{\MATHIT{is\_fresh}}
  50 \newcommand{\FILTER}{\MATHIT{filter}}
  51 \newcommand{\FILTEROPEN}{\MATHIT{filter\_open}}
  52 \newcommand{\ISOPEN}{\MATHIT{is\_open}}
  53 \newcommand{\DEEPCLOSE}{\MATHIT{deep\_close}}
  54
  55 \newcommand{\BRANCHTAG}{\ensuremath{\mathtt{B}}}
  56 \newcommand{\FOCUSTAG}{\ensuremath{\mathtt{S}}}
  57
  58 \newlength{\sidecondlen}
  59 \setlength{\sidecondlen}{2cm}
  60
  61 \begin{document}
  62 \maketitle
  63
  64 \section{Semantics}
  65
  66 \subsection{Language}
  67
  68 \[
  69 \begin{array}{rcll}
  70  S & ::= & & \mbox{(\textbf{continuationals})}\\
  71    &     & \TACTIC{T} & \mbox{(tactic)}\\[2ex]
  72    &  |  & \DOT & \mbox{(dot)} \\
  73    &  |  & \SEMICOLON & \mbox{(semicolon)} \\
  74    &  |  & \BRANCH & \mbox{(branch)} \\
  75    &  |  & \SHIFT & \mbox{(shift)} \\
  76    &  |  & \POS{i} & \mbox{(relative positioning)} \\
  77    &  |  & \MERGE & \mbox{(merge)} \\[2ex]
  78    &  |  & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\
  79    &  |  & \ENDFOCUS & \mbox{(unfocus)} \\[2ex]
  80    T & : := & & \mbox{(\textbf{tactics})}\\
  81      &   & \SKIP & \mbox{(skip)} \\
  82      & | & \mathtt{reflexivity} & \\
  83      & | & \mathtt{apply}~t & \\
  84      & | & \dots &
  85 \end{array}
  86 \]
  87
  88 \subsection{Status}
  89
  90 \[
  91 \begin{array}{rcll}
  92  \SWITCH & = & \OPEN~\mathit{goal} ~ | ~ \CLOSED~\mathit{goal} & \\
  93  \mathit{locator} & = & \INT\times\SWITCH & \\
  94  \mathit{tag} & = & \BRANCHTAG ~ | ~ \FOCUSTAG \\[2ex]
  95
  96  \xi & = & (\INT\times\alpha)~\LIST& \mbox{(metasenv)} \\
  97  \Gamma & = & \mathit{locator}~\LIST & \mbox{(context)} \\
  98  \tau & = & \SWITCH~\LIST & \mbox{(todo)} \\
  99  \kappa & = & \SWITCH~\LIST & \mbox{(dot's future)} \\[2ex]
 100
 101  \mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST
 102  \\[2ex]
 103
 104  \mathit{status} & = & \xi\times\mathit{stack} \\
 105 \end{array}
 106 \]
 107
 108 \paragraph{Utilities}
 109 \begin{itemize}
 110  \item \ZEROPOS: map $g -> 0, \OPEN~g$
 111  \item \INITPOS: map $g -> i, \OPEN~g$
 112  \item \ISFRESH: $\OPEN~g, 0 -> true | \_ -> false$
 113  \item \FILTEROPEN: $G -> \FILTER(\ISOPEN,G)$
 114  \item \DEEPCLOSE: prende uno stack ed un insieme di goal da chiudere, traversa
 115   lo stack rimuovendo le occorrenze dei goal da $\tau$ e $\kappa$ e marcandole
 116   chiuse in $\Gamma$
 117 \end{itemize}
 118
 119 \paragraph{Invariants}
 120 \begin{itemize}
 121  \item $\forall \ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s \in\tau\cup\kappa,
 122   \exists g, s = \OPEN~g$ (i goal in $\tau$ e $\kappa$ sono aperti)
 123  \item la lista dei goal nel metasenv contiene tutti e soli i goal presenti
 124   sullo stack
 125  \item lo stack puo' contenere goal duplicati nel caso di uso della select
 126 \end{itemize}
 127
 128 \subsection{Semantics}
 129
 130 \[
 131 \begin{array}{rcll}
 132  \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} &
 133   \mbox{(continuationals semantics)} \\
 134  \TSEMOP{\cdot} & : & T -> \xi -> \SWITCH ->
 135   \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tactics semantics)} \\
 136 \end{array}
 137 \]
 138
 139 \[
 140 \begin{array}{rcl}
 141  \mathit{apply\_tac} & : & T -> \xi -> \GOAL ->
 142   \xi\times\GOAL~\LIST\times\GOAL~\LIST
 143 \end{array}
 144 \]
 145
 146 \[
 147 \begin{array}{rlcc}
 148  \TSEM{T}{\xi}{\OPEN~g} & = & \mathit{apply\_tac}(T,\xi,n) & T\neq\SKIP\\
 149  \TSEM{\SKIP}{\xi}{\CLOSED~g} & = & \langle \xi, [], [g]\rangle &
 150 \end{array}
 151 \]
 152
 153 \[
 154 \begin{array}{rcl}
 155
 156  \SEM{\TACTIC{T}}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
 157  & =
 158  & \langle
 159    \xi_n,
 160    \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t}
 161    :: \DEEPCLOSE(G^c_n,S)
 162    \rangle
 163  \\[1ex]
 164
 165  \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~
 166  \left\{
 167  \begin{array}{rcll}
 168   \langle\xi_0, G^o_0, G^c_0\rangle & = & \langle\xi, [], []\rangle \\
 169   \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle
 170   & =
 171   & \langle\xi_i, G^o_i, G^c_i\rangle
 172   & s_{i+1}\in G^c_i \\
 173   \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle
 174   & =
 175   & \langle\xi, (G^o_i\setminus G^c)\cup G^o, G^c_i\cup G^c\rangle
 176   & s_{i+1}\not\in G^c_i \\[1ex]
 177   & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{s_{i+1}}
 178   \\
 179  \end{array}
 180  \right.
 181  }
 182  \\[2ex]
 183
 184  \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S}
 185  & =
 186  & \langle \xi, \ENTRY{s_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle
 187  \\[1ex]
 188  & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN
 189  \\[2ex]
 190
 191  \SEM{~\DOT~}{\ENTRY{[]}{\tau}{s::\kappa}{t}::S}
 192  & =
 193  & \langle \xi, \ENTRY{\Gamma}{\tau}{\kappa}{t}::S \rangle
 194  \\[2ex]
 195
 196  \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[1ex]
 197
 198  \SEM{~\BRANCH~}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
 199  \quad
 200  & =
 201  & \langle\xi, \ENTRY{s_1'}{[]}{[]}{\BRANCHTAG}
 202    ::\ENTRY{[s_2';\cdots;s_n']}{\tau}{\kappa}{t}::S
 203  \\[1ex]
 204  & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[s_1';\cdots;s_n']
 205  \\[2ex]
 206
 207  \SEM{~\SHIFT~}
 208   {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t}::S}
 209  & =
 210  & \langle
 211    \xi, \ENTRY{s_1}{[]}{[]}{\BRANCHTAG}
 212         ::\ENTRY{\GIN[2]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t}::S
 213    \rangle
 214  \\[2ex]
 215
 216  \SEM{\POS{i}}
 217   {\ENTRY{[s]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
 218  & =
 219  & \langle \xi, \ENTRY{s_i}{[]}{[]}{\BRANCHTAG}
 220    ::\ENTRY{s_i :: (\Gamma'\setminus [s_i])}{\tau'}{\kappa'}{t'}::S \rangle
 221  \\[1ex]
 222  & & \mathrm{where} ~ \langle i,s'\rangle = s_i\in \Gamma'~\land~\ISFRESH(s)
 223  \\[2ex]
 224
 225  \SEM{\POS{i}}
 226   {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}
 227   ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
 228  & =
 229  & \langle \xi, \ENTRY{s_i}{[]}{[]}{\BRANCHTAG}
 230  ::\ENTRY{\Gamma'\setminus [s_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S
 231    \rangle
 232  \\[1ex]
 233  & & \mathrm{where} ~ \langle i, s'\rangle = s_i\in \Gamma'
 234  \\[2ex]
 235
 236  \SEM{~\MERGE~}
 237   {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}
 238   ::S}
 239  & =
 240  & \langle \xi,
 241    \ENTRY{\tau\cup\FILTEROPEN(\Gamma)\cup\Gamma'\cup\kappa}{\tau'}{\kappa'}{t'}
 242    :: S
 243    \rangle
 244  \\[2ex]
 245
 246  \SEM{\FOCUS{g_1,\dots,g_n}}{S}
 247  & =
 248  & \langle \xi, \ENTRY{[\OPEN~g_1;\cdots;\OPEN~g_n]}{[]}{[]}{\FOCUSTAG}::S
 249    \rangle
 250  \\[1ex]
 251  & & \mathrm{where} ~
 252  \forall ~ i=1,\dots,n,~\exists~\alpha_i,n_i,~\langle n_i,\alpha_i\rangle\in\xi
 253  \\[2ex]
 254
 255  \SEM{\ENDFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S}
 256  & =
 257  & \langle \xi, S\rangle \\[2ex]
 258
 259 \end{array}
 260 \]
 261
 262 \end{document}
 263