/
Do.lean
251 lines (225 loc) · 10.4 KB
/
Do.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Lean.Parser.Term
namespace Lean
namespace Parser
builtin_initialize registerBuiltinParserAttribute `builtin_doElem_parser ``Category.doElem
builtin_initialize registerBuiltinDynamicParserAttribute `doElem_parser `doElem
@[inline] def doElemParser (rbp : Nat := 0) : Parser :=
categoryParser `doElem rbp
namespace Term
def leftArrow : Parser := unicodeSymbol "← " "<- "
@[builtin_term_parser] def liftMethod := leading_parser:minPrec
leftArrow >> termParser
def doSeqItem := leading_parser
ppLine >> doElemParser >> optional "; "
def doSeqIndent := leading_parser
many1Indent doSeqItem
def doSeqBracketed := leading_parser
"{" >> withoutPosition (many1 doSeqItem) >> ppLine >> "}"
/-- A `doSeq` is a sequence of `doElem`, the main argument after the `do` keyword and other
do elements that take blocks. It can either have the form `"{" (doElem ";"?)* "}"` or
`many1Indent (doElem ";"?)`, where `many1Indent` ensures that all the items are at
the same or higher indentation level as the first line. -/
def doSeq :=
withAntiquot (mkAntiquot "doSeq" decl_name% (isPseudoKind := true)) <|
doSeqBracketed <|> doSeqIndent
/-- `termBeforeDo` is defined as `withForbidden("do", term)`, which will parse a term but
disallows `do` outside of a bracketing construct. This is used for parsers like `for _ in t do ...`
or `unless t do ...`, where we do not want `t do ...` to be parsed as an application of `t` to a
`do` block, which would otherwise be allowed. -/
def termBeforeDo := withForbidden "do" termParser
attribute [run_builtin_parser_attribute_hooks] doSeq termBeforeDo
builtin_initialize
register_parser_alias doSeq
register_parser_alias termBeforeDo
def notFollowedByRedefinedTermToken :=
-- Remark: we don't currently support `open` and `set_option` in `do`-blocks,
-- but we include them in the following list to fix the ambiguity where
-- an "open" command follows the `do`-block.
-- If we don't add `do`, then users would have to indent `do` blocks or use `{ ... }`.
notFollowedBy ("set_option" <|> "open" <|> "if" <|> "match" <|> "match_expr" <|> "let" <|> "let_expr" <|> "have" <|>
"do" <|> "dbg_trace" <|> "assert!" <|> "for" <|> "unless" <|> "return" <|> symbol "try")
"token at 'do' element"
@[builtin_doElem_parser] def doLet := leading_parser
"let " >> optional "mut " >> letDecl
@[builtin_doElem_parser] def doLetElse := leading_parser
"let " >> optional "mut " >> termParser >> " := " >> termParser >>
checkColGt >> " | " >> doSeq
@[builtin_doElem_parser] def doLetExpr := leading_parser
"let_expr " >> matchExprPat >> " := " >> termParser >>
checkColGt >> " | " >> doSeq
@[builtin_doElem_parser] def doLetMetaExpr := leading_parser
"let_expr " >> matchExprPat >> " ← " >> termParser >>
checkColGt >> " | " >> doSeq
@[builtin_doElem_parser] def doLetRec := leading_parser
group ("let " >> nonReservedSymbol "rec ") >> letRecDecls
def doIdDecl := leading_parser
atomic (ident >> optType >> ppSpace >> leftArrow) >>
doElemParser
def doPatDecl := leading_parser
atomic (termParser >> ppSpace >> leftArrow) >>
doElemParser >> optional (checkColGt >> " | " >> doSeq)
@[builtin_doElem_parser] def doLetArrow := leading_parser
withPosition ("let " >> optional "mut " >> (doIdDecl <|> doPatDecl))
-- We use `letIdDeclNoBinders` to define `doReassign`.
-- Motivation: we do not reassign functions, and avoid parser conflict
def letIdDeclNoBinders := node ``letIdDecl <|
atomic (ident >> pushNone >> optType >> " := ") >> termParser
@[builtin_doElem_parser] def doReassign := leading_parser
notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl)
@[builtin_doElem_parser] def doReassignArrow := leading_parser
notFollowedByRedefinedTermToken >> (doIdDecl <|> doPatDecl)
@[builtin_doElem_parser] def doHave := leading_parser
"have" >> Term.haveDecl
/-
In `do` blocks, we support `if` without an `else`.
Thus, we use indentation to prevent examples such as
```
if c_1 then
if c_2 then
action_1
else
action_2
```
from being parsed as
```
if c_1 then {
if c_2 then {
action_1
} else {
action_2
}
}
```
We also have special support for `else if` because we don't want to write
```
if c_1 then
action_1
else if c_2 then
action_2
else
action_3
```
-/
def elseIf := atomic (group (withPosition ("else " >> checkLineEq >> " if ")))
-- ensure `if $e then ...` still binds to `e:term`
def doIfLetPure := leading_parser " := " >> termParser
def doIfLetBind := leading_parser " ← " >> termParser
def doIfLet := leading_parser (withAnonymousAntiquot := false)
"let " >> termParser >> (doIfLetPure <|> doIfLetBind)
def doIfProp := leading_parser (withAnonymousAntiquot := false)
optIdent >> termParser
def doIfCond :=
withAntiquot (mkAntiquot "doIfCond" decl_name% (anonymous := false) (isPseudoKind := true)) <|
doIfLet <|> doIfProp
-- must reset cache as `withPositionAfterLinebreak` will look at syntax not produced by this parser (or even
-- current category call)
@[builtin_doElem_parser] def doIf := leading_parser withResetCache <| withPositionAfterLinebreak <| ppRealGroup <|
ppRealFill (ppIndent ("if " >> doIfCond >> " then") >> ppSpace >> doSeq) >>
many (checkColGe "'else if' in 'do' must be indented" >>
group (ppDedent ppSpace >> ppRealFill (elseIf >> doIfCond >> " then " >> doSeq))) >>
optional (checkColGe "'else' in 'do' must be indented" >>
ppDedent ppSpace >> ppRealFill ("else " >> doSeq))
@[builtin_doElem_parser] def doUnless := leading_parser
"unless " >> withForbidden "do" termParser >> " do " >> doSeq
def doForDecl := leading_parser
optional (atomic (ident >> " : ")) >> termParser >> " in " >> withForbidden "do" termParser
/--
`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass.
`break` and `continue` are supported inside `for` loops.
`for x in e, x2 in e2, ... do s` iterates of the given collections in parallel,
until at least one of them is exhausted.
The types of `e2` etc. must implement the `ToStream` typeclass.
-/
@[builtin_doElem_parser] def doFor := leading_parser
"for " >> sepBy1 doForDecl ", " >> "do " >> doSeq
def doMatchAlts := ppDedent <| matchAlts (rhsParser := doSeq)
@[builtin_doElem_parser] def doMatch := leading_parser:leadPrec
"match " >> optional Term.generalizingParam >> optional Term.motive >>
sepBy1 matchDiscr ", " >> " with" >> doMatchAlts
def doMatchExprAlts := ppDedent <| matchExprAlts (rhsParser := doSeq)
def optMetaFalse :=
optional (atomic ("(" >> nonReservedSymbol "meta" >> " := " >> nonReservedSymbol "false" >> ") "))
@[builtin_doElem_parser] def doMatchExpr := leading_parser:leadPrec
"match_expr " >> optMetaFalse >> termParser >> " with" >> doMatchExprAlts
def doCatch := leading_parser
ppDedent ppLine >> atomic ("catch " >> binderIdent) >> optional (" : " >> termParser) >> darrow >> doSeq
def doCatchMatch := leading_parser
ppDedent ppLine >> "catch " >> doMatchAlts
def doFinally := leading_parser
ppDedent ppLine >> "finally " >> doSeq
@[builtin_doElem_parser] def doTry := leading_parser
"try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
/-- `break` exits the surrounding `for` loop. -/
@[builtin_doElem_parser] def doBreak := leading_parser "break"
/-- `continue` skips to the next iteration of the surrounding `for` loop. -/
@[builtin_doElem_parser] def doContinue := leading_parser "continue"
/--
`return e` inside of a `do` block makes the surrounding block evaluate to `pure e`,
skipping any further statements.
Note that uses of the `do` keyword in other syntax like in `for _ in _ do`
do not constitute a surrounding block in this sense;
in supported editors, the corresponding `do` keyword of the surrounding block
is highlighted when hovering over `return`.
`return` not followed by a term starting on the same line is equivalent to `return ()`.
-/
@[builtin_doElem_parser] def doReturn := leading_parser:leadPrec
withPosition ("return" >> optional (ppSpace >> checkLineEq >> termParser))
/--
`dbg_trace e` prints `e` (which can be an interpolated string literal) to stderr.
It should only be used for debugging.
-/
@[builtin_doElem_parser] def doDbgTrace := leading_parser:leadPrec
"dbg_trace " >> ((interpolatedStr termParser) <|> termParser)
/--
`assert! cond` panics if `cond` evaluates to `false`.
-/
@[builtin_doElem_parser] def doAssert := leading_parser:leadPrec
"assert! " >> termParser
/-
We use `notFollowedBy` to avoid counterintuitive behavior.
For example, the `if`-term parser doesn't enforce indentation restrictions,
but we don't want it to be used when `doIf` fails.
Note that parser priorities would not solve this problem
since the `doIf` parser is failing while the `if` parser is succeeding.
The first `notFollowedBy` prevents this problem.
Consider the `doElem` `x := (a, b⟩`.
It contains an error since we are using `⟩` instead of `)`.
Thus, `doReassign` parser fails.
However, `doExpr` would succeed consuming just `x`,
and cryptic error message is generated after that.
The second `notFollowedBy` prevents this problem.
-/
@[builtin_doElem_parser] def doExpr := leading_parser
notFollowedByRedefinedTermToken >> termParser >>
notFollowedBy (symbol ":=" <|> symbol "←" <|> symbol "<-")
"unexpected token after 'expr' in 'do' block"
@[builtin_doElem_parser] def doNested := leading_parser
"do " >> doSeq
@[builtin_term_parser] def «do» := leading_parser:argPrec
ppAllowUngrouped >> "do " >> doSeq
/-
macros for using `unless`, `for`, `try`, `return` as terms.
They expand into `do unless ...`, `do for ...`, `do try ...`, and `do return ...`
-/
/-- `unless e do s` is a nicer way to write `if !e do s`. -/
@[builtin_term_parser] def termUnless := leading_parser
"unless " >> withForbidden "do" termParser >> " do " >> doSeq
@[builtin_term_parser] def termFor := leading_parser
"for " >> sepBy1 doForDecl ", " >> " do " >> doSeq
@[builtin_term_parser] def termTry := leading_parser
"try " >> doSeq >> many (doCatch <|> doCatchMatch) >> optional doFinally
/--
`return` used outside of `do` blocks creates an implicit block around it
and thus is equivalent to `pure e`, but helps with avoiding parentheses.
-/
@[builtin_term_parser] def termReturn := leading_parser:leadPrec
withPosition ("return" >> optional (ppSpace >> checkLineEq >> termParser))
end Term
end Parser
end Lean