@@ -180,7 +180,7 @@ global context $\vC$, $\MO{NewProof}\;\vt$ sets up the proof state as:
180180
181181The local context is initially empty, and the initial hole queue is the $\vx$ standing for
182182the entire expression. The proof term is reset with the $\MO{NewTerm}$ operation.
183−In an existing proof state $(\vC, \Delta, \ve, \vQ)$,
183+In an existing proof state $(\vC, \Delta, \ve, \vP, \vQ)$,
184184$\MO{NewTerm}\;\vt$ discards the proof term and hole queue, and
185185updates the proof state to:
186186
@@ -217,6 +217,9 @@ may fail. We have the following primitive meta-operations:
217217$\Gamma$, returning its type.
218218$\MO{Check}$ will fail
219219if the expression is not well-typed.
220+\item $\MO{Convert}_\Gamma\;\ve_1\;\ve_2$, which checks that the well-typed
221+expressions $\ve_1$ and $\ve_2$ respect the cumulativity relation
222+(i.e. $\Gamma\proves\ve_1\cumul\ve_2$), and fails otherwise.
220223\item $\Eval\;\ve$, which evaluates a well-typed expression $\ve$ relative to a context
221224$\Gamma$, returning its normal form. $\MO{Normalise}$ reduces under binders,
222225but does not reduce definitions which are not total.
@@ -226,19 +229,20 @@ which attempts to unify $\ve_1$ and $\ve_2$ by finding the values with which
226229holes must be instantiated for $\ve_1$ and $\ve_2$ to be convertible relative
227230to $\Gamma$ (i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold).
228231\item $\Subst\;\vx\;\ve$, which instantiates a hole $\vx$ directly with a term
229−$\ve$, typically arising from unification.
232+$\ve$, typically arising from unification and removes $\vx$ from the hole
233+queue.
230234\end{itemize}
231235
232236\noindent
233−Additionally, we have $\MO{Focus}$, $\MO{Unfocus}$, $\MO{NewHole}$
234−and $\MO{NextHole}$
237+Additionally, we have $\MO{Focus}$, $\MO{Unfocus}$, $\MO{NewHole}$,
238+$\MO{NextHole}$ and $\MO{RemoveHole}$
235239operations which manipulate and inspect
236240the hole queue. $\MO{Focus}\;\vn$ moves a hole to the head of the hole queue:
237241
238242\DM{
239243\MO{Focus}\;\vn\;=\;\RW{do}\;\AR{
240−(\vC,\Delta,\vP,\vQ;\vn;\vQ')\gets\MO{Get}\\
241−\MO{Put}\;(\vC,\Delta,\vP,\vn;\vQ;\vQ')\\
244+(\vC,\Delta,\ve,\vP,\vQ;\vn;\vQ')\gets\MO{Get}\\
245+\MO{Put}\;(\vC,\Delta,\ve,\vP,\vn;\vQ;\vQ')\\
242246}
243247}
244248
@@ -248,25 +252,31 @@ end of the hole queue:
248252
249253\DM{
250254\MO{Unfocus}\;=\;\RW{do}\;\AR{
251−(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\
252−\MO{Put}\;(\vC,\Delta,\vP,\vQ;\vn)\\
255+(\vC,\Delta,\ve,\vP,\vn;\vQ)\gets\MO{Get}\\
256+\MO{Put}\;(\vC,\Delta,\ve,\vP,\vQ;\vn)\\
253257}
254258}
255259
256260\noindent
257261$\MO{NewHole}$ declares that a new hole has been created and is to be solved
258−next, and $\MO{NextHole}$ returns the next hole to be solved:
262+next; $\MO{NextHole}$ returns the next hole to be solved, and $\MO{RemoveHole}$
263+removes a hole from the head of the queue:
259264
260265\DM{
261266\AR{
262267\MO{NewHole}\;=\;\RW{do}\;\AR{
263268(\vC,\Delta,\vP,\vQ)\gets\MO{Get}\\
264−\MO{Put}\;(\vC,\Delta,\vP,\vn;\vQ)\\
269+\MO{Put}\;(\vC,\Delta,\ve,\vP,\vn;\vQ)\\
265270}
266271\\
267272\MO{NextHole}\;=\;\RW{do}\;\AR{
268−(\vC,\Delta,\vP,\vn;\vQ)\gets\MO{Get}\\
269−\MO{Return}\;\vn
273+(\vC,\Delta,\ve,\vP,\vn;\vQ)\gets\MO{Get}\\
274+\RW{return}\;\vn
275+}
276+\\
277+\MO{RemoveHole}\;=\;\RW{do}\;\AR{
278+(\vC,\Delta,\ve,\vP,\vn;\vQ)\gets\MO{Get}\\
279+\MO{Put}\;(\vC,\Delta,\ve,\vP,\vQ)
270280}
271281}
272282}
@@ -278,18 +288,21 @@ form:
278288
279289\DM{
280290\PA{\A\A}{
281−\MO{Tactic}_\Gamma & \;\vec{\VV{args}} & \;\vt & \MoRet{\vt'}
291+\MO{Tac}_\Gamma & \;\vec{\VV{args}} & \;\vt & \MoRet{\RW{do}\;\AR{
292+\ldots\\
293+\RW{return}\:\vt'}
294+}
282295}
283296}
284297
285−A tactic takes a sequence of zero or more arguments $\vec{\VV{args}}$ followed
286−by the sub-term $\vt$ on which it is operating. It runs relative to a context
287−$\Gamma$ which contains all the bindings and pattern bindings in scope at that
288−point in the term. The sub-term $\vt$ will either be a hole binding
289−$\hole{\vx}{\vT}\SC\ve$ or a guess binding $\guess{\vx}{\vT}{\vv}\SC\ve$. The
290−tactic returns a new term $\vt'$ which can take any form, provided it is
291−well-typed, with a type convertible to the type of $\vt$.
292−Tactics may also have the side effect of updating the proof state,
298+A tactic $\MO{Tac}$ takes a sequence of zero or more arguments
299+$\vec{\VV{args}}$ followed by the sub-term $\vt$ on which it is operating. It
300+runs relative to a context $\Gamma$ which contains all the bindings and pattern
301+bindings in scope at that point in the term. The sub-term $\vt$ will either be
302+a hole binding $\hole{\vx}{\vT}\SC\ve$ or a guess binding
303+$\guess{\vx}{\vT}{\vv}\SC\ve$. The tactic returns a new term $\vt'$ which can
304+take any form, provided it is well-typed, with a type convertible to the type
305+of $\vt$. Tactics may also have the side effect of updating the proof state,
293306therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
294307
295308Tactics are executed by a higher level meta-operation $\MO{Tactic}$,
@@ -321,23 +334,23 @@ tactic.
321334& \MO{Tactic'} & \Gamma & (\lam{\vx}{\vT}\SC\ve)
322335& \MoRet{
323336\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\
324−\lam{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\lam{\vx}{\vT'})\;\ve}
337+\RW{return}\;(\lam{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\lam{\vx}{\vT'})\;\ve)}
325338}
326339\\
327340& \MO{Tactic'} & \Gamma & (\all{\vx}{\vT}\SC\ve)
328341& \MoRet{
329342\RW{do}\; \AR{\vT'\Gets\;\MO{Tactic'}\;\Gamma\;\vT\\
330−\all{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\all{\vx}{\vT'})\;\ve}
343+\RW{return}\;(\all{\vx}{\vT'}\SC \MO{Tactic'}\;(\Gamma;\all{\vx}{\vT'})\;\ve)}
331344}
332345\\
333346& \MO{Tactic'} & \Gamma & (\LET\;\vx\defq\vt\Hab\vT\SC\ve)
334347& \MoRet{\RW{do}\;\AR{\vt'\Gets\;\MO{Tactic'}\;\Gamma\;\vt\\
335348\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}} \\
349+\RW{return}\;(\LET\;\vx\defq\vt'\Hab\vT'\SC
350+\MO{Tactic'}\;(\Gamma;\LET\;\vx\defq\vt'\Hab\vT')\;\ve)}} \\
338351& \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}
352+\MoRet{\RW{return}\;(\MO{Tactic'}\;\Gamma\;\vf)\; (\MO{Tactic'}\;\Gamma\;\va)}\\
353+& \MO{Tactic'} & \Gamma & \vt & \MoRet{\RW{return}\;\vt}
341354}
342355}
343356}
@@ -385,7 +398,7 @@ resolve the existing problems with $\MO{ReUnify}$.
385398\AR{
386399(\tx=\te,\tp)\gets\PrimUnify\;\ve_1\;\ve_2\\
387400\vec{\MO{Subst}}\;\tx\;\te\\
388−\MO{SubstProblems}\;(\tx=\te)\\
401+\MO{SubstProblems}\;\tx\;\te\\
389402(\vC,\Delta,\VV{term},\tP,\vQ)\gets\MO{Get}\\
390403\vec{\MO{ReUnify}}\;\tP
391404}
@@ -395,7 +408,7 @@ resolve the existing problems with $\MO{ReUnify}$.
395408\MO{ReUnify}\;(\Gamma,\ve_1,\ve_2)\;=\;\RW{do}\;\AR{
396409(\tx=\te,\tp)\Gets\PrimUnify\;\ve_1\;\ve_2\\
397410\vec{\MO{Subst}}\;\tx\;\te\\
398−\MO{Return}\;\tp
411+\RW{return}\;\tp
399412}
400413}
401414}
@@ -413,14 +426,16 @@ keeping $\vx$ at the head:
413426\DM{
414427\PA{\A\A}{
415428\MO{Claim}_\Gamma & (\vy \Hab\vS) & (\hole{\vx}{\vT}\SC\ve) &
416− \MoRet{\RW{return}\;\hole{\vx}{\vT}\SC\hole{\vy}{\vS}\SC\ve} \\
429+ \MoRet{\RW{do}\;\AR{\MO{NewHole}\;\vy\\
430+ \RW{return}\;\hole{\vx}{\vT}\SC\hole{\vy}{\vS}\SC\ve}} \\
417431}
418432}
419433
420−An obvious difficulty is in ensuring that names are unique throughout a proof term.
421−The implementation ensures that any hole created by the $\MO{Claim}$ tactic
422−has a unique name by checking against existing names in scope and modifying
423−the name if necessary. In this paper, we will assume that all created names are fresh.
434+An obvious difficulty is in ensuring that names are unique throughout a proof
435+term. The implementation ensures that any hole created by the $\MO{NewHole}$
436+operation has a unique name by checking against existing names in scope and
437+modifying the name if necessary. In this paper, we will assume that all created
438+names are fresh.
424439
425440The $\MO{Fill}$ tactic, given a value $\vv$, attempts to solve the current goal
426441with $\vv$, creating a guess binding in its place. $\MO{Fill}$ attempts to
@@ -474,12 +489,14 @@ Therefore the resulting proof term is:
474489
475490The $\MO{Solve}$ tactic operates on a guess binding. If the guess is \remph{pure}, i.e., it
476491is a \TT{} term containing no hole or guess bindings, then the value attached to
477−the guess is substituted into its scope:
492+the guess is substituted into its scope, and the corresponding hole removed
493+from the hole queue:
478494
479495\DM{
480496\PA{\A}{
481497\MO{Solve}_\Gamma & (\guess{\vx}{\vT}{\vv}\SC\ve) &
482− \MoRet{\RW{return}\;\ve[\vv/\vx]\hg\mbox{(if $\MO{Pure}\;\vv$)}}
498+ \MoRet{\RW{do}\;\AR{\MO{RemoveHole}\\
499+ \RW{return}\;\ve[\vv/\vx]\hg\mbox{(if $\MO{Pure}\;\vv$)}}}
483500}
484501}
485502
@@ -523,13 +540,15 @@ binding requires that the goal normalises to a function type:
523540}
524541
525542\noindent
526−Creating a $\forall$ binding requires that the goal is a $\TC{Type}$:
543+Creating a $\forall$ binding requires that the goal type converts
544+with $\TC{Type}$:
527545
528546\DM{
529547\PA{\A\A}{
530548\MO{Pi}_\Gamma & (\vn\Hab\vS) & (\hole{\vx}{\Type}\SC\vx) &
531549 \MoRet{\RW{do}\;\AR{
532− \Type\;\leftarrow\;\Check\;\vS\\
550+ \vV\;\leftarrow\;\Check\;\vS\\
551+ \MO{Convert}_\Gamma\;\vV\;\Type\\
533552 \RW{return}\;\all{\vn}{\vS}\SC\hole{\vx}{\Type}\SC\vx
534553 }
535554 }
@@ -543,7 +562,8 @@ Creating a $\LET$ binding requires a type and a value.
543562\PA{\A\A}{
544563\MO{Let}_\Gamma & (\vn\Hab\vS\defq\vv) & (\hole{\vx}{\vT}\SC\vx) &
545564 \MoRet{\RW{do}\;\AR{
546− \Type\;\leftarrow\;\Check\;\vS\\
565+ \vV\;\leftarrow\;\Check\;\vS\\
566+ \MO{Convert}_\Gamma\;\vV\;\Type\\
547567 \vS'\;\leftarrow\;\Check\;\vv\\
548568 \Unify\;\vS\;\vS'\\
549569 \RW{return}\;\LET\;\vn\Hab\vS\defq\vv\SC\hole{\vx}{\vT}\SC\vx
@@ -798,11 +818,11 @@ Note in particular that each tactic which introduces a guess ($\MO{Fill}$
798818and $\MO{Solve}$ is closed with a $\MO{Solve}$).
799819
800820Setting up elaboration in this way, with a proof state captured in a monad,
801−and a primitive collection of tactics,
802−makes it easy to derive more complex tactics for elaborating higher level language constructs,
803−in much the same way as the \texttt{Ltac} language in Coq. As a result, the
804−description of elaboration of
805−a language construct (or a program such as $\FN{id}$) bears a strong resemblance to
821+and a primitive collection of tactics, makes it easy to derive more complex
822+tactics for elaborating higher level language constructs, in much the same way
823+as the \texttt{Ltac} language in Coq~\cite{Delahaye2000}. As a result, the
824+description of elaboration of a language construct (or a program such as
825+$\FN{id}$) bears a strong resemblance to
806826a Coq proof script.
807827
808828\FFIG{
@@ -865,11 +885,9 @@ The system state is a tuple, $(\vC,\vA,\vI)$, containing:
865885\item Type class information, $\vI$, containing method signatures and dictionaries for type classes
866886\end{itemize}
867887
868−In the implementation, the system state is captured in a monad, \texttt{Idris}.
869−This monad includes additional information such as syntax overloadings,
870−command line options, and optimisations, which do not concern us here. Elaboration
871−of expressions requires access to the system state in particular in order to expand
872−implicit arguments and resolve type classes.
888+In the implementation, the system state is captured in a monad, \texttt{Idris},
889+which includes additional information such as syntax overloadings, command line
890+options, and optimisations, which do not concern us here.
873891
874892For each global name, $\vA$ records whether its arguments are explicit, implicit,
875893or type class constraints. For example, recall the declaration
@@ -996,7 +1014,7 @@ We will use a subset of full \Idris{}, which we call \IdrisM{}, to explain
9961014elaboration of expressions. \IdrisM{} expression syntax is given in Figure
9971015\ref{idrism} and declaration syntax given in Figure \ref{idrismd}.
9981016\IdrisM{} is a subset of \Idris{} without syntactic sugar --- that is, without
999−tuple syntax, \texttt{do}-notation or infix operators --- and with implicit
1017+\texttt{do}-notation or infix operators --- and with implicit
10001018arguments in types bound explicitly
10011019(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\;\va\;\vn$
10021020instead of simply $\Vect\;\va\;\vn$).
@@ -1147,7 +1165,9 @@ $\vV$ and $\vX$.
11471165\ttinterp{\ve}
11481166}
11491167}
1150−\subsubsection{Elaborating applications}
1168+\subsubsection{Elaborating Applications}
1169+
1170+\label{sect:elabapps}
11511171
11521172There are two cases to consider when elaborating applications:
11531173
@@ -1200,17 +1220,21 @@ Finally, any type class instance arguments are resolved with the
12001220built-in $\MO{Instance}$ tactic.
12011221
12021222\DM{
1203−\ttinterp{\vx\;\ta}\;\mq\;
12041223\AR{
1224+\ttinterp{\vx\;\ta}\;\mq\;
12051225\RW{do}\;
12061226\AR{
12071227(\tn,\tv)\;\gets\;\MO{Expand}\;\vx\;\ta\\
12081228\vec{\MO{Claim}}\;(\tn\Hab\tT)\\
12091229\MO{Fill}\;\vx\;\tn\\
1210−\vec{\MO{Focus}}\;\tn;\;\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\
1230+\vec{\MO{ElabArg}}\;\tn\;\tv\hg\mbox{(for non-placeholder $\vv$)}\\
12111231\MO{Solve} \\
12121232\vec{\MO{Instance}}\;\tn\hg\mbox{(for type class constraint argument $\vn$)}
12131233}
1234+\medskip
1235+\\
1236+\MO{ElabArg}\;\vn\;\vv\;\mq\;
1237+\MO{Focus}\;\vn;\;\ttinterp{\vv}
12141238}
12151239}
12161240
@@ -1220,10 +1244,10 @@ context, then recursively searches the global context. $\MO{Instance}$ is covere
12201244in detail in Section \ref{sect:instance}.
12211245
12221246To elaborate a simple function application, of an arbitrary expression to an
1223−arbitrary argument, we need not worry about implicit arguments or class
1224−constraints. Instead, the function and argument are elaborated, and the results
1225−applied. Since elaboration is type directed, however, there must be an
1226−appropriate type for the function.
1247+arbitrary argument (possibly with a dependent type), we need not worry about
1248+implicit arguments or class constraints. Instead, the function and argument are
1249+elaborated, and the results applied. Since elaboration is type directed,
1250+however, there must be an appropriate type for the function.
12271251
12281252\DM{
12291253\ttinterp{\ve\;\va}\;\mq\;\RW{do}\;
@@ -1446,24 +1470,25 @@ ftest' n False x = ...
14461470
14471471\noindent
14481472Elaboration of \texttt{with} builds the type declaration and auxiliary function
1449−automatically. It checks the left hand side, resulting in a set of patterns
1450−$\tp$, then splits these patterns into those necessary to type
1451−$\vW$, and the rest ($\tp_w$ and $\tp_n$ respectively) using
1473+automatically. The elaborator checks the left hand side, resulting in a set of
1474+patterns $\tp$, then infers a type $\vW$ for the expression $\vw$. The patterns
1475+$\tp$ are then split into those necessary to type $\vW$, and the rest ($\tp_w$
1476+and $\tp_n$ respectively) using
14521477$\MO{SplitContext}$. Then, it builds a new declaration, abstracting over
1453−the matched expression $\ve$ in the types of $\tp_n$.
1478+the matched expression $\vw$ in the types of $\tp_n$.
14541479$\MO{Abstract}\;\ve\;\vw\;\vp$ simply replaces any occurrence of $\vw$ in
14551480$\vp$ with the name $\ve$.
14561481
14571482\DM{
14581483\AR{
1459−\MO{ElabClause}\;(\vx\;\ttt\;\iwith\;\ve\;\vec{\VV{pclause}})\;\mq\\
1484+\MO{ElabClause}\;(\vx\;\ttt\;\iwith\;\vw\;\vec{\VV{pclause}})\;\mq\\
14601485\hg\hg\edo{
14611486\MO{NewProof}\;\TC{Infer};\;
14621487\ttinterp{\DC{MkInfer}\;\_\;(\vx\;\ttt)}\\
14631488\DC{MkInfer}\;\vT\;\VV{lhs}\gets\MO{Term}\\
14641489\tp\gets\MO{Patterns}\\
14651490\MO{NewTerm}\;\TC{Infer};\;
1466−\ttinterp{\DC{MkInfer}\;\_\;\ve}\\
1491+\ttinterp{\DC{MkInfer}\;\_\;\vw}\\
14671492\DC{MkInfer}\;\vW\;\vw'\gets\MO{Term}\\
14681493(\tp_w,\tp_n)\;\gets\;\MO{SplitContext}\;\vW\;\tp\\
14691494\MO{TTDecl}\;(\vx'\Hab\tp_{w}\to(\ve\Hab\vW)\to\vec{\MO{Abstract}}\;\ve\;\vw'\;\tp_{n}\to\vT)\\
@@ -1508,7 +1533,9 @@ Therefore, a type class declaration elaborates to a record type containing all
15081533of the functions in the class, and an instance is simply an instance of the
15091534record. The methods are translated to top level functions which extract the
15101535relevant function from the dictionary. For example, for the \texttt{Show} type
1511−class, the \texttt{class} declaration is translated to:
1536+class, the \texttt{class} declaration is translated (in the elaborated code,
1537+using the surface \Idris{} syntax for readability)
1538+to:
15121539
15131540\begin{SaveVerbatim}{showdata}
15141541
@@ -1670,8 +1697,9 @@ constructing programs in \TT{}.
16701697\label{sect:instance}
16711698
16721699When elaborating applications, recall that implicit arguments are filled in by
1673−unification, and type class constraints by an $\MO{Instance}$ tactic which searches
1674−the context for an instance of the required type class.
1700+unification as described in Section \ref{sect:elabapps}, and type class
1701+constraints by an $\MO{Instance}$ tactic which searches the context for an
1702+instance of the required type class.
16751703
16761704The $\MO{Instance}$ tactic begins by trying to find a solution in the local context,
16771705using the $\MO{Trivial}$ tactic, which attempts
@@ -1788,9 +1816,9 @@ the vector append function, containing a metavariable \texttt{append\_rec}:
17881816
17891817\begin{SaveVerbatim}{vappmv}
17901818
1791−(++) : Vect A n -> Vect A m -> Vect A (n + m)
1792−(++) Nil ys = ys
1793−(++) (x :: xs) ys = x :: ?append_rec
1819+(++) : Vect a n -> Vect a m -> Vect a (n + m)
1820+Nil ++ ys = ys
1821+(x :: xs) ++ ys = x :: ?append_rec
17941822
17951823\end{SaveVerbatim}
17961824\useverb{vappmv}
@@ -1862,10 +1890,11 @@ lookup_default_case i xs def (Just x) = x
18621890\end{SaveVerbatim}
18631891\useverb{listlookupmv}
18641892
1865−To elaborate a $\icase$ expression involves \texttt{let} binding the scrutinee of
1866−the $\icase$ expression and creating a metavariable $\VV{xcase}$ to implement the
1867−pattern matching. Then the elaborator builds a new pattern matching definition for $\VV{xcase}$
1868−and elaborate it:
1893+To elaborate a $\icase$ expression involves \texttt{let} binding the scrutinee
1894+of the $\icase$ expression, introducing a new name $\VV{scrutinee}$, and
1895+creating a metavariable $\VV{xcase}$ to implement the pattern matching. Then
1896+the elaborator builds a new pattern matching definition for $\VV{xcase}$ and
1897+elaborates it:
18691898
18701899\DM{
18711900\AR{