@@ -130,6 +130,11 @@ either indicates success, or reports an error $\MO{Err}$:
130130\RW{data}\:\MO{Result}\:\vt\:=\:\MO{Success}\:\vt\:\mid\:\MO{Failure}\:\MO{Err}
131131}
132132
133+\noindent
134+If any operation fails during a proof (e.g. a subterm fails to type check)
135+then the entire proof fails (i.e. returns $\MO{Failure}\:\ve$ with some error
136+message $\ve$) unless otherwise handled.
137+
133138The \texttt{Elab} monad supports various operations for querying and updating
134139the proof state, manipulating terms, generating fresh names, etc. However, we
135140will describe \Idris{} elaboration in terms of meta-operations on the proof
@@ -225,8 +230,9 @@ $\ve$, typically arising from unification.
225230\end{itemize}
226231
227232\noindent
228−Additionally, we have $\MO{Focus}$, $\MO{Unfocus}$ and $\MO{NewHole}$
229−operations which manipulate
233+Additionally, we have $\MO{Focus}$, $\MO{Unfocus}$, $\MO{NewHole}$
234+and $\MO{NextHole}$
235+operations which manipulate and inspect
230236the hole queue. $\MO{Focus}\:\vn$ moves a hole to the head of the hole queue:
231237
232238\DM{
@@ -249,13 +255,20 @@ end of the hole queue:
249255
250256\noindent
251257$\MO{NewHole}$ declares that a new hole has been created and is to be solved
252−next:
258+next, and $\MO{NextHole}$ returns the next hole to be solved:
253259
254260\DM{
261+\AR{
255262\MO{NewHole}\:=\:\RW{do}\:\AR{
256263(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\
257264\MO{Put}\:(\vC,\Delta,\vP,\vn;\vQ)\\
258265}
266+\\
267+\MO{NextHole}\:=\:\RW{do}\:\AR{
268+(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\
269+\MO{Return}\:\vn
270+}
271+}
259272}
260273
261274\noindent
@@ -279,7 +292,7 @@ well-typed, with a type convertible to the type of $\vt$.
279292Tactics may also have the side effect of updating the proof state,
280293therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
281294
282−Tactics are executed by a higher level meta-operation $\MO{RunTac}$,
295+Tactics are executed by a higher level meta-operation $\MO{Tactic}$,
283296given in Figure \ref{runtac} which
284297locates the appropriate sub-term, applies the tactic with the context
285298local to this sub-term, and
@@ -290,7 +303,43 @@ tactic.
290303% added to the \remph{head} of the hole queue.
291304
292305\FFIG{
293−\mbox{\textbf{RunTac definition goes here}}
306+\AR{
307+\MO{Tactic}\:\VV{tac}\:=\:\RW{do}\:\AR{
308+\ve\Gets\MO{Term}\\
309+\vh\Gets\MO{NextHole}\\
310+\ve'\Gets\MO{Tactic'}\:\langle\rangle\:\ve\:\VV{tac}\:\vh\\
311+\MO{SetTerm}\:\ve'
312+}
313+\medskip
314+\\
315+\PA{\A\A\A}{
316+\RW{where} \\
317+& \MO{Tactic'} & \Gamma & (\hole{\vx}{\vT}\SC\ve)
318+& \MoRet{\VV{tac}_\Gamma\:(\hole{\vx}{\vT}\SC\ve)\hg\mbox{if}\:\vx=\vh} \\
319+& \MO{Tactic'} & \Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve)
320+& \MoRet{\VV{tac}_\Gamma\:(\guess{\vx}{\vT}{\vv}\SC\ve)\hg\mbox{if}\:\vx=\vh} \\
321+& \MO{Tactic'} & \Gamma & (\lam{\vx}{\vT}\SC\ve)
322+& \MoRet{
323+\RW{do}\: \AR{\vT'\Gets\:\MO{Tactic'}\:\Gamma\:\vT\\
324+\lam{\vx}{\vT'}\SC \MO{Tactic'}\:(\Gamma;\lam{\vx}{\vT'})\:\ve}
325+}
326+\\
327+& \MO{Tactic'} & \Gamma & (\all{\vx}{\vT}\SC\ve)
328+& \MoRet{
329+\RW{do}\: \AR{\vT'\Gets\:\MO{Tactic'}\:\Gamma\:\vT\\
330+\all{\vx}{\vT'}\SC \MO{Tactic'}\:(\Gamma;\all{\vx}{\vT'})\:\ve}
331+}
332+\\
333+& \MO{Tactic'} & \Gamma & (\LET\:\vx\defq\vt\Hab\vT\SC\ve)
334+& \MoRet{\RW{do}\:\AR{\vt'\Gets\:\MO{Tactic'}\:\Gamma\:\vt\\
335+\vT'\Gets\:\MO{Tactic'}\:\Gamma\:\vT\\
336+\LET\:\vx\defq\vt'\Hab\vT'\SC
337+\MO{Tactic'}\:(\Gamma;\LET\:\vx\defq\vt'\Hab\vT')\:\ve}} \\
338+& \MO{Tactic'} & \Gamma & (\vf\:\va) &
339+\MoRet{\MO{Return}\:(\MO{Tactic'}\:\Gamma\:\vf)\: (\MO{Tactic'}\:\Gamma\:\va)}\\
340+& \MO{Tactic'} & \Gamma & \vt & \MoRet{\MO{Return}\:\vt}
341+}
342+}
294343}
295344{Applying tactics to the proof state}
296345{runtac}
@@ -446,8 +495,10 @@ handle failure using the $\MO{Try}$ tactic combinator:
446495\DM{
447496\PA{\A\A\A}{
448497\MO{Try}_\Gamma & \VV{t1} & \VV{t2} & \vt &
449− \MoRet{\AR{\VV{t1}_\Gamma\:\vt\hg\mbox{(if $\VV{t1}$ succeeds)} \\
450− \VV{t2}_\Gamma\:\vt\hg\mbox{(otherwise)}}}
498+ \MoRet{\RW{case}\:\AR{\VV{t1}_\Gamma\:\vt\:\RW{of}\\
499+ \MO{Success}\:\vt'\cq\MO{Success}\:\vt'\\
500+ \MO{Failure}\:\_\cq\VV{t2}_\Gamma\:\vt\\
501+ }}
451502}
452503}
453504
@@ -577,7 +628,7 @@ building the right hand side.
577628
578629\subsubsection{Example}
579630
580−To illustrate how tactics are applied, using $\MO{RunTac}$, to build a
631+To illustrate how tactics are applied, using $\MO{Tactic}$, to build a
581632complete term by refining a proof state, let us consider the following
582633\TT{} definition for the identify function:
583634
@@ -591,7 +642,7 @@ complete term by refining a proof state, let us consider the following
591642We can build $\FN{id}$ either as a complete term, or by applying a sequence of
592643tactics. To achieve this, we create a proof state initialised with the type of
593644$\FN{id}$ and apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using
594−$\MO{RunTac}$. Note that the types on each $\MO{Lambda}$ are taken from
645+$\MO{Tactic}$. Note that the types on each $\MO{Lambda}$ are taken from
595646the goal type.
596647
597648\DM{
@@ -599,14 +650,14 @@ the goal type.
599650\MO{MkId}\:\mq\:\RW{do}\:
600651 \AR{
601652 \MO{NewProof}\:\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA \\
602− \MO{RunTac}\;\MO{Attack} \\
603− \MO{RunTac}\;(\MO{Lambda}\;\vA) \\
604− \MO{RunTac}\;\MO{Attack} \\
605− \MO{RunTac}\;(\MO{Lambda}\;\va) \\
606− \MO{RunTac}\;(\MO{Fill}\;\va)\\
607− \MO{RunTac}\;\MO{Solve}\\
608− \MO{RunTac}\;\MO{Solve}\\
609− \MO{RunTac}\;\MO{Solve}\\
653+ \MO{Tactic}\;\MO{Attack} \\
654+ \MO{Tactic}\;(\MO{Lambda}\;\vA) \\
655+ \MO{Tactic}\;\MO{Attack} \\
656+ \MO{Tactic}\;(\MO{Lambda}\;\va) \\
657+ \MO{Tactic}\;(\MO{Fill}\;\va)\\
658+ \MO{Tactic}\;\MO{Solve}\\
659+ \MO{Tactic}\;\MO{Solve}\\
660+ \MO{Tactic}\;\MO{Solve}\\
610661 \MO{Term}
611662 }
612663}
@@ -737,9 +788,9 @@ $\MO{Attack}$/$\MO{Solve}$ pairs are unnecessary in this case, as the term
737788is already in a form suitable for introduction. However, we retain these for
738789uniform treatment of introductions.
739790
740−To aid readability, we will elide $\MO{RunTac}$, and use a semi-colon to indicate
791+To aid readability, we will elide $\MO{Tactic}$, and use a semi-colon to indicate
741792sequencing --- in the implementation we use wrapper functions for each tactic to
742−apply $\MO{RunTac}$.
793+apply $\MO{Tactic}$.
743794Using this convention, we can build $\FN{id}$'s type and definition as shown
744795in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof
745796state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term.