git.iko.soy/Idris-dev
on master help sign in
extend and fix parser library documentation
0ec3bdcmartinbaker
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.
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.
26 - Parser - This takes the list of tokens and outputs the code.
27
27
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
32
32
33The advantage of using two stages, like this, is that things like whitespace and
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.
34comments don't need to be considered in every parser rule.
35
35
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
38Idris type system prevents the construction of recognisers/rules that can't
39consume the input.
39consume the input.
40
40
41The Lexer is similar but works at the level of characters rather than tokens, and
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.
43a string when a rule is matched.
44
44
45The following pages contain a tutorial for the :ref:`parserLibraryLexer` and a
45The following pages contain a tutorial for the :ref:`parserLibraryLexer` and a
docs/parserLibrary/whitespace.rst+63−37
@@ -8,11 +8,11 @@ discussed how to handle whitespace and comments.
8
8
9In some grammars whitespace and comments would not be considered significant and
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
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``.
14
14
15−Also, I'm not sure if it is an problem for error messages and so on if some
15+Also, I'm not sure if it would be problem for error messages and so on if some
16text does not have corresponding tokens.
16text does not have corresponding tokens.
17
17
18So, on this page, we will add a token for whitespace and comments.
18So, on this page, we will add a token for whitespace and comments.
@@ -85,42 +85,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
85So 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.
86need 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
87This 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:
88+that there is an optional space to the right of every atom or operator.
89+First we add versions of ``intLiteral`` , ``openParen`` , ``closeParen``
90+and ``op`` that allow optional spaces/comments to the right of them:
89
91
90.. code-block:: idris
92.. code-block:: idris
91
93
92− partial
94+ intLiteralC : Rule Integer
95+ intLiteralC = (intLiteral <* commentSpace) <|> intLiteral
96+
93− exprAtom : Rule Integer
97+ openParenC : Rule Integer
94− exprAtom = (intLiteral <* commentSpace)
98+ openParenC = (openParen <* commentSpace) <|> openParen
95− <|> intLiteral <|> (paren expr)
99+
96−
100+ closeParenC : Rule Integer
97− partial
101+ closeParenC = (closeParen <* commentSpace) <|> closeParen
102+
103+ ||| like op but followed by optional comment or space
104+ opC : String -> Rule Integer
105+ opC s = ((op s) <* commentSpace) <|> (op s)
106+
107+Then we just use these functions instead of the original functions:
108+
109+.. code-block:: idris
110+
111+ expr : Rule Integer
112+
98− expr1 : Rule Integer
113+ factor : Rule Integer
114+ factor = intLiteralC <|> do
115+ openParenC
116+ r <- expr
117+ closeParenC
118+ pure r
119+
120+ term : Rule Integer
99− expr1 = map multInt exprAtom <*> (
121+ term = map multInt factor <*> (
100− (((op "*") <* commentSpace) <|> (op "*"))
122+ (opC "*")
101− *> exprAtom)
123+ *> factor)
102−
124+ <|> factor
103− partial
125+
104− exprMult : Rule Integer
105− exprMult = expr1 <|> exprAtom
106−
107− partial
108− expr2 : Rule Integer
109− expr2 = map addInt exprMult <*> (
126+ expr = map addInt term <*> (
110− (((op "+") <* commentSpace) <|> (op "+"))
127+ (opC "+")
111− *> exprMult)
128+ *> term)
112−
113− partial
114− exprAdd : Rule Integer
115− exprAdd = expr2 <|> exprMult
116−
117− partial
118− expr3 : Rule Integer
119− expr3 = map subInt exprAdd <*> (
129+ <|> map subInt term <*> (
120− (((op "-") <* commentSpace) <|> (op "-"))
130+ (opC "-")
121− *> expr)
131+ *> term)
122−
132+ <|> term
123− expr = expr3 <|> exprAdd
133+
134+ calc : String -> Either (ParseError (TokenData ExpressionToken))
135+ (Integer, List (TokenData ExpressionToken))
136+ calc s = parse expr (fst (lex expressionTokens s))
137+
138+ lft : (ParseError (TokenData ExpressionToken)) -> IO ()
139+ lft (Error s lst) = putStrLn ("error:"++s)
140+
141+ rht : (Integer, List (TokenData ExpressionToken)) -> IO ()
142+ rht i = putStrLn ("right " ++ (show i))
143+
144+ main : IO ()
145+ main = do
146+ putStr "alg>"
147+ x <- getLine
148+ either lft rht (calc x) -- eliminator for Either
149+
124
150
125Defining Block Structure using Indents
151Defining Block Structure using Indents
126--------------------------------------
152--------------------------------------