git.iko.soy/Idris-dev
on 3ce4e48 help sign in
Idris-dev/docs/parserLibrary/parser.rst
276 lines 9.2 kB history raw
1Parser
2======
4On the previous page we implemented a lexer to lex a very simple expression, on this
5page we will go on to implement a parser for it.
7To run our parser we call 'doParse'. This requires the output from the lexer (a list of tokens) and a Grammar.
9.. code-block:: idris
11 doParse : {c : Bool} ->
12 (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
13 ParseResult xs c ty
15So we need to define the Grammar for our parser
17.. code-block:: idris
19 ||| Description of a language's grammar. The `tok` parameter is the type
20 ||| of tokens, and the `consumes` flag is True if the language is guaranteed
21 ||| to be non-empty - that is, successfully parsing the language is guaranteed
22 ||| to consume some input.
23 public export
24 data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where
25 Empty : (val : ty) -> Grammar tok False ty
26 Terminal : String -> (tok -> Maybe a) -> Grammar tok True a
27 NextIs : String -> (tok -> Bool) -> Grammar tok False tok
28 EOF : Grammar tok False ()
30 Fail : Bool -> String -> Grammar tok c ty
31 Commit : Grammar tok False ()
32 MustWork : Grammar tok c a -> Grammar tok c a
34 SeqEat : Grammar tok True a -> Inf (a -> Grammar tok c2 b) ->
35 Grammar tok True b
36 SeqEmpty : {c1, c2 : Bool} ->
37 Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
38 Grammar tok (c1 || c2) b
39 Alt : {c1, c2 : Bool} ->
40 Grammar tok c1 ty -> Grammar tok c2 ty ->
41 Grammar tok (c1 && c2) ty
43.. code-block:: idris
45 -- from Idris2/src/Parser/Support.idr
46 public export
47 Rule : Type -> Type
48 Rule ty = Grammar (TokenData ExpressionToken) True ty
50.. code-block:: idris
52 export
53 intLiteral : Rule Integer
54 intLiteral
55 = terminal --"Expected integer literal"
56 (\x => case tok x of
57 Number i => Just i
58 _ => Nothing)
60In order to try this out, here is a temporary function, this calls
61parse which takes two parameters:
62* The grammar (in this case intLiteral)
63* The token list from the lexer.
65.. code-block:: idris
67 test1 : String -> Either (ParseError (TokenData ExpressionToken))
68 (Integer, List (TokenData ExpressionToken))
69 test1 s = parse intLiteral (fst (lex expressionTokens s))
71As required, if we pass it a string which is a number literal then it will return the
72number in the 'Right' option.
74.. code-block:: idris
76 *parserEx> test1 "123"
77 Right (123, []) : Either (ParseError (TokenData ExpressionToken))
78 (Integer, List (TokenData ExpressionToken))
80If we pass it a string which is not a number literal then it will return an
81error message.
83.. code-block:: idris
85 *parserEx> test1 "a"
86 Left (Error "End of input"
87 []) : Either (ParseError (TokenData ExpressionToken))
88 (Integer, List (TokenData ExpressionToken))
90If we pass it a number followed by something else, then it will still be
91successful, this is because we are not specifically checking for end-of-file.
93.. code-block:: idris
95 *parserEx> test1 "123a"
96 Right (123, []) : Either (ParseError (TokenData ExpressionToken))
97 (Integer, List (TokenData ExpressionToken))
98 *parserEx>
100.. code-block:: idris
102 ||| Succeeds if running the predicate on the next token returns Just x,
103 ||| returning x. Otherwise fails.
104 export
105 terminal : (tok -> Maybe a) -> Grammar tok True a
106 terminal = Terminal
108.. code-block:: idris
110 openParen : Rule Integer
111 openParen = terminal (\x => case tok x of
112 OParen => Just 0
113 _ => Nothing)
115.. code-block:: idris
117 test2 : String -> Either (ParseError (TokenData ExpressionToken))
118 (Integer, List (TokenData ExpressionToken))
119 test2 s = parse openParen (fst (lex expressionTokens s))
121.. code-block:: idris
123 *parserEx> test2 "("
124 Right (0, []) : Either (ParseError (TokenData ExpressionToken))
125 (Integer, List (TokenData ExpressionToken))
126 *parserEx> test2 "123"
127 Left (Error "Unrecognised token"
128 [MkToken 0
129 0
130 (Number 123)]) : Either (ParseError (TokenData ExpressionToken))
131 (Integer,
132 List (TokenData ExpressionToken))
133 *parserEx>
135.. code-block:: idris
137 test3 : String -> Either (ParseError (TokenData ExpressionToken))
138 (Integer, List (TokenData ExpressionToken))
139 test3 s = parse (map const openParen <*> intLiteral) (fst (lex expressionTokens s))
141.. code-block:: idris
143 *parserEx> test3 "(123"
144 Right (0, []) : Either (ParseError (TokenData ExpressionToken))
145 (Integer, List (TokenData ExpressionToken))
146 *parserEx> test3 "(("
147 Left (Error "Unrecognised token"
148 [MkToken 0
149 (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n')))
150 "(" of
151 (incol, "") => c + cast (length incol)
152 (incol, b) => cast (length incol))
153 OParen]) : Either (ParseError (TokenData ExpressionToken))
154 (Integer, List (TokenData ExpressionToken))
156 *parserEx> test3 "123"
157 Left (Error "Unrecognised token"
158 [MkToken 0
159 0
160 (Number 123)]) : Either (ParseError (TokenData ExpressionToken))
161 (Integer,
162 List (TokenData ExpressionToken))
163 *parserEx> test3 "123("
164 Left (Error "Unrecognised token"
165 [MkToken 0 0 (Number 123),
166 MkToken 0
167 (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n')))
168 "321" of
169 (incol, "") => c + cast (length incol)
170 (incol, b) => cast (length incol))
171 OParen]) : Either (ParseError (TokenData ExpressionToken))
172 (Integer, List (TokenData ExpressionToken))
173 *parserEx>
175.. code-block:: idris
177 closeParen : Rule Integer
178 closeParen = terminal (\x => case tok x of
179 CParen => Just 0
180 _ => Nothing)
182.. code-block:: idris
184 ||| Matches if this is an operator token and string matches, that is,
185 ||| it is the required type of operator.
186 op : String -> Rule Integer
187 op s = terminal (\x => case tok x of
188 (Operator s1) => if s==s1 then Just 0 else Nothing
189 _ => Nothing)
191.. code-block:: idris
193 paren : Rule Integer -> Rule Integer
194 paren exp = openParen *> exp <* closeParen
196.. code-block:: idris
198 addInt : Integer -> Integer -> Integer
199 addInt a b = a+b
201 export
202 add : Grammar tok c1 Integer ->
203 Grammar tok c2 Integer ->
204 Grammar tok c3 Integer ->
205 Grammar tok ((c1 || c2) || c3) Integer
206 add x y z = map addInt (x *> y) <*> z
208.. code-block:: idris
210 subInt : Integer -> Integer -> Integer
211 subInt a b = a-b
213 export
214 sub : Grammar tok c1 Integer ->
215 Grammar tok c2 Integer ->
216 Grammar tok c3 Integer ->
217 Grammar tok ((c1 || c2) || c3) Integer
218 sub x y z = map subInt (x *> y) <*> z
221 multInt : Integer -> Integer -> Integer
222 multInt a b = a*b
224 export
225 mult : Grammar tok c1 Integer ->
226 Grammar tok c2 Integer ->
227 Grammar tok c3 Integer ->
228 Grammar tok ((c1 || c2) || c3) Integer
229 mult x y z = map multInt (x *> y) <*> z
231.. code-block:: idris
233 partial
234 expr : Rule Integer
235 expr = (add (op "+") expr expr)
236 <|> (sub (op "-") expr expr)
237 <|> (mult (op "*") expr expr)
238 <|> intLiteral <|> (paren expr)
240.. code-block:: idris
242 *parserEx> parse expr (fst (lex expressionTokens "(1)"))
243 Right (1, []) : Either (ParseError (TokenData ExpressionToken))
244 (Integer, List (TokenData ExpressionToken))
245 *parserEx>
247.. code-block:: idris
249 parse : (act : Grammar tok c ty) -> (xs : List tok)
251 parse intLiteral (fst (lex expressionTokens "1"))
253.. code-block:: idris
255 *parserEx> parse expr (fst (lex expressionTokens "1+2"))
256 Right (1,
257 [MkToken 0
258 (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "1" of
259 (incol, "") => c + cast (length incol)
260 (incol, b) => cast (length incol))
261 (Operator "+"),
262 MkToken 0
263 (case fspan (\ARG => not (intToBool (prim__eqChar ARG '\n'))) "+" of
264 (incol, "") => c + cast (length incol)
265 (incol, b) => cast (length incol))
266 (Number 2)]) : Either (ParseError (TokenData ExpressionToken))
267 (Integer, List (TokenData ExpressionToken))
268 *parserEx>
270.. code-block:: idris
272 partial
273 test : String -> Either (ParseError (TokenData ExpressionToken))
274 (Integer, List (TokenData ExpressionToken))
275 test s = parse expr (fst (lex expressionTokens s))