@@ -1,248 +1,7 @@
1module Text.Parser
1module Text.Parser
3−import public Control.Delayed
5%default total
3%default total
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
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.
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 ()
22− Fail : String -> Grammar tok c ty
23− Commit : Grammar tok False ()
25− SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 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
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)
39−(>>=) : {c1 : Bool} ->
41− inf c1 (a -> Grammar tok c2 b) ->
42− Grammar tok (c1 || c2) b
43−(>>=) {c1 = False} = SeqEmpty
44−(>>=) {c1 = True} = SeqEat
46−||| Sequence a grammar followed by the grammar it returns.
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
54−||| Give two alternative grammars. If both consume, the combination is
55−||| guaranteed to consume.
57−(<|>) : Grammar tok c1 ty ->
59− Grammar tok (c1 && c2) ty
62−||| Allows the result of a grammar to be mapped to a different value.
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)
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.
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)
89−||| Sequence two grammars. If both succeed, use the value of the first one.
90−||| Guaranteed to consume if either grammar consumes.
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
97−||| Sequence two grammars. If both succeed, use the value of the second one.
98−||| Guaranteed to consume if either grammar consumes.
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
105−||| Always succeed with the given value.
107−pure : (val : ty) -> Grammar tok False ty
110−||| Check whether the next token satisfies a predicate
112−nextIs : (tok -> Bool) -> Grammar tok False tok
115−||| Look at the next token in the input
117−peek : Grammar tok False tok
118−peek = nextIs (const True)
120−||| Succeeds if running the predicate on the next token returns Just x,
121−||| returning x. Otherwise fails.
123−terminal : (tok -> Maybe a) -> Grammar tok True a
126−||| Always fail with a message
128−fail : String -> Grammar tok c ty
131−||| Succeed if the input is empty
133−eof : Grammar tok False ()
136−||| Commit to an alternative; if the current branch of an alternative
137−||| fails to parse, no more branches will be tried
139−commit : Grammar tok False ()
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
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} ->
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
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))
168−doParse : {c : Bool} ->
169− (commit : Bool) -> (xs : List tok) -> (act : Grammar tok 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
177− doParse com [] (Terminal f) | sml = Failure com "End of input" []
178− doParse com (x :: xs) (Terminal f) | sml
180− (Failure com "Unrecognised token" (x :: xs))
181− (\a => NonEmptyRes com {xs=[]} a xs)
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
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!" []
232−data ParseError tok = Error String (List tok)
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
238−parse : (xs : List tok) -> (act : Grammar tok c ty) ->
239− Either (ParseError tok) (ty, List tok)
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)
246||| Parse one or more things
5||| Parse one or more things
248some : Grammar tok True a ->
7some : Grammar tok True a ->