diff options
| -rw-r--r-- | sec/compiler.ltx | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/sec/compiler.ltx b/sec/compiler.ltx index efe7cf2..f7a53b3 100644 --- a/sec/compiler.ltx +++ b/sec/compiler.ltx @@ -29,13 +29,13 @@ We present a simplified form of the Idris types used in the compiler. \subsection{Parser} -The \lang{} parser is derived from \textcite{bidir}. At its core is a -data type for parser combinators.\@ \textcite{bidir} gave a type system -for the combinators such that well-formed combinators can parse an -input: in linear time; without backtracking; and with only a single -token of lookahead. They implemented both an interpreter and a staged -compiler for expressions. The interpreter only reports errors about -the combinators at run time. +The \lang{} parser is derived from \textcite{alg-parsing}. At its core +is a data type for parser combinators.\@ \textcite{alg-parsing} gave a +type system for the combinators such that well-formed combinators can +parse an input: in linear time; without backtracking; and with only a +single token of lookahead. They implemented both an interpreter and a +staged compiler for expressions using MetaML~\cite{metaml}. The +interpreter only reports errors about the combinators at run time. We adapted the combinator interpreter for Idris 2. First, we used dependant types to statically enforce a combinator is well-formed. The |