diff options
Diffstat (limited to 'sec/compiler.ltx')
| -rw-r--r-- | sec/compiler.ltx | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/sec/compiler.ltx b/sec/compiler.ltx index f7a53b3..e8c1664 100644 --- a/sec/compiler.ltx +++ b/sec/compiler.ltx @@ -38,10 +38,10 @@ 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 -``parse'' interpretation function requires a certificate that a parser -is well-formed. Second, our interpreter produces a certificate that -the list of unprocessed tokens is a suffix of the input tokens. This +dependant types to statically enforce a combinator is well-formed; the +interpretation function takes a certificate that a parser is +well-formed. Second, our interpreter produces a certificate that the +list of unprocessed tokens is a suffix of the input tokens. This certificate is required to satisfy the Idris termination checker when interpreting fixed point combinators. Finally, we thread state throughout the combinators. |