diff options
| -rw-r--r-- | sec/compiler.ltx | 16 |
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{ |