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