From: Stefano Zacchiroli Date: Mon, 3 Oct 2005 10:09:31 +0000 (+0000) Subject: restated ... X-Git-Tag: V_0_7_2_3~261 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f26b2b816de0744f666a0ab8ee26fa670ad6a1b8;p=helm.git restated ... --- diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex index 32c6832df..be235a2c1 100644 --- a/helm/ocaml/tactics/doc/main.tex +++ b/helm/ocaml/tactics/doc/main.tex @@ -8,10 +8,10 @@ \newcommand{\MATITA}{\ding{46}\textsf{\textbf{Matita}}} \title{Continuationals semantics for \MATITA} -\author{Enrico Tassi \qquad Stefano Zacchiroli \\ +\author{Claudio Sacerdoti Coen \quad Enrico Tassi \quad Stefano Zacchiroli \\ \small Department of Computer Science, University of Bologna \\ \small Mura Anteo Zamboni, 7 -- 40127 Bologna, ITALY \\ -\small \{\texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}} +\small \{\texttt{sacerdot}, \texttt{tassi}, \texttt{zacchiro}\}\texttt{@cs.unibo.it}} \newcommand{\DOT}{\mbox{\textbf{.}}} \newcommand{\SEMICOLON}{\mbox{\textbf{;}}} @@ -21,7 +21,7 @@ \newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}} \newcommand{\SKIP}{\ensuremath{\mathtt{skip}}} \newcommand{\TACTICAL}[1]{\ensuremath{\mathtt{tactical}~\mathit{#1}}} -\newcommand{\GOTO}[2]{\ensuremath{\mathtt{goal} ~ #1 ~ #2}} +\newcommand{\SELECT}[2]{\ensuremath{\mathtt{select} ~ #1 ~ #2}} \newcommand{\GOAL}{\ensuremath{\mathit{goal}}} \newcommand{\GOALSWITCH}{\ensuremath{\mathit{goal\_switch}}} @@ -40,11 +40,10 @@ \newcommand{\FILTERFUN}[2]{\FUN{filter}{#1,#2}} \newcommand{\MAPFUN}[2]{\FUN{map}{#1,#2}} \newcommand{\DEEPMAPFUN}[2]{\FUN{deep\_map}{#1,#2}} -% \newcommand{\ISCLOSEDFUN}{\ensuremath{\mathit{is\_closed}}} \newcommand{\ISOPENFUN}{\ensuremath{\mathit{is\_open}}} -% \newcommand{\OPENFUN}{\ensuremath{\mathit{open}}} \newcommand{\CLOSEFUN}{\ensuremath{\mathit{close}}} \newcommand{\GOALOFFUN}{\ensuremath{\mathit{goal\_of}}} +\newcommand{\DEEPCLOSEFUN}[2]{\FUN{deep\_close}{#1,#2}} \begin{document} \maketitle @@ -56,12 +55,12 @@ \[ \begin{array}{rcll} C & ::= & & \mbox{(\textbf{continuationals})} \\ - & & \DOT & \mbox{(dot)} \\ + & & C ~ \DOT & \mbox{(dot)} \\ & | & C ~ \SEMICOLON ~ C & \mbox{(semicolon)} \\ & | & \BRANCH & \mbox{(branch)} \\ & | & \SHIFT & \mbox{(shift)} \\ & | & \MERGE & \mbox{(merge)} \\ - & | & \GOTO{n}{C} & \mbox{(goto)} \\ + & | & \SELECT{n_1,\dots,n_k}{C} & \mbox{(select)} \\ & | & \TACTICAL{T} & \mbox{(tactical)} \\[2ex] T & ::= & & \mbox{(\textbf{tacticals})} \\ @@ -75,7 +74,7 @@ \[ \begin{array}{rcll} \mathit{status} & = & \xi\times\Gamma\times\tau\times\kappa & \\ - \xi & & & \mbox{(metasenv)} \\ + \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)} \\ @@ -96,17 +95,40 @@ \[ \begin{array}{rcl} - \mathit{apply\_tac} & : & \mathit{tac} -> \xi -> \GOAL -> - \xi\times\GOAL~\LIST\times\GOAL~\LIST \\[1ex] \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 \\[1ex] + & (\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 \\ + \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} \] @@ -121,9 +143,10 @@ \[ \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}::\DEEPMAPFUN{\CLOSEFUN}{G^C_n,\Gamma}, + \MAPFUN{\mathtt{Open}}{G^O_n}::\DEEPCLOSEFUN{G^C_n}{\Gamma}, \tau\setminus G^C_n,\kappa\setminus G^O_n\rangle \\[1ex] @@ -156,18 +179,32 @@ \SEM{C_1}{\xi}{\Gamma}{\tau}{\kappa} \\[2ex] - \SEM{~\DOT~}{\xi}{(g::G)::\Gamma}{\tau}{K::\kappa} + \SEM{C~\DOT~}{\xi}{\Gamma}{\tau}{\kappa} & = - & \langle\xi, [g]::\Gamma, \tau, - (\MAPFUN{\mathtt{Open}}{\FILTERFUN{\ISOPENFUN}{G}}\cup K)::\kappa\rangle - \\[2ex] + & \langle \xi'', \Gamma'', \tau'', \kappa'' \rangle + \\[1ex] - \SEM{~\DOT~}{\xi}{[]::\Gamma}{\tau}{(n::N)::\kappa} - & = - & \langle\xi, [\OPEN{n}]::\Gamma, \tau, N::\kappa\rangle + \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] @@ -176,29 +213,38 @@ & = & \langle\xi, [g_i]::[g_{i+1};\dots;g_n]::\Gamma, - (T\cup\MAPFUN{\GOALOFFUN}{\FILTERFUN{\ISOPENFUN}{G}}\cup K)::\tau, + \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, - (T - \cup\FILTERFUN{\ISOPENFUN}{G} - \cup[g_i;\dots;g_n] - \cup\MAPFUN{\mathtt{Open}}{K})::\Gamma, - \tau, - \kappa\rangle + & \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{\GOTO{n}{C}}{\xi}{\Gamma}{\tau}{\kappa} + \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}{[\OPEN{n}]::\Gamma}{[]::\tau}{[]::\kappa} + = \SEM{C}{\xi}{\MAPFUN{\mathtt{Open}}{[n_1;\dots;n_k]}::\Gamma}{[]::\tau}{[]::\kappa} \\[2ex] \end{array}