Explain why we parse to intrinsically well-scoped AST.

1 files changed, 10 insertions, 6 deletions

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index 3f0044a..c7e161c 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -81,12 +81,16 @@ constructor such as \letkw{} or \foldkw{}. The term is
 enforced by the term constructors; an extrinsically well-scoped term
 would use a separate predicate to prove raw syntax is well-scoped.
 
-\TODO{
-  \begin{itemize}
-    \item why not raw syntax?
-    \item why not extrinsic syntax?
-  \end{itemize}
-}
+Normally parsers produce ``raw'' abstract syntax trees with concrete
+names instead of deBruijn indices. We use dependant state to directly
+create the well-scoped AST because starting from a well-scoped AST
+simplifies the type checker.
+
+We also had the option to produce a raw AST and an extrinsic
+certificate it is well-scoped. Extrinsic certificates are best for
+certifying properties of preexisting structures. As our parser is
+creating the well-scoped AST, the raw AST cannot have been used in any
+prior computations, so we do not need to reference the raw AST.
 
 \subsection{Bidirectional Type Checker}
 \TODO{