@@ -8,23 +8,23 @@
88
99An \Idris{} program consists of a series of declarations --- data types,
1010functions, classes and instances. In this section, we describe how these
11−high level declarations are translated into a \TT{} program consisting of
11+high-level declarations are translated into a \TT{} program consisting of
1212inductive families and pattern matching function definitions. We will need to
1313work at the \remph{declaration} level, and at the \remph{expression} level,
1414defining the following meta-operations.
1515
1616\begin{itemize}
1717\item $\ttinterp{\cdot}$, which builds a \TT{} expression from an \Idris{} expression.
18−\item $\MO{Elab}$, which processes a top level \Idris{} declaration by generating
18+\item $\MO{Elab}$, which processes a top-level \Idris{} declaration by generating
1919one or more \TT{} declarations.
20−\item $\MO{TTDecl}$, which adds a top level \TT{} declaration.
20+\item $\MO{TTDecl}$, which adds a top-level \TT{} declaration.
2121\end{itemize}
2222
2323
2424\subsection{The Development Calculus \TTdev}
2525
26−\TT{} expressions are built by using high level \Idris{} expressions to
27−direct a tactic based theorem prover, which builds the \TT{} expressions
26+\TT{} expressions are built by using high-level \Idris{} expressions to
27+direct a tactic-based theorem prover, which builds the \TT{} expressions
2828step by step, by refinement. In order to build expressions in this way,
2929the type theory needs to support
3030\remph{incomplete} terms, and a method for term construction.
@@ -40,7 +40,7 @@ These extensions are given in Figure \ref{ttdev}.
4040The \remph{guess} binding is
4141similar to a $\LET$ binding, but without any computational force,
4242i.e. there are no reduction rules for guess bindings.
43−Using binders to represent holes is useful in a dependently typed setting since
43+Using binders to represent holes is useful in a dependently-typed setting since
4444one value may determine another. Attaching a guess to a binder ensures that
4545instantiating one such variable also instantiates all of its dependencies.
4646%The
@@ -87,12 +87,11 @@ instantiating one such variable also instantiates all of its dependencies.
8787
8888\label{sect:prfstate}
8989
90−We will build expressions in \TT{} from high level \Idris{} expressions by
91−creating a top level hole binding with the appropriate type, and refining it
90+We will build expressions in \TT{} from high-level \Idris{} expressions by
91+creating a top-level hole binding with the appropriate type, and refining it
9292according to the structure of the \Idris{} expression. Noting the Curry-Howard
9393correspondence between programs and proofs, and the relationship between our
94−method for elaboration and tactic
95−based theorem proving, we refer to a development as a \emph{proof}.
94+method for elaboration and tactic-based theorem proving, we refer to a development as a \emph{proof}.
9695A proof state is a tuple, $(\vC, \Delta, \ve, \vP, \vQ)$, containing:
9796
9897\begin{itemize}
@@ -118,7 +117,7 @@ When the hole queue is empty, and there are no remaining unification
118117problems, the proof term is complete.
119118
120119Creating a \TT{} expression from an \Idris{} expression involves creating
121−a new proof state, with an empty proof term, and using the high level definition
120+a new proof state, with an empty proof term, and using the high-level definition
122121to direct the building of a final proof state, with a complete proof term.
123122
124123In the implementation, the proof state is captured in an elaboration monad,
@@ -890,7 +889,7 @@ a Coq proof script.
890889
891890\label{sect:sysstate}
892891
893−To elaborate \Idris{} programs we will build expressions from high level
892+To elaborate \Idris{} programs we will build expressions from high-level
894893declarations of functions, data types and classes, and add the resulting
895894definitions to a global system state.
896895The system state is a tuple, $(\vC,\vA,\vI)$, containing:
@@ -1035,7 +1034,7 @@ arguments in types bound explicitly
10351034(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\;\vn\;\va$
10361035instead of simply $\Vect\;\vn\;\va$).
10371036Note that we separate implicit and type constraint bindings, to ensure that they
1038−only appear in top level declarations.
1037+only appear in top-level declarations.
10391038It is in general straightforward to
10401039convert full \Idris{} to \IdrisM{} --- syntactic sugar is implemented by a
10411040direct source transformation, and implicit arguments can be identified as the names
@@ -1091,10 +1090,7 @@ elaboration will fail.
10911090If we are building the left hand side of a pattern clause, however, there is a
10921091problem, as it is the left hand side which \remph{defines} variables. In this
10931092context, we assume that attempting to elaborate a variable which does not type
1094−check means that the variable is a pattern variable\footnote{In Haskell,
1095−pattern variables are all lower case, so type checking can assume that a
1096−lower case name in a pattern refers to a variable. In \Idris{} however, a
1097−name in a pattern may refer to a function, if forced by some dependency.}:
1093+check means that the variable is a pattern variable:
10981094
10991095\DM{
11001096\ttpinterp{\vx}\;\mq\;
@@ -1103,6 +1099,11 @@ name in a pattern may refer to a function, if forced by some dependency.}:
11031099}
11041100}
11051101
1102+In Haskell, for comparison,
1103+pattern variables are all lower case, so type checking can assume that a
1104+lower case name in a pattern refers to a variable. In \Idris{} however, a
1105+name in a pattern may refer to a function, if forced by some dependency.
1106+
11061107We also need to elaborate \remph{placeholders}, which are subexpressions we expect to
11071108solve by unification. In this case, we simply move on to the next hole in the queue, moving
11081109the current hole to the end of the queue with $\MO{Unfocus}$:
@@ -1425,14 +1426,14 @@ the right hand side $\ve$ to use the lifted definitions, rather than the origina
14251426\subsubsection{Elaborating the \texttt{with} rule}
14261427
14271428The \texttt{with} rule allows \remph{dependent} pattern matching on intermediate values.
1428−Translating this into \TT{} involves constructing an auxiliary top level
1429+Translating this into \TT{} involves constructing an auxiliary top-level
14291430definition for
14301431the intermediate pattern match. For example, recall \tFN{natToBin}:
14311432
14321433\useverb{natToBin}
14331434
14341435\noindent
1435−This is equivalent to the following, using top level definitions only:
1436+This is equivalent to the following, using top-level definitions only:
14361437
14371438\begin{SaveVerbatim}{natToBinw}
14381439
@@ -1454,8 +1455,10 @@ natToBin' (S (j + j)) odd = True :: natToBin j
14541455
14551456\noindent
14561457Additionally, the elaborator abstracts over the term being analysed in the type
1457−of the generated auxiliary definition\footnote{This is sometimes referred to
1458−as ``magic \texttt{with}''.} and reorders the arguments as required.
1458+of the generated auxiliary definition
1459+%\footnote{This is sometimes referred to
1460+%as ``magic \texttt{with}''.}
1461+and reorders the arguments as required.
14591462For example:
14601463
14611464\begin{SaveVerbatim}{magicwith}
@@ -1533,7 +1536,7 @@ A $\iwith$ block in a clause for $\vx$
15331536results in an auxiliary definition $\vx'$, where $\vx'$ is a fresh name,
15341537which takes an extra argument corresponding to the intermediate result which
15351538is to be matched.
1536−$\MO{MatchWith}$ matches the left hand side of the top level definition against
1539+$\MO{MatchWith}$ matches the left hand side of the top-level definition against
15371540each $\VV{pclause}$, using the result of the match to build each pattern clause
15381541for $\vx'$.
15391542The clauses in the with block must be of a specific form: they must have an initial
@@ -1554,7 +1557,7 @@ Classes are implemented as dictionaries of functions for each instance,
15541557following the implementation of first class type classes in Coq~\cite{Sozeau2008}.
15551558Therefore, a class declaration elaborates to a record type containing all
15561559of the functions in the class, and an instance is simply an instance of the
1557−record. The methods are translated to top level functions which extract the
1560+record. The methods are translated to top-level functions which extract the
15581561relevant function from the dictionary. For example, for the \texttt{Show}
15591562class, the \texttt{class} declaration is translated (in the elaborated code,
15601563using the surface \Idris{} syntax for readability)
@@ -1585,7 +1588,7 @@ showNat = InstanceShow show' where
15851588\end{SaveVerbatim}
15861589\useverb{shownatf}
15871590
1588−The call to \tFN{show} in the body of the instance uses the top level \tFN{show}
1591+The call to \tFN{show} in the body of the instance uses the top-level \tFN{show}
15891592function, with the instance resolved by the elaborator.
15901593Where instances have constraints, these constraints are passed on to
15911594the function declaration for the instance. For example, for \texttt{Show (List a)}:
@@ -1710,7 +1713,7 @@ defined instance:
17101713Adding default definitions is straightforward: simply insert the default definition where
17111714there is a method missing in an \texttt{instance} declaration.
17121715
1713−\textbf{Remark:} Here, we have added a higher level language construct
1716+Here, we have added a higher level language construct
17141717(classes) simply by elaborating in terms of lower level language constructs
17151718(data types and functions). We achieve type class resolution by implementing a
17161719tactic, $\MO{Instance}$. We can build several extensions this way because we
@@ -1814,8 +1817,8 @@ dependent pattern matching definitions and expansion of implicit arguments
18141817and classes. In order to make the language truly general purpose, however, we
18151818will need to add higher level extensions. Full \Idris{} is \IdrisM{} extended
18161819with \texttt{do}-notation, idiom brackets~\cite{McBride2007}, \texttt{case} expressions,
1817−pattern matching \texttt{let}, metavariables and tactic based theorem proving.
1818−The majority of these extensions are straightforward transformations of high level
1820+pattern matching \texttt{let}, metavariables and tactic-based theorem proving.
1821+The majority of these extensions are straightforward transformations of high-level
18191822\Idris{} programs --- for example, \texttt{do}-notation can be reduced directly to
18201823\IdrisM{} function applications. Some, however, require further support. In this section,
18211824we complete the presentation of \IdrisM{} by extending it with metavariables
@@ -1877,7 +1880,7 @@ append_rec a m n x xs ys = app xs ys
18771880\end{SaveVerbatim}
18781881\useverb{appendrec_def}
18791882
1880−Elaborating a metavariable involves adding a new top level definition which is applied
1883+Elaborating a metavariable involves adding a new top-level definition which is applied
18811884to all of the variables in local scope.
18821885
18831886\DM{
@@ -1894,8 +1897,8 @@ to all of the variables in local scope.
18941897
18951898A \texttt{case} expression allows pattern matching on intermediate values. The difficulty
18961899in elaborating \texttt{case} expressions is that \TT{} allows matching only on
1897−\emph{top level} values. Elaborating a \texttt{case} expression, therefore,
1898−involves creating a new top level function standing for the expression, and applying it.
1900+\emph{top-level} values. Elaborating a \texttt{case} expression, therefore,
1901+involves creating a new top-level function standing for the expression, and applying it.
18991902The natural
19001903way to implement this is to use a metavariable. For example, we have already seen
19011904\texttt{lookup\_default}: