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{\DOT}{\mbox{\textbf{.}}}
  17 \newcommand{\SEMICOLON}{\mbox{\textbf{;}}}
  18 \newcommand{\BRANCH}{\mbox{\textbf{[}}}
  19 \newcommand{\SHIFT}{\mbox{\textbf{\textbar}}}
  20 \newcommand{\MERGE}{\mbox{\textbf{]}}}
  21 \newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}}
  22 \newcommand{\SKIP}{\ensuremath{\mathtt{skip}}}
  23 \newcommand{\TACTICAL}[1]{\ensuremath{\mathtt{tactical}~\mathit{#1}}}
  24 \newcommand{\OLDTACTICAL}[1]{\ensuremath{\mathtt{old\_tactical}~\mathit{#1}}}
  25 \newcommand{\SELECT}[1]{\ensuremath{\mathtt{select} ~ #1}}
  26 \newcommand{\ENDSELECT}[1]{\ensuremath{\mathtt{end}}}
  27
  28 \newcommand{\GOAL}{\ensuremath{\mathit{goal}}}
  29 \newcommand{\GOALSWITCH}{\ensuremath{\mathit{goal\_switch}}}
  30 \newcommand{\LIST}{\ensuremath{\mathtt{list}}}
  31 \newcommand{\BOOL}{\ensuremath{\mathtt{bool}}}
  32 \newcommand{\STACK}{\ensuremath{\mathtt{stack}}}
  33 \newcommand{\OPEN}[1]{\ensuremath{\mathtt{Open}~#1}}
  34 \newcommand{\CLOSED}[1]{\ensuremath{\mathtt{Closed}~#1}}
  35
  36 \newcommand{\SEMOP}[1]{|[#1|]}
  37 \newcommand{\TSEMOP}[1]{{}_t|[#1|]}
  38 \newcommand{\SEM}[5]{\SEMOP{#1}_{#2,#3,#4,#5}}
  39 \newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}}
  40
  41 \newcommand{\FUN}[2]{\ensuremath{\mathit{#1}(#2)}}
  42 \newcommand{\FILTERFUN}[2]{\FUN{filter}{#1,#2}}
  43 \newcommand{\MAPFUN}[2]{\FUN{map}{#1,#2}}
  44 \newcommand{\DEEPMAPFUN}[2]{\FUN{deep\_map}{#1,#2}}
  45 \newcommand{\ISOPENFUN}{\ensuremath{\mathit{is\_open}}}
  46 \newcommand{\CLOSEFUN}{\ensuremath{\mathit{close}}}
  47 \newcommand{\GOALOFFUN}{\ensuremath{\mathit{goal\_of}}}
  48 \newcommand{\DEEPCLOSEFUN}[2]{\FUN{deep\_close}{#1,#2}}
  49
  50 \begin{document}
  51 \maketitle
  52
  53 \section{Foo}
  54
  55 \subsection{Language}
  56
  57 \[
  58 \begin{array}{rcll}
  59  S & ::= & & \mbox{(\textbf{toplevel grammar})}\\
  60    &     & \varepsilon & \\
  61    &  |  & T~ P~ S & \\[2ex]
  62
  63  T & ::= & & \mbox{(\textbf{tactical})} \\
  64    &     & \APPLY{tac} & \mbox{(tactic application)} \\
  65    &  |  & \SKIP & \mbox{(closed goal skipping)} \\
  66    &  |  & \OLDTACTICAL{tcl} & \mbox{(non step-by-step tactical)} \\
  67    &  |  & \SELECT{n_1,\dots,n_k}{S} & \mbox{(select)} \\[2ex]
  68
  69  P & ::= & & \mbox{(\textbf{punctuation})} \\
  70    &     & \DOT & \mbox{(dot)} \\
  71    &  |  & \SEMICOLON & \mbox{(semicolon)} \\
  72    &  |  & \BRANCH & \mbox{(branch)} \\
  73    &  |  & \SHIFT & \mbox{(shift)} \\
  74    &  |  & \MERGE ~ M & \mbox{(merge)} \\[2ex]
  75
  76  M & ::= & & \mbox{(\textbf{merge-punctuation})} \\
  77    &     & \varepsilon & \\
  78    &  |  & \MERGE ~ M& \mbox{(multi-merge)} \\
  79    &  |  & \DOT & \mbox{(merge and choose)} \\[2ex]
  80
  81 \end{array}
  82 \]
  83
  84 \subsection{Status}
  85
  86 \[
  87 \begin{array}{rcll}
  88  \mathit{status} & = & \xi\times\Gamma\times\tau\times\kappa & \\
  89  \xi & = & \langle n,\alpha\rangle~\LIST& \mbox{(metasenv)} \\
  90  \Gamma & = & \GOALSWITCH~\LIST~\STACK & \mbox{(context)} \\
  91  \GOALSWITCH & = & \OPEN{n} \quad | \quad \CLOSED{n} & \\
  92  \tau & = & \GOAL~\LIST~\STACK & \mbox{(todo)} \\
  93  \kappa & = & \GOAL~\LIST~\STACK & \mbox{(dot continuations)} \\
  94 \end{array}
  95 \]
  96
  97 \subsection{Semantics}
  98
  99 \[
 100 \begin{array}{rcll}
 101  \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} &
 102   \mbox{(continuationals semantics)} \\
 103  \TSEMOP{\cdot} & : & T -> \xi -> \GOALSWITCH ->
 104   \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tacticals semantics)} \\
 105 \end{array}
 106 \]
 107
 108 \[
 109 \begin{array}{rcl}
 110  \mathit{filter} & : & (\alpha->\BOOL)->\alpha~\LIST->\alpha~\LIST \\
 111  \mathit{map} & : & (\alpha->\beta)->\alpha~\LIST->\beta~\LIST \\
 112  \mathit{deep\_map} & :
 113   & (\alpha->\beta)->\alpha~\LIST~\STACK->\beta~\LIST~\STACK \\
 114  \in & : & \alpha->\alpha~\LIST->\BOOL \\
 115  \cup & : & \alpha~\LIST->\alpha~\LIST->\alpha~\LIST \\
 116  \setminus & : & \alpha~\LIST->\alpha~\LIST->\alpha~\LIST \\
 117 \end{array}
 118 \]
 119
 120 \[
 121 \begin{array}{rcl}
 122  \mathit{apply\_tac} & : & \mathit{tac} -> \xi -> \GOAL ->
 123   \xi\times\GOAL~\LIST\times\GOAL~\LIST \\[1ex]
 124 %  \ISCLOSEDFUN & : & \GOALSWITCH -> \BOOL \\
 125  \ISOPENFUN & : & \GOALSWITCH -> \BOOL \\
 126  \CLOSEFUN & : & \GOALSWITCH -> \GOALSWITCH \\[1ex]
 127 %  \OPENFUN & : & \GOAL -> \GOALSWITCH \\[1ex]
 128  \GOALOFFUN & : & \GOALSWITCH -> \GOAL \\[1ex]
 129  \mathit{deep\_close} & :
 130  & \GOAL~\LIST -> \GOALSWITCH~\STACK -> \GOALSWITCH~\STACK \\[1ex]
 131 \end{array}
 132 \]
 133
 134 \[
 135 \begin{array}{rcl}
 136  \DEEPCLOSEFUN{G}{\Gamma}
 137  & =
 138  & \MAPFUN{\mathit{fold}
 139   (\lambda g.\lambda acc.
 140    \mathit{if}~\GOALOFFUN(g)\in G~\land\ISOPENFUN(g)~
 141    \mathit{then}~[]~
 142    \mathit{else}~[g]\cup\mathit{acc})
 143    []}{\Gamma}
 144 \end{array}
 145 \]
 146
 147 \[
 148 \begin{array}{rlcc}
 149  \TSEM{\APPLY{tac}}{\xi}{\OPEN{n}} & =
 150  & \mathit{apply\_tac}(\mathit{tac},\xi,n) & \\
 151  \TSEM{\SKIP}{\xi}{\CLOSED{n}} & = & \langle \xi, [], [n]\rangle & \\
 152 \end{array}
 153 \]
 154
 155 \[
 156 \begin{array}{rcl}
 157  \SEM{\TACTICAL{T}}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
 158  \quad (n\geq 1)
 159  & =
 160  & \langle\xi_n,
 161  \MAPFUN{\mathtt{Open}}{G^O_n}::\DEEPCLOSEFUN{G^C_n}{\Gamma},
 162    \tau\setminus G^C_n,\kappa\setminus G^O_n\rangle
 163  \\[1ex]
 164
 165  \multicolumn{3}{l}{\hspace{2em}\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   & g_{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   & g_{i+1}\not\in G^C_i \\
 177   & & \mathit{where} ~ \langle\xi,G^O,G^C\rangle=\TSEM{T}{\xi_i}{g_{i+1}}
 178   \\
 179  \end{array}
 180  \right.
 181  }
 182  \\[2ex]
 183
 184  \SEM{C_1 ~ \SEMICOLON ~ C_2}{\xi}{\Gamma}{\tau}{\kappa}
 185  & =
 186  & \SEM{C_2}{\xi'}{\Gamma'}{\tau'}{\kappa'}
 187  \\[1ex]
 188
 189  & & \mathit{where} ~
 190  \langle\xi',\Gamma',\tau',\kappa',\rangle =
 191  \SEM{C_1}{\xi}{\Gamma}{\tau}{\kappa}
 192  \\[2ex]
 193
 194  \SEM{C~\DOT~}{\xi}{\Gamma}{\tau}{\kappa}
 195  & =
 196  & \langle \xi'', \Gamma'', \tau'', \kappa'' \rangle
 197  \\[1ex]
 198
 199  \multicolumn{3}{l}{\hspace{2em}\mathit{where} ~
 200   \langle \xi',G::\Gamma',\tau',K::\kappa' \rangle
 201    = \SEM{C}{\xi}{\Gamma}{\tau}{\kappa}}
 202  \\[1ex]
 203
 204  \multicolumn{3}{l}{\hspace{2em}\mathit{and} ~
 205  \langle \xi'', \Gamma'', \tau'', \kappa'' \rangle =
 206  \left\{
 207  \begin{array}{ll}
 208   \langle \xi', [g]::\Gamma', \tau', (\MAPFUN{\GOALOFFUN}{G'}\cup K)::\kappa'
 209   \rangle
 210   & \FILTERFUN{\ISOPENFUN}{G} = g::G'
 211   \\
 212   \langle \xi', [\mathtt{Open}~n]::\Gamma', \tau', K'::\kappa' \rangle
 213   & \FILTERFUN{\ISOPENFUN}{G} = []~\land~K=n::K'
 214  \end{array}
 215  \right.}
 216  \\[2ex]
 217
 218  \SEM{~\BRANCH~}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
 219  \quad (n\geq 2)
 220  & =
 221  & \langle\xi, [g_1]::[g_2;\dots;g_n]::\Gamma, []::\tau, []::\kappa\rangle
 222  \\[2ex]
 223
 224  \SEM{~\SHIFT~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
 225  & =
 226  & \langle\xi,
 227    [g_i]::[g_{i+1};\dots;g_n]::\Gamma,
 228    \tau'::\tau,
 229    []::\kappa\rangle
 230  \\[1ex]
 231
 232  & & \mathit{where} ~
 233    \tau' = T\cup\MAPFUN{\GOALOFFUN}{\FILTERFUN{\ISOPENFUN}{G}}\cup K
 234  \\[2ex]
 235
 236  \SEM{~\MERGE~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
 237  & =
 238  & \langle \xi, \Gamma'::\Gamma, \tau, \kappa \rangle
 239  \\[1ex]
 240
 241  & & \mathit{where} ~
 242    \Gamma' =
 243     T \cup\FILTERFUN{\ISOPENFUN}{G}
 244      \cup[g_i;\dots;g_n]
 245      \cup\MAPFUN{\mathtt{Open}}{K}
 246  \\[2ex]
 247
 248  \SEM{\SELECT{n_1,\dots,n_k}{C}}{\xi}{\Gamma}{\tau}{\kappa}
 249  & =
 250  & \langle \xi',\Gamma',\tau',\kappa' \rangle
 251  \\[1ex]
 252
 253  & & \mathit{where} ~
 254  \forall ~ i=1,\dots,k,~\exists ~ \alpha_i,~\langle n_i,\alpha_i\rangle \in \xi
 255  \\[1ex]
 256
 257  & & \mathit{and} ~
 258  \langle \xi', []::\Gamma', []::\tau', []::\kappa' \rangle
 259  = \SEM{C}{\xi}{\MAPFUN{\mathtt{Open}}{[n_1;\dots;n_k]}::\Gamma}{[]::\tau}{[]::\kappa}
 260  \\[2ex]
 261
 262 \end{array}
 263 \]
 264
 265 \end{document}
 266