@@ -82,7 +82,7 @@ A proof state is a tuple, $(\vC, \Delta, \ve, \vQ)$, containing:
8282%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
8383\end{itemize}
8484
85−The \remph{hole queue} is a list of names of hole and guess binders
85+The \remph{hole queue} is a priority queue of names of hole and guess binders
8686$\langle\vx_1,\vx_2,\ldots,\vx_n\rangle$
8787in the proof term ---
8888we ensure that each bound name is unique. Holes essentially refer to \remph{sub goals}
@@ -204,6 +204,7 @@ primitive meta-operations:
204204
205205\begin{itemize}
206206\item $\MO{Focus}\:\vn$, which moves $\vn$ to the head of the hole queue.
207+\item $\MO{Unfocus}$, which moves the current hole to the back of the hole queue.
207208\item $\Check\:\ve$, which type checks an expression $\ve$ relative to a context
208209$\Gamma$, returning its type.
209210$\MO{Check}$ will fail
@@ -212,8 +213,8 @@ if the expression is not well-typed.
212213$\Gamma$, returning its normal form.
213214\item
214215$\Unify\:\ve_1\:\ve_2$,
215−which unifies $\ve_1$ and $\ve_2$ by finding the values that holes must be instantiated
216−with for $\ve_1$ and $\ve_2$ to be convertible relative to $\Gamma$
216+which unifies $\ve_1$ and $\ve_2$ by finding the values with which holes must be instantiated
217+for $\ve_1$ and $\ve_2$ to be convertible relative to $\Gamma$
217218(i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold). $\MO{Unify}$ will fail
218219if it cannot find such values. If successful, $\MO{Unify}$ will update the proof state.
219220\end{itemize}
@@ -237,7 +238,7 @@ well-typed, with a type convertible to the type of $\vt$.
237238Tactics may also have the side effect of updating the proof state,
238239therefore we will describe tactics in a pseudo-code with $\RW{do}$ notation.
239240
240−We define a set of primitive tactics: $\MO{Create}$, $\MO{Fill}$ and $\MO{Solve}$
241+We define a set of primitive tactics: $\MO{Claim}$, $\MO{Fill}$ and $\MO{Solve}$
241242which are used to create and destroy holes; and $\MO{Lambda}$, $\MO{Pi}$, $\MO{Let}$
242243and $\MO{Attack}$ which are used to create binders.
243244
@@ -254,6 +255,10 @@ keeping $\vx$ at the head:
254255}
255256}
256257
258+An obvious difficulty is in ensuring that names are unique throughout a proof term.
259+In the implementation, we ensure that any hole created by the $\MO{Claim}$ tactic
260+has a unique name. In this paper, we will assume that all names are fresh.
261+
257262The $\MO{Fill}$ tactic, given a value $\vv$, attempts to solve the current goal
258263with $\vv$, creating a guess binding in its place. $\MO{Fill}$ attempts to
259264solve other holes by unifying the expected type of $\vx$ with the type of $\vv$:
@@ -458,7 +463,8 @@ are closed with a $\MO{Solve}$.
458463Setting up elaboration in this way, with a proof state captured in a monad,
459464and a primitive collection of tactics,
460465makes it easy to derive more complex tactics for elaborating higher level language constructs,
461−in much the same way as the \texttt{Ltac} language in Coq. As a result, elaboration of
466+in much the same way as the \texttt{Ltac} language in Coq. As a result, the
467+description of elaboration of
462468a language construct (or a program such as $\FN{id}$) bears a strong resemblance to
463469a Coq proof script.
464470
@@ -509,13 +515,333 @@ a Coq proof script.
509515
510516\subsection{Elaborating Expressions}
511517
518+\newcommand{\piimp}[2]{\mbox{\texttt{\{ $#1$ : $#2$ \} -> }}}
519+%\mathtt{\{}#1\mathtt{:}#2\mbox{\texttt{\} -> }}}
520+\newcommand{\piexp}[2]{\mbox{\texttt{( $#1$ : $#2$ ) -> }}}
521+%\newcommand{\piexp}[2]{\mathtt{(}#1\mathtt{:}#2\mbox{\texttt{) -> }}}
522+\newcommand{\piconst}[1]{\mbox{\texttt{$#1$ => }}}
523+\newcommand{\icase}{\mathtt{case}}
524+\newcommand{\iwith}{\mathtt{with}}
525+\newcommand{\idata}{\mathtt{data}}
526+\newcommand{\iclass}{\mathtt{class}}
527+\newcommand{\iinstance}{\mathtt{instance}}
528+\newcommand{\iwhere}{\mathtt{where}}
529+\newcommand{\iof}{\mathtt{of}}
530+\newcommand{\ilet}[2]{\mathtt{let}\;#1\;\mathtt{=}\;#2\;\mathtt{in}}
531+\newcommand{\ilam}[1]{\mathtt{\backslash}\;#1\;\mathtt{=>}}
532+\newcommand{\iarg}[2]{\mbox{\texttt{\{ $#1$ = $#2$ \}}}}
533+\newcommand{\ihab}[2]{\mbox{\texttt{$#1$ : $#2$}}}
534+\newcommand{\carg}[1]{\mbox{\texttt{\{\{ $#1$ \}\}}}}
535+\newcommand{\fatarrow}{\mbox{\texttt{=>}}}
536+\newcommand{\ibar}{\mbox{\texttt{|}}}
537+\newcommand{\mvar}[1]{\mbox{\texttt{?}}#1}
512538
513−\IdrisM{}, a subset of \Idris{} not including syntactic sugar (e.g. pairs, do notation, etc).
539+\FFIG{
540+\AR{
541+\begin{array}{rll@{\hg}rll}
542+\ve ::= & \vc & (\mbox{constant}) &
543+\mid & \vx & (\mbox{variable}) \\
544+\mid & \vt & (\mbox{type}) &
545+\mid & \ve\:\ta & (\mbox{function application}) \\
546+\mid & \ilam{\vx}\:\ve & (\mbox{lambda abstraction}) &
547+\mid & \ilet{\vx}{\ve}\:\ve & (\mbox{let binding}) \\
548+\mid & \icase\:\ve\:\iof\:\vec{\VV{alt}} & (\mbox{case expression}) &
549+\mid & \mvar{\vx} & (\mbox{metavariable}) \\
550+\mid & \_ & (\mbox{placeholder})
551+\end{array}
552+\medskip\\
553+\begin{array}{rll}
554+\va :: = & \ve & (\mbox{normal argument}) \\
555+\mid & \iarg{\vx}{\ve} & (\mbox{implicit argument with value}) \\
556+\mid & \carg{\ve} & (\mbox{explicit class instance})
557+\medskip\\
558+\VV{alt} ::= & \ve\:\fatarrow\:\ve & (\mbox{case alternative})\\
559+\end{array}
560+\medskip\\
561+\begin{array}{rll}
562+\vt ::= & \ve & (\mbox{expression}) \\
563+\mid & \piimp{\vx}{\vt}\vt & (\mbox{implicit function space}) \\
564+\mid & \piexp{\vx}{\vt}\vt & (\mbox{explicit function space}) \\
565+\mid & \VV{constr}\;\vt & (\mbox{constrained type}) \\
566+\end{array}
567+\medskip\\
568+\begin{array}{rll}
569+\VV{constr} ::= & \piconst{\ttt} & (\mbox{type class constraint}) \\
570+\end{array}
571+}
572+}
573+{\IdrisM{} expressions}
574+{idrism}
575+
576+\FFIG{
577+\AR{
578+\begin{array}{rll}
579+\vd ::= & \ihab{\vx}{\vt} & (\mbox{type declaration}) \\
580+\mid & \VV{pclause} & (\mbox{pattern clause}) \\
581+\mid & \VV{ddecl} & (\mbox{data type declaration}) \\
582+\mid & \VV{cdecl} & (\mbox{class declaration}) \\
583+\mid & \VV{idecl} & (\mbox{instance declaration}) \\
584+\end{array}
585+\medskip\\
586+\begin{array}{ll}
587+\begin{array}{rll}
588+\VV{pclause} ::= &
589+\vx\:\ttt\:[\ibar\;\te]\mbox{\texttt{ = }}\ve \hg[\iwhere\;\td]\\
590+\mid & \AR{
591+\vx\:\ttt\:[\ibar\;\te]\;\iwith\;\ve\\
592+\hg\vec{\VV{pclause}}
593+}
594+\end{array}
595+&
596+\begin{array}{rll}
597+\VV{ddecl} ::= & \idata\;\ihab{\vx}{\vt}\;\iwhere\;\vec{\VV{con}}\\
598+\VV{con} ::= & \ihab{\vx}{\vt}\\
599+\medskip\\
600+\VV{cdecl} ::= & \iclass\;[\VV{constr}]\;\vx\;(\ihab{\tx}{\ttt})\;\iwhere\;\td
601+\\
602+\VV{idecl} ::= & \iinstance\:[\VV{constr}]\;\vx\;\vt\;\iwhere\;\td
603+\end{array}
604+\end{array}
605+}
606+}
607+{\IdrisM{} declarations}
608+{idrismd}
609+
610+\IdrisM{}, a subset of \Idris{} not including syntactic sugar (e.g. pairs, do notation,
611+infix operators, etc),
612+and with implicit types written in full.
613+Extensions over \TT{}: implicit syntax, case expressions. Functions are applied to
614+multiple arguments, rather than one at a time (this helps with implicit syntax).
615+\IdrisM{} also supports explicit \demph{metavariables}. A metavariable \texttt{?mvar}
616+creates a new global function \tFN{mvar}, with its type such that it would
617+be type correct to apply \tFN{mvar} to all of the variables in scope.
514618
515619Implicit and type class arguments? Expanded at the application site (we need to know
516620it's the global name after all and we do that by type).
517621
518−\subsection{Elaborating Data Types}
622+We define a meta-operation $\ttinterp{\cdot}$ which runs relative to a proof state.
623+Its effect is to update the proof state so that the hole in focus contains a representation
624+of the given expression, by applying tactics. We assume that the proof
625+state has already been set up, which means that we always know the type of the
626+expression we are building.
627+
628+\subsubsection{Elaborating variables and constants}
629+
630+In the simplest cases, there is a direct translation from an \IdrisM{} expression to
631+a \TT{} expression --- we build \TT{} representations of variables and constants using
632+the \MO{Fill} tactic:
633+
634+\DM{
635+\AR{
636+\ttinterp{\vx}\:\mq\:\MO{Fill}\:\vx;\:\MO{Solve}\\
637+\ttinterp{\vc}\:\mq\:\MO{Fill}\:\vc;\:\MO{Solve}\\
638+}
639+}
640+
641+We need not concern ourselves with type checking variables or constants here --- $\MO{Fill}$
642+will handle this, type checking $\vx$ or $\vc$ and unifying the result with the
643+hole type. If there are any errors, elaboration will fail.
644+
645+We also need to elaborate \remph{placeholders}, which are subexpressions we expect to
646+solve by unification. In this case, we simply move on to the next hole in the queue, moving
647+the current hole to the end of the queue with $\MO{Unfocus}$:
648+
649+\DM{
650+\ttinterp{\_}\:\mq\:\MO{Unfocus}
651+}
652+
653+On encountering a placeholder, our assumption is that unification will eventually solve
654+the hole.
655+
656+\subsubsection{Elaborating bindings}
657+
658+To elaborate a $\lambda$ binding, we $\MO{Attack}$ the hole, which must be a function type
659+or elaboration will fail,
660+apply the $\MO{Lambda}$ tactic, elaborate the scope, then $\MO{Solve}$, which discharges
661+the $\MO{Attack}$:
662+
663+\DM{
664+\ttinterp{\ilam{\vx}\ve}\:\mq\:
665+\RW{do}\:
666+\AR{
667+\MO{Attack};\;\MO{Lambda}\:\vx\\
668+\ttinterp{\ve}\\
669+\MO{Solve}
670+}
671+}
672+
673+Note that there is no type on the $\lambda$-binding in \IdrisM{}. There is no need --- since
674+elaboration is type directed, the $\MO{Lambda}$ tactic finds the type of the binding by
675+looking at the type of the hole. In full \Idris{}, types are allowed on bindings, and the
676+elaborator merely checks that the given type is equivalent to the inferred type.
677+
678+Elaborating a function type is more tricky, since we have to elaborate the argument
679+type (itself an \IdrisM{} expression) then elaborate the scope. To achieve this, we
680+create a new goal $\vX$ for the argument type $\vt$, where $\vX$ is a fresh name,
681+and introduce a function binding with argument type $\vX$. We can then focus on
682+$\vX$, and elaborate it with the expression $\vt$. Finally, we elaborate the
683+scope of the binding.
684+
685+\DM{
686+\AR{
687+\ttinterp{\piexp{\vx}{\vt}\ve}\:\mq\:
688+\RW{do}\:
689+\AR{
690+\MO{Attack};\;\MO{Claim}\:(\vX\Hab\Set)\\
691+\MO{Pi}\:(\vx\Hab\vX)\\
692+\MO{Focus}\:\vX\\
693+\ttinterp{\vt};\;
694+\ttinterp{\ve}\\
695+\MO{Solve}
696+}
697+}
698+}
699+
700+Elaborating $\vt$ will involve solving unification problems, which will, if the
701+program is type correct, solve $\vX$. After focussing on $\vX$ and elaborating
702+$\vt$, there is no need to refocus on the hole representing the scope, as it was
703+previously at the head of the hole queue before focussing on $\vX$.
704+Elaboration of implicit and constraint
705+argument types is exactly the same --- \TT{} makes no distinction between then.
706+
707+To elaborate a \texttt{let} binding, we take a similar approach, creating new subgoals
708+for the \texttt{let}-bound value and its type, then elaborating the scope. Again,
709+if elaborating the scope is successful, unification will solve the claimed variables
710+$\vV$ and $\vX$.
711+
712+\DM{
713+\ttinterp{\ilet{\vx}{\vv}\:{\ve}}\:\mq\:\RW{do}\:
714+\AR{
715+\MO{Attack};\;
716+\MO{Claim}\:(\vX\Hab\Set);\;
717+\MO{Claim}\:(\vV\Hab\vX)\\
718+\MO{Let}\:(\vx\Hab\vX\defq\vV)\\
719+\MO{Focus}\:\vV\\
720+\ttinterp{\vv};\;
721+\ttinterp{\ve}
722+}
723+}
724+
725+\subsubsection{Elaborating applications}
726+
727+There are two cases to consider when elaborating applications:
728+
729+\begin{itemize}
730+\item Applying a global function name to arguments, some of which may be implicit.
731+\item Applying an expression, which does not have implicit arguments, to an argument.
732+\end{itemize}
733+
734+In the first case, we must expand the application to include implicit arguments.
735+For example \texttt{vAdd xs ys} is expanded to
736+\texttt{vAdd \{a=\_\} \{n=\_\} \{\{\_\}\} xs ys}, adding the implicit arguments
737+\texttt{a} and \texttt{n} and a type class instance argument. The meta-operation
738+$\MO{Expand}\:\vx\:\ta$, given a global function name $\vx$ and the
739+arguments supplied by the programmer $\ta$, returns a new argument list
740+$\ta'$ with implicit and type class arguments added. Each value in
741+$\ta'$ is paired with an explicit name for the argument.
742+
743+Implicit arguments are solved by unification
744+--- the type or value of another argument determines the value of an implicit argument,
745+with the appeal to $\MO{Unify}$ in the $\MO{Fill}$ tactic solving as many extra holes
746+as it can. However, unification problems can take several forms. For example, assuming
747+$\vf$, $\vg$, $\vx$ are holes, we might have unification problems of the following
748+forms:
749+
750+\DM{
751+\AR{
752+\MO{Unify}_\Gamma\;\vf\:\TC{Int}\\
753+\MO{Unify}_\Gamma\;(\vf\:\vx)\:\TC{Int}\\
754+\MO{Unify}_\Gamma\;(\vf\:\vx)\:(\vg\:\vx)\\
755+}
756+}
757+
758+The first problem has a solution: $\vf=\TC{Int}$. The second and third problems have
759+no solution without further information. In the second case, we cannot conclude
760+anything about $\vf$ or $\vx$ just from knowing that $\vf\:\vx\:=\:\TC{Int}$.
761+In the third case, although we have $\vx\:=\:\vx$ in argument position, we cannot
762+conclude that $\vf\:=\:\vg$ unless we know that the function which solves $\vf$ or
763+$\vg$ is injective.
764+
765+Once $\vf$ or $\vg$ is solved in some other way, perhaps by being given explicitly
766+in another argument, these unification problems can make progress. Otherwise, unification
767+fails. As a result, the order in which functions and arguments are
768+elaborated matters. Sometimes, we may learn more by elaborating a function first
769+and the arguments later, sometimes it may be the other way around.
770+
771+One option when unification fails is to store the problem (i.e. the expressions to be
772+unified with their local context) and refine it with further information when it becomes
773+available. In practice, we have found a simpler approach to be effective: try
774+elaborating the function first, then arguments. If that fails, try elaborating the
775+arguments first.
776+
777+Elaborating a global function application makes a $\MO{Claim}$ for each argument
778+in turn. Then the function is elaborated, applied to each of the claimed arguments.
779+Finally, each argument which has been given explicitly is elaborated. If this fails,
780+elaboration tries again in the opposite order. Finally, we resolve any type
781+class instance arguments with the built-in $\MO{Instance}$ tactic.
782+
783+\DM{
784+\ttinterp{\vx\:\ta}\:\mq\:
785+\AR{
786+\RW{do}\:
787+\AR{
788+(\tn,\tv)\:\gets\:\MO{Expand}\:\vx\:\ta\\
789+\vec{\MO{Claim}}\:(\tn\Hab\tT)\\
790+\MO{Try}\:\AR{
791+(\RW{do}\:\AR{
792+\MO{Fill}\:\vx\:\tn\\
793+\vec{\MO{Focus}}\:\tn;\:\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\
794+\MO{Solve})
795+}\\
796+(\RW{do}\:\AR{
797+\vec{\MO{Focus}}\:\tn;\:\ttinterp{\tv}\hg\mbox{(for non-placeholder $\vv$)}\\
798+\MO{Fill}\:\vx\:\tn\\
799+\MO{Solve})
800+}}
801+\\
802+\vec{\MO{Instance}}\:\tn\hg\mbox{(for type class constraint argument $\vn$)}
803+}
804+}
805+}
806+
807+The $\MO{Instance}$ tactic focuses on the given hole and searches the context for
808+a type class instance which would solve the goal directly. First, it examines the local
809+context, then recursively searches the global context.
810+
811+To elaborate a simple function application, of an arbitrary expression to an arbitrary
812+argument, we need not worry about implicit arguments or class constraints. Instead,
813+we simply elaborate the function and argument, and apply the results. Since elaboration
814+is type directed, however, we do need to construct an appropriate type for the function.
815+As before, we try elaboration in two orders, as we may learn something from elaborating
816+the function or argument which helps with unification:
817+
818+\DM{
819+\ttinterp{\ve\:\va}\:\mq\:\RW{do}\:
820+\AR{
821+\MO{Claim}\:(\vA\Hab\Set);\;\MO{Claim}\:(\vB\Hab\Set)\\
822+\MO{Claim}\:(\vf\Hab\vA\to\vB);\;\MO{Claim}\:(\vs\Hab\vA)\\
823+\MO{Try}\:
824+\AR{
825+(\RW{do}\:\AR{
826+\MO{Focus}\:\vf;\;\ttinterp{\ve}\\
827+\MO{Focus}\:\vs;\;\ttinterp{\va})}\\
828+(\RW{do}\:\AR{
829+\MO{Focus}\:\vs;\;\ttinterp{\va}\\
830+\MO{Focus}\:\vf;\;\ttinterp{\ve})}\\
831+}
832+}
833+}
834+
835+\subsubsection{Elaborating metavariables}
836+
837+\subsubsection{Elaborating \texttt{case} expressions}
838+
839+\subsection{Elaborating Declarations}
840+
841+
842+\subsubsection{Elaborating Data Types}
843+
844+\subsubsection{Elaborating Pattern Matching}
519845
520−\subsection{Elaborating Pattern Matching}
846+\subsubsection{Elaborating Class and Instance Declarations}
521847