8 S & ::= & & \mbox{(\textbf{continuationals})}\\
9 & & \TACTIC{T} & \mbox{(tactic)}\\[2ex]
10 & | & \DOT & \mbox{(dot)} \\
11 & | & \SEMICOLON & \mbox{(semicolon)} \\
12 & | & \BRANCH & \mbox{(branch)} \\
13 & | & \SHIFT & \mbox{(shift)} \\
14 & | & \POS{i} & \mbox{(relative positioning)} \\
15 & | & \MERGE & \mbox{(merge)} \\[2ex]
16 & | & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\
17 & | & \UNFOCUS & \mbox{(unfocus)} \\[2ex]
18 & | & S ~ S & \mbox{(sequential composition)} \\[2ex]
19 T & : := & & \mbox{(\textbf{tactics})}\\
20 & & \SKIP & \mbox{(skip)} \\
21 & | & \mathtt{reflexivity} & \\
22 & | & \mathtt{apply}~t & \\
31 \xi & & & \mbox{(proof status)} \\
32 \mathit{goal} & & & \mbox{(proof goal)} \\[2ex]
34 \SWITCH & = & \OPEN~\mathit{goal} ~ | ~ \CLOSED~\mathit{goal} & \\
35 \mathit{locator} & = & \INT\times\SWITCH & \\
36 \mathit{tag} & = & \BRANCHTAG ~ | ~ \FOCUSTAG \\[2ex]
38 \Gamma & = & \mathit{locator}~\LIST & \mbox{(context)} \\
39 \tau & = & \mathit{locator}~\LIST & \mbox{(todo)} \\
40 \kappa & = & \mathit{locator}~\LIST & \mbox{(dot's future)} \\[2ex]
42 \mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST
45 \mathit{status} & = & \xi\times\mathit{stack} \\
51 \item $\ZEROPOS([g_1;\cdots;g_n]) =
52 [\langle 0,\OPEN~g_1\rangle;\cdots;\langle 0,\OPEN~g_n\rangle]$
53 \item $\INITPOS([\langle i_1,s_1\rangle;\cdots;\langle i_n,s_n\rangle]) =
54 [\langle 1,s_1\rangle;\cdots;\langle n,s_n\rangle]$
58 \mathit{true} & \mathrm{if} ~ s = \langle n, \OPEN~g\rangle\land n > 0 \\
59 \mathit{false} & \mathrm{otherwise} \\
62 \item $\FILTEROPEN(\mathit{locs})=
65 [] & \mathrm{if}~\mathit{locs} = [] \\
66 \langle i,\OPEN~g\rangle :: \FILTEROPEN(\mathit{tl})
67 & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} \\
68 \FILTEROPEN(\mathit{tl})
69 & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
72 \item $\REMOVEGOALS(G,\mathit{locs}) =
75 [] & \mathrm{if}~\mathit{locs} = [] \\
76 \REMOVEGOALS(G,\mathit{tl})
77 & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl}
79 hd :: \REMOVEGOALS(G,\mathit{tl})
80 & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
83 \item $\DEEPCLOSE(G,S)$: (intuition) given a set of goals $G$ and a stack $S$
84 it returns a new stack $S'$ identical to the given one with the exceptions
85 that each locator whose goal is in $G$ is marked as closed in $\Gamma$ stack
86 components and removed from $\tau$ and $\kappa$ components.
87 \item $\GOALS(S)$: (inutition) return all goals appearing in whatever position
88 on a given stack $S$, appearing in an \OPEN{} switch.
91 \paragraph{Invariants}
93 \item $\forall~\mathrm{entry}~\ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s
94 \in\tau\cup\kappa, \exists g, s = \OPEN~g$ (each locator on the stack in
95 $\tau$ and $\kappa$ components has an \OPEN~switch).
96 \item Unless \FOCUS{} is used the stack contains no duplicate goals.
97 \item $\forall~\mathrm{locator}~l\in\Gamma \mbox{(with the exception of the
98 top-level $\Gamma$)}, \ISFRESH(l)$.
101 \subsection{Semantics}
105 \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} &
106 \mbox{(continuationals semantics)} \\
107 \TSEMOP{\cdot} & : & T -> \xi -> \SWITCH ->
108 \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tactics semantics)} \\
114 \mathit{apply\_tac} & : & T -> \xi -> \GOAL ->
115 \xi\times\GOAL~\LIST\times\GOAL~\LIST
121 \TSEM{T}{\xi}{\OPEN~g} & = & \mathit{apply\_tac}(T,\xi,n) & T\neq\SKIP\\
122 \TSEM{\SKIP}{\xi}{\CLOSED~g} & = & \langle \xi, [], [g]\rangle &
129 \SEM{\TACTIC{T}}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
133 \ENTRY{\Gamma'}{\tau'}{\kappa'}{t}
134 % \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t}
135 :: \DEEPCLOSE(G^c_n,S)
138 \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~ n\geq 1}
140 \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
141 \Gamma' = \ZEROPOS(G^o_n)
142 \land \tau' = \REMOVEGOALS(G^c_n,\tau)
143 \land \kappa' = \REMOVEGOALS(G^o_n,\kappa)
146 \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
149 \langle\xi_0, G^o_0, G^c_0\rangle & = & \langle\xi, [], []\rangle \\
150 \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle
152 & \langle\xi_i, G^o_i, G^c_i\rangle
153 & l_{i+1}\in G^c_i \\
154 \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle
156 & \langle\xi, (G^o_i\setminus G^c)\cup G^o, G^c_i\cup G^c\rangle
157 & l_{i+1}\not\in G^c_i \\[1ex]
158 & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{l_{i+1}} \\
164 \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S}
166 & \langle \xi, \ENTRY{l_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle
168 & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN \land n\geq 1
171 \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{l::\kappa}{t}::S}
173 & \langle \xi, \ENTRY{[l]}{\tau}{\kappa}{t}::S \rangle
175 & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=[]
178 \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[1ex]
180 \SEM{~\BRANCH~}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
183 & \langle\xi, \ENTRY{[l_1']}{[]}{[]}{\BRANCHTAG}
184 ::\ENTRY{[l_2';\cdots;l_n']}{\tau}{\kappa}{t}::S
186 & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[l_1';\cdots;l_n']
190 {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t'}
194 \xi, \ENTRY{[l_1]}{\tau\cup\FILTEROPEN(\Gamma)}{[]}{\BRANCHTAG}
195 ::\ENTRY{\GIN[2]}{\tau'}{\kappa'}{t'}::S
198 & & \mathrm{where} ~ n\geq 1
202 {\ENTRY{[l]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
204 & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
205 ::\ENTRY{l :: (\Gamma'\setminus [l_i])}{\tau'}{\kappa'}{t'}::S \rangle
207 & & \mathrm{where} ~ \langle i,l'\rangle = l_i\in \Gamma'~\land~\ISFRESH(l)
211 {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}
212 ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
214 & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
215 ::\ENTRY{\Gamma'\setminus [l_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S
218 & & \mathrm{where} ~ \langle i, l'\rangle = l_i\in \Gamma'
222 {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}
226 \ENTRY{\tau\cup\FILTEROPEN(\Gamma)\cup\Gamma'\cup\kappa}{\tau'}{\kappa'}{t'}
231 \SEM{\FOCUS{g_1,\dots,g_n}}{S}
233 & \langle \xi, \ENTRY{\ZEROPOS([g_1;\cdots;g_n])}{[]}{[]}{\FOCUSTAG}
238 \forall i=1,\dots,n,~g_i\in\GOALS(S)
241 \SEM{\UNFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S}
243 & \langle \xi, S\rangle \\[2ex]