@@ -98,16 +98,18 @@ by implementation details. These meta-operations include:
9898\item \demph{Queries} which retrieve values from the proof state, without modifying
9999the state. For example, we can:
100100\begin{itemize}
101+\item Get the type of the current sub goal
101102\item Retrieve the local context $\Gamma$ at the current sub goal
102103\item Type check or normalise a term relative to $\Gamma$
103−\item Unify two terms (potentially solving sub goals) relative to $\Gamma$
104104\end{itemize}
105+\item \demph{Unification}, which unifies two terms (potentially solving sub goals)
106+relative to $\Gamma$
105107\item \demph{Tactics} which update the proof term. Tactics operate on the sub term
106108at the binder specified by the head of the hole queue $\vQ$.
107109\item \demph{Focussing} on a specific sub goal, which brings a different sub goal to the
108110head of the hole queue.
109−\item \demph{Deferring} a sub goal, which adds a new definition to the global context
110−$\vC$ which solves the sub goal.
111+%\item \demph{Deferring} a sub goal, which adds a new definition to the global context
112+%$\vC$ which solves the sub goal.
111113\end{itemize}
112114
113115Elaboration of an \Idris{} expression involves creating a new proof state, running
@@ -117,7 +119,110 @@ the final proof term, which must be a \TT{} program (i.e. does not contain any o
117119
118120\subsection{System State}
119121
120−We need the global state, for implicits, global context.
122+The system state is a tuple, $(\vC,\vA,\vI)$, containing:
123+
124+\begin{itemize}
125+\item A global context, $\vC$, containing pattern matching definitions
126+\item Implicit arguments, $\vA$, recording which arguments are implicit for each global name
127+\item Type class instances, $\vI$, containing dictionaries for type classes
128+\end{itemize}
129+
130+In the implementation, the system state is captured in a monad, \texttt{Idris}, and
131+includes additional information such as syntax overloadings,
132+command line options, and optimisations, which do not concern us here. Elaboration
133+of expressions requires access to the system state in particular in order to expand
134+implicit arguments and resolve type classes.
135+
136+For each global name, $\vA$ records whether its arguments are explicit, implicit,
137+or type class constraints. For example, recall the declaration
138+of \texttt{vAdd}:
139+
140+\begin{SaveVerbatim}{vAddImpT}
141+
142+vAdd : Num a => Vect a n -> Vect a n -> Vect a n
143+
144+\end{SaveVerbatim}
145+\useverb{vAddImpT}
146+
147+\noindent
148+Written in full, and giving each argument an explicit name, we get the
149+type declaration:
150+
151+\begin{SaveVerbatim}{vAddImpT}
152+
153+vAdd : (a : _) -> (n : _) -> (c : Num a) ->
154+ (xs : Vect a n) -> (ys : Vect a n) -> Vect a n
155+
156+\end{SaveVerbatim}
157+\useverb{vAddImpT}
158+
159+\noindent
160+For \tFN{vAdd}, we record that \texttt{a} and \texttt{n} are implicit,
161+\texttt{c} is a constraint, and \texttt{xs} and \texttt{ys} are explicit. When
162+the elaborator encounters an application of \tFN{vAdd}, it knows that unless these arguments
163+are given explicitly, the application must be expanded.
164+
165+\newcommand{\Check}{\MO{Check}_\Gamma}
166+\newcommand{\Eval}{\MO{Normalise}_\Gamma}
167+\newcommand{\Unify}{\MO{Unify}_\Gamma}
168+
169+\subsection{Tactics}
170+
171+% Meta-operations Check, Normalise, Unify
172+In order to build \TT{} expressions from \Idris{} programs, we define a collection
173+of meta-operations for querying and modifying the proof state. Meta-operations
174+may have side-effects including failure, or updating the proof state. We have the following
175+primitive meta-operations:
176+
177+\begin{itemize}
178+\item $\MO{Focus}\:\vn$, which moves $\vn$ to the head of the hole queue
179+\item $\MO{Check}$, which type checks an expression relative to a context
180+$\Gamma$. \\
181+$\Check\:\ve\:\mq\:(\vv,\vt)$ means that checking an expression $\ve$
182+returns a well typed value $\vv$ and its type $\vt$. $\MO{Check}$ will fail
183+if the expression is not well-typed.
184+\item $\MO{Normalise}$, which evaluates a well-typed expression relative to a context
185+$\Gamma$.\\
186+$\Eval\:\ve\:\mq\:\vv$ means that evaluating the expression $\ve$ returns the
187+value $\vv$.
188+\item $\MO{Unify}$, which unifies two well-typed expressions.
189+\\
190+$\Unify\:\ve_1\:\ve_2\:\mq\:\tv$ means that unifying $\ve_1$ and $\ve_2$ produces a
191+mapping $\tv$ from hole names to the values the holes must be instantiated with for
192+$\ve_1$ and $\ve_2$ to be convertible relative to $\Gamma$
193+(i.e. for $\Gamma\proves\ve_1\converts\ve_2$ to hold). $\MO{Unify}$ will fail
194+if it cannot find such a mapping.
195+\end{itemize}
196+
197+\remph{Tactics} are specifically meta-operations which operate on the sub-term given
198+by the hole at the head of the hole queue in the proof state.
199+
200+
201+Creating and destroying holes: Claim, Exact, Solve
202+
203+Attack, Lambda, Pi, Let
204+
205+Apply
206+
207+
208+%--- give unify in full, esp. as it solves sub goals? Maybe...
209+
210+% Unify' G x t = Success (x, t) if ?x : t in G
211+% Unify' G t x = Success (x, t) if ?x : t in G
212+% Unify' G (b x. e) (b' x'. e') = Unify' G b b'; Unify' G;b e e'[x/x']
213+% Unify' G ((\x.e) x) e' = Unify' G e e'
214+% Unify' G e ((\x.e') x) = Unify' G e e'
215+% Unify' G (f es) (f' es') = vs <- Unify' G f f'; Injective f
216+
217+% Unify' G x y = Success () if G |- x == y
218+% Unify' G . . = Failure
219+
220+% Unify' G (\x : t . e) (\x : t' . e') = Unify' G t t'; Unify' G e e'
221+% ...
222+
223+
224+%\DM{
225+%}
121226
122227\subsection{Elaborating Expressions}
123228