X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fdoc%2Fmain.tex;h=00208b0c25724c2efac60938aae49d77332067c4;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=15091f009652379c7899f998d1482bd4ec694e1a;hpb=3d5c86473cd2549335e7ee99600b0aaf499ca651;p=helm.git diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex index 15091f009..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} @@ -23,7 +23,7 @@ \newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}} \newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}} \newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}} -\newcommand{\ENDFOCUS}{\ensuremath{\mathtt{unfocus}}} +\newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}} \newcommand{\SKIP}{\MATHTT{skip}} \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}} @@ -42,7 +42,7 @@ \newcommand{\ENTRY}[4]{\langle#1,#2,#3,#4\rangle} \newcommand{\TSEM}[3]{\TSEMOP{#1}_{#2,#3}} -\newcommand{\GIN}[1][1]{\ensuremath{[s_{#1};\cdots;s_n]}} +\newcommand{\GIN}[1][1]{\ensuremath{[l_{#1};\cdots;l_n]}} \newcommand{\ZEROPOS}{\MATHIT{zero\_pos}} \newcommand{\INITPOS}{\MATHIT{init\_pos}} @@ -51,9 +51,11 @@ \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{S}}} +\newcommand{\FOCUSTAG}{\ensuremath{\mathtt{F}}} \newlength{\sidecondlen} \setlength{\sidecondlen}{2cm} @@ -61,203 +63,7 @@ \begin{document} \maketitle -\section{Semantics} - -\subsection{Language} - -\[ -\begin{array}{rcll} - S & ::= & & \mbox{(\textbf{continuationals})}\\ - & & \TACTIC{T} & \mbox{(tactic)}\\[2ex] - & | & \DOT & \mbox{(dot)} \\ - & | & \SEMICOLON & \mbox{(semicolon)} \\ - & | & \BRANCH & \mbox{(branch)} \\ - & | & \SHIFT & \mbox{(shift)} \\ - & | & \POS{i} & \mbox{(relative positioning)} \\ - & | & \MERGE & \mbox{(merge)} \\[2ex] - & | & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\ - & | & \ENDFOCUS & \mbox{(unfocus)} \\[2ex] - T & : := & & \mbox{(\textbf{tactics})}\\ - & & \SKIP & \mbox{(skip)} \\ - & | & \mathtt{reflexivity} & \\ - & | & \mathtt{apply}~t & \\ - & | & \dots & -\end{array} -\] - -\subsection{Status} - -\[ -\begin{array}{rcll} - \SWITCH & = & \OPEN~\mathit{goal} ~ | ~ \CLOSED~\mathit{goal} & \\ - \mathit{locator} & = & \INT\times\SWITCH & \\ - \mathit{tag} & = & \BRANCHTAG ~ | ~ \FOCUSTAG \\[2ex] - - \xi & = & (\INT\times\alpha)~\LIST& \mbox{(metasenv)} \\ - \Gamma & = & \mathit{locator}~\LIST & \mbox{(context)} \\ - \tau & = & \SWITCH~\LIST & \mbox{(todo)} \\ - \kappa & = & \SWITCH~\LIST & \mbox{(dot's future)} \\[2ex] - - \mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST - \\[2ex] - - \mathit{status} & = & \xi\times\mathit{stack} \\ -\end{array} -\] - -\paragraph{Utilities} -\begin{itemize} - \item \ZEROPOS: map $g -> 0, \OPEN~g$ - \item \INITPOS: map $g -> i, \OPEN~g$ - \item \ISFRESH: $\OPEN~g, 0 -> true | \_ -> false$ - \item \FILTEROPEN: $G -> \FILTER(\ISOPEN,G)$ - \item \DEEPCLOSE: prende uno stack ed un insieme di goal da chiudere, traversa - lo stack rimuovendo le occorrenze dei goal da $\tau$ e $\kappa$ e marcandole - chiuse in $\Gamma$ -\end{itemize} - -\paragraph{Invariants} -\begin{itemize} - \item $\forall \ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s \in\tau\cup\kappa, - \exists g, s = \OPEN~g$ (i goal in $\tau$ e $\kappa$ sono aperti) - \item la lista dei goal nel metasenv contiene tutti e soli i goal presenti - sullo stack - \item lo stack puo' contenere goal duplicati nel caso di uso della select -\end{itemize} - -\subsection{Semantics} - -\[ -\begin{array}{rcll} - \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} & - \mbox{(continuationals semantics)} \\ - \TSEMOP{\cdot} & : & T -> \xi -> \SWITCH -> - \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tactics semantics)} \\ -\end{array} -\] - -\[ -\begin{array}{rcl} - \mathit{apply\_tac} & : & T -> \xi -> \GOAL -> - \xi\times\GOAL~\LIST\times\GOAL~\LIST -\end{array} -\] - -\[ -\begin{array}{rlcc} - \TSEM{T}{\xi}{\OPEN~g} & = & \mathit{apply\_tac}(T,\xi,n) & T\neq\SKIP\\ - \TSEM{\SKIP}{\xi}{\CLOSED~g} & = & \langle \xi, [], [g]\rangle & -\end{array} -\] - -\[ -\begin{array}{rcl} - - \SEM{\TACTIC{T}}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S} - & = - & \langle - \xi_n, - \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t} - :: \DEEPCLOSE(G^c_n,S) - \rangle - \\[1ex] - - \multicolumn{3}{l}{\hspace{\sidecondlen}\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 - & s_{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 - & s_{i+1}\not\in G^c_i \\[1ex] - & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{s_{i+1}} - \\ - \end{array} - \right. - } - \\[2ex] - - \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S} - & = - & \langle \xi, \ENTRY{s_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle - \\[1ex] - & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN - \\[2ex] - - \SEM{~\DOT~}{\ENTRY{[]}{\tau}{s::\kappa}{t}::S} - & = - & \langle \xi, \ENTRY{\Gamma}{\tau}{\kappa}{t}::S \rangle - \\[2ex] - - \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[1ex] - - \SEM{~\BRANCH~}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S} - \quad - & = - & \langle\xi, \ENTRY{s_1'}{[]}{[]}{\BRANCHTAG} - ::\ENTRY{[s_2';\cdots;s_n']}{\tau}{\kappa}{t}::S - \\[1ex] - & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[s_1';\cdots;s_n'] - \\[2ex] - - \SEM{~\SHIFT~} - {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t}::S} - & = - & \langle - \xi, \ENTRY{s_1}{[]}{[]}{\BRANCHTAG} - ::\ENTRY{\GIN[2]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t}::S - \rangle - \\[2ex] - - \SEM{\POS{i}} - {\ENTRY{[s]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S} - & = - & \langle \xi, \ENTRY{s_i}{[]}{[]}{\BRANCHTAG} - ::\ENTRY{s_i :: (\Gamma'\setminus [s_i])}{\tau'}{\kappa'}{t'}::S \rangle - \\[1ex] - & & \mathrm{where} ~ \langle i,s'\rangle = s_i\in \Gamma'~\land~\ISFRESH(s) - \\[2ex] - - \SEM{\POS{i}} - {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG} - ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S} - & = - & \langle \xi, \ENTRY{s_i}{[]}{[]}{\BRANCHTAG} - ::\ENTRY{\Gamma'\setminus [s_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S - \rangle - \\[1ex] - & & \mathrm{where} ~ \langle i, s'\rangle = s_i\in \Gamma' - \\[2ex] - - \SEM{~\MERGE~} - {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'} - ::S} - & = - & \langle \xi, - \ENTRY{\tau\cup\FILTEROPEN(\Gamma)\cup\Gamma'\cup\kappa}{\tau'}{\kappa'}{t'} - :: S - \rangle - \\[2ex] - - \SEM{\FOCUS{g_1,\dots,g_n}}{S} - & = - & \langle \xi, \ENTRY{[\OPEN~g_1;\cdots;\OPEN~g_n]}{[]}{[]}{\FOCUSTAG}::S - \rangle - \\[1ex] - & & \mathrm{where} ~ - \forall ~ i=1,\dots,n,~\exists~\alpha_i,n_i,~\langle n_i,\alpha_i\rangle\in\xi - \\[2ex] - - \SEM{\ENDFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S} - & = - & \langle \xi, S\rangle \\[2ex] - -\end{array} -\] +\input{body.tex} \end{document}