From 8294ab5e9530609dc0931a807315a95f86427b9a Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 26 Jun 2025 18:17:30 +0100 Subject: Fix 935--940. --- sec/compiler.ltx | 14 +++++++------- 1 file 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 -- cgit v1.2.3