------------------------------------------------------------------------ -- Total recognisers based on the same principles as the parsers in -- TotalParserCombinators.Parser -- -- Nils Anders Danielsson ------------------------------------------------------------------------ -- Recognisers are less complicated than parsers, and the following -- code should be easier to follow than the code under -- TotalParserCombinators. module TotalRecognisers where -- Very simple recognisers, including a formal semantics and a proof -- of decidability. import TotalRecognisers.Simple -- Proof showing that the set of languages accepted by these -- recognisers is exactly the set of languages which can be decided by -- Agda programs (when the alphabet is {true, false}). import TotalRecognisers.Simple.ExpressiveStrength -- More complicated recognisers, which can handle left recursion. (The -- set of basic combinators is also different: tok has been replaced -- by sat, and nonempty and cast have been added.) import TotalRecognisers.LeftRecursion -- These recognisers have the same (maximal) expressive strength as -- the simple ones, as long as the alphabet is finite. For infinite -- alphabets it is shown that the expressive strength is not maximal. import TotalRecognisers.LeftRecursion.ExpressiveStrength -- A tiny library of derived combinators. import TotalRecognisers.LeftRecursion.Lib -- An example: a left recursive expression grammar. import TotalRecognisers.LeftRecursion.Expression -- The recognisers form a *-continuous Kleene algebra. import TotalRecognisers.LeftRecursion.KleeneAlgebra -- A direct proof which shows that the context-sensitive language -- { aⁿbⁿcⁿ | n ∈ ℕ } can be decided. import TotalRecognisers.LeftRecursion.NotOnlyContextFree