X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fdoc%2Fmain.tex;h=00208b0c25724c2efac60938aae49d77332067c4;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=be235a2c1fe9cdbecc73177a699034aee014b2f1;hpb=f26b2b816de0744f666a0ab8ee26fa670ad6a1b8;p=helm.git diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex index be235a2c1..00208b0c2 100644 --- a/helm/ocaml/tactics/doc/main.tex +++ b/helm/ocaml/tactics/doc/main.tex @@ -1,4 +1,4 @@ -\documentclass[a4paper,draft]{article} +\documentclass[a4paper]{article} \usepackage{a4wide} \usepackage{pifont} @@ -13,242 +13,57 @@ \small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\ \small \{\texttt{sacerdot}, \texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}} -\newcommand{\DOT}{\mbox{\textbf{.}}} -\newcommand{\SEMICOLON}{\mbox{\textbf{;}}} -\newcommand{\BRANCH}{\mbox{\textbf{[}}} -\newcommand{\SHIFT}{\mbox{\textbf{\textbar}}} -\newcommand{\MERGE}{\mbox{\textbf{]}}} +\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{\SKIP}{\ensuremath{\mathtt{skip}}} -\newcommand{\TACTICAL}[1]{\ensuremath{\mathtt{tactical}~\mathit{#1}}} -\newcommand{\SELECT}[2]{\ensuremath{\mathtt{select} ~ #1 ~ #2}} - -\newcommand{\GOAL}{\ensuremath{\mathit{goal}}} -\newcommand{\GOALSWITCH}{\ensuremath{\mathit{goal\_switch}}} -\newcommand{\LIST}{\ensuremath{\mathtt{list}}} -\newcommand{\BOOL}{\ensuremath{\mathtt{bool}}} -\newcommand{\STACK}{\ensuremath{\mathtt{stack}}} -\newcommand{\OPEN}[1]{\ensuremath{\mathtt{Open}~#1}} -\newcommand{\CLOSED}[1]{\ensuremath{\mathtt{Closed}~#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}[5]{\SEMOP{#1}_{#2,#3,#4,#5}} +\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{\FUN}[2]{\ensuremath{\mathit{#1}(#2)}} -\newcommand{\FILTERFUN}[2]{\FUN{filter}{#1,#2}} -\newcommand{\MAPFUN}[2]{\FUN{map}{#1,#2}} -\newcommand{\DEEPMAPFUN}[2]{\FUN{deep\_map}{#1,#2}} -\newcommand{\ISOPENFUN}{\ensuremath{\mathit{is\_open}}} -\newcommand{\CLOSEFUN}{\ensuremath{\mathit{close}}} -\newcommand{\GOALOFFUN}{\ensuremath{\mathit{goal\_of}}} -\newcommand{\DEEPCLOSEFUN}[2]{\FUN{deep\_close}{#1,#2}} +\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{open\_goals}} + +\newcommand{\BRANCHTAG}{\ensuremath{\mathtt{B}}} +\newcommand{\FOCUSTAG}{\ensuremath{\mathtt{F}}} + +\newlength{\sidecondlen} +\setlength{\sidecondlen}{2cm} \begin{document} \maketitle -\section{Foo} - -\subsection{Language} - -\[ -\begin{array}{rcll} - C & ::= & & \mbox{(\textbf{continuationals})} \\ - & & C ~ \DOT & \mbox{(dot)} \\ - & | & C ~ \SEMICOLON ~ C & \mbox{(semicolon)} \\ - & | & \BRANCH & \mbox{(branch)} \\ - & | & \SHIFT & \mbox{(shift)} \\ - & | & \MERGE & \mbox{(merge)} \\ - & | & \SELECT{n_1,\dots,n_k}{C} & \mbox{(select)} \\ - & | & \TACTICAL{T} & \mbox{(tactical)} \\[2ex] - - T & ::= & & \mbox{(\textbf{tacticals})} \\ - & & \APPLY{tac} & \mbox{(tactic application)} \\ - & | & \SKIP & \mbox{(closed goal skipping)} \\ -\end{array} -\] - -\subsection{Status} - -\[ -\begin{array}{rcll} - \mathit{status} & = & \xi\times\Gamma\times\tau\times\kappa & \\ - \xi & = & \langle n,\alpha\rangle~\LIST& \mbox{(metasenv)} \\ - \Gamma & = & \GOALSWITCH~\LIST~\STACK & \mbox{(context)} \\ - \GOALSWITCH & = & \OPEN{n} \quad | \quad \CLOSED{n} & \\ - \tau & = & \GOAL~\LIST~\STACK & \mbox{(todo)} \\ - \kappa & = & \GOAL~\LIST~\STACK & \mbox{(dot continuations)} \\ -\end{array} -\] - -\subsection{Semantics} - -\[ -\begin{array}{rcll} - \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} & - \mbox{(continuationals semantics)} \\ - \TSEMOP{\cdot} & : & T -> \xi -> \GOALSWITCH -> - \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tacticals semantics)} \\ -\end{array} -\] - -\[ -\begin{array}{rcl} - \mathit{filter} & : & (\alpha->\BOOL)->\alpha~\LIST->\alpha~\LIST \\ - \mathit{map} & : & (\alpha->\beta)->\alpha~\LIST->\beta~\LIST \\ - \mathit{deep\_map} & : - & (\alpha->\beta)->\alpha~\LIST~\STACK->\beta~\LIST~\STACK \\ - \in & : & \alpha->\alpha~\LIST->\BOOL \\ - \cup & : & \alpha~\LIST->\alpha~\LIST->\alpha~\LIST \\ - \setminus & : & \alpha~\LIST->\alpha~\LIST->\alpha~\LIST \\ -\end{array} -\] - -\[ -\begin{array}{rcl} - \mathit{apply\_tac} & : & \mathit{tac} -> \xi -> \GOAL -> - \xi\times\GOAL~\LIST\times\GOAL~\LIST \\[1ex] -% \ISCLOSEDFUN & : & \GOALSWITCH -> \BOOL \\ - \ISOPENFUN & : & \GOALSWITCH -> \BOOL \\ - \CLOSEFUN & : & \GOALSWITCH -> \GOALSWITCH \\[1ex] -% \OPENFUN & : & \GOAL -> \GOALSWITCH \\[1ex] - \GOALOFFUN & : & \GOALSWITCH -> \GOAL \\[1ex] - \mathit{deep\_close} & : - & \GOAL~\LIST -> \GOALSWITCH~\STACK -> \GOALSWITCH~\STACK \\[1ex] -\end{array} -\] - -\[ -\begin{array}{rcl} - \DEEPCLOSEFUN{G}{\Gamma} - & = - & \MAPFUN{\mathit{fold} - (\lambda g.\lambda acc. - \mathit{if}~\GOALOFFUN(g)\in G~\land\ISOPENFUN(g)~ - \mathit{then}~[]~ - \mathit{else}~[g]\cup\mathit{acc}) - []}{\Gamma} -\end{array} -\] - -\[ -\begin{array}{rlcc} - \TSEM{\APPLY{tac}}{\xi}{\OPEN{n}} & = - & \mathit{apply\_tac}(\mathit{tac},\xi,n) & \\ - \TSEM{\SKIP}{\xi}{\CLOSED{n}} & = & \langle \xi, [], [n]\rangle & \\ -\end{array} -\] - -\[ -\begin{array}{rcl} - \SEM{\TACTICAL{T}}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa} - \quad (n\geq 1) - & = - & \langle\xi_n, - \MAPFUN{\mathtt{Open}}{G^O_n}::\DEEPCLOSEFUN{G^C_n}{\Gamma}, - \tau\setminus G^C_n,\kappa\setminus G^O_n\rangle - \\[1ex] - - \multicolumn{3}{l}{\hspace{2em}\mathit{where} ~ - \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 - & g_{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 - & g_{i+1}\not\in G^C_i \\ - & & \mathit{where} ~ \langle\xi,G^O,G^C\rangle=\TSEM{T}{\xi_i}{g_{i+1}} - \\ - \end{array} - \right. - } - \\[2ex] - - \SEM{C_1 ~ \SEMICOLON ~ C_2}{\xi}{\Gamma}{\tau}{\kappa} - & = - & \SEM{C_2}{\xi'}{\Gamma'}{\tau'}{\kappa'} - \\[1ex] - - & & \mathit{where} ~ - \langle\xi',\Gamma',\tau',\kappa',\rangle = - \SEM{C_1}{\xi}{\Gamma}{\tau}{\kappa} - \\[2ex] - - \SEM{C~\DOT~}{\xi}{\Gamma}{\tau}{\kappa} - & = - & \langle \xi'', \Gamma'', \tau'', \kappa'' \rangle - \\[1ex] - - \multicolumn{3}{l}{\hspace{2em}\mathit{where} ~ - \langle \xi',G::\Gamma',\tau',K::\kappa' \rangle - = \SEM{C}{\xi}{\Gamma}{\tau}{\kappa}} - \\[1ex] - - \multicolumn{3}{l}{\hspace{2em}\mathit{and} ~ - \langle \xi'', \Gamma'', \tau'', \kappa'' \rangle = - \left\{ - \begin{array}{ll} - \langle \xi', [g]::\Gamma', \tau', (\MAPFUN{\GOALOFFUN}{G'}\cup K)::\kappa' - \rangle - & \FILTERFUN{\ISOPENFUN}{G} = g::G' - \\ - \langle \xi', [\mathtt{Open}~n]::\Gamma', \tau', K'::\kappa' \rangle - & \FILTERFUN{\ISOPENFUN}{G} = []~\land~K=n::K' - \end{array} - \right.} - \\[2ex] - - \SEM{~\BRANCH~}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa} - \quad (n\geq 2) - & = - & \langle\xi, [g_1]::[g_2;\dots;g_n]::\Gamma, []::\tau, []::\kappa\rangle - \\[2ex] - - \SEM{~\SHIFT~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa} - & = - & \langle\xi, - [g_i]::[g_{i+1};\dots;g_n]::\Gamma, - \tau'::\tau, - []::\kappa\rangle - \\[1ex] - - & & \mathit{where} ~ - \tau' = T\cup\MAPFUN{\GOALOFFUN}{\FILTERFUN{\ISOPENFUN}{G}}\cup K - \\[2ex] - - \SEM{~\MERGE~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa} - & = - & \langle \xi, \Gamma'::\Gamma, \tau, \kappa \rangle - \\[1ex] - - & & \mathit{where} ~ - \Gamma' = - T \cup\FILTERFUN{\ISOPENFUN}{G} - \cup[g_i;\dots;g_n] - \cup\MAPFUN{\mathtt{Open}}{K} - \\[2ex] - - \SEM{\SELECT{n_1,\dots,n_k}{C}}{\xi}{\Gamma}{\tau}{\kappa} - & = - & \langle \xi',\Gamma',\tau',\kappa' \rangle - \\[1ex] - - & & \mathit{where} ~ - \forall ~ i=1,\dots,k,~\exists ~ \alpha_i,~\langle n_i,\alpha_i\rangle \in \xi - \\[1ex] - - & & \mathit{and} ~ - \langle \xi', []::\Gamma', []::\tau', []::\kappa' \rangle - = \SEM{C}{\xi}{\MAPFUN{\mathtt{Open}}{[n_1;\dots;n_k]}::\Gamma}{[]::\tau}{[]::\kappa} - \\[2ex] - -\end{array} -\] +\input{body.tex} \end{document}