@@ -73,6 +73,7 @@ getLetIdentifier src@(Src left _ text) =
73
73
where parseLetIdentifier = do
74
74
setSourcePos left
75
75
_let
76
+ whitespace
76
77
begin <- getSourcePos
77
78
(tokens, _) <- Megaparsec. match label
78
79
end <- getSourcePos
@@ -86,7 +87,9 @@ getLamIdentifier (Src left _ text) =
86
87
where parseLetIdentifier = do
87
88
setSourcePos left
88
89
_lambda
90
+ whitespace
89
91
_openParens
92
+ whitespace
90
93
begin <- getSourcePos
91
94
(tokens, _) <- Megaparsec. match label
92
95
end <- getSourcePos
@@ -100,7 +103,9 @@ getForallIdentifier (Src left _ text) =
100
103
where parseLetIdentifier = do
101
104
setSourcePos left
102
105
_forall
106
+ whitespace
103
107
_openParens
108
+ whitespace
104
109
begin <- getSourcePos
105
110
(tokens, _) <- Megaparsec. match label
106
111
end <- getSourcePos
@@ -116,6 +121,7 @@ getImportHash (Src left _ text) =
116
121
where parseImportHashPosition = do
117
122
setSourcePos left
118
123
_ <- importType_
124
+ whitespace
119
125
begin <- getSourcePos
120
126
(tokens, _) <- Megaparsec. match $ optional importHash_
121
127
end <- getSourcePos
@@ -166,37 +172,57 @@ binderExprFromText txt =
166
172
167
173
closedLet = do
168
174
_let
175
+ nonemptyWhitespace
169
176
_ <- label
177
+ whitespace
170
178
_ <- optional (do
171
179
_colon
180
+ nonemptyWhitespace
172
181
expr)
173
182
_equal
183
+ whitespace
174
184
_ <- expr
185
+ whitespace
175
186
(do
176
187
_in
188
+ nonemptyWhitespace
177
189
_ <- expr
178
190
return () )
179
191
<|> closedLet
180
192
181
193
closedLambda = do
182
194
_lambda
195
+ whitespace
183
196
_openParens
197
+ whitespace
184
198
_ <- label
199
+ whitespace
185
200
_colon
201
+ nonemptyWhitespace
186
202
_ <- expr
203
+ whitespace
187
204
_closeParens
205
+ whitespace
188
206
_arrow
207
+ whitespace
189
208
_ <- expr
190
209
return ()
191
210
192
211
closedPi = do
193
212
_forall
213
+ whitespace
194
214
_openParens
215
+ whitespace
195
216
_ <- label
217
+ whitespace
196
218
_colon
219
+ nonemptyWhitespace
197
220
_ <- expr
221
+ whitespace
198
222
_closeParens
223
+ whitespace
199
224
_arrow
225
+ whitespace
200
226
_ <- expr
201
227
return ()
202
228
@@ -219,33 +245,45 @@ binderExprFromText txt =
219
245
220
246
letBinder = do
221
247
_let
248
+ nonemptyWhitespace
222
249
name <- label
223
- mType <- optional (do _colon; _type <- expr; return (Nothing , _type))
250
+ whitespace
251
+ mType <- optional (do _colon; nonemptyWhitespace; _type <- expr; whitespace; return (Nothing , _type))
224
252
225
253
-- if the bound value does not parse, skip and replace with 'hole'
226
- value <- try (do _equal; expr)
254
+ value <- try (do _equal; whitespace; expr <* whitespace )
227
255
<|> (do skipManyTill anySingle (lookAhead boundary <|> _in); return holeExpr)
228
256
inner <- parseBinderExpr
229
257
return (Let (Binding Nothing name Nothing mType Nothing value) inner)
230
258
231
259
forallBinder = do
232
260
_forall
261
+ whitespace
233
262
_openParens
263
+ whitespace
234
264
name <- label
265
+ whitespace
235
266
_colon
267
+ nonemptyWhitespace
236
268
-- if the bound type does not parse, skip and replace with 'hole'
237
- typ <- try (do e <- expr; _closeParens; _arrow; return e)
269
+ typ <- try (do e <- expr; whitespace; _closeParens; whitespace ; _arrow; return e)
238
270
<|> (do skipManyTill anySingle _arrow; return holeExpr)
271
+ whitespace
239
272
inner <- parseBinderExpr
240
273
return (Pi name typ inner)
241
274
242
275
lambdaBinder = do
243
276
_lambda
277
+ whitespace
244
278
_openParens
279
+ whitespace
245
280
name <- label
281
+ whitespace
246
282
_colon
283
+ nonemptyWhitespace
247
284
-- if the bound type does not parse, skip and replace with 'hole'
248
- typ <- try (do e <- expr; _closeParens; _arrow; return e)
285
+ typ <- try (do e <- expr; whitespace; _closeParens; whitespace ; _arrow; return e)
249
286
<|> (do skipManyTill anySingle _arrow; return holeExpr)
287
+ whitespace
250
288
inner <- parseBinderExpr
251
289
return (Lam name typ inner)
0 commit comments