@@ -100,6 +100,10 @@ A proof state is a tuple, $(\vC, \Delta, \ve, \vP, \vQ)$, containing:
100100\item A local context, $\Delta$, containing pattern bindings
101101\item A proof term, $\ve$, in \TTdev{}
102102\item Unsolved unification problems, $\vP$
103+\begin{itemize}
104+\item These take the form $(\Gamma,\ve_1,\ve_2)$, i.e. the context in which
105+the problem is run, and the expressions to be unified.
106+\end{itemize}
103107\item A hole queue, $\vQ$
104108%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
105109\end{itemize}
@@ -314,14 +318,38 @@ sub-terms in normal form.
314318\end{itemize}
315319
316320$\MO{Unify}$ attempts to solve the given unification problem using
317−$\MO{PrimUnify}$, then attempts to further refine existing problems in the proof
318−state. This operation is given in Figure \ref{unifyps}.
321+$\MO{PrimUnify}$,
322+then attempts to further refine existing problems in the proof
323+state. This operation is given in Figure \ref{unifyps}. After attempting to
324+solve the problem with $\MO{PrimUnify}$ and updating the proof term with
325+any solutions found, it updates the existing problems (with $\MO{SubstProblems}$
326+which applies $\MO{Subst}$ across the terms in the problems), then attempts to
327+resolve the existing problems with $\MO{ReUnify}$.
319328
320329\FFIG{
321−\mbox{\textbf{[UNIFY ALGORITHM GOES HERE] }}
330+%\mbox{\textbf{[UNIFY ALGORITHM GOES HERE] }}
322331%Show how it uses a PrimUnify
323332%operation to update
324333%the proof state with new problems, and solve the old ones
334+\AR{
335+\Unify\:\ve_1\:\ve_2\:=\:\RW{do}\:
336+\AR{
337+(\tx=\te,\tp)\gets\PrimUnify\:\ve_1\:\ve_2\\
338+\vec{\MO{Subst}}\:\tx\:\te\\
339+\MO{SubstProblems}\:(\tx=\te)\\
340+(\vC,\Delta,\VV{term},\tP,\vQ)\gets\MO{Get}\\
341+\vec{\MO{ReUnify}}\:\tP
342+}
343+\medskip
344+\\
345+\AR{
346+\MO{ReUnify}\:(\Gamma,\ve_1,\ve_2)\:=\:\RW{do}\:\AR{
347+(\tx=\te,\tp)\Gets\PrimUnify\:\ve_1\:\ve_2\\
348+\vec{\MO{Subst}}\:\tx\:\te\\
349+\MO{Return}\:\tp
350+}
351+}
352+}
325353}
326354{The $\MO{Unify}$ meta-operation}
327355{unifyps}