Skip to content

Commit 8168fd6

Browse files
jrr6jrr6
committed
feat: allow conversion of binders to instance-implicit
1 parent fe80bb5 commit 8168fd6

File tree

4 files changed

+217
-84
lines changed

4 files changed

+217
-84
lines changed

‎src/Lean/Elab/BuiltinCommand.lean

+25-9
Original file line numberDiff line numberDiff line change
@@ -151,17 +151,24 @@ private partial def elabChoiceAux (cmds : Array Syntax) (i : Nat) : CommandElabM
151151
open Lean.Parser.Term
152152

153153
private def typelessBinder? : Syntax → Option (Array (TSyntax [`ident, `Lean.Parser.Term.hole]) × BinderInfo)
154-
| `(bracketedBinderF|($ids*)) => some (ids, .default)
155-
| `(bracketedBinderF|{$ids*}) => some (ids, .implicit)
156-
| `(bracketedBinderF|⦃$ids*⦄) => some (ids, .strictImplicit)
157-
| _ => none
154+
| `(bracketedBinderF|($ids*)) => some (ids, .default)
155+
| `(bracketedBinderF|{$ids*}) => some (ids, .implicit)
156+
| `(bracketedBinderF|⦃$ids*⦄) => some (ids, .strictImplicit)
157+
| `(bracketedBinderF|[$id:ident]) => some (#[id], .instImplicit)
158+
| _ => none
158159

159160
/-- If `id` is an identifier, return true if `ids` contains `id`. -/
160161
private def containsId (ids : Array (TSyntax [`ident, ``Parser.Term.hole])) (id : TSyntax [`ident, ``Parser.Term.hole]) : Bool :=
161162
id.raw.isIdent && ids.any fun id' => id'.raw.getId == id.raw.getId
162163

164+
/-- Elaborates `binders` using `withSynthesize` and `withAutoBoundImplicit`. -/
165+
private def elabBindersSynthesizingAutoBound (binders : TSyntaxArray ``bracketedBinder) :=
166+
runTermElabM fun _ => Term.withSynthesize <| Term.withAutoBoundImplicit <|
167+
Term.elabBinders binders fun _ => pure ()
168+
163169
/--
164-
Auxiliary method for processing binder annotation update commands: `variable (α)` and `variable {α}`.
170+
Auxiliary method for processing binder annotation update commands:
171+
`variable (α)`, `variable {α}`, `variable ⦃α⦄`, and `variable [α]`.
165172
The argument `binder` is the binder of the `variable` command.
166173
The method returns an array containing the "residue", that is, variables that do not correspond to updates.
167174
Recall that a `bracketedBinder` can be of the form `(x y)`.
@@ -211,12 +218,22 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
211218
| .implicit => `(bracketedBinderF| {$id $[: $ty?]?})
212219
| .strictImplicit => `(bracketedBinderF| {{$id $[: $ty?]?}})
213220
| .instImplicit => do
214-
let some ty := ty? | throwErrorAt id "instance-implicit binders must provide an explicit type"
221+
let some ty := ty?
222+
| throwErrorAt binder "cannot update binder annotation of variable `{id}` to instance-implicit:\n\
223+
variable was originally declared without an explicit type"
215224
`(bracketedBinderF| [$(⟨id⟩) : $ty])
216225
for id in ids.reverse do
217226
if let some idx := binderIds.findFinIdx? fun binderId => binderId.raw.isIdent && binderId.raw.getId == id.raw.getId then
218227
binderIds := binderIds.eraseIdx idx
219228
modifiedVarDecls := true
229+
let newBinder ← mkBinder id binderInfo
230+
if binderInfo.isInstImplicit then
231+
-- We elaborate the new binder to make sure it's valid as instance-implicit
232+
try
233+
elabBindersSynthesizingAutoBound #[newBinder]
234+
catch e =>
235+
throwErrorAt binder m!"cannot update binder annotation of variable `{id}` to instance-implicit:\n\
236+
{e.toMessageData}"
220237
varDeclsNew := varDeclsNew.push (← mkBinder id binderInfo)
221238
else
222239
varDeclsNew := varDeclsNew.push (← mkBinder id binderInfo')
@@ -228,16 +245,15 @@ private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBin
228245
| .default => `(bracketedBinderF| ($binderId))
229246
| .implicit => `(bracketedBinderF| {$binderId})
230247
| .strictImplicit => `(bracketedBinderF| {{$binderId}})
231-
| .instImplicit => throwErrorAt binderId "instance-implicit binders must provide an explicit type"
248+
| .instImplicit => throwUnsupportedSyntax
232249
else
233250
return #[binder]
234251

235252
@[builtin_command_elab «variable»] def elabVariable : CommandElab
236253
| `(variable $binders*) => do
237254
let binders ← binders.flatMapM replaceBinderAnnotation
238255
-- Try to elaborate `binders` for sanity checking
239-
runTermElabM fun _ => Term.withSynthesize <| Term.withAutoBoundImplicit <|
240-
Term.elabBinders binders fun _ => pure ()
256+
elabBindersSynthesizingAutoBound binders
241257
-- Remark: if we want to produce error messages when variables shadow existing ones, here is the place to do it.
242258
for binder in binders do
243259
let varUIds ← (← getBracketedBinderIds binder) |>.mapM (withFreshMacroScope ∘ MonadQuotation.addMacroScope)

‎tests/lean/run/varBinderUpdate.lean

+192
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,192 @@
1+
/-!
2+
# Changing variable binder annotations
3+
4+
Tests the use of the `variable` command to update the binder annotations of existing variables. -/
5+
6+
/-! Test updating between default and implicit annotations. -/
7+
8+
namespace Ex1
9+
10+
variable {α : Type}
11+
variable [Add α]
12+
variable (α)
13+
def f (a : α) := a + a
14+
/--
15+
info: f Nat 5 : Nat
16+
-/
17+
#guard_msgs in
18+
#check f Nat 5
19+
variable {α}
20+
def g (b : α) := b
21+
/--
22+
info: g 5 : Nat
23+
-/
24+
#guard_msgs in
25+
#check g 5
26+
/--
27+
info: Ex1.f (α : Type) [Add α] (a : α) : α
28+
-/
29+
#guard_msgs in
30+
#check f
31+
/--
32+
info: Ex1.g {α : Type} (b : α) : α
33+
-/
34+
#guard_msgs in
35+
#check g
36+
end Ex1
37+
38+
namespace Ex2
39+
40+
variable {α β : Type}
41+
variable (α)
42+
def f (a : α) := a
43+
def g (b : β) := b
44+
/--
45+
info: f Nat 5 : Nat
46+
-/
47+
#guard_msgs in
48+
#check f Nat 5
49+
/--
50+
info: g 5 : Nat
51+
-/
52+
#guard_msgs in
53+
#check g 5
54+
/--
55+
info: Ex2.f (α : Type) (a : α) : α
56+
-/
57+
#guard_msgs in
58+
#check f
59+
/--
60+
info: Ex2.g {β : Type} (b : β) : β
61+
-/
62+
#guard_msgs in
63+
#check g
64+
/--
65+
error: redundant binder annotation update
66+
-/
67+
#guard_msgs in
68+
variable (α)
69+
end Ex2
70+
71+
namespace Ex3
72+
73+
variable {α : Type}
74+
variable (f : α → α)
75+
variable (α)
76+
def g (a : α) := f a
77+
/--
78+
info: Ex3.g (α : Type) (f : α → α) (a : α) : α
79+
-/
80+
#guard_msgs in
81+
#check g
82+
variable {f}
83+
def h (a : α) := f a
84+
/--
85+
info: Ex3.h (α : Type) {f : α → α} (a : α) : α
86+
-/
87+
#guard_msgs in
88+
#check h
89+
end Ex3
90+
91+
namespace Ex4
92+
93+
variable {α β : Type}
94+
variable (α γ)
95+
def g (a : α) (b : β) (c : γ) := (a, b, c)
96+
/--
97+
info: g Nat Bool 10 "hello" true : Nat × String × Bool
98+
-/
99+
#guard_msgs in
100+
#check g Nat Bool 10 "hello" true
101+
end Ex4
102+
103+
/-! Test updating from and to instance-implicit. -/
104+
105+
namespace Ex5
106+
107+
variable [i : Add α]
108+
variable (i)
109+
def f (x y : α) := x + y
110+
/--
111+
info: Ex5.f.{u_1} {α : Type u_1} (i : Add α) (x y : α) : α
112+
-/
113+
#guard_msgs in
114+
#check f
115+
variable [i]
116+
def g (x y : α) := x + y
117+
/--
118+
info: Ex5.g.{u_1} {α : Type u_1} [i : Add α] (x y : α) : α
119+
-/
120+
#guard_msgs in
121+
#check g
122+
end Ex5
123+
124+
/-! Test that variables with default values/tactics cannot be updated. -/
125+
126+
namespace Ex6
127+
128+
variable (a : Nat)
129+
variable (h : a = a := rfl)
130+
/--
131+
error: cannot update binder annotation of variables with default values/tactics
132+
-/
133+
#guard_msgs in
134+
variable {h}
135+
end Ex6
136+
137+
/-! Test that variables that cannot be instance-implicit fail to be updated thereto. -/
138+
139+
namespace Ex7
140+
141+
variable (n : Nat)
142+
/--
143+
error: cannot update binder annotation of variable `n` to instance-implicit:
144+
invalid binder annotation, type is not a class instance
145+
Nat
146+
use the command `set_option checkBinderAnnotations false` to disable the check
147+
-/
148+
#guard_msgs in
149+
variable [n]
150+
variable (x)
151+
/--
152+
error: cannot update binder annotation of variable `x` to instance-implicit:
153+
variable was originally declared without an explicit type
154+
-/
155+
#guard_msgs in
156+
variable [x]
157+
end Ex7
158+
159+
/-! Test updating to and from strict-implicit annotations. -/
160+
161+
namespace Ex8
162+
163+
variable {α : Type} (β : Type)
164+
variable ⦃α⦄
165+
def f (a : α) (_ : β) := a
166+
/--
167+
info: Ex8.f ⦃α : Type⦄ (β : Type) (a : α) : β → α
168+
-/
169+
#guard_msgs in
170+
#check f
171+
variable (α)
172+
variable ⦃β⦄
173+
def g (a : α) (b : β) := (a, b)
174+
/--
175+
info: Ex8.g (α : Type) ⦃β : Type⦄ (a : α) (b : β) : α × β
176+
-/
177+
#guard_msgs in
178+
#check g
179+
variable {β}
180+
def h (b : β) := b
181+
/--
182+
info: Ex8.h {β : Type} (b : β) : β
183+
-/
184+
#guard_msgs in
185+
#check h
186+
variable {{β}}
187+
/--
188+
error: redundant binder annotation update
189+
-/
190+
#guard_msgs in
191+
variable ⦃β⦄
192+
end Ex8

‎tests/lean/varBinderUpdate.lean

-61
This file was deleted.

‎tests/lean/varBinderUpdate.lean.expected.out

-14
This file was deleted.

0 commit comments

Comments
 (0)