@@ -100,6 +100,10 @@ A proof state is a tuple, $(\vC, \Delta, \ve, \vP, \vQ)$, containing:
100\item A local context, $\Delta$, containing pattern bindings
100\item A local context, $\Delta$, containing pattern bindings
101\item A proof term, $\ve$, in \TTdev{}
101\item A proof term, $\ve$, in \TTdev{}
102\item Unsolved unification problems, $\vP$
102\item Unsolved unification problems, $\vP$
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.
103\item A hole queue, $\vQ$
107\item A hole queue, $\vQ$
104%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
108%\item \remph{Deferred} definitions, $\vD$, for introducing global metavariables
105\end{itemize}
109\end{itemize}
@@ -314,14 +318,38 @@ sub-terms in normal form.
314\end{itemize}
318\end{itemize}
316$\MO{Unify}$ attempts to solve the given unification problem using
320$\MO{Unify}$ attempts to solve the given unification problem using
317−$\MO{PrimUnify}$, then attempts to further refine existing problems in the proof
322+then attempts to further refine existing problems in the proof
318−state. This operation is given in Figure \ref{unifyps}.
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}$.
321−\mbox{\textbf{[UNIFY ALGORITHM GOES HERE] }}
330+%\mbox{\textbf{[UNIFY ALGORITHM GOES HERE] }}
322%Show how it uses a PrimUnify
331%Show how it uses a PrimUnify
323%operation to update
332%operation to update
324%the proof state with new problems, and solve the old ones
333%the proof state with new problems, and solve the old ones
335+\Unify\:\ve_1\:\ve_2\:=\:\RW{do}\:
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
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\\
326{The $\MO{Unify}$ meta-operation}
354{The $\MO{Unify}$ meta-operation}