-
Notifications
You must be signed in to change notification settings - Fork 350
/
Notation.lean
338 lines (273 loc) · 14 KB
/
Notation.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
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
/-
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
Notation for operators defined at Prelude.lean
-/
prelude
import Init.Prelude
-- DSL for specifying parser precedences and priorities
namespace Lean.Parser.Syntax
syntax:65 (name := addPrec) prec " + " prec:66 : prec
syntax:65 (name := subPrec) prec " - " prec:66 : prec
syntax:65 (name := addPrio) prio " + " prio:66 : prio
syntax:65 (name := subPrio) prio " - " prio:66 : prio
end Lean.Parser.Syntax
macro "max" : prec => `(1024) -- maximum precedence used in term parsers, in particular for terms in function position (`ident`, `paren`, ...)
macro "arg" : prec => `(1023) -- precedence used for application arguments (`do`, `by`, ...)
macro "lead" : prec => `(1022) -- precedence used for terms not supposed to be used as arguments (`let`, `have`, ...)
macro "(" p:prec ")" : prec => p
macro "min" : prec => `(10) -- minimum precedence used in term parsers
macro "min1" : prec => `(11) -- `(min+1) we can only `min+1` after `Meta.lean`
/-
`max:prec` as a term. It is equivalent to `eval_prec max` for `eval_prec` defined at `Meta.lean`.
We use `max_prec` to workaround bootstrapping issues. -/
macro "max_prec" : term => `(1024)
macro "default" : prio => `(1000)
macro "low" : prio => `(100)
macro "mid" : prio => `(1000)
macro "high" : prio => `(10000)
macro "(" p:prio ")" : prio => p
-- Basic notation for defining parsers
syntax stx "+" : stx
syntax stx "*" : stx
syntax stx "?" : stx
syntax:2 stx " <|> " stx:1 : stx
macro_rules
| `(stx| $p +) => `(stx| many1($p))
| `(stx| $p *) => `(stx| many($p))
| `(stx| $p ?) => `(stx| optional($p))
| `(stx| $p₁ <|> $p₂) => `(stx| orelse($p₁, $p₂))
/- Comma-separated sequence. -/
macro:max x:stx ",*" : stx => `(stx| sepBy($x, ",", ", "))
macro:max x:stx ",+" : stx => `(stx| sepBy1($x, ",", ", "))
/- Comma-separated sequence with optional trailing comma. -/
macro:max x:stx ",*,?" : stx => `(stx| sepBy($x, ",", ", ", allowTrailingSep))
macro:max x:stx ",+,?" : stx => `(stx| sepBy1($x, ",", ", ", allowTrailingSep))
macro "!" x:stx : stx => `(stx| notFollowedBy($x))
syntax (name := rawNatLit) "nat_lit " num : term
infixr:90 " ∘ " => Function.comp
infixr:35 " × " => Prod
infixl:55 " ||| " => HOr.hOr
infixl:58 " ^^^ " => HXor.hXor
infixl:60 " &&& " => HAnd.hAnd
infixl:65 " + " => HAdd.hAdd
infixl:65 " - " => HSub.hSub
infixl:70 " * " => HMul.hMul
infixl:70 " / " => HDiv.hDiv
infixl:70 " % " => HMod.hMod
infixl:75 " <<< " => HShiftLeft.hShiftLeft
infixl:75 " >>> " => HShiftRight.hShiftRight
infixr:80 " ^ " => HPow.hPow
prefix:100 "-" => Neg.neg
prefix:100 "~~~" => Complement.complement
/-
Remark: the infix commands above ensure a delaborator is generated for each relations.
We redefine the macros below to be able to use the auxiliary `binop%` elaboration helper for binary operators.
It addresses issue #382. -/
macro_rules | `($x ||| $y) => `(binop% HOr.hOr $x $y)
macro_rules | `($x ^^^ $y) => `(binop% HXor.hXor $x $y)
macro_rules | `($x &&& $y) => `(binop% HAnd.hAnd $x $y)
macro_rules | `($x + $y) => `(binop% HAdd.hAdd $x $y)
macro_rules | `($x - $y) => `(binop% HSub.hSub $x $y)
macro_rules | `($x * $y) => `(binop% HMul.hMul $x $y)
macro_rules | `($x / $y) => `(binop% HDiv.hDiv $x $y)
macro_rules | `($x % $y) => `(binop% HMod.hMod $x $y)
macro_rules | `($x <<< $y) => `(binop% HShiftLeft.hShiftLeft $x $y)
macro_rules | `($x >>> $y) => `(binop% HShiftRight.hShiftRight $x $y)
macro_rules | `($x ^ $y) => `(binop% HPow.hPow $x $y)
-- declare ASCII alternatives first so that the latter Unicode unexpander wins
infix:50 " <= " => LE.le
infix:50 " ≤ " => LE.le
infix:50 " < " => LT.lt
infix:50 " >= " => GE.ge
infix:50 " ≥ " => GE.ge
infix:50 " > " => GT.gt
infix:50 " = " => Eq
infix:50 " == " => BEq.beq
infix:50 " ~= " => HEq
infix:50 " ≅ " => HEq
/-
Remark: the infix commands above ensure a delaborator is generated for each relations.
We redefine the macros below to be able to use the auxiliary `binrel%` elaboration helper for binary relations.
It has better support for applying coercions. For example, suppose we have `binrel% Eq n i` where `n : Nat` and
`i : Int`. The default elaborator fails because we don't have a coercion from `Int` to `Nat`, but
`binrel%` succeeds because it also tries a coercion from `Nat` to `Int` even when the nat occurs before the int. -/
macro_rules | `($x <= $y) => `(binrel% LE.le $x $y)
macro_rules | `($x ≤ $y) => `(binrel% LE.le $x $y)
macro_rules | `($x < $y) => `(binrel% LT.lt $x $y)
macro_rules | `($x > $y) => `(binrel% GT.gt $x $y)
macro_rules | `($x >= $y) => `(binrel% GE.ge $x $y)
macro_rules | `($x ≥ $y) => `(binrel% GE.ge $x $y)
macro_rules | `($x = $y) => `(binrel% Eq $x $y)
macro_rules | `($x == $y) => `(binrel% BEq.beq $x $y)
infixr:35 " /\\ " => And
infixr:35 " ∧ " => And
infixr:30 " \\/ " => Or
infixr:30 " ∨ " => Or
notation:max "¬" p:40 => Not p
infixl:35 " && " => and
infixl:30 " || " => or
notation:max "!" b:40 => not b
infixl:65 " ++ " => HAppend.hAppend
infixr:67 " :: " => List.cons
infixr:20 " <|> " => HOrElse.hOrElse
infixr:60 " >> " => HAndThen.hAndThen
infixl:55 " >>= " => Bind.bind
infixl:60 " <*> " => Seq.seq
infixl:60 " <* " => SeqLeft.seqLeft
infixr:60 " *> " => SeqRight.seqRight
infixr:100 " <$> " => Functor.map
syntax (name := termDepIfThenElse) ppGroup(ppDedent("if " ident " : " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
macro_rules
| `(if $h:ident : $c then $t:term else $e:term) => ``(dite $c (fun $h:ident => $t) (fun $h:ident => $e))
syntax (name := termIfThenElse) ppGroup(ppDedent("if " term " then" ppSpace term ppDedent(ppSpace "else") ppSpace term)) : term
macro_rules
| `(if $c then $t:term else $e:term) => ``(ite $c $t $e)
macro "if " "let " pat:term " := " d:term " then " t:term " else " e:term : term =>
`(match $d:term with | $pat:term => $t | _ => $e)
syntax:min term "<|" term:min : term
macro_rules
| `($f $args* <| $a) => let args := args.push a; `($f $args*)
| `($f <| $a) => `($f $a)
syntax:min term "|>" term:min1 : term
macro_rules
| `($a |> $f $args*) => let args := args.push a; `($f $args*)
| `($a |> $f) => `($f $a)
-- Haskell-like pipe <|
-- Note that we have a whitespace after `$` to avoid an ambiguity with the antiquotations.
syntax:min term atomic("$" ws) term:min : term
macro_rules
| `($f $args* $ $a) => let args := args.push a; `($f $args*)
| `($f $ $a) => `($f $a)
syntax "{ " ident (" : " term)? " // " term " }" : term
macro_rules
| `({ $x : $type // $p }) => ``(Subtype (fun ($x:ident : $type) => $p))
| `({ $x // $p }) => ``(Subtype (fun ($x:ident : _) => $p))
/-
`without_expected_type t` instructs Lean to elaborate `t` without an expected type.
Recall that terms such as `match ... with ...` and `⟨...⟩` will postpone elaboration until
expected type is known. So, `without_expected_type` is not effective in this case. -/
macro "without_expected_type " x:term : term => `(let aux := $x; aux)
syntax "[" term,* "]" : term
syntax "%[" term,* "|" term "]" : term -- auxiliary notation for creating big list literals
namespace Lean
macro_rules
| `([ $elems,* ]) => do
let rec expandListLit (i : Nat) (skip : Bool) (result : Syntax) : MacroM Syntax := do
match i, skip with
| 0, _ => pure result
| i+1, true => expandListLit i false result
| i+1, false => expandListLit i true (← ``(List.cons $(elems.elemsAndSeps[i]) $result))
if elems.elemsAndSeps.size < 64 then
expandListLit elems.elemsAndSeps.size false (← ``(List.nil))
else
`(%[ $elems,* | List.nil ])
namespace Parser.Tactic
syntax (name := intro) "intro " notFollowedBy("|") (colGt term:max)* : tactic
syntax (name := intros) "intros " (colGt (ident <|> "_"))* : tactic
syntax (name := rename) "rename " term " => " ident : tactic
syntax (name := revert) "revert " (colGt ident)+ : tactic
syntax (name := clear) "clear " (colGt ident)+ : tactic
syntax (name := subst) "subst " (colGt ident)+ : tactic
syntax (name := assumption) "assumption" : tactic
syntax (name := contradiction) "contradiction" : tactic
syntax (name := apply) "apply " term : tactic
syntax (name := exact) "exact " term : tactic
syntax (name := refine) "refine " term : tactic
syntax (name := refine') "refine' " term : tactic
syntax (name := constructor) "constructor" : tactic
syntax (name := case) "case " ident (ident <|> "_")* " => " tacticSeq : tactic
syntax (name := allGoals) "allGoals " tacticSeq : tactic
syntax (name := focus) "focus " tacticSeq : tactic
syntax (name := skip) "skip" : tactic
syntax (name := done) "done" : tactic
syntax (name := traceState) "traceState" : tactic
syntax (name := failIfSuccess) "failIfSuccess " tacticSeq : tactic
syntax (name := generalize) "generalize " atomic(ident " : ")? term:51 " = " ident : tactic
syntax (name := paren) "(" tacticSeq ")" : tactic
syntax (name := withReducible) "withReducible " tacticSeq : tactic
syntax (name := withReducibleAndInstances) "withReducibleAndInstances " tacticSeq : tactic
syntax (name := first) "first " withPosition((group(colGe "|" tacticSeq))+) : tactic
syntax (name := rotateLeft) "rotateLeft" (num)? : tactic
syntax (name := rotateRight) "rotateRight" (num)? : tactic
macro "try " t:tacticSeq : tactic => `(first | $t | skip)
macro:1 x:tactic " <;> " y:tactic:0 : tactic => `(tactic| focus ($x:tactic; allGoals $y:tactic))
syntax ("·" <|> ".") tacticSeq : tactic
macro_rules
| `(tactic| ·%$dot $ts:tacticSeq) => `(tactic| {%$dot ($ts:tacticSeq) })
macro "rfl" : tactic => `(exact rfl)
macro "admit" : tactic => `(exact sorry)
macro "inferInstance" : tactic => `(exact inferInstance)
syntax locationWildcard := "*"
syntax locationHyp := (colGt ident)+ ("⊢" <|> "|-")? -- TODO: delete
syntax locationTargets := (colGt ident)+ ("⊢" <|> "|-")?
syntax location := withPosition("at " locationWildcard <|> locationHyp)
syntax (name := change) "change " term (location)? : tactic
syntax (name := changeWith) "change " term " with " term (location)? : tactic
syntax rwRule := ("←" <|> "<-")? term
syntax rwRuleSeq := "[" rwRule,+,? "]"
syntax (name := rewriteSeq) "rewrite " rwRuleSeq (location)? : tactic
syntax (name := erewriteSeq) "erewrite " rwRuleSeq (location)? : tactic
syntax (name := rwSeq) "rw " rwRuleSeq (location)? : tactic
syntax (name := erwSeq) "erw " rwRuleSeq (location)? : tactic
def rwWithRfl (kind : SyntaxNodeKind) (atom : String) (stx : Syntax) : MacroM Syntax := do
-- We show the `rfl` state on `]`
let seq := stx[1]
let rbrak := seq[2]
-- Replace `]` token with one without position information in the expanded tactic
let seq := seq.setArg 2 (mkAtom "]")
let tac := stx.setKind kind |>.setArg 0 (mkAtomFrom stx atom) |>.setArg 1 seq
`(tactic| $tac; try (withReducible rfl%$rbrak))
@[macro rwSeq] def expandRwSeq : Macro :=
rwWithRfl ``Lean.Parser.Tactic.rewriteSeq "rewrite"
@[macro erwSeq] def expandERwSeq : Macro :=
rwWithRfl ``Lean.Parser.Tactic.erewriteSeq "erewrite"
syntax (name := injection) "injection " term (" with " (colGt (ident <|> "_"))+)? : tactic
syntax simpPre := "↓"
syntax simpPost := "↑"
syntax simpLemma := (simpPre <|> simpPost)? term
syntax simpErase := "-" ident
syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? (location)? : tactic
syntax (name := simpAll) "simp_all " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpErase <|> simpLemma),* "]")? : tactic
-- Auxiliary macro for lifting have/suffices/let/...
-- It makes sure the "continuation" `?_` is the main goal after refining
macro "refineLift " e:term : tactic => `(focus (refine noImplicitLambda% $e; rotateRight))
macro "have " d:haveDecl : tactic => `(refineLift have $d:haveDecl; ?_)
/- We use a priority > default, to avoid ambiguity with previous `have` notation -/
macro (priority := high) "have" x:ident " := " p:term : tactic => `(have $x:ident : _ := $p)
macro "suffices " d:sufficesDecl : tactic => `(refineLift suffices $d:sufficesDecl; ?_)
macro "let " d:letDecl : tactic => `(refineLift let $d:letDecl; ?_)
macro "show " e:term : tactic => `(refineLift show $e:term from ?_)
syntax (name := letrec) withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
macro_rules
| `(tactic| let rec $d:letRecDecls) => `(tactic| refineLift let rec $d:letRecDecls; ?_)
-- Similar to `refineLift`, but using `refine'`
macro "refineLift' " e:term : tactic => `(focus (refine' noImplicitLambda% $e; rotateRight))
macro "have' " d:haveDecl : tactic => `(refineLift' have $d:haveDecl; ?_)
macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x:ident : _ := $p)
macro "let' " d:letDecl : tactic => `(refineLift' let $d:letDecl; ?_)
syntax inductionAlt := "| " (group("@"? ident) <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
syntax (name := induction) "induction " term,+ (" using " ident)? ("generalizing " ident+)? (inductionAlts)? : tactic
syntax casesTarget := atomic(ident " : ")? term
syntax (name := cases) "cases " casesTarget,+ (" using " ident)? (inductionAlts)? : tactic
syntax (name := existsIntro) "exists " term : tactic
syntax "repeat " tacticSeq : tactic
macro_rules
| `(tactic| repeat $seq) => `(tactic| first | ($seq); repeat $seq | skip)
syntax "trivial" : tactic
macro_rules | `(tactic| trivial) => `(tactic| assumption)
macro_rules | `(tactic| trivial) => `(tactic| rfl)
macro_rules | `(tactic| trivial) => `(tactic| contradiction)
macro_rules | `(tactic| trivial) => `(tactic| apply True.intro)
macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial)
macro "unhygienic " t:tacticSeq : tactic => `(set_option tactic.hygienic false in $t:tacticSeq)
end Tactic
namespace Attr
-- simp attribute syntax
syntax (name := simp) "simp" (Tactic.simpPre <|> Tactic.simpPost)? (prio)? : attr
end Attr
end Parser
end Lean
macro "‹" type:term "›" : term => `((by assumption : $type))