TotalParserCombinators.agda

------------------------------------------------------------------------
-- A total parser combinator library
--
-- Nils Anders Danielsson
------------------------------------------------------------------------

module TotalParserCombinators where

-- Check out TotalRecognisers for an introduction to the ideas used
-- below in the simplified setting of recognisers (as opposed to
-- parsers).

import TotalRecognisers

-- The parser type, and its semantics.

import TotalParserCombinators.Parser
import TotalParserCombinators.Semantics

-- Forcing of parsers (can be used for inspection/debugging purposes).

import TotalParserCombinators.Force

-- Some lemmas about initial bags.

import TotalParserCombinators.InitialBag

-- A small library of derived parser combinators.

import TotalParserCombinators.Lib

-- A Brzozowski derivative operator for parsers.

import TotalParserCombinators.Derivative

-- A breadth-first backend, based on the derivative operator.

import TotalParserCombinators.BreadthFirst

-- An alternative, coinductive definition of equality (and related
-- orderings) between parsers.

import TotalParserCombinators.CoinductiveEquality

-- Language equivalence and parser equivalence are both congruences.
-- The various orderings are compatible preorders.

import TotalParserCombinators.Congruence
import TotalParserCombinators.Congruence.Sound

-- However, it is possible to construct combinators which do not
-- preserve equality.

import TotalParserCombinators.NotACongruence

-- Proofs of various laws, for instance the monad laws.

import TotalParserCombinators.Laws

-- A proof showing that all functions of type List Bool → List R can
-- be realised using parser combinators (for any R, assuming that bag
-- equality is used for the lists of results).

import TotalParserCombinators.ExpressiveStrength

-- Definitions of asymmetric choice, and and not. Note that no
-- extension of the library is required to define these combinators,
-- which make use of a general operator which lifts initial bag
-- operations to parsers. This operator is defined using the
-- breadth-first backend's derivative operator.

import TotalParserCombinators.Pointwise
import TotalParserCombinators.AsymmetricChoice
import TotalParserCombinators.And
import TotalParserCombinators.Not

-- A lookahead operator cannot be defined.

import TotalParserCombinators.NoLookahead

-- An alternative semantics.

import TotalParserCombinators.Semantics.Continuation

-- Simplification of parsers.

import TotalParserCombinators.Simplification

-- Definition of unambiguity.

import TotalParserCombinators.Unambiguity

-- An example: a left recursive expression grammar.

import TotalParserCombinators.Examples.Expression

-- Recognisers defined on top of the parsers, and a variant of the
-- left recursive expression grammar mentioned above.

import TotalParserCombinators.Recogniser
import TotalParserCombinators.Recogniser.Expression

-- Another example: parsing PBM image files.

import TotalParserCombinators.Examples.PBM

-- An extended example: mixfix operator parsing.

import Mixfix

-- For code related to the paper "Structurally Recursive Descent
-- Parsing", developed together with Ulf Norell, see the following
-- module:

import StructurallyRecursiveDescentParsing