Backpack docs: more carefully describe unification versus unioning.
authorEdward Z. Yang <ezyang@cs.stanford.edu>
Fri, 8 May 2015 22:09:20 +0000 (15:09 -0700)
committerEdward Z. Yang <ezyang@cs.stanford.edu>
Mon, 11 May 2015 23:02:07 +0000 (16:02 -0700)
Signed-off-by: Edward Z. Yang <ezyang@cs.stanford.edu>
docs/backpack/algorithm.pdf
docs/backpack/algorithm.tex

index 8207286..d9c9b76 100644 (file)
Binary files a/docs/backpack/algorithm.pdf and b/docs/backpack/algorithm.pdf differ
index 7674050..1b582a0 100644 (file)
@@ -428,9 +428,8 @@ After merging this in, the final shape of \verb|q| is:
 
 The shapes we've given for individual declarations have been quite
 simple.  Merging combines two shapes, filling requirements with
-implementations and substituting information we learn about the
-identities of \verb|Name|s; it is the most complicated part of the
-shaping process.
+implementations, unifying \verb|Name|s, and unioning requirements; it is
+the most complicated part of the shaping process.
 
 The best way to think about merging is that we take two packages with
 inputs (requirements) and outputs (provisions) and ``wiring'' them up so
@@ -448,17 +447,17 @@ proceeds as follows:
         $p$.} For each requirement $M$ of $q$ that is provided by $p$ (in particular,
         all of its required \verb|Name|s are provided),
         substitute each \verb|Module| occurrence of \verb|HOLE:M| with the
-        provided $p(M)$, merge the names, and remove the requirement from $q$.
-        Error if a provision is insufficient for the requirement.
+        provided $p(M)$, unify the names, and remove the requirement from $q$.
+        If the names of the provision are not a superset of the required names, error.
     \item If mutual recursion is supported, \emph{fill every requirement of $p$ with provided modules from $q$.}
     \item \emph{Merge leftover requirements.}  For each requirement $M$ of $q$ that is not
-        provided by $p$ but required by $p$, merge the names.  (It's not
+        provided by $p$ but required by $p$, unify the names, and union them together to form the new requirement.  (It's not
         necessary to substitute \verb|Module|s, since they are guaranteed to be the same.)
     \item \emph{Add provisions of $q$.} Union the provisions of $p$ and $q$, erroring
         if there is a duplicate that doesn't have the same identity.
 \end{enumerate}
 %
-To merge two sets of names, union the two sets, handling each pair of names with matching \verb|OccName|s $n$ and $m$ as follows:
+To unify two sets of names, find each pair of names with matching \verb|OccName|s $n$ and $m$ and do the following:
 
 \begin{enumerate}
     \item If both are from holes, pick a canonical representative $m$ and substitute $n$ with $m$.