@@ -75,6 +75,8 @@ typing rules for binders ensure that no $?$ bindings leak into types.
7575
7676\subsection{Proof State}
7777
78+\label{sect:prfstate}
79+
7880A proof state is a tuple, $(\vC, \Delta, \ve, \vQ)$, containing:
7981
8082\begin{itemize}
@@ -150,6 +152,8 @@ matching definition in the term on the right hand side.
150152
151153\subsection{System State}
152154
155+\label{sect:sysstate}
156+
153157The system state is a tuple, $(\vC,\vA,\vI)$, containing:
154158
155159\begin{itemize}
@@ -615,23 +619,38 @@ a Coq proof script.
615619{\IdrisM{} declarations}
616620{idrismd}
617621
618−\IdrisM{}, a subset of \Idris{} not including syntactic sugar (e.g. pairs, do notation,
619−infix operators, etc),
620−and with implicit types written in full.
621−Extensions over \TT{}: implicit syntax, case expressions. Functions are applied to
622−multiple arguments, rather than one at a time (this helps with implicit syntax).
623−\IdrisM{} also supports explicit \demph{metavariables}. A metavariable \texttt{?mvar}
624−creates a new global function \tFN{mvar}, with its type such that it would
625−be type correct to apply \tFN{mvar} to all of the variables in scope.
626−
627−Implicit and type class arguments? Expanded at the application site (we need to know
628−it's the global name after all and we do that by type).
629−
630−We define a meta-operation $\ttinterp{\cdot}$ which runs relative to a proof state.
631−Its effect is to update the proof state so that the hole in focus contains a representation
632−of the given expression, by applying tactics. We assume that the proof
633−state has already been set up, which means that we always know the type of the
634−expression we are building.
622+We define a language \IdrisM{}, with expression syntax given in Figure \ref{idrism}
623+and declaration syntax given in Figure \ref{idrismd}.
624+\IdrisM{} is a subset of \Idris{} without syntactic sugar --- that is, without
625+tuple sytax, \texttt{do}-notation or infix operators --- and with implicit
626+arguments in types bound explicitly
627+(e.g. $\piimp{\va}{\_}\piimp{\vn}{\_}\TC{Vect}\:\va\:\vn$
628+instead of simply $\Vect\:\va\:\vn$).
629+It is in general straightforward to
630+convert full \Idris{} to \IdrisM{} --- syntactic sugar is implemented by a
631+direct source transformation, and implicit arguments can be identified as the names
632+which are free in a type in a non-function position.
633+%
634+\IdrisM{} differs from \TT{} in several important respects. It has implicit
635+syntax and type classes, and functions are applied to multiple arguments rather
636+than one at a time.
637+
638+%Extensions over \TT{}: implicit syntax, case expressions. Functions are applied to
639+%multiple arguments, rather than one at a time (this helps with implicit syntax).
640+%\IdrisM{} also supports explicit \demph{metavariables}. A metavariable \texttt{?mvar}
641+%creates a new global function \tFN{mvar}, with its type such that it would
642+%be type correct to apply \tFN{mvar} to all of the variables in scope.
643+
644+%Implicit and type class arguments? Expanded at the application site (we need to know
645+%it's the global name after all and we do that by type).
646+
647+To elaborate expressions, we define a meta-operation $\ttinterp{\cdot}$ which
648+runs relative to a proof state (see Section \ref{sect:prfstate}. Its effect is
649+to update the proof state so that the hole in focus contains a representation
650+of the given expression, by applying tactics. We assume that the proof state
651+has already been set up, which means that elaboration can always be
652+\remph{type-directed}. The proof state contains the type of the expression we
653+are building.
635654
636655\subsubsection{Elaborating variables and constants}
637656
@@ -856,9 +875,10 @@ the function or argument which helps with unification:
856875
857876\subsection{Elaborating Declarations}
858877
859−We can use $\ttinterp{\cdot}$ to
860−build the top level $\MO{Elab}$ operation, which translates \IdrisM{} type, function
861−and class declarations into \TT{} declarations.
878+To elaborate declarations, we define a meta-operation $\MO{Elab}$, which runs
879+relative to the system state (see Section \ref{sect:sysstate}) and has access to the
880+current proof state. $\MO{Elab}$ uses $\ttinterp{\cdot}$ to help translate
881+\IdrisM{} type, function and class declarations into \TT{} declarations.
862882
863883\newcommand{\edo}[1]{\RW{do}\:\AR{#1}}
864884
@@ -909,11 +929,11 @@ declaration.
909929
910930\subsubsection{Elaborating Pattern Matching}
911931
912−Work clause by clause, $\MO{ElabClause}$ returns a left and right hand side, and
932+[Work clause by clause, $\MO{ElabClause}$ returns a left and right hand side, and
913933may have the side effect of adding things to the context, such as definitions in
914−$\iwhere$ clauses. Collect together in a full definition at the end.
934+$\iwhere$ clauses. Collect together in a full definition at the end.
915935
916−In the simplest case, no $\iwhere$ clause:
936+In the simplest case, no $\iwhere$ clause:]
917937
918938\DM{
919939\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?
@@ -1222,12 +1242,12 @@ Then we elaborate \texttt{instance} declarations as follows:
12221242Adding default definitions is straightforward: simply insert the default definition where
12231243there is a method missing in an \texttt{instance} declaration.
12241244
1225−Key point: we've added a higher level language construct simply by elaborating in terms of
1245+[Key point: we've added a higher level language construct simply by elaborating in terms of
12261246a lower level language construct. In particular, we don't need to worry about type
12271247class \remph{resolution}, because we have a tactic to do that.
12281248We can build a lot of extensions this way because we
12291249have effectively built, bottom up, an Embedded Domain Specific Language for constructing
1230−programs in \TT{}.
1250+programs in \TT{}.]
12311251
12321252\subsubsection{The $\MO{Instance}$ tactic}
12331253