3a6bd7b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

document do notation for grammar

3a6bd7bmartinbaker7 years ago

docs/parserLibrary/parser.rst+100−25

compare with master

unifiedsplit

@@ -3,8 +3,8 @@

3Parser

4======

6−To run our parser we call 'parse'. This requires a Grammar and the output

6+To run the parser we call ``parse``. This requires a Grammar and the output

7−from the lexer (a list of tokens).

7+from the lexer (which is a list of tokens).

9.. code-block:: idris

@@ -54,12 +54,12 @@ consume input.

54 Grammar tok (c1 && c2) ty

56So an example of a Grammer type may look something like this:

57−'Grammar (TokenData ExpressionToken) True Integer'.

57+``Grammar (TokenData ExpressionToken) True Integer``.

58−

59This is a complicated type name and a given parser will need to use it a lot.

58This is a complicated type name and a given parser will need to use it a lot.

60So to reduce the amount of typing we can use the following type synonym (similar

59So to reduce the amount of typing we can use the following type synonym (similar

61to what is done in Idris 2

60to what is done in Idris 2

62: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr

61: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr

62+)

64.. code-block:: idris

@@ -71,12 +71,12 @@ Parser Example

71--------------

73On the previous page we implemented a lexer to 'lex' a very simple expression, on

74−this page we will go on to implement a parser for this running example.

74+this page we will go on to add a parser for this running example.

76.. list-table::

78− * - Expressed in Backus–Naur form (BNF) the syntax we are aiming at is something

78+ * - The syntax we are aiming at is something

79− like this:

79+ like this (expressed in Backus–Naur form (BNF)):

80 - .. code-block:: idris

82 <expr> ::= <integer literal>

@@ -90,7 +90,7 @@ this page we will go on to implement a parser for this running example.

90.. list-table::

92 * - To start, here is a Grammar to parse an integer literal (that is, a

93− sequence of numbers).

93+ sequence of numeric characters).

95 - .. code-block:: idris

@@ -144,7 +144,7 @@ successful, this is because we are not specifically checking for end-of-file.

144

145.. list-table::

146

147− * - The 'intLiteral' function above uses the 'terminal' function to

147+ * - The ``intLiteral`` function above uses the ``terminal`` function to

148 construct the grammar

149 - .. code-block:: idris

150

@@ -174,10 +174,10 @@ Idris 2 uses a slightly different version which stores an error message like

174 OParen => Just 0

175 _ => Nothing)

176

177−Integer value is not really relevant for parenthesis so '0' is used as

177+Integer value is not really relevant for parenthesis so ``0`` (zero) is used as

178a default value.

179

180−As before, we can test this out with a function like this:

180+As before, this can be tested with a function like this:

181

182.. code-block:: idris

183

@@ -202,10 +202,10 @@ error for anything else:

202 List (TokenData ExpressionToken))

203

204Now we have two Grammars we can try combining them. The following test looks

205−for 'openParen' followed by 'intLiteral', the two Grammars are combined using

205+for ``openParen`` followed by ``intLiteral``, the two Grammars are combined using

206−'<*>'. The 'map const' part uses the integer value from the first.

206+``<*>``. The ``map const`` part uses the integer value from the first.

207

208−The following test is looking for '(' followed by a number:

208+The following test is looking for ``(`` followed by a number:

209

210.. code-block:: idris

211

@@ -213,8 +213,8 @@ The following test is looking for '(' followed by a number:

213 (Integer, List (TokenData ExpressionToken))

214 test3 s = parse (map const openParen <*> intLiteral) (fst (lex expressionTokens s))

215

216−We can see below that '(' followed by a number is successfully parsed but other

216+We can see below that ``(`` followed by a number is successfully parsed but, as

217−token lists are not:

217+required, other token lists are not:

218

219.. code-block:: idris

220

@@ -270,21 +270,85 @@ token lists are not:

270 paren : Rule Integer -> Rule Integer

271 paren exp = openParen *> exp <* closeParen

272

273−The use of '*>' and '<*' instead of '<*>' is an easy way to use the integer

273+The use of ``*>`` and ``<*`` instead of ``<*>`` is an easy way to use the integer

274value from the inner expression.

275

276+So lets try to use this to define a grammar which recognises either:

277+

278+- An integer literal

279+- An integer literal inside parenthesis

280+- An integer literal inside parenthesis inside parenthesis

281+- ... and so on.

282+

283+This requires a recursively defined structure like this:

284+

285+.. code-block:: idris

286+

287+ partial

288+ expr : Rule Integer

289+ expr = intLiteral <|> (paren expr)

290+

291+This is a valid grammar because every time it is called it is guaranteed to

292+consume a token. However, as an Idris structure, it is problematic due to

293+the recursion. Defining it as partial allows it to compile but at runtime

294+we are likely to get a crash with an (unhelpful) error message like

295+``killed by signal 11``.

296+

297+So a better method is to use ``do`` notation as described in the following

298+section.

299+

300+Monadic Combinator

301+------------------

302+

303+In addition to ``<|>`` and ``<*>`` there is a ``>>=`` combinator, which is

304+defined like this:

305+

306+.. code-block:: idris

307+

308+ ||| Sequence two grammars. If either consumes some input, the sequence is

309+ ||| guaranteed to consume some input. If the first one consumes input, the

310+ ||| second is allowed to be recursive (because it means some input has been

311+ ||| consumed and therefore the input is smaller)

312+ export %inline

313+ (>>=) : {c1 : Bool} ->

314+ Grammar tok c1 a ->

315+ inf c1 (a -> Grammar tok c2 b) ->

316+ Grammar tok (c1 || c2) b

317+ (>>=) {c1 = False} = SeqEmpty

318+ (>>=) {c1 = True} = SeqEat

319+

276.. list-table::

320.. list-table::

277

321

278− * - Now for the operations, in this case: '+', '-' and '*'.

322+ * - This allows us to use ``do`` notation for the previous parenthesis example:

279− The syntax we require is that operators like '+' are infix operators, which

280− would require a definition like this:

281

323

282 - .. code-block:: idris

324 - .. code-block:: idris

283

325

284− expr = (add expr (op "+") expr)

326+ expr = intLiteral <|> do

327+ openParen

328+ r <- expr

329+ closeParen

330+ pure r

331+

332+This can be more flexible than using the ``<*>`` operator. Also it is defined

333+using ``Inf`` so we can implement recursively defined grammars like the above.

334+

335+Implementing the Arithmetic Operators

336+-------------------------------------

337+

338+.. list-table::

339+

340+ * - Now for the operations, in this case: ``+``, ``-`` and ``*``.

341+ The syntax we require for these infix operators

342+ would require recursive grammars like this:

343+

344+ - .. code-block:: idris

285

345

286−This is a potentially infinite structure which is not total.

346+ expr = expr (op "+") expr

347+

348+As already explained, ``do`` notation can allow us to use recursive

349+definitions but not necessarily left-recursion like this.

350+

287−In order to work up to this gradually I will start with prefix operators

351+In order to work up to this gradually lets start with prefix operators

288(sometimes known as Polish notation) then modify later for infix operators.

352(sometimes known as Polish notation) then modify later for infix operators.

289

353

290.. list-table::

354.. list-table::

@@ -295,7 +359,7 @@ In order to work up to this gradually I will start with prefix operators

295

359

296 expr = (add (op "+") expr expr)

360 expr = (add (op "+") expr expr)

297

361

298−where 'op' is defined like this:

362+where `op` is defined like this:

299

363

300.. code-block:: idris

364.. code-block:: idris

301

365

@@ -308,7 +372,7 @@ where 'op' is defined like this:

308

372

309.. list-table::

373.. list-table::

310

374

311− * - and 'add' is defined like this:

375+ * - and ``add`` is defined like this:

312

376

313 - .. code-block:: idris

377 - .. code-block:: idris

314

378

@@ -439,6 +503,17 @@ So far we have implemented a prefix notation for operators (like this:

439'expr + expr'). To do this we must be able to deal with potentially

503'expr + expr'). To do this we must be able to deal with potentially

440infinite data structures (see Codata Types here :ref:`sect-typefuns`).

504infinite data structures (see Codata Types here :ref:`sect-typefuns`).

441

505

506+.. code-block:: idris

507+

508+ expression = ["+"|"-"] term {("+"|"-") term} .

509+

510+ term = factor {("*"|"/") factor} .

511+

512+ factor =

513+ ident

514+ | number

515+ | "(" expression ")"

516+

442First alter the grammar to have infix operations:

517First alter the grammar to have infix operations:

443

518

444.. code-block:: idris

519.. code-block:: idris