@@ -0,0 +1,229 @@
5+-- TODO: Add some primitives for helping with error messages.
6+-- e.g. perhaps set a string to state what we're currently trying to
7+-- parse, or to say what the next expected token is in words
9+||| Description of a language's grammar. The `tok` parameter is the type
10+||| of tokens, and the `consumes` flag is True if the language is guaranteed
11+||| to be non-empty - that is, successfully parsing the language is guaranteed
12+||| to consume some input.
14+data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
15+ Empty : (val : ty) -> Grammar tok False ty
16+ Terminal : (tok -> Maybe a) -> Grammar tok True a
17+ NextIs : (tok -> Bool) -> Grammar tok False tok
18+ EOF : Grammar tok False ()
20+ Fail : String -> Grammar tok c ty
21+ Commit : Grammar tok False ()
23+ SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
25+ SeqEmpty : {c1, c2 : Bool} ->
26+ Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
27+ Grammar tok (c1 || c2) b
28+ Alt : {c1, c2 : Bool} ->
29+ Grammar tok c1 ty -> Grammar tok c2 ty ->
30+ Grammar tok (c1 && c2) ty
33+inf : Bool -> Type -> Type
37+||| Sequence two grammars. If either consumes some input, the sequence is
38+||| guaranteed to consume some input. If the first one consumes input, the
39+||| second is allowed to be recursive (because it means some input has been
40+||| consumed and therefore the input is smaller)
42+(>>=) : {c1 : Bool} ->
43+ Grammar tok c1 a -> inf c1 (a -> Grammar tok c2 b) ->
44+ Grammar tok (c1 || c2) b
45+(>>=) {c1 = False} = SeqEmpty
46+(>>=) {c1 = True} = SeqEat
48+||| Give two alternative grammars. If both consume, the combination is
49+||| guaranteed to consume.
51+(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->
52+ Grammar tok (c1 && c2) ty
56+pure : (val : ty) -> Grammar tok False ty
59+||| Check whether the next token satisfies a predicate
61+nextIs : (tok -> Bool) -> Grammar tok False tok
64+||| Look at the next token in the input
66+peek : Grammar tok False tok
67+peek = nextIs (const True)
69+||| Succeeds if running the predicate on the next token returns Just x,
70+||| returning x. Otherwise fails.
72+terminal : (tok -> Maybe a) -> Grammar tok True a
75+||| Always fail with a message
77+fail : String -> Grammar tok c ty
80+||| Succeed if the input is empty
82+eof : Grammar tok False ()
85+||| Commit to an alternative; if the current branch of an alternative
86+||| fails to parse, no more branches will be tried
88+commit : Grammar tok False ()
91+data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
92+ Failure : {xs : List tok} ->
93+ (committed : Bool) ->
94+ (err : String) -> (rest : List tok) -> ParseResult xs c ty
95+ EmptyRes : (committed : Bool) ->
96+ (val : ty) -> (more : List tok) -> ParseResult more False ty
97+ NonEmptyRes : (committed : Bool) ->
98+ (val : ty) -> (more : List tok) ->
99+ ParseResult (x :: xs ++ more) c ty
101+weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
102+ ParseResult xs c ty -> ParseResult xs (whatever && c) ty
103+weakenRes (Failure com msg ts) = Failure com msg ts
104+weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs
105+weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs
106+weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more
108+shorter : (more : List tok) -> .(ys : List tok) ->
109+ LTE (S (length more)) (S (length (ys ++ more)))
110+shorter more [] = lteRefl
111+shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
113+doParse : {c : Bool} ->
114+ (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
116+doParse com xs act with (smallerAcc xs)
117+ doParse com xs (Empty val) | sml = EmptyRes com val xs
118+ doParse com [] (Fail str) | sml = Failure com str []
119+ doParse com (x :: xs) (Fail str) | sml = Failure com str (x :: xs)
120+ doParse com xs Commit | sml = EmptyRes True () xs
122+ doParse com [] (Terminal f) | sml = Failure com "End of input" []
123+ doParse com (x :: xs) (Terminal f) | sml
125+ (Failure com "Unrecognised token" (x :: xs))
126+ (\a => NonEmptyRes com {xs=[]} a xs)
128+ doParse com [] EOF | sml = EmptyRes com () []
129+ doParse com (x :: xs) EOF | sml
130+ = Failure com "Expected end of input" (x :: xs)
131+ doParse com [] (NextIs f) | sml = Failure com "End of input" []
132+ doParse com (x :: xs) (NextIs f) | sml
134+ then EmptyRes com x (x :: xs)
135+ else Failure com "Unrecognised token" (x :: xs)
136+ doParse com xs (Alt x y) | sml with (doParse False xs x | sml)
137+ doParse com xs (Alt x y) | sml | Failure com' msg ts
138+ = if com' -- If the alternative had committed, don't try the
139+ -- other branch (and reset commit flag)
140+ then Failure com msg ts
141+ else weakenRes (doParse False xs y | sml)
142+ -- Successfully parsed the first option, so use the outer commit flag
143+ doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
144+ = EmptyRes com val xs
145+ doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)
146+ = NonEmptyRes com val more
147+ doParse com xs (SeqEmpty act next) | (Access morerec)
148+ = case doParse com xs act | Access morerec of
149+ Failure com msg ts => Failure com msg ts
150+ EmptyRes com val xs =>
151+ case doParse com xs (next val) | (Access morerec) of
152+ Failure com' msg ts => Failure com' msg ts
153+ EmptyRes com' val xs => EmptyRes com' val xs
154+ NonEmptyRes com' val more => NonEmptyRes com' val more
155+ NonEmptyRes {x} {xs=ys} com val more =>
156+ case (doParse com more (next val) | morerec _ (shorter more ys)) of
157+ Failure com' msg ts => Failure com' msg ts
158+ EmptyRes com' val _ => NonEmptyRes com' val more
159+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
160+ rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
161+ NonEmptyRes com' val more'
162+ doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)
163+ doParse com xs (SeqEat act next) | sml | Failure com' msg ts
164+ = Failure com' msg ts
165+ doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)
166+ = case doParse com' more (next val) | morerec _ (shorter more ys) of
167+ Failure com' msg ts => Failure com' msg ts
168+ EmptyRes com' val _ => NonEmptyRes com' val more
169+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
170+ rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
171+ NonEmptyRes com' val more'
172+ -- This next line is not strictly necessary, but it stops the coverage
173+ -- checker taking a really long time and eating lots of memory...
174+ doParse _ _ _ | sml = Failure True "Help the coverage checker!" []
177+data ParseError tok = Error String (List tok)
179+||| Parse a list of tokens according to the given grammar. If successful,
180+||| returns a pair of the parse result and the unparsed tokens (the remaining
183+parse : (xs : List tok) -> (act : Grammar tok c ty) ->
184+ Either (ParseError tok) (ty, List tok)
186+ = case doParse False xs act of
187+ Failure _ msg ts => Left (Error msg ts)
188+ EmptyRes _ val rest => pure (val, rest)
189+ NonEmptyRes _ val rest => pure (val, rest)
191+||| Parse one or more things
193+some : Grammar tok True a ->
194+ Grammar tok True (List a)
197+ pure (x :: xs)) <|> pure [x]
199+||| Parse zero or more things (may match the empty input)
201+many : Grammar tok True a ->
202+ Grammar tok False (List a)
206+||| Parse one or more things, separated by another thing
208+sepBy1 : Grammar tok True () -> Grammar tok True a ->
209+ Grammar tok True (List a)
210+sepBy1 sep p = do x <- p
213+ pure (x :: xs)) <|> pure [x]
215+||| Parse zero or more things, separated by another thing. May
216+||| match the empty input.
218+sepBy : Grammar tok True () -> Grammar tok True a ->
219+ Grammar tok False (List a)
220+sepBy sep p = sepBy1 sep p <|> pure []
222+||| Optionally parse a thing, with a default value if the grammar doesn't
223+||| match. May match the empty input.
225+optional : Grammar tok True a -> (ifNothing : a) ->
227+optional p def = p <|> pure def