\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{\ENDFOCUS}{\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{\OLDTACTICAL}[1]{\ensuremath{\mathtt{old\_tactical}~\mathit{#1}}}
-\newcommand{\SELECT}[1]{\ensuremath{\mathtt{select} ~ #1}}
-\newcommand{\ENDSELECT}[1]{\ensuremath{\mathtt{end}}}
-
-\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{[s_{#1};\cdots;s_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{\BRANCHTAG}{\ensuremath{\mathtt{B}}}
+\newcommand{\FOCUSTAG}{\ensuremath{\mathtt{S}}}
+
+\newlength{\sidecondlen}
+\setlength{\sidecondlen}{2cm}
\begin{document}
\maketitle
-\section{Foo}
+\section{Semantics}
\subsection{Language}
\[
\begin{array}{rcll}
- S & ::= & & \mbox{(\textbf{toplevel grammar})}\\
- & & \varepsilon & \\
- & | & T~ P~ S & \\[2ex]
-
- T & ::= & & \mbox{(\textbf{tactical})} \\
- & & \APPLY{tac} & \mbox{(tactic application)} \\
- & | & \SKIP & \mbox{(closed goal skipping)} \\
- & | & \OLDTACTICAL{tcl} & \mbox{(non step-by-step tactical)} \\
- & | & \SELECT{n_1,\dots,n_k}{S} & \mbox{(select)} \\[2ex]
-
- P & ::= & & \mbox{(\textbf{punctuation})} \\
- & & \DOT & \mbox{(dot)} \\
+ S & ::= & & \mbox{(\textbf{continuationals})}\\
+ & & \TACTIC{T} & \mbox{(tactic)}\\[2ex]
+ & | & \DOT & \mbox{(dot)} \\
& | & \SEMICOLON & \mbox{(semicolon)} \\
& | & \BRANCH & \mbox{(branch)} \\
& | & \SHIFT & \mbox{(shift)} \\
- & | & \MERGE ~ M & \mbox{(merge)} \\[2ex]
-
- M & ::= & & \mbox{(\textbf{merge-punctuation})} \\
- & & \varepsilon & \\
- & | & \MERGE ~ M& \mbox{(multi-merge)} \\
- & | & \DOT & \mbox{(merge and choose)} \\[2ex]
-
+ & | & \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}
\]
\[
\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)} \\
+ \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 -> \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 \\
+ \TSEMOP{\cdot} & : & T -> \xi -> \SWITCH ->
+ \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tactics semantics)} \\
\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}
+ \mathit{apply\_tac} & : & T -> \xi -> \GOAL ->
+ \xi\times\GOAL~\LIST\times\GOAL~\LIST
\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 & \\
+ \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{\TACTICAL{T}}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
- \quad (n\geq 1)
+
+ \SEM{\TACTIC{T}}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
& =
- & \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
+ & \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{2em}\mathit{where} ~
+ \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_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_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
- & g_{i+1}\not\in G^C_i \\
- & & \mathit{where} ~ \langle\xi,G^O,G^C\rangle=\TSEM{T}{\xi_i}{g_{i+1}}
+ & \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{C_1 ~ \SEMICOLON ~ C_2}{\xi}{\Gamma}{\tau}{\kappa}
+ \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S}
& =
- & \SEM{C_2}{\xi'}{\Gamma'}{\tau'}{\kappa'}
+ & \langle \xi, \ENTRY{s_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle
\\[1ex]
-
- & & \mathit{where} ~
- \langle\xi',\Gamma',\tau',\kappa',\rangle =
- \SEM{C_1}{\xi}{\Gamma}{\tau}{\kappa}
+ & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN
\\[2ex]
- \SEM{C~\DOT~}{\xi}{\Gamma}{\tau}{\kappa}
+ \SEM{~\DOT~}{\ENTRY{[]}{\tau}{s::\kappa}{t}::S}
& =
- & \langle \xi'', \Gamma'', \tau'', \kappa'' \rangle
- \\[1ex]
+ & \langle \xi, \ENTRY{\Gamma}{\tau}{\kappa}{t}::S \rangle
+ \\[2ex]
- \multicolumn{3}{l}{\hspace{2em}\mathit{where} ~
- \langle \xi',G::\Gamma',\tau',K::\kappa' \rangle
- = \SEM{C}{\xi}{\Gamma}{\tau}{\kappa}}
- \\[1ex]
+ \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[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.}
+ \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{~\BRANCH~}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
- \quad (n\geq 2)
+ \SEM{~\SHIFT~}
+ {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t}::S}
& =
- & \langle\xi, [g_1]::[g_2;\dots;g_n]::\Gamma, []::\tau, []::\kappa\rangle
+ & \langle
+ \xi, \ENTRY{s_1}{[]}{[]}{\BRANCHTAG}
+ ::\ENTRY{\GIN[2]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t}::S
+ \rangle
\\[2ex]
- \SEM{~\SHIFT~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
+ \SEM{\POS{i}}
+ {\ENTRY{[s]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
& =
- & \langle\xi,
- [g_i]::[g_{i+1};\dots;g_n]::\Gamma,
- \tau'::\tau,
- []::\kappa\rangle
+ & \langle \xi, \ENTRY{s_i}{[]}{[]}{\BRANCHTAG}
+ ::\ENTRY{s_i :: (\Gamma'\setminus [s_i])}{\tau'}{\kappa'}{t'}::S \rangle
\\[1ex]
-
- & & \mathit{where} ~
- \tau' = T\cup\MAPFUN{\GOALOFFUN}{\FILTERFUN{\ISOPENFUN}{G}}\cup K
+ & & \mathrm{where} ~ \langle i,s'\rangle = s_i\in \Gamma'~\land~\ISFRESH(s)
\\[2ex]
- \SEM{~\MERGE~}{\xi}{G::[g_i;\dots;g_n]::\Gamma}{T::\tau}{K::\kappa}
+ \SEM{\POS{i}}
+ {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}
+ ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
& =
- & \langle \xi, \Gamma'::\Gamma, \tau, \kappa \rangle
+ & \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]
- & & \mathit{where} ~
- \Gamma' =
- T \cup\FILTERFUN{\ISOPENFUN}{G}
- \cup[g_i;\dots;g_n]
- \cup\MAPFUN{\mathtt{Open}}{K}
+ \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{\SELECT{n_1,\dots,n_k}{C}}{\xi}{\Gamma}{\tau}{\kappa}
+ \SEM{\FOCUS{g_1,\dots,g_n}}{S}
& =
- & \langle \xi',\Gamma',\tau',\kappa' \rangle
+ & \langle \xi, \ENTRY{[\OPEN~g_1;\cdots;\OPEN~g_n]}{[]}{[]}{\FOCUSTAG}::S
+ \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}
+ & & \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}
\]
projects / helm.git / commitdiff