@@ -75,6 +75,8 @@ typing rules for binders ensure that no $?$ bindings leak into types.
76\subsection{Proof State}
76\subsection{Proof State}
78A proof state is a tuple, $(\vC, \Delta, \ve, \vQ)$, containing:
80A proof state is a tuple, $(\vC, \Delta, \ve, \vQ)$, containing:
80\begin{itemize}
82\begin{itemize}
@@ -150,6 +152,8 @@ matching definition in the term on the right hand side.
151\subsection{System State}
153\subsection{System State}
155+\label{sect:sysstate}
153The system state is a tuple, $(\vC,\vA,\vI)$, containing:
157The system state is a tuple, $(\vC,\vA,\vI)$, containing:
155\begin{itemize}
159\begin{itemize}
@@ -615,23 +619,38 @@ a Coq proof script.
615{\IdrisM{} declarations}
619{\IdrisM{} declarations}
622+We define a language \IdrisM{}, with expression syntax given in Figure \ref{idrism}
623+and declaration syntax given in Figure \ref{idrismd}.
618−\IdrisM{}, a subset of \Idris{} not including syntactic sugar (e.g. pairs, do notation,
624+\IdrisM{} is a subset of \Idris{} without syntactic sugar --- that is, without
619−infix operators, etc),
625+tuple sytax, \texttt{do}-notation or infix operators --- and with implicit
620−and with implicit types written in full.
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.
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
621−Extensions over \TT{}: implicit syntax, case expressions. Functions are applied to
638+%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).
639+%multiple arguments, rather than one at a time (this helps with implicit syntax).
623−\IdrisM{} also supports explicit \demph{metavariables}. A metavariable \texttt{?mvar}
640+%\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
641+%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.
642+%be type correct to apply \tFN{mvar} to all of the variables in scope.
627−Implicit and type class arguments? Expanded at the application site (we need to know
644+%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).
645+%it's the global name after all and we do that by type).
630−We define a meta-operation $\ttinterp{\cdot}$ which runs relative to a proof state.
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
631−Its effect is to update the proof state so that the hole in focus contains a representation
649+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
650+of the given expression, by applying tactics. We assume that the proof state
633−state has already been set up, which means that we always know the type of the
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
634−expression we are building.
653+are building.
636\subsubsection{Elaborating variables and constants}
655\subsubsection{Elaborating variables and constants}
@@ -856,9 +875,10 @@ the function or argument which helps with unification:
857\subsection{Elaborating Declarations}
876\subsection{Elaborating Declarations}
859−We can use $\ttinterp{\cdot}$ to
878+To elaborate declarations, we define a meta-operation $\MO{Elab}$, which runs
860−build the top level $\MO{Elab}$ operation, which translates \IdrisM{} type, function
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
861−and class declarations into \TT{} declarations.
881+\IdrisM{} type, function and class declarations into \TT{} declarations.
863\newcommand{\edo}[1]{\RW{do}\:\AR{#1}}
883\newcommand{\edo}[1]{\RW{do}\:\AR{#1}}
@@ -909,11 +929,11 @@ declaration.
910\subsubsection{Elaborating Pattern Matching}
930\subsubsection{Elaborating Pattern Matching}
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
913may have the side effect of adding things to the context, such as definitions in
933may 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.
916−In the simplest case, no $\iwhere$ clause:
936+In the simplest case, no $\iwhere$ clause:]
919\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?
939\MO{ElabClause}\:(\vx\:\ttt\:=\:\ve)\:\mq\:?
@@ -1222,12 +1242,12 @@ Then we elaborate \texttt{instance} declarations as follows:
1222Adding default definitions is straightforward: simply insert the default definition where
1242Adding default definitions is straightforward: simply insert the default definition where
1223there is a method missing in an \texttt{instance} declaration.
1243there is a method missing in an \texttt{instance} declaration.
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
1226a lower level language construct. In particular, we don't need to worry about type
1246a lower level language construct. In particular, we don't need to worry about type
1227class \remph{resolution}, because we have a tactic to do that.
1247class \remph{resolution}, because we have a tactic to do that.
1228We can build a lot of extensions this way because we
1248We can build a lot of extensions this way because we
1229have effectively built, bottom up, an Embedded Domain Specific Language for constructing
1249have effectively built, bottom up, an Embedded Domain Specific Language for constructing
1230−programs in \TT{}.
1250+programs in \TT{}.]
1232\subsubsection{The $\MO{Instance}$ tactic}
1252\subsubsection{The $\MO{Instance}$ tactic}