------------------------------------------------------------------------ -- A breadth-first backend ------------------------------------------------------------------------ -- Similar to Brzozowski's "Derivatives of Regular Expressions". module TotalParserCombinators.BreadthFirst where -- Definition of the derivative and the parser backend. open import TotalParserCombinators.BreadthFirst.Derivative public using (∂; ∂-initial; parseComplete) -- The parser is sound and complete with respect to the semantics. open import TotalParserCombinators.BreadthFirst.SoundComplete public using (sound; complete; ∂-sound; ∂-complete) -- A proof showing that the breadth-first backend does not introduce -- any unneeded ambiguity. open import TotalParserCombinators.BreadthFirst.LeftInverse public using (complete∘sound) -- A proof showing that the breadth-first backend does not remove any -- ambiguity. open import TotalParserCombinators.BreadthFirst.RightInverse public using (sound∘complete) -- Some additional lemmas. open import TotalParserCombinators.BreadthFirst.Lemmas public