git.iko.soy/Idris-dev
on master help sign in
start on Defining Block Structure using Indents
d689c19martinbaker
docs/parserLibrary/whitespace.rst+25−7
compare with master
unifiedsplit
@@ -48,13 +48,13 @@ This is added to the ``TokenMap`` like this:
48 (operator, \x => Operator x),
48 (operator, \x => Operator x),
49 (is '(' ,\x => OParen),
49 (is '(' ,\x => OParen),
50 (is ')' ,\x => CParen),
50 (is ')' ,\x => CParen),
51− (space, Comment),
51+ (spaces, Comment),
52 (comment, Comment)]
52 (comment, Comment)]
53
53
54As you can see, the comment is defined like a single line Idris comment,
54As you can see, the comment is defined like a single line Idris comment,
55it starts with ``--`` and continues for the remainder of the line.
55it starts with ``--`` and continues for the remainder of the line.
56
56
57−We don't need to define ``space`` because it is already defined in
57+We don't need to define ``spaces`` because it is already defined in
58: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Lexer.idr
58: https://github.com/idris-lang/Idris-dev/blob/master/libs/contrib/Text/Lexer.idr
59like this:
59like this:
60
60
@@ -75,11 +75,6 @@ Whitespace and Comments in Parser
75
75
76Now that there are ``Comment`` tokens the parser needs to be able to handle them.
76Now that there are ``Comment`` tokens the parser needs to be able to handle them.
77
77
78−So far we don't have any syntax that requires spaces to be significant so we
79−need to define the grammar so that it will parse with, or without, spaces.
80−This needs to be done in a systematic way, here I have defined the grammar so
81−that there is an optional space to the right of every atom or operator:
82−
83.. code-block:: idris
78.. code-block:: idris
84
79
85 commentSpace : Rule Integer
80 commentSpace : Rule Integer
@@ -87,6 +82,11 @@ that there is an optional space to the right of every atom or operator:
87 Comment s => Just 0
82 Comment s => Just 0
88 _ => Nothing)
83 _ => Nothing)
89
84
85+So far we don't have any syntax that requires spaces to be significant so we
86+need to define the grammar so that it will parse with, or without, spaces.
87+This 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:
89+
90.. code-block:: idris
90.. code-block:: idris
91
91
92 partial
92 partial
@@ -122,6 +122,24 @@ that there is an optional space to the right of every atom or operator:
122
122
123 expr = expr3 <|> exprAdd
123 expr = expr3 <|> exprAdd
124
124
125+Defining Block Structure using Indents
126+--------------------------------------
127+
128+Many languages such as Python, Haskell and Idris use indents to delimit
129+the block structure of the language.
130+
131+We can see how Idris2 does it here
132+: https://github.com/edwinb/Idris2/blob/master/src/Parser/Support.idr
133+
134+.. code-block:: idris
135+
136+ export
137+ IndentInfo : Type
138+ IndentInfo = Int
139+
140+ export
141+ init : IndentInfo
142+ init = 0
125
143
126
144
127
145