summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-01-02 11:40:08 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2011-01-02 11:40:08 -0500
commit6b1732f501a644128c58ce3b3d8635706d870db8 (patch)
tree12713d5958382cff3237f0a499207f8520f11d81 /doc
parent47c3f97fcb06ec6b269d2242ca3eca3a0bbde118 (diff)
Add a note about Explify to the manual
Diffstat (limited to 'doc')
-rw-r--r--doc/manual.tex2
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 8aa8485f..fee2a2aa 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -2226,6 +2226,8 @@ The compiler reads a \texttt{.urp} file, figures out which \texttt{.urs} and \te
This is where type inference takes place, translating programs into an explicit form with no more wildcards. This phase is the most likely source of compiler error messages.
+Those crawling through the compiler source will also want to be aware of another compiler phase, Explify, that occurs immediately afterward. This phase just translates from an AST language that includes unification variables to a very similar language that doesn't; all variables should have been determined by the end of Elaborate, anyway. The new AST language also drops some features that are used only for static checking and that have no influence on runtime behavior, like disjointness constraints.
+
\subsection{Unnest}
Named local function definitions are moved to the top level, to avoid the need to generate closures.