-
Notifications
You must be signed in to change notification settings - Fork 2
/
TotalRecognisers.agda
71 lines (45 loc) · 2.37 KB
/
TotalRecognisers.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
------------------------------------------------------------------------
-- 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 (generally) be easier to follow than the code under
-- TotalParserCombinators.
module TotalRecognisers where
------------------------------------------------------------------------
-- Recognisers which do not support left recursion
-- 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
-- An example: a right recursive expression grammar.
import TotalRecognisers.Simple.Expression
-- An alternative backend (without correctness proof).
import TotalRecognisers.Simple.AlternativeBackend
------------------------------------------------------------------------
-- Recognisers which do support left recursion
-- 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
-- An example of how nonempty can be used: parsing of matching
-- parentheses, along with a correctness proof.
import TotalRecognisers.LeftRecursion.MatchingParentheses
-- 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