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{Enrico Tassi \qquad Stefano Zacchiroli \\
  12 \small Department of Computer Science, University of Bologna \\
  13 \small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\
  14 \small \{\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{\GOTO}[2]{\ensuremath{\mathtt{goal} ~ #1 ~ #2}}
  25
  26 \newcommand{\GOAL}{\ensuremath{\mathit{goal}}}
  27 \newcommand{\GOALSWITCH}{\ensuremath{\mathit{goal\_switch}}}
  28 \newcommand{\LIST}{\ensuremath{\mathtt{list}}}
  29 \newcommand{\STACK}{\ensuremath{\mathtt{stack}}}
  30 \newcommand{\OPEN}[1]{\ensuremath{\mathtt{Open}~#1}}
  31 \newcommand{\CLOSED}[1]{\ensuremath{\mathtt{Closed}~#1}}
  32
  33 \newcommand{\SEMOP}[1]{|[#1|]}
  34 \newcommand{\TSEMOP}[1]{{}_t|[#1|]}
  35 \newcommand{\SEM}[5]{\SEMOP{#1}_{#2,#3,#4,#5}}
  36 \newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}}
  37
  38 \newcommand{\FUN}[2]{\ensuremath{\mathit{#1}(#2)}}
  39 \newcommand{\FILTEROPEN}[1]{\FUN{filter\_open}{#1}}
  40 \newcommand{\MAPOPEN}[1]{\FUN{map\_open}{#1}}
  41 \newcommand{\DEEPCLOSE}[1]{\FUN{deep\_close}{#1}}
  42
  43 \begin{document}
  44 \maketitle
  45
  46 \section{Foo}
  47
  48 \subsection{Language}
  49
  50 \[
  51 \begin{array}{rcll}
  52  C & ::= & & \mbox{(\textbf{continuationals})} \\
  53    &     & \DOT & \mbox{(dot)} \\
  54    &  |  & C ~ \SEMICOLON ~ C & \mbox{(semicolon)} \\
  55    &  |  & \BRANCH & \mbox{(branch)} \\
  56    &  |  & \SHIFT & \mbox{(shift)} \\
  57    &  |  & \MERGE & \mbox{(merge)} \\
  58    &  |  & \GOTO{n}{C} & \mbox{(goto)} \\
  59    &  |  & \TACTICAL{T} & \mbox{(tactical)} \\[2ex]
  60
  61  T & ::= & & \mbox{(\textbf{tacticals})} \\
  62    &     & \APPLY{tac} & \mbox{(tactic application)} \\
  63    &  |  & \SKIP & \mbox{(closed goal skipping)} \\
  64 \end{array}
  65 \]
  66
  67 \subsection{Status}
  68
  69 \[
  70 \begin{array}{rcll}
  71  \mathit{status} & = & \xi\times\Gamma\times\tau\times\kappa & \\
  72  \xi & & & \mbox{(metasenv)} \\
  73  \Gamma & = & \GOALSWITCH~\LIST~\STACK & \mbox{(context)} \\
  74  \GOALSWITCH & = & \OPEN{g} \quad | \quad \CLOSED{g} & \\
  75  \tau & = & \GOAL~\LIST~\STACK & \mbox{(todo)} \\
  76  \kappa & = & \GOAL~\LIST~\STACK & \mbox{(dot continuations)} \\
  77 \end{array}
  78 \]
  79
  80 \subsection{Semantics}
  81
  82 \[
  83 \begin{array}{rcll}
  84  \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} &
  85   \mbox{(continuationals semantics)} \\
  86  \TSEMOP{\cdot} & : & T -> \xi -> \GOALSWITCH ->
  87   \GOAL~\LIST \times \GOAL~\LIST & \mbox{(tacticals semantics)} \\
  88 \end{array}
  89 \]
  90
  91 \[
  92 \begin{array}{rcl}
  93  \mathit{apply\_tac} & : & \mathit{tac} -> \xi -> \GOAL ->
  94   \GOAL~\LIST\times\GOAL~\LIST \\
  95  \mathit{map\_open} & : & \GOAL~\LIST -> \GOALSWITCH~\LIST \\
  96  \mathit{filter\_open} & : & \GOALSWITCH~\LIST -> \GOAL~\LIST \\
  97  \mathit{deep\_close} & :
  98  & \GOAL~\LIST -> \GOALSWITCH~\LIST~\STACK -> \GOALSWITCH~\LIST~\STACK \\
  99  \cup & : & \alpha~\LIST -> \alpha~\LIST -> \alpha~\LIST\\
 100  \setminus & : & \alpha~\LIST -> \alpha~\LIST -> \alpha~\LIST\\
 101 \end{array}
 102 \]
 103
 104 \[
 105 \begin{array}{rlcc}
 106  \TSEM{\APPLY{tac}}{\xi}{\OPEN{g}} & =
 107  & \mathit{apply\_tac}(\mathit{tac},\xi,g) & \\
 108  \TSEM{\SKIP}{\xi}{\CLOSED{g}} & = & \langle [], [g]\rangle & \\
 109 \end{array}
 110 \]
 111
 112 \[
 113 \begin{array}{rcl}
 114  \SEM{\TACTICAL{T}}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
 115  & =
 116  & \langle\xi_n,\MAPOPEN{G^O_n}::\DEEPCLOSE{G^C_n,\Gamma},\tau,\kappa\rangle
 117  \\[1ex]
 118
 119  \multicolumn{3}{l}{\hspace{2em}
 120  \left\{
 121  \begin{array}{rcll}
 122   \langle\xi_0, G^O_0, G^C_0\rangle & = & \langle\xi, [], []\rangle \\
 123   \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle
 124   & =
 125   & \langle\xi_i, G^O_i, G^C_i\rangle
 126   & g_i\in G^C_i \\
 127   \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle
 128   & =
 129   & \langle\xi, (G^O_i\setminus G^C)\cup G^O, G^C_i\cup G^C\rangle
 130   & g_i\not\in G^C_i \\
 131   & & \mathit{where} ~ \langle\xi,G^O,G^C\rangle=\TSEM{T}{\xi_i}{g_{i+1}}
 132   \\
 133  \end{array}
 134  \right.
 135  }
 136  \\[2ex]
 137
 138  \SEM{C_1 ~ \SEMICOLON ~ C_2}{\xi}{\Gamma}{\tau}{\kappa}
 139  & =
 140  & \SEM{C_2}{\xi'}{\Gamma'}{\tau'}{\kappa'}
 141  \\[1ex]
 142
 143  & & \mathit{where} ~
 144  \langle\xi',\Gamma',\tau',\kappa',\rangle =
 145  \SEM{C_1}{\xi}{\Gamma}{\tau}{\kappa}
 146  \\[2ex]
 147
 148  \SEM{~\DOT~}{\xi}{(g::G)::\Gamma}{\tau}{K::\kappa}
 149  & =
 150  & \langle\xi, [g]::\Gamma, \tau,
 151    (\FILTEROPEN{G}\cup K)::\kappa\rangle
 152  \\[2ex]
 153
 154  \SEM{~\DOT~}{\xi}{[]::\Gamma}{\tau}{(g::G)::\kappa}
 155  & =
 156  & \langle\xi, [g]::\Gamma, \tau, G::\kappa\rangle
 157  \\[2ex]
 158
 159  \SEM{~\BRANCH~}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
 160  & =
 161  & \langle\xi, [g_1]::[g_2;\dots;g_n]::\Gamma, []::\tau, []::\kappa\rangle
 162  \\[2ex]
 163
 164  \SEM{~\SHIFT~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
 165  & =
 166  & \langle\xi,
 167    [g_i]::[g_{i+1};\dots;g_n]::\Gamma,
 168    (T\cup\FILTEROPEN{G}\cup K)::\tau,
 169    []::\kappa\rangle
 170  \\[2ex]
 171
 172  \SEM{~\MERGE~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
 173  & =
 174  & \langle\xi,
 175    (T\cup G\cup[g_i;\dots;g_n]\cup\MAPOPEN{K})::\Gamma,
 176    \tau,
 177    \kappa\rangle
 178  \\[2ex]
 179
 180  \SEM{\GOTO{g}{C}}{\xi}{\Gamma}{\tau}{\kappa}
 181  & =
 182  & \langle\xi',\Gamma',\tau\setminus[g],\kappa\setminus[g]\rangle
 183  \\[1ex]
 184
 185  & & \mathit{where} ~
 186  \langle \xi', []::\Gamma', []::\tau, []::\kappa\rangle
 187  = \SEM{C}{\xi}{[g]::\Gamma}{[]::\tau}{[]::\kappa}
 188  \\[2ex]
 189
 190 \end{array}
 191 \]
 192
 193 \end{document}
 194