------------------------------------------------------------------------
-- A derivative operator for parsers
------------------------------------------------------------------------

-- Similar to the derivative operator in Brzozowski's "Derivatives of
-- Regular Expressions".

module TotalParserCombinators.Derivative where

-- Definition of the derivative.

open import TotalParserCombinators.Derivative.Definition public

-- The derivative operator is sound and complete with respect to the
-- semantics.

open import TotalParserCombinators.Derivative.SoundComplete public
  hiding (complete′)

-- A proof showing that the derivative operator does not introduce any
-- unneeded ambiguity.

open import TotalParserCombinators.Derivative.LeftInverse public

-- A proof showing that the derivative operator does not remove any
-- ambiguity.

open import TotalParserCombinators.Derivative.RightInverse public
  hiding (sound∘complete′)

-- Some corollaries.

open import TotalParserCombinators.Derivative.Corollaries public