fc0acd9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #4805 from martinbaker/parseLibDoc2

fc0acd9Niklas Larsson7 years ago

docs/parserLibrary/introduction.rst+7−7

compare with master

unifiedsplit

@@ -25,21 +25,21 @@ complicated parser can be made out of many smaller ones.

25 - Lexer - This takes the input string and turns it into a list of Tokens.

26 - Parser - This takes the list of tokens and outputs the code.

28−.. image:: ../image/parserTopLevel.png

28+ - .. image:: ../image/parserTopLevel.png

29− :width: 307px

29+ :width: 307px

30− :height: 76px

30+ :height: 76px

31− :alt: diagram illustrating these stages of lexer and parser

31+ :alt: diagram illustrating these stages of lexer and parser

33The advantage of using two stages, like this, is that things like whitespace and

34comments don't need to be considered in every parser rule.

36−The Idris parser library differs from Parsec in that you need to say in the

36+The Idris parser library differs from Parsec in that you need to say, in the

37−Recogniser whether a rule is guaranteed to consume input. This means that the

37+Recogniser, whether a rule is guaranteed to consume input. This means that the

38Idris type system prevents the construction of recognisers/rules that can't

39consume the input.

41The Lexer is similar but works at the level of characters rather than tokens, and

42−you need to provide a TokenMap which says how to build a token representation from

42+you need to provide a TokenMap which defines how to build a token from

43a string when a rule is matched.

45The following pages contain a tutorial for the :ref:`parserLibraryLexer` and a

docs/parserLibrary/lexer.rst+25−19

@@ -10,13 +10,16 @@ module:

11 lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))

13+.. list-table::

14+

13−This function takes a String and returns a list of tokens. With the tokens we

15+ * - This function takes a String and returns a list of tokens. With the

14−have indexes back to the original string which can be used in error messages:

16+ tokens we have indexes back to the original string which can be used

17+ in error messages:

16−.. image:: ../image/tokenise.png

19+ - .. image:: ../image/tokenise.png

17− :width: 330px

20+ :width: 330px

18− :height: 73px

21+ :height: 73px

19− :alt: diagram illustrating these stages of lexer

22+ :alt: diagram illustrating these stages of lexer

21TokenMap

24TokenMap

22--------

25--------

@@ -34,21 +37,24 @@ this information:

34 (Lexer, String -> tokenType)

37 (Lexer, String -> tokenType)

36So for each Lexer in the list, if a substring in the input matches, run

39So for each Lexer in the list, if a substring in the input matches, run

37−the associated function to produce a token of type `tokenType`

40+the associated function to produce a token of type ``tokenType``

39−from Text.Lexer.Core:

42+.. list-table::

41−.. code-block:: idris

44+ * - from Text.Lexer.Core

45+ : https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Lexer/Core.idr

43− TokenMap : (tokenType : Type) -> Type

47+ - .. code-block:: idris

44− TokenMap tokenType = List (Lexer, String -> tokenType)

46−We can create a tokenMap by using a function like this:

49+ TokenMap : (tokenType : Type) -> Type

50+ TokenMap tokenType = List (Lexer, String -> tokenType)

52+ * - We can create a tokenMap by using a function like this:

53+

48−.. code-block:: idris

54+ - .. code-block:: idris

50− myTokenMap : TokenMap Token

56+ myTokenMap : TokenMap Token

51− myTokenMap = [(is 'a',CharLit)]

57+ myTokenMap = [(is 'a',CharLit)]

53Once we have a TokenMap we can use it to lex many strings.

59Once we have a TokenMap we can use it to lex many strings.

@@ -74,7 +80,7 @@ combined, for example,

75.. list-table::

81.. list-table::

77− * - <+> means sequence two recognisers. If either consumes a character,

83+ * - ``<+>`` means sequence two recognisers. If either consumes a character,

78 the sequence is guaranteed to consume a character.

84 the sequence is guaranteed to consume a character.

80 - .. code-block:: idris

86 - .. code-block:: idris

@@ -83,7 +89,7 @@ combined, for example,

83 SeqEat (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))

89 SeqEat (Pred (\ARG => intToBool (prim__eqChar ARG 'a')))

84 (Delay (is 'b')) : Recognise True

90 (Delay (is 'b')) : Recognise True

86− * - <|> means if both consume, the combination is guaranteed

92+ * - ``<|>`` means if both consume, the combination is guaranteed

87 to consumer a character:

93 to consumer a character:

89 - .. code-block:: idris

95 - .. code-block:: idris

@@ -161,7 +167,7 @@ able to parse simple arithmetic expressions, like this:

161so we need:

167so we need:

162

168

163- Numbers (for now integer literals are good enough).

169- Numbers (for now integer literals are good enough).

164−- Some operators (for now '+', '-' and '*' will do.

170+- Some operators (for now ``+``, ``-`` and ``*`` will do.

165- Opening and closing Parentheses.

171- Opening and closing Parentheses.

166

172

167We can define these, as tokens, like this:

173We can define these, as tokens, like this:

@@ -178,7 +184,7 @@ We can define these, as tokens, like this:

178 | EndInput

184 | EndInput

179

185

180It may help with debugging and to implement error messages to

186It may help with debugging and to implement error messages to

181−implement 'show' for these tokens:

187+implement ``show`` for these tokens:

182

188

183.. code-block:: idris

189.. code-block:: idris

184

190

docs/parserLibrary/parser.rst+190−112

@@ -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

@@ -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,13 +53,13 @@ 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'.

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>

@@ -89,8 +89,8 @@ 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

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,87 @@ 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+.. list-table::

284+

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

286+

287+ - .. code-block:: idris

288+

289+ partial

290+ expr : Rule Integer

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

292+

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

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

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

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

297+``killed by signal 11``.

298+

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

300+section.

301+

302+Monadic Combinator

303+------------------

304+

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

306+defined like this:

307+

308+.. code-block:: idris

309+

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

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

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

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

314+ export %inline

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

316+ Grammar tok c1 a ->

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

318+ Grammar tok (c1 || c2) b

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

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

321+

322+.. list-table::

323+

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

325+

326+ - .. code-block:: idris

327+

328+ expr = intLiteral <|> do

329+ openParen

330+ r <- expr

331+ closeParen

332+ pure r

333+

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

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

336+

337+Implementing the Arithmetic Operators

338+-------------------------------------

339+

276.. list-table::

340.. list-table::

277

341

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

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

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

343+ The syntax we require for these infix operators

280− would require a definition like this:

344+ would require recursive grammars like this:

281

345

282 - .. code-block:: idris

346 - .. code-block:: idris

283

347

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

348+ expr = expr (op "+") expr

349+

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

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

285

352

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

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

353+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.

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

289

355

290.. list-table::

356.. list-table::

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

295

361

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

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

297

363

298−where 'op' is defined like this:

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

299

365

300.. code-block:: idris

366.. code-block:: idris

301

367

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

308

374

309.. list-table::

375.. list-table::

310

376

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

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

378+

379+ Where:

380+

381+ - x is the add operator.

382+ - y is the first operand.

383+ - z is the second operand.

312

384

313 - .. code-block:: idris

385 - .. code-block:: idris

314

386

@@ -322,40 +394,37 @@ where 'op' is defined like this:

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

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

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

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

324

396

325−Where:

326

397

327−- x is the add operator.

328−- y is the first operand.

329−- z is the second operand.

330

398

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

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

332

400

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

401+.. list-table::

334

402

335−.. code-block:: idris

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

336

404

337− subInt : Integer -> Integer -> Integer

405+ - .. code-block:: idris

338− subInt a b = a-b

339

406

340− export

407+ subInt : Integer -> Integer -> Integer

341− sub : Grammar tok c1 Integer ->

408+ subInt a b = a-b

342− Grammar tok c2 Integer ->

343− Grammar tok c3 Integer ->

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

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

346

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

347

416

348− multInt : Integer -> Integer -> Integer

417+ multInt : Integer -> Integer -> Integer

349− multInt a b = a*b

418+ multInt a b = a*b

350

419

351− export

420+ export

352− mult : Grammar tok c1 Integer ->

421+ mult : Grammar tok c1 Integer ->

353− Grammar tok c2 Integer ->

422+ Grammar tok c2 Integer ->

354− Grammar tok c3 Integer ->

423+ Grammar tok c3 Integer ->

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

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

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

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

357

426

358−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

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

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

360

429

361.. code-block:: idris

430.. code-block:: idris

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

408 List (TokenData ExpressionToken))

477 List (TokenData ExpressionToken))

409

478

410However 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,

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

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

412

481

413.. code-block:: idris

482.. code-block:: idris

414

483

@@ -435,8 +504,8 @@ Infix Notation

435--------------

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

436

505

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

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

438−'+ 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:

439−'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

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

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

441

510

442First alter the grammar to have infix operations:

511First alter the grammar to have infix operations:

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

494

563

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

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

496

565

497−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

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

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

499

568

500−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

501so 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

502first tokens would not be consumed.

571first tokens would not be consumed.

503

572

@@ -524,52 +593,64 @@ That is we convert a general context-free grammar to a LL(1) grammar. Although

524not 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.

525

594

526This 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

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

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

528

597

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

598+.. list-table::

530−

531−.. code-block:: idris

532

599

533− paren : Rule Integer -> Rule Integer

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

534− paren exp = openParen *> exp <* closeParen

601+ Where braces ``{ ... }`` mean the contents can occur 1 or more times.

535

602

536− addInt : Integer -> Integer -> Integer

603+ - .. code-block:: idris

537− addInt a b = a+b

538

604

539− subInt : Integer -> Integer -> Integer

605+ 'expression' ::= ('+'|'-') 'term' {('+'|'-') 'term'}

540− subInt a b = a-b

541

606

542− multInt : Integer -> Integer -> Integer

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

543− multInt a b = a*b

544

608

545− partial

609+ 'factor' ::=

546− expr : Rule Integer

610+ number

611+ | '(' 'expression' ')'

547

612

548− partial

549− exprAtom : Rule Integer

550− exprAtom = intLiteral <|> (paren expr)

551

613

552− partial

614+.. code-block:: idris

553− expr1 : Rule Integer

554− expr1 = map multInt exprAtom <*> ((op "*") *> exprAtom)

555

615

556− partial

557− exprMult : Rule Integer

616+ expr : Rule Integer

558− exprMult = expr1 <|> exprAtom

559

617

560− partial

618+ factor : Rule Integer

619+ factor = intLiteral <|> do

620+ openParen

621+ r <- expr

622+ closeParen

623+ pure r

624+

561− expr2 : Rule Integer

625+ term : Rule Integer

562− expr2 = map addInt exprMult <*> ((op "+") *> exprMult)

626+ term = map multInt factor <*> (

627+ (op "*")

628+ *> factor)

629+ <|> factor

630+

631+ expr = map addInt term <*> (

632+ (op "+")

633+ *> term)

634+ <|> map subInt term <*> (

635+ (op "-")

636+ *> term)

637+ <|> term

638+

639+ calc : String -> Either (ParseError (TokenData ExpressionToken))

640+ (Integer, List (TokenData ExpressionToken))

641+ calc s = parse expr (fst (lex expressionTokens s))

563

642

564− partial

643+ lft : (ParseError (TokenData ExpressionToken)) -> IO ()

565− exprAdd : Rule Integer

644+ lft (Error s lst) = putStrLn ("error:"++s)

566− exprAdd = expr2 <|> exprMult

567

645

568− partial

646+ rht : (Integer, List (TokenData ExpressionToken)) -> IO ()

569− expr3 : Rule Integer

647+ rht i = putStrLn ("right " ++ (show i))

570− expr3 = map subInt exprAdd <*> ((op "-") *> expr)

571

648

572− expr = expr3 <|> exprAdd

649+ main : IO ()

650+ main = do

651+ putStr "alg>"

652+ x <- getLine

653+ either lft rht (calc x) -- eliminator for Either

573

654

574As the following tests show, this now handles infix operators and precedence.

655As the following tests show, this now handles infix operators and precedence.

575

656

@@ -579,44 +660,41 @@ As the following tests show, this now handles infix operators and precedence.

579

660

580 - .. code-block:: idris

661 - .. code-block:: idris

581

662

582− *parserExInfix> test "2*3"

663+ *algebraREPL> :exec

583− Right (6,

664+ alg>2*3

584− []) : Either (ParseError (TokenData ExpressionToken))

665+ right (6, [])

585− (Integer, List (TokenData ExpressionToken))

586

666

587 * - Check that atomic number literals work:

667 * - Check that atomic number literals work:

588

668

589 - .. code-block:: idris

669 - .. code-block:: idris

590

670

591− *parserExInfix> test "2"

671+ *algebraREPL> :exec

592− Right (2,

672+ alg>2

593− []) : Either (ParseError (TokenData ExpressionToken))

673+ right (2, [])

594− (Integer, List (TokenData ExpressionToken))

595

674

596 * - Check that '*' has a higher precedence than '+'.

675 * - Check that '*' has a higher precedence than '+'.

597

676

598 - .. code-block:: idris

677 - .. code-block:: idris

599

678

600− *parserExInfix> test "2+3*4"

679+ *algebraREPL> :exec

601− Right (14,

680+ alg>2+3*4

602− []) : Either (ParseError (TokenData ExpressionToken))

681+ right (14, [])

603− (Integer, List (TokenData ExpressionToken))

604

682

605 * - Also '*' has a higher precedence than '+' when the order is reversed.

683 * - Also '*' has a higher precedence than '+' when the order is reversed.

606

684

607 - .. code-block:: idris

685 - .. code-block:: idris

608

686

609− *parserExInfix> test "3*4+2"

687+ *algebraREPL> :exec

610− Right (14,

688+ alg>3*4+2

611− []) : Either (ParseError (TokenData ExpressionToken))

689+ right (14, [])

612− (Integer, List (TokenData ExpressionToken))

613

690

614 * - Also precedence can be overridden by parenthesis.

691 * - Also precedence can be overridden by parenthesis.

615

692

616 - .. code-block:: idris

693 - .. code-block:: idris

617

694

618− *parserExInfix> test "(2+3)*4"

695+ *algebraREPL> :exec

619− Right (20,

696+ alg>(2+3)*4

620− []) : Either (ParseError (TokenData ExpressionToken))

697+ right (20, [])

621− (Integer, List (TokenData ExpressionToken))

622

698

699+This is still not correct because it does not correctly parse multiple sums or terms

700+like ``1+2+3`` or ``1*2*3``.

docs/parserLibrary/whitespace.rst+131−35

@@ -8,14 +8,16 @@ discussed how to handle whitespace and comments.

9In some grammars whitespace and comments would not be considered significant and

10so we might be tempted not to generate any tokens for them. However, in the

11−running example, we may want to make spaces significant. For example, we might

11+running example, we may want to make spaces significant in the future. For

12−want to implement function application expressed by juxtaposition as in

12+example, we might want to implement function application expressed by

13−Haskell and Idris like this: ``f x``.

13+juxtaposition as in Haskell and Idris like this: ``f x``.

15−Also, I'm not sure if it is an problem for error messages and so on if some

15+So, on this page, we will add a token for whitespace and comments. We will

16−text does not have corresponding tokens.

16+then consider two ways to process this:

18−So, on this page, we will add a token for whitespace and comments.

18+- Filter all whitespace tokens from the lexer results before passing to

19+ the parser.

20+- Process the whitespace tokens in the parser.

20Whitespace and Comments in Lexer

22Whitespace and Comments in Lexer

21--------------------------------

23--------------------------------

@@ -70,10 +72,31 @@ like this:

70 spaces : Lexer

72 spaces : Lexer

71 spaces = some space

73 spaces = some space

75+If these whitespace tokens are not significant, that is, they can appear

76+anywhere and they are optional then we can filter them out before the parser

77+gets them like this:

78+

79+.. code-block:: idris

80+

81+ processWhitespace : (List (TokenData ExpressionToken), Int, Int, String)

82+ -> (List (TokenData ExpressionToken), Int, Int, String)

83+ processWhitespace (x,l,c,s) = ((filter notComment x),l,c,s) where

84+ notComment : TokenData ExpressionToken -> Bool

85+ notComment t = case tok t of

86+ Comment _ => False

87+ _ => True

88+

89+ calc : String -> Either (ParseError (TokenData ExpressionToken))

90+ (Integer, List (TokenData ExpressionToken))

91+ calc s = parse expr (fst (processWhitespace (lex expressionTokens s)))

92+

93+

73Whitespace and Comments in Parser

94Whitespace and Comments in Parser

74---------------------------------

95---------------------------------

97+If we sometimes require whitespace to be significant then we can't filter

98+them out as above. In this case the ``Comment`` tokens are sent to the parser

76−Now that there are ``Comment`` tokens the parser needs to be able to handle them.

99+which now needs to be able to handle them.

100

78.. code-block:: idris

101.. code-block:: idris

102

@@ -85,42 +108,68 @@ Now that there are ``Comment`` tokens the parser needs to be able to handle them

85So far we don't have any syntax that requires spaces to be significant so we

108So far we don't have any syntax that requires spaces to be significant so we

86need to define the grammar so that it will parse with, or without, spaces.

109need to define the grammar so that it will parse with, or without, spaces.

87This needs to be done in a systematic way, here I have defined the grammar so

110This needs to be done in a systematic way, here I have defined the grammar so

88−that there is an optional space to the right of every atom or operator:

111+that there is an optional space to the right of every atom or operator.

112+First add versions of ``intLiteral`` , ``openParen`` , ``closeParen``

113+and ``op`` that allow optional spaces/comments to the right of them:

114

90.. code-block:: idris

115.. code-block:: idris

116

92− partial

93− exprAtom : Rule Integer

117+ intLiteralC : Rule Integer

94− exprAtom = (intLiteral <* commentSpace)

118+ intLiteralC = (intLiteral <* commentSpace) <|> intLiteral

95− <|> intLiteral <|> (paren expr)

119+

120+ openParenC : Rule Integer

121+ openParenC = (openParen <* commentSpace) <|> openParen

122

97− partial

98− expr1 : Rule Integer

123+ closeParenC : Rule Integer

99− expr1 = map multInt exprAtom <*> (

100− (((op "*") <* commentSpace) <|> (op "*"))

124+ closeParenC = (closeParen <* commentSpace) <|> closeParen

101− *> exprAtom)

102

125

103− partial

126+ ||| like op but followed by optional comment or space

104− exprMult : Rule Integer

127+ opC : String -> Rule Integer

105− exprMult = expr1 <|> exprAtom

128+ opC s = ((op s) <* commentSpace) <|> (op s)

106

129

107− partial

130+Then just use these functions instead of the original functions:

108− expr2 : Rule Integer

131+

109− expr2 = map addInt exprMult <*> (

132+.. code-block:: idris

110− (((op "+") <* commentSpace) <|> (op "+"))

111− *> exprMult)

112

133

113− partial

114− exprAdd : Rule Integer

134+ expr : Rule Integer

115− exprAdd = expr2 <|> exprMult

116

135

117− partial

136+ factor : Rule Integer

137+ factor = intLiteralC <|> do

138+ openParenC

139+ r <- expr

140+ closeParenC

141+ pure r

142+

118− expr3 : Rule Integer

143+ term : Rule Integer

119− expr3 = map subInt exprAdd <*> (

144+ term = map multInt factor <*> (

120− (((op "-") <* commentSpace) <|> (op "-"))

145+ (opC "*")

121− *> expr)

146+ *> factor)

147+ <|> factor

148+

149+ expr = map addInt term <*> (

150+ (opC "+")

151+ *> term)

152+ <|> map subInt term <*> (

153+ (opC "-")

154+ *> term)

155+ <|> term

156+

157+ calc : String -> Either (ParseError (TokenData ExpressionToken))

158+ (Integer, List (TokenData ExpressionToken))

159+ calc s = parse expr (fst (lex expressionTokens s))

160+

161+ lft : (ParseError (TokenData ExpressionToken)) -> IO ()

162+ lft (Error s lst) = putStrLn ("error:"++s)

163+

164+ rht : (Integer, List (TokenData ExpressionToken)) -> IO ()

165+ rht i = putStrLn ("right " ++ (show i))

166+

167+ main : IO ()

168+ main = do

169+ putStr "alg>"

170+ x <- getLine

171+ either lft rht (calc x) -- eliminator for Either

122

172

123− expr = expr3 <|> exprAdd

124

173

125Defining Block Structure using Indents

174Defining Block Structure using Indents

126--------------------------------------

175--------------------------------------

@@ -141,14 +190,61 @@ We can see how Idris2 does it here

141 init : IndentInfo

190 init : IndentInfo

142 init = 0

191 init = 0

143

192

193+EndInput Token

194+--------------

195+

196+So far, the parser will return a successful result even if the full input

197+is not consumed. To ensure that the top level syntax is fully matched we

198+add a ``EndInput`` token to indicate the last token.

199+

200+``EndInput`` is added to the other tokens like this:

144

201

202+.. code-block:: idris

145

203

204+ data ExpressionToken = Number Integer

205+ | Operator String

206+ | OParen

207+ | CParen

208+ | Comment String

209+ | EndInput

146

210

211+A rule to consume this token is added:

147

212

213+.. code-block:: idris

148

214

215+ eoi : Rule Integer

216+ eoi = terminal (\x => case tok x of

217+ EndInput => Just 0

218+ _ => Nothing)

149

219

220+Instead of using ``expr`` at the top level of the syntax we can now define

221+``exprFull`` as shown here. This will make sure that only when ``EndInput``

222+is consumed will the parse be successful:

150

223

224+.. code-block:: idris

225+

226+ exprFull : Rule Integer

227+ exprFull = expr <* eoi

228+

229+The following code makes sure ``EndInput`` is added to the end of the token

230+list:

231+

232+.. code-block:: idris

233+

234+ processWhitespace : (List (TokenData ExpressionToken), Int, Int, String)

235+ -> (List (TokenData ExpressionToken), Int, Int, String)

236+ processWhitespace (x,l,c,s) = ((filter notComment x)++

237+ [MkToken l c EndInput],l,c,s) where

238+ notComment : TokenData ExpressionToken -> Bool

239+ notComment t = case tok t of

240+ Comment _ => False

241+ _ => True

151

242

243+All we have to do now is use ``exprFull`` instead of ``expr``:

244+

245+.. code-block:: idris

152

246

247+ calc : String -> Either (ParseError (TokenData ExpressionToken))

248+ (Integer, List (TokenData ExpressionToken))

249+ calc s = parse exprFull (fst (processWhitespace (lex expressionTokens s)))

153

250

154−