-- 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