@@ -130,6 +130,11 @@ either indicates success, or reports an error $\MO{Err}$:
130\RW{data}\:\MO{Result}\:\vt\:=\:\MO{Success}\:\vt\:\mid\:\MO{Failure}\:\MO{Err}
130\RW{data}\:\MO{Result}\:\vt\:=\:\MO{Success}\:\vt\:\mid\:\MO{Failure}\:\MO{Err}
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.
133The \texttt{Elab} monad supports various operations for querying and updating
138The \texttt{Elab} monad supports various operations for querying and updating
134the proof state, manipulating terms, generating fresh names, etc. However, we
139the proof state, manipulating terms, generating fresh names, etc. However, we
135will describe \Idris{} elaboration in terms of meta-operations on the proof
140will describe \Idris{} elaboration in terms of meta-operations on the proof
@@ -225,8 +230,9 @@ $\ve$, typically arising from unification.
225\end{itemize}
230\end{itemize}
228−Additionally, we have $\MO{Focus}$, $\MO{Unfocus}$ and $\MO{NewHole}$
233+Additionally, we have $\MO{Focus}$, $\MO{Unfocus}$, $\MO{NewHole}$
229−operations which manipulate
235+operations which manipulate and inspect
230the hole queue. $\MO{Focus}\:\vn$ moves a hole to the head of the hole queue:
236the hole queue. $\MO{Focus}\:\vn$ moves a hole to the head of the hole queue:
@@ -249,13 +255,20 @@ end of the hole queue:
251$\MO{NewHole}$ declares that a new hole has been created and is to be solved
257$\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:
255\MO{NewHole}\:=\:\RW{do}\:\AR{
262\MO{NewHole}\:=\:\RW{do}\:\AR{
256(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\
263(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\
257\MO{Put}\:(\vC,\Delta,\vP,\vn;\vQ)\\
264\MO{Put}\:(\vC,\Delta,\vP,\vn;\vQ)\\
267+\MO{NextHole}\:=\:\RW{do}\:\AR{
268+(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\
@@ -279,7 +292,7 @@ well-typed, with a type convertible to the type of $\vt$.
279Tactics may also have the side effect of updating the proof state,
292Tactics may also have the side effect of updating the proof state,
280therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
293therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
282−Tactics are executed by a higher level meta-operation $\MO{RunTac}$,
295+Tactics are executed by a higher level meta-operation $\MO{Tactic}$,
283given in Figure \ref{runtac} which
296given in Figure \ref{runtac} which
284locates the appropriate sub-term, applies the tactic with the context
297locates the appropriate sub-term, applies the tactic with the context
285local to this sub-term, and
298local to this sub-term, and
@@ -290,7 +303,43 @@ tactic.
290% added to the \remph{head} of the hole queue.
303% added to the \remph{head} of the hole queue.
293−\mbox{\textbf{RunTac definition goes here}}
306+\AR{
307+\MO{Tactic}\:\VV{tac}\:=\:\RW{do}\:\AR{
309+\vh\Gets\MO{NextHole}\\
310+\ve'\Gets\MO{Tactic'}\:\langle\rangle\:\ve\:\VV{tac}\:\vh\\
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)
323+\RW{do}\: \AR{\vT'\Gets\:\MO{Tactic'}\:\Gamma\:\vT\\
324+\lam{\vx}{\vT'}\SC \MO{Tactic'}\:(\Gamma;\lam{\vx}{\vT'})\:\ve}
327+& \MO{Tactic'} & \Gamma & (\all{\vx}{\vT}\SC\ve)
329+\RW{do}\: \AR{\vT'\Gets\:\MO{Tactic'}\:\Gamma\:\vT\\
330+\all{\vx}{\vT'}\SC \MO{Tactic'}\:(\Gamma;\all{\vx}{\vT'})\:\ve}
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}
295{Applying tactics to the proof state}
344{Applying tactics to the proof state}
@@ -446,8 +495,10 @@ handle failure using the $\MO{Try}$ tactic combinator:
447\PA{\A\A\A}{
496\PA{\A\A\A}{
448\MO{Try}_\Gamma & \VV{t1} & \VV{t2} & \vt &
497\MO{Try}_\Gamma & \VV{t1} & \VV{t2} & \vt &
449− \MoRet{\AR{\VV{t1}_\Gamma\:\vt\hg\mbox{(if $\VV{t1}$ succeeds)} \\
498+ \MoRet{\RW{case}\:\AR{\VV{t1}_\Gamma\:\vt\:\RW{of}\\
499+ \MO{Success}\:\vt'\cq\MO{Success}\:\vt'\\
450− \VV{t2}_\Gamma\:\vt\hg\mbox{(otherwise)}}}
500+ \MO{Failure}\:\_\cq\VV{t2}_\Gamma\:\vt\\
@@ -577,7 +628,7 @@ building the right hand side.
578\subsubsection{Example}
629\subsubsection{Example}
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
581complete term by refining a proof state, let us consider the following
632complete term by refining a proof state, let us consider the following
582\TT{} definition for the identify function:
633\TT{} definition for the identify function:
@@ -591,7 +642,7 @@ complete term by refining a proof state, let us consider the following
591We can build $\FN{id}$ either as a complete term, or by applying a sequence of
642We can build $\FN{id}$ either as a complete term, or by applying a sequence of
592tactics. To achieve this, we create a proof state initialised with the type of
643tactics. To achieve this, we create a proof state initialised with the type of
593$\FN{id}$ and apply a series of $\MO{Lambda}$ and $\MO{Fill}$ operations using
644$\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
595the goal type.
646the goal type.
@@ -599,14 +650,14 @@ the goal type.
599\MO{MkId}\:\mq\:\RW{do}\:
650\MO{MkId}\:\mq\:\RW{do}\:
601 \MO{NewProof}\:\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA \\
652 \MO{NewProof}\:\all{\vA}{\Type}\SC\all{\va}{\vA}\SC\vA \\
602− \MO{RunTac}\;\MO{Attack} \\
653+ \MO{Tactic}\;\MO{Attack} \\
603− \MO{RunTac}\;(\MO{Lambda}\;\vA) \\
654+ \MO{Tactic}\;(\MO{Lambda}\;\vA) \\
604− \MO{RunTac}\;\MO{Attack} \\
655+ \MO{Tactic}\;\MO{Attack} \\
605− \MO{RunTac}\;(\MO{Lambda}\;\va) \\
656+ \MO{Tactic}\;(\MO{Lambda}\;\va) \\
606− \MO{RunTac}\;(\MO{Fill}\;\va)\\
657+ \MO{Tactic}\;(\MO{Fill}\;\va)\\
607− \MO{RunTac}\;\MO{Solve}\\
658+ \MO{Tactic}\;\MO{Solve}\\
608− \MO{RunTac}\;\MO{Solve}\\
659+ \MO{Tactic}\;\MO{Solve}\\
609− \MO{RunTac}\;\MO{Solve}\\
660+ \MO{Tactic}\;\MO{Solve}\\
610 \MO{Term}
661 \MO{Term}
@@ -737,9 +788,9 @@ $\MO{Attack}$/$\MO{Solve}$ pairs are unnecessary in this case, as the term
737is already in a form suitable for introduction. However, we retain these for
788is already in a form suitable for introduction. However, we retain these for
738uniform treatment of introductions.
789uniform treatment of introductions.
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
741sequencing --- in the implementation we use wrapper functions for each tactic to
792sequencing --- in the implementation we use wrapper functions for each tactic to
742−apply $\MO{RunTac}$.
793+apply $\MO{Tactic}$.
743Using this convention, we can build $\FN{id}$'s type and definition as shown
794Using this convention, we can build $\FN{id}$'s type and definition as shown
744in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof
795in Figure \ref{idelab}. Note that $\MO{Term}$ retrieves the proof term from the current proof
745state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term.
796state. Both $\MO{MkIdType}$ and $\MO{MkId}$ finish by returning a completed \TT{} term.