/
BuiltinTerm.lean
253 lines (219 loc) · 10.8 KB
/
BuiltinTerm.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
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Elab.Term
namespace Lean.Elab.Term
open Meta
/-- The universe of propositions. `Prop ≡ Sort 0`. -/
@[builtinTermElab «prop»] def elabProp : TermElab := fun _ _ =>
return mkSort levelZero
private def elabOptLevel (stx : Syntax) : TermElabM Level :=
if stx.isNone then
pure levelZero
else
elabLevel stx[0]
/-- A specific universe in Lean's infinite hierarchy of universes. -/
@[builtinTermElab «sort»] def elabSort : TermElab := fun stx _ =>
return mkSort (← elabOptLevel stx[1])
/-- A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`. -/
@[builtinTermElab «type»] def elabTypeStx : TermElab := fun stx _ =>
return mkSort (mkLevelSucc (← elabOptLevel stx[1]))
/-
the method `resolveName` adds a completion point for it using the given
expected type. Thus, we propagate the expected type if `stx[0]` is an identifier.
It doesn't "hurt" if the identifier can be resolved because the expected type is not used in this case.
Recall that if the name resolution fails a synthetic sorry is returned.-/
@[builtinTermElab «pipeCompletion»] def elabPipeCompletion : TermElab := fun stx expectedType? => do
let e ← elabTerm stx[0] none
unless e.isSorry do
addDotCompletionInfo stx e expectedType?
throwErrorAt stx[1] "invalid field notation, identifier or numeral expected"
@[builtinTermElab «completion»] def elabCompletion : TermElab := fun stx expectedType? => do
/- `ident.` is ambiguous in Lean, we may try to be completing a declaration name or access a "field". -/
if stx[0].isIdent then
/- If we can elaborate the identifier successfully, we assume it is a dot-completion. Otherwise, we treat it as
identifier completion with a dangling `.`.
Recall that the server falls back to identifier completion when dot-completion fails. -/
let s ← saveState
try
let e ← elabTerm stx[0] none
addDotCompletionInfo stx e expectedType?
catch _ =>
s.restore
addCompletionInfo <| CompletionInfo.id stx stx[0].getId (danglingDot := true) (← getLCtx) expectedType?
throwErrorAt stx[1] "invalid field notation, identifier or numeral expected"
else
elabPipeCompletion stx expectedType?
/-- A placeholder term, to be synthesized by unification. -/
@[builtinTermElab «hole»] def elabHole : TermElab := fun stx expectedType? => do
let mvar ← mkFreshExprMVar expectedType?
registerMVarErrorHoleInfo mvar.mvarId! stx
pure mvar
@[builtinTermElab «syntheticHole»] def elabSyntheticHole : TermElab := fun stx expectedType? => do
let arg := stx[1]
let userName := if arg.isIdent then arg.getId else Name.anonymous
let mkNewHole : Unit → TermElabM Expr := fun _ => do
let mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque userName
registerMVarErrorHoleInfo mvar.mvarId! stx
pure mvar
if userName.isAnonymous then
mkNewHole ()
else
let mctx ← getMCtx
match mctx.findUserName? userName with
| none => mkNewHole ()
| some mvarId =>
let mvar := mkMVar mvarId
let mvarDecl ← getMVarDecl mvarId
let lctx ← getLCtx
if mvarDecl.lctx.isSubPrefixOf lctx then
pure mvar
else match mctx.getExprAssignment? mvarId with
| some val =>
let val ← instantiateMVars val
if mctx.isWellFormed lctx val then
pure val
else
withLCtx mvarDecl.lctx mvarDecl.localInstances do
throwError "synthetic hole has already been defined and assigned to value incompatible with the current context{indentExpr val}"
| none =>
if mctx.isDelayedAssigned mvarId then
-- We can try to improve this case if needed.
throwError "synthetic hole has already beend defined and delayed assigned with an incompatible local context"
else if lctx.isSubPrefixOf mvarDecl.lctx then
let mvarNew ← mkNewHole ()
modifyMCtx fun mctx => mctx.assignExpr mvarId mvarNew
pure mvarNew
else
throwError "synthetic hole has already been defined with an incompatible local context"
@[builtinTermElab «letMVar»] def elabLetMVar : TermElab := fun stx expectedType? => do
match stx with
| `(let_mvar% ? $n := $e; $b) =>
match (← getMCtx).findUserName? n.getId with
| some _ => throwError "invalid 'let_mvar%', metavariable '?{n.getId}' has already been used"
| none =>
let e ← elabTerm e none
let mvar ← mkFreshExprMVar (← inferType e) MetavarKind.syntheticOpaque n.getId
assignExprMVar mvar.mvarId! e
-- We use `mkSaveInfoAnnotation` to make sure the info trees for `e` are saved even if `b` is a metavariable.
return mkSaveInfoAnnotation (← elabTerm b expectedType?)
| _ => throwUnsupportedSyntax
private def getMVarFromUserName (ident : Syntax) : MetaM Expr := do
match (← getMCtx).findUserName? ident.getId with
| none => throwError "unknown metavariable '?{ident.getId}'"
| some mvarId => instantiateMVars (mkMVar mvarId)
@[builtinTermElab «waitIfTypeMVar»] def elabWaitIfTypeMVar : TermElab := fun stx expectedType? => do
match stx with
| `(wait_if_type_mvar% ? $n; $b) =>
tryPostponeIfMVar (← inferType (← getMVarFromUserName n))
elabTerm b expectedType?
| _ => throwUnsupportedSyntax
@[builtinTermElab «waitIfTypeContainsMVar»] def elabWaitIfTypeContainsMVar : TermElab := fun stx expectedType? => do
match stx with
| `(wait_if_type_contains_mvar% ? $n; $b) =>
if (← instantiateMVars (← inferType (← getMVarFromUserName n))).hasExprMVar then
tryPostpone
elabTerm b expectedType?
| _ => throwUnsupportedSyntax
@[builtinTermElab «waitIfContainsMVar»] def elabWaitIfContainsMVar : TermElab := fun stx expectedType? => do
match stx with
| `(wait_if_contains_mvar% ? $n; $b) =>
if (← getMVarFromUserName n).hasExprMVar then
tryPostpone
elabTerm b expectedType?
| _ => throwUnsupportedSyntax
private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr := do
let mvar ← mkFreshExprMVar type MetavarKind.syntheticOpaque
let mvarId := mvar.mvarId!
let ref ← getRef
let declName? ← getDeclName?
registerSyntheticMVar ref mvarId <| SyntheticMVarKind.tactic tacticCode (← saveContext)
return mvar
/-- `by tac` constructs a term of the expected type by running the tactic(s) `tac`. -/
@[builtinTermElab byTactic] def elabByTactic : TermElab := fun stx expectedType? =>
match expectedType? with
| some expectedType => mkTacticMVar expectedType stx
| none => throwError ("invalid 'by' tactic, expected type has not been provided")
@[builtinTermElab noImplicitLambda] def elabNoImplicitLambda : TermElab := fun stx expectedType? =>
elabTerm stx[1] (mkNoImplicitLambdaAnnotation <$> expectedType?)
@[builtinTermElab cdot] def elabBadCDot : TermElab := fun stx _ =>
throwError "invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)"
@[builtinTermElab strLit] def elabStrLit : TermElab := fun stx _ => do
match stx.isStrLit? with
| some val => pure $ mkStrLit val
| none => throwIllFormedSyntax
private def mkFreshTypeMVarFor (expectedType? : Option Expr) : TermElabM Expr := do
let typeMVar ← mkFreshTypeMVar MetavarKind.synthetic
match expectedType? with
| some expectedType => discard <| isDefEq expectedType typeMVar
| _ => pure ()
return typeMVar
@[builtinTermElab numLit] def elabNumLit : TermElab := fun stx expectedType? => do
let val ← match stx.isNatLit? with
| some val => pure val
| none => throwIllFormedSyntax
let typeMVar ← mkFreshTypeMVarFor expectedType?
let u ← getDecLevel typeMVar
let mvar ← mkInstMVar (mkApp2 (Lean.mkConst ``OfNat [u]) typeMVar (mkRawNatLit val))
let r := mkApp3 (Lean.mkConst ``OfNat.ofNat [u]) typeMVar (mkRawNatLit val) mvar
registerMVarErrorImplicitArgInfo mvar.mvarId! stx r
return r
@[builtinTermElab rawNatLit] def elabRawNatLit : TermElab := fun stx expectedType? => do
match stx[1].isNatLit? with
| some val => return mkRawNatLit val
| none => throwIllFormedSyntax
@[builtinTermElab scientificLit]
def elabScientificLit : TermElab := fun stx expectedType? => do
match stx.isScientificLit? with
| none => throwIllFormedSyntax
| some (m, sign, e) =>
let typeMVar ← mkFreshTypeMVarFor expectedType?
let u ← getDecLevel typeMVar
let mvar ← mkInstMVar (mkApp (Lean.mkConst ``OfScientific [u]) typeMVar)
let r := mkApp5 (Lean.mkConst ``OfScientific.ofScientific [u]) typeMVar mvar (mkRawNatLit m) (toExpr sign) (mkRawNatLit e)
registerMVarErrorImplicitArgInfo mvar.mvarId! stx r
return r
@[builtinTermElab charLit] def elabCharLit : TermElab := fun stx _ => do
match stx.isCharLit? with
| some val => return mkApp (Lean.mkConst ``Char.ofNat) (mkRawNatLit val.toNat)
| none => throwIllFormedSyntax
/- A literal of type `Name`. -/
@[builtinTermElab quotedName] def elabQuotedName : TermElab := fun stx _ =>
match stx[0].isNameLit? with
| some val => pure $ toExpr val
| none => throwIllFormedSyntax
/--
A resolved name literal. Evaluates to the full name of the given constant if
existent in the current context, or else fails. -/
@[builtinTermElab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ =>
return toExpr (← resolveGlobalConstNoOverloadWithInfo stx[2])
@[builtinTermElab typeOf] def elabTypeOf : TermElab := fun stx _ => do
inferType (← elabTerm stx[1] none)
@[builtinTermElab ensureTypeOf] def elabEnsureTypeOf : TermElab := fun stx expectedType? =>
match stx[2].isStrLit? with
| none => throwIllFormedSyntax
| some msg => do
let refTerm ← elabTerm stx[1] none
let refTermType ← inferType refTerm
elabTermEnsuringType stx[3] refTermType (errorMsgHeader? := msg)
@[builtinTermElab ensureExpectedType] def elabEnsureExpectedType : TermElab := fun stx expectedType? =>
match stx[1].isStrLit? with
| none => throwIllFormedSyntax
| some msg => elabTermEnsuringType stx[2] expectedType? (errorMsgHeader? := msg)
/-- `open ... in e` makes the given namespaces available in the term `e`. -/
@[builtinTermElab «open»] def elabOpen : TermElab := fun stx expectedType? => do
try
pushScope
let openDecls ← elabOpenDecl stx[1]
withTheReader Core.Context (fun ctx => { ctx with openDecls := openDecls }) do
elabTerm stx[3] expectedType?
finally
popScope
/-- `set_option opt val in e` sets the option `opt` to the value `val` in the term `e`. -/
@[builtinTermElab «set_option»] def elabSetOption : TermElab := fun stx expectedType? => do
let options ← Elab.elabSetOption stx[1] stx[2]
withTheReader Core.Context (fun ctx => { ctx with maxRecDepth := maxRecDepth.get options, options := options }) do
elabTerm stx[4] expectedType?
end Lean.Elab.Term