@@ -1,248 +1,7 @@
11module Text.Parser
22
3−import public Control.Delayed
4−
53%default total
64
7−-- TODO: Add some primitives for helping with error messages.
8−-- e.g. perhaps set a string to state what we're currently trying to
9−-- parse, or to say what the next expected token is in words
10−
11−||| Description of a language's grammar. The `tok` parameter is the type
12−||| of tokens, and the `consumes` flag is True if the language is guaranteed
13−||| to be non-empty - that is, successfully parsing the language is guaranteed
14−||| to consume some input.
15−export
16−data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
17− Empty : (val : ty) -> Grammar tok False ty
18− Terminal : (tok -> Maybe a) -> Grammar tok True a
19− NextIs : (tok -> Bool) -> Grammar tok False tok
20− EOF : Grammar tok False ()
21−
22− Fail : String -> Grammar tok c ty
23− Commit : Grammar tok False ()
24−
25− SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
26− Grammar tok True b
27− SeqEmpty : {c1, c2 : Bool} ->
28− Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
29− Grammar tok (c1 || c2) b
30− Alt : {c1, c2 : Bool} ->
31− Grammar tok c1 ty -> Grammar tok c2 ty ->
32− Grammar tok (c1 && c2) ty
33−
34−||| Sequence two grammars. If either consumes some input, the sequence is
35−||| guaranteed to consume some input. If the first one consumes input, the
36−||| second is allowed to be recursive (because it means some input has been
37−||| consumed and therefore the input is smaller)
38−export %inline
39−(>>=) : {c1 : Bool} ->
40− Grammar tok c1 a ->
41− inf c1 (a -> Grammar tok c2 b) ->
42− Grammar tok (c1 || c2) b
43−(>>=) {c1 = False} = SeqEmpty
44−(>>=) {c1 = True} = SeqEat
45−
46−||| Sequence a grammar followed by the grammar it returns.
47−export
48−join : {c1 : Bool} ->
49− Grammar tok c1 (Grammar tok c2 a) ->
50− Grammar tok (c1 || c2) a
51−join {c1 = False} p = SeqEmpty p id
52−join {c1 = True} p = SeqEat p id
53−
54−||| Give two alternative grammars. If both consume, the combination is
55−||| guaranteed to consume.
56−export
57−(<|>) : Grammar tok c1 ty ->
58− Grammar tok c2 ty ->
59− Grammar tok (c1 && c2) ty
60−(<|>) = Alt
61−
62−||| Allows the result of a grammar to be mapped to a different value.
63−export
64−Functor (Grammar tok c) where
65− map f (Empty val) = Empty (f val)
66− map f (Fail msg) = Fail msg
67− map f (Terminal g) = Terminal (\t => map f (g t))
68− map f (Alt x y) = Alt (map f x) (map f y)
69− map f (SeqEat act next)
70− = SeqEat act (\val => map f (next val))
71− map f (SeqEmpty act next)
72− = SeqEmpty act (\val => map f (next val))
73− -- The remaining constructors (NextIs, EOF, Commit) have a fixed type,
74− -- so a sequence must be used.
75− map {c = False} f p = SeqEmpty p (Empty . f)
76−
77−||| Sequence a grammar with value type `a -> b` and a grammar
78−||| with value type `a`. If both succeed, apply the function
79−||| from the first grammar to the value from the second grammar.
80−||| Guaranteed to consume if either grammar consumes.
81−export
82−(<*>) : {c1 : Bool} ->
83− Grammar tok c1 (a -> b) ->
84− inf c1 (Grammar tok c2 a) ->
85− Grammar tok (c1 || c2) b
86−(<*>) {c1 = False} x y = SeqEmpty x (\f => map f y)
87−(<*>) {c1 = True} x y = SeqEat x (\f => map f y)
88−
89−||| Sequence two grammars. If both succeed, use the value of the first one.
90−||| Guaranteed to consume if either grammar consumes.
91−export
92−(<*) : Grammar tok c1 a ->
93− inf c1 (Grammar tok c2 b) ->
94− Grammar tok (c1 || c2) a
95−(<*) x y = map const x <*> y
96−
97−||| Sequence two grammars. If both succeed, use the value of the second one.
98−||| Guaranteed to consume if either grammar consumes.
99−export
100−(*>) : Grammar tok c1 a ->
101− inf c1 (Grammar tok c2 b) ->
102− Grammar tok (c1 || c2) b
103−(*>) x y = map (const id) x <*> y
104−
105−||| Always succeed with the given value.
106−export
107−pure : (val : ty) -> Grammar tok False ty
108−pure = Empty
109−
110−||| Check whether the next token satisfies a predicate
111−export
112−nextIs : (tok -> Bool) -> Grammar tok False tok
113−nextIs = NextIs
114−
115−||| Look at the next token in the input
116−export
117−peek : Grammar tok False tok
118−peek = nextIs (const True)
119−
120−||| Succeeds if running the predicate on the next token returns Just x,
121−||| returning x. Otherwise fails.
122−export
123−terminal : (tok -> Maybe a) -> Grammar tok True a
124−terminal = Terminal
125−
126−||| Always fail with a message
127−export
128−fail : String -> Grammar tok c ty
129−fail = Fail
130−
131−||| Succeed if the input is empty
132−export
133−eof : Grammar tok False ()
134−eof = EOF
135−
136−||| Commit to an alternative; if the current branch of an alternative
137−||| fails to parse, no more branches will be tried
138−export
139−commit : Grammar tok False ()
140−commit = Commit
141−
142−data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
143− Failure : {xs : List tok} ->
144− (committed : Bool) ->
145− (err : String) -> (rest : List tok) -> ParseResult xs c ty
146− EmptyRes : (committed : Bool) ->
147− (val : ty) -> (more : List tok) -> ParseResult more False ty
148− NonEmptyRes : (committed : Bool) ->
149− (val : ty) -> (more : List tok) ->
150− ParseResult (x :: xs ++ more) c ty
151−
152−-- Take the result of an alternative branch, reset the commit flag to
153−-- the commit flag from the outer alternative, and weaken the 'consumes'
154−-- flag to take both alternatives into account
155−weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
156− (com' : Bool) ->
157− ParseResult xs c ty -> ParseResult xs (whatever && c) ty
158−weakenRes com' (Failure com msg ts) = Failure com' msg ts
159−weakenRes {whatever=True} com' (EmptyRes com val xs) = EmptyRes com' val xs
160−weakenRes {whatever=False} com' (EmptyRes com val xs) = EmptyRes com' val xs
161−weakenRes com' (NonEmptyRes com val more) = NonEmptyRes com' val more
162−
163−shorter : (more : List tok) -> .(ys : List tok) ->
164− LTE (S (length more)) (S (length (ys ++ more)))
165−shorter more [] = lteRefl
166−shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
167−
168−doParse : {c : Bool} ->
169− (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
170− ParseResult xs c ty
171−doParse com xs act with (sizeAccessible xs)
172− doParse com xs (Empty val) | sml = EmptyRes com val xs
173− doParse com [] (Fail str) | sml = Failure com str []
174− doParse com (x :: xs) (Fail str) | sml = Failure com str (x :: xs)
175− doParse com xs Commit | sml = EmptyRes True () xs
176−
177− doParse com [] (Terminal f) | sml = Failure com "End of input" []
178− doParse com (x :: xs) (Terminal f) | sml
179− = maybe
180− (Failure com "Unrecognised token" (x :: xs))
181− (\a => NonEmptyRes com {xs=[]} a xs)
182− (f x)
183− doParse com [] EOF | sml = EmptyRes com () []
184− doParse com (x :: xs) EOF | sml
185− = Failure com "Expected end of input" (x :: xs)
186− doParse com [] (NextIs f) | sml = Failure com "End of input" []
187− doParse com (x :: xs) (NextIs f) | sml
188− = if f x
189− then EmptyRes com x (x :: xs)
190− else Failure com "Unrecognised token" (x :: xs)
191− doParse com xs (Alt x y) | sml with (doParse False xs x | sml)
192− doParse com xs (Alt x y) | sml | Failure com' msg ts
193− = if com' -- If the alternative had committed, don't try the
194− -- other branch (and reset commit flag)
195− then Failure com msg ts
196− else weakenRes com (doParse False xs y | sml)
197− -- Successfully parsed the first option, so use the outer commit flag
198− doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
199− = EmptyRes com val xs
200− doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)
201− = NonEmptyRes com val more
202− doParse com xs (SeqEmpty act next) | (Access morerec)
203− = case doParse com xs act | Access morerec of
204− Failure com msg ts => Failure com msg ts
205− EmptyRes com val xs =>
206− case doParse com xs (next val) | (Access morerec) of
207− Failure com' msg ts => Failure com' msg ts
208− EmptyRes com' val xs => EmptyRes com' val xs
209− NonEmptyRes com' val more => NonEmptyRes com' val more
210− NonEmptyRes {x} {xs=ys} com val more =>
211− case (doParse com more (next val) | morerec _ (shorter more ys)) of
212− Failure com' msg ts => Failure com' msg ts
213− EmptyRes com' val _ => NonEmptyRes com' val more
214− NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
215− rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
216− NonEmptyRes com' val more'
217− doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)
218− doParse com xs (SeqEat act next) | sml | Failure com' msg ts
219− = Failure com' msg ts
220− doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)
221− = case doParse com' more (next val) | morerec _ (shorter more ys) of
222− Failure com' msg ts => Failure com' msg ts
223− EmptyRes com' val _ => NonEmptyRes com' val more
224− NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
225− rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
226− NonEmptyRes com' val more'
227− -- This next line is not strictly necessary, but it stops the coverage
228− -- checker taking a really long time and eating lots of memory...
229− doParse _ _ _ | sml = Failure True "Help the coverage checker!" []
230−
231−public export
232−data ParseError tok = Error String (List tok)
233−
234−||| Parse a list of tokens according to the given grammar. If successful,
235−||| returns a pair of the parse result and the unparsed tokens (the remaining
236−||| input).
237−export
238−parse : (xs : List tok) -> (act : Grammar tok c ty) ->
239− Either (ParseError tok) (ty, List tok)
240−parse xs act
241− = case doParse False xs act of
242− Failure _ msg ts => Left (Error msg ts)
243− EmptyRes _ val rest => pure (val, rest)
244− NonEmptyRes _ val rest => pure (val, rest)
245−
2465||| Parse one or more things
2476export
2487some : Grammar tok True a ->