------------------------------------------------------------------------ -- Mixfix operator grammars, and parsing of mixfix operators -- -- Nils Anders Danielsson ------------------------------------------------------------------------ module Mixfix where -- There are two separate developments here. One is very close to the -- paper "Parsing Mixfix Operators" (by me and Ulf Norell), and uses -- directed acyclic precedence graphs and grammars which are neither -- left nor right recursive. The other uses precedence graphs which -- may be cyclic and grammars which can be both left and right -- recursive (following an alternative definition of grammars given in -- the paper). The two grammar schemes are equivalent when restricted -- to acyclic precedence graphs. -- The grammars which use DAGs have the advantage that they can be -- implemented using a larger variety of parser combinator libraries. -- This could lead to a more efficient implementation. On the other -- hand the definition of the other grammars does not attempt to avoid -- left and right recursion, which means that it is arguably a bit -- easier to understand and work with (compare the proofs in -- Mixfix.Acyclic.Show and Mixfix.Cyclic.Show, for instance). ------------------------------------------------------------------------ -- Shared code -- Fixity and associativity. import Mixfix.Fixity -- Operators. import Mixfix.Operator -- Precedence-correct expressions, parametrised on abstract precedence -- graphs. import Mixfix.Expr ------------------------------------------------------------------------ -- Acyclic graphs -- A custom-made parser combinator library (with a formal semantics). import Mixfix.Acyclic.Lib -- Acyclic precedence graphs. import Mixfix.Acyclic.PrecedenceGraph -- Mixfix operator grammars. The resulting expressions are -- precedence-correct by construction. import Mixfix.Acyclic.Grammar -- A minor lemma. import Mixfix.Acyclic.Lemma -- Linearisation of operators, and a proof showing that all the -- generated strings are syntactically correct (although perhaps -- ambiguous). If the result is combined with the one in -- Mixfix.Cyclic.Uniqueness we get that every expression has a unique -- representation. (Two different expressions may have the same -- representation, though.) import Mixfix.Acyclic.Show -- An example. import Mixfix.Acyclic.Example ------------------------------------------------------------------------ -- Cyclic graphs -- A custom-made parser combinator library (with a formal semantics). import Mixfix.Cyclic.Lib -- Cyclic precedence graphs. (These graphs are not used below, because -- Mixfix.Cyclic.Grammar can handle arbitrary precedence graphs.) import Mixfix.Cyclic.PrecedenceGraph -- Mixfix operator grammars. The resulting expressions are -- precedence-correct by construction. import Mixfix.Cyclic.Grammar -- A constructive proof (i.e. a "show" function) showing that every -- expression has at least one representation. import Mixfix.Cyclic.Show -- A proof showing that every expression has at most one -- representation. import Mixfix.Cyclic.Uniqueness -- An example. import Mixfix.Cyclic.Example ------------------------------------------------------------------------ -- Equivalence -- For acyclic precedence graphs the two grammar definitions above are -- equivalent. -- Note that this proof only establishes language equivalence, not -- parser equivalence (see TotalParserCombinators.Semantics). In other -- words, the two definitions are seen as equivalent if they yield the -- same language, even though the number of parse trees corresponding -- to a certain (input string, result)-pair may vary between the two -- definitions. For instance, when parsing the string s using one -- grammar the result could contain the expression e once, whereas -- parsing with the other grammar could yield a result containing two -- copies of e. This is not a big problem: syntactic equality of -- expressions is decidable, so extra occurrences of e can be filtered -- out. The same considerations apply to the equivalence proofs in -- Mixfix.Acyclic.Lib and Mixfix.Cyclic.Lib. Note that I believe that -- it is easy (but tedious) to strengthen all these proofs so that -- parser equivalence is established, but I have not tried to do this. import Mixfix.Equivalence