-\documentclass[a4paper,draft]{article}
+\documentclass[a4paper]{article}
\usepackage{a4wide}
\usepackage{pifont}
\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}}
\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}}
\newcommand{\FILTEROPEN}{\MATHIT{filter\_open}}
\newcommand{\ISOPEN}{\MATHIT{is\_open}}
\newcommand{\DEEPCLOSE}{\MATHIT{deep\_close}}
+\newcommand{\REMOVEGOALS}{\MATHIT{remove\_goals}}
+\newcommand{\GOALS}{\MATHIT{goals}}
\newcommand{\BRANCHTAG}{\ensuremath{\mathtt{B}}}
-\newcommand{\FOCUSTAG}{\ensuremath{\mathtt{S}}}
+\newcommand{\FOCUSTAG}{\ensuremath{\mathtt{F}}}
\newlength{\sidecondlen}
\setlength{\sidecondlen}{2cm}
& | & \POS{i} & \mbox{(relative positioning)} \\
& | & \MERGE & \mbox{(merge)} \\[2ex]
& | & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\
- & | & \ENDFOCUS & \mbox{(unfocus)} \\[2ex]
+ & | & \UNFOCUS & \mbox{(unfocus)} \\[2ex]
+ & | & S ~ S & \mbox{(sequential composition)} \\[2ex]
T & : := & & \mbox{(\textbf{tactics})}\\
& & \SKIP & \mbox{(skip)} \\
& | & \mathtt{reflexivity} & \\
\[
\begin{array}{rcll}
+ \xi & & & \mbox{(proof status)} \\
+ \mathit{goal} & & & \mbox{(proof goal)} \\[2ex]
+
\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]
+ \tau & = & \mathit{locator}~\LIST & \mbox{(todo)} \\
+ \kappa & = & \mathit{locator}~\LIST & \mbox{(dot's future)} \\[2ex]
\mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST
\\[2ex]
\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$
+ \item $\ZEROPOS([g_1;\cdots;g_n]) =
+ [\langle 0,\OPEN~g_1\rangle;\cdots;\langle 0,\OPEN~g_n\rangle]$
+ \item $\INITPOS([\langle i_1,s_1\rangle;\cdots;\langle i_n,s_n\rangle]) =
+ [\langle 1,\OPEN~s_1\rangle;\cdots;\langle n,\OPEN~s_n\rangle]$
+ \item $\ISFRESH(s) =
+ \left\{
+ \begin{array}{ll}
+ \mathit{true} & \mathrm{if} ~ s = \langle n, \OPEN~g\rangle\land n > 0 \\
+ \mathit{false} & \mathrm{otherwise} \\
+ \end{array}
+ \right.$
+ \item $\FILTEROPEN(\mathit{locs})=
+ \left\{
+ \begin{array}{ll}
+ [] & \mathrm{if}~\mathit{locs} = [] \\
+ \langle i,\OPEN~g\rangle :: \FILTEROPEN(\mathit{tl})
+ & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} \\
+ \FILTEROPEN(\mathit{tl})
+ & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
+ \end{array}
+ \right.$
+ \item $\REMOVEGOALS(G,\mathit{locs}) =
+ \left\{
+ \begin{array}{ll}
+ [] & \mathrm{if}~\mathit{locs} = [] \\
+ \REMOVEGOALS(G,\mathit{tl})
+ & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl}
+ \land g\in G\\
+ hd :: \REMOVEGOALS(G,\mathit{tl})
+ & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
+ \end{array}
+ \right.$
+ \item $\DEEPCLOSE(G,S)$: (intuition) given a set of goals $G$ and a stack $S$
+ it returns a new stack $S'$ identical to the given one with the exceptions
+ that each locator whose goal is in $G$ is marked as closed in $\Gamma$ stack
+ components and removed from $\tau$ and $\kappa$ components.
+ \item $\GOALS(S)$: (inutition) return all goals appearing in whatever position
+ on a given stack $S$.
\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
+ \item $\forall~\mathrm{entry}~\ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s
+ \in\tau\cup\kappa, \exists g, s = \OPEN~g$ (each locator on the stack in
+ $\tau$ and $\kappa$ components has an \OPEN~switch).
+ \item Unless \FOCUS{} is used the stack contains no duplicate goals.
\end{itemize}
\subsection{Semantics}
& =
& \langle
\xi_n,
- \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t}
+ \ENTRY{\Gamma'}{\tau'}{\kappa'}{t}
+% \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} ~
+ \Gamma' = \ZEROPOS(G^o_n)
+ \land \tau' = \REMOVEGOALS(G^c_n,\tau)
+ \land \kappa' = \REMOVEGOALS(G^o_n,\kappa)
+ }
+ \\[1ex]
+ \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
\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 \\
+ & l_{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}}
- \\
+ & l_{i+1}\not\in G^c_i \\[1ex]
+ & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{l_{i+1}} \\
\end{array}
\right.
}
- \\[2ex]
+ \\[6ex]
\SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S}
& =
- & \langle \xi, \ENTRY{s_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle
+ & \langle \xi, \ENTRY{l_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle
\\[1ex]
- & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN
+ & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN \land n\geq 1
\\[2ex]
- \SEM{~\DOT~}{\ENTRY{[]}{\tau}{s::\kappa}{t}::S}
+ \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{l::\kappa}{t}::S}
& =
- & \langle \xi, \ENTRY{\Gamma}{\tau}{\kappa}{t}::S \rangle
+ & \langle \xi, \ENTRY{[l]}{\tau}{\kappa}{t}::S \rangle
+ \\[1ex]
+ & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=[]
\\[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
+ & \langle\xi, \ENTRY{[l_1']}{[]}{[]}{\BRANCHTAG}
+ ::\ENTRY{[l_2';\cdots;l_n']}{\tau}{\kappa}{t}::S
\\[1ex]
- & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[s_1';\cdots;s_n']
+ & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[l_1';\cdots;l_n']
\\[2ex]
\SEM{~\SHIFT~}
- {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t}::S}
+ {\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
+ \xi, \ENTRY{[l_1]}{\tau\cup\FILTEROPEN(\Gamma)}{[]}{\BRANCHTAG}
+ ::\ENTRY{\GIN[2]}{\tau'}{\kappa'}{t'}::S
\rangle
+ \\[1ex]
+ & & \mathrm{where} ~ n\geq 1
\\[2ex]
- \SEM{\POS{i}}
- {\ENTRY{[s]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
+ \SEM{~\POS{i}~}
+ {\ENTRY{[l]}{[]}{[]}{\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
+ & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
+ ::\ENTRY{l :: (\Gamma'\setminus [l_i])}{\tau'}{\kappa'}{t'}::S \rangle
\\[1ex]
- & & \mathrm{where} ~ \langle i,s'\rangle = s_i\in \Gamma'~\land~\ISFRESH(s)
+ & & \mathrm{where} ~ \langle i,l'\rangle = l_i\in \Gamma'~\land~\ISFRESH(l)
\\[2ex]
- \SEM{\POS{i}}
+ \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
+ & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
+ ::\ENTRY{\Gamma'\setminus [l_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S
\rangle
\\[1ex]
- & & \mathrm{where} ~ \langle i, s'\rangle = s_i\in \Gamma'
+ & & \mathrm{where} ~ \langle i, l'\rangle = l_i\in \Gamma'
\\[2ex]
\SEM{~\MERGE~}
\SEM{\FOCUS{g_1,\dots,g_n}}{S}
& =
- & \langle \xi, \ENTRY{[\OPEN~g_1;\cdots;\OPEN~g_n]}{[]}{[]}{\FOCUSTAG}::S
+ & \langle \xi, \ENTRY{[\OPEN~g_1;\cdots;\OPEN~g_n]}{[]}{[]}{\FOCUSTAG}
+ ::\DEEPCLOSE(S)
\rangle
\\[1ex]
& & \mathrm{where} ~
- \forall ~ i=1,\dots,n,~\exists~\alpha_i,n_i,~\langle n_i,\alpha_i\rangle\in\xi
+ \forall i=1,\dots,n,~g_i\in\GOALS(S)
\\[2ex]
- \SEM{\ENDFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S}
+ \SEM{\UNFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S}
& =
& \langle \xi, S\rangle \\[2ex]
projects / helm.git / commitdiff