------------------------------------------------------------------------ -- Mixfix operator grammars, and parsing of mixfix operators -- -- Nils Anders Danielsson ------------------------------------------------------------------------ module Mixfix.README 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. import Mixfix.Equivalence