50db7e1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

tidy up

50db7e1martinbaker7 years ago

docs/parserLibrary/parser.rst+62−55

compare with master

unifiedsplit

@@ -3,7 +3,7 @@

3Parser

4======

6−To run the 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

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

9.. code-block:: idris

@@ -18,13 +18,13 @@ If successful this returns 'Right' with a pair of

19otherwise it returns 'Left' with the error message.

21−So we need to define the Grammar for our parser, this is done using the following

21+So we need to define the grammar for our parser, this is done using the following

22'Grammar' data structure. This is a combinator structure, similar in principle

23to the recogniser combinator for the lexer, which was discussed on the

24previous page.

26−As with the Recogniser the Grammar type is dependent on a boolean 'consumes'

26+As with the Recogniser the ``Grammar`` type is dependent on a boolean 'consumes'

27−value which allows us to ensure that complicated Grammar structures will always

27+value which allows us to ensure that complicated ``Grammar`` structures will always

28consume input.

30.. code-block:: idris

@@ -53,7 +53,7 @@ consume input.

53 Grammar tok c1 ty -> Grammar tok c2 ty ->

54 Grammar tok (c1 && c2) ty

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

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

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

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

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

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

90.. list-table::

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

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

93 sequence of numeric characters).

95 - .. code-block:: idris

@@ -280,13 +280,15 @@ So lets try to use this to define a grammar which recognises either:

280- An integer literal inside parenthesis inside parenthesis

281- ... and so on.

282

283−This requires a recursively defined structure like this:

283+.. list-table::

284

285−.. code-block:: idris

285+ * - This requires a recursively defined structure like this:

286

287+ - .. code-block:: idris

288+

287− partial

289+ partial

288− expr : Rule Integer

290+ expr : Rule Integer

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

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

290

292

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

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

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

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

@@ -330,7 +332,7 @@ defined like this:

330 pure r

332 pure r

331

333

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

334This 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.

335+using ``Inf`` so we can implement recursively defined grammars as above.

334

336

335Implementing the Arithmetic Operators

337Implementing the Arithmetic Operators

336-------------------------------------

338-------------------------------------

@@ -359,7 +361,7 @@ In order to work up to this gradually lets start with prefix operators

359

361

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

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

361

363

362−where `op` is defined like this:

364+where ``op`` is defined like this:

363

365

364.. code-block:: idris

366.. code-block:: idris

365

367

@@ -374,6 +376,12 @@ where `op` is defined like this:

374

376

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

377 * - and ``add`` is defined like this:

376

378

379+ Where:

380+

381+ - x is the add operator.

382+ - y is the first operand.

383+ - z is the second operand.

384+

377 - .. code-block:: idris

385 - .. code-block:: idris

378

386

379 addInt : Integer -> Integer -> Integer

387 addInt : Integer -> Integer -> Integer

@@ -386,40 +394,37 @@ where `op` is defined like this:

386 Grammar tok ((c1 || c2) || c3) Integer

394 Grammar tok ((c1 || c2) || c3) Integer

387 add x y z = map addInt (x *> y) <*> z

395 add x y z = map addInt (x *> y) <*> z

388

396

389−Where:

390

397

391−- x is the add operator.

392−- y is the first operand.

393−- z is the second operand.

394

398

395The resulting integer will be the sum of the two operands.

399The resulting integer will be the sum of the two operands.

396

400

397−The other operators are defined in a similar way:

401+.. list-table::

398

402

399−.. code-block:: idris

403+ * - The other operators are defined in a similar way:

400

404

401− subInt : Integer -> Integer -> Integer

405+ - .. code-block:: idris

402− subInt a b = a-b

403

406

404− export

407+ subInt : Integer -> Integer -> Integer

405− sub : Grammar tok c1 Integer ->

408+ subInt a b = a-b

406− Grammar tok c2 Integer ->

407− Grammar tok c3 Integer ->

408− Grammar tok ((c1 || c2) || c3) Integer

409− sub x y z = map subInt (x *> y) <*> z

410

409

410+ export

411+ sub : Grammar tok c1 Integer ->

412+ Grammar tok c2 Integer ->

413+ Grammar tok c3 Integer ->

414+ Grammar tok ((c1 || c2) || c3) Integer

415+ sub x y z = map subInt (x *> y) <*> z

411

416

412− multInt : Integer -> Integer -> Integer

417+ multInt : Integer -> Integer -> Integer

413− multInt a b = a*b

418+ multInt a b = a*b

414

419

415− export

420+ export

416− mult : Grammar tok c1 Integer ->

421+ mult : Grammar tok c1 Integer ->

417− Grammar tok c2 Integer ->

422+ Grammar tok c2 Integer ->

418− Grammar tok c3 Integer ->

423+ Grammar tok c3 Integer ->

419− Grammar tok ((c1 || c2) || c3) Integer

424+ Grammar tok ((c1 || c2) || c3) Integer

420− mult x y z = map multInt (x *> y) <*> z

425+ mult x y z = map multInt (x *> y) <*> z

421

426

422−So the top level Grammar can now be defined as follows. Note that this is

427+So the top level ``Grammar`` can now be defined as follows. Note that this is

423partial as it is a potentially infinite structure and so not total.

428partial as it is a potentially infinite structure and so not total.

424

429

425.. code-block:: idris

430.. code-block:: idris

@@ -472,7 +477,7 @@ Then an invalid syntax:

472 List (TokenData ExpressionToken))

477 List (TokenData ExpressionToken))

473

478

474However if we try something that is invalid, but starts with a valid token,

479However if we try something that is invalid, but starts with a valid token,

475−then it will return 'Right' (to indicate success)

480+then it will return ``Right`` (to indicate success)

476

481

477.. code-block:: idris

482.. code-block:: idris

478

483

@@ -499,21 +504,10 @@ Infix Notation

499--------------

504--------------

500

505

501So far we have implemented a prefix notation for operators (like this:

506So far we have implemented a prefix notation for operators (like this:

502−'+ expr expr') but the aim is to implemented an infix notation (like this:

507+``+ expr expr``) but the aim is to implemented an infix notation (like this:

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

508+``expr + expr``). To do this we must be able to deal with potentially

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

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

505

510

506−.. code-block:: idris

507−

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

509−

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

511−

512− factor =

513− ident

514− | number

515− | "(" expression ")"

516−

517First alter the grammar to have infix operations:

511First alter the grammar to have infix operations:

518

512

519.. code-block:: idris

513.. code-block:: idris

@@ -569,10 +563,10 @@ If we have a rule like this:

569

563

570 A -> (x<*>y) <|> (x<*>z)

564 A -> (x<*>y) <|> (x<*>z)

571

565

572−If 'x<*>y' fails but 'x<*>z' would succeed a problem is that, 'x<*>y' has

566+If ``x<*>y`` fails but ``x<*>z`` would succeed a problem is that, ``x<*>y`` has

573−already consumed 'x', so now 'x<*>z' will fail.

567+already consumed ``x``, so now ``x<*>z`` will fail.

574

568

575−so we could write code to backtrack. That is 'try' 'x<*>y' without consuming

569+so we could write code to backtrack. That is ``try`` ``x<*>y`` without consuming

576so that, if the first token succeeds but the following tokens fail, then the

570so that, if the first token succeeds but the following tokens fail, then the

577first tokens would not be consumed.

571first tokens would not be consumed.

578

572

@@ -599,9 +593,22 @@ That is we convert a general context-free grammar to a LL(1) grammar. Although

599not every context-free grammar can be converted to a LL(1) grammar.

593not every context-free grammar can be converted to a LL(1) grammar.

600

594

601This still does not solve the infinite recursion issue and there is another

595This still does not solve the infinite recursion issue and there is another

602−problem: the precedence of the operators +, - and * is not explicit.

596+problem: the precedence of the operators ``+``, ``-`` and ``*`` is not explicit.

597+

598+.. list-table::

599+

600+ * - To resolve this we can alter the example to have a BNF like this:

601+

602+ - .. code-block:: idris

603+

604+ 'expression' ::= ['+'|'-'] 'term' {('+'|'-') 'term'}

605+

606+ 'term' ::= 'factor' {'*' 'factor'}

607+

608+ 'factor' ::=

609+ number

610+ | '(' 'expression' ')'

603

611

604−To resolve this we can alter the example like this:

605

612

606.. code-block:: idris

613.. code-block:: idris

607

614