-
Notifications
You must be signed in to change notification settings - Fork 349
/
Term.lean
1773 lines (1579 loc) · 75.4 KB
/
Term.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
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
/-
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Lean.ReservedNameAction
import Lean.Meta.AppBuilder
import Lean.Meta.CollectMVars
import Lean.Meta.Coe
import Lean.Linter.Deprecated
import Lean.Elab.Config
import Lean.Elab.Level
import Lean.Elab.DeclModifiers
import Lean.Elab.PreDefinition.WF.TerminationHint
namespace Lean.Elab
namespace Term
/-- Saved context for postponed terms and tactics to be executed. -/
structure SavedContext where
declName? : Option Name
options : Options
openDecls : List OpenDecl
macroStack : MacroStack
errToSorry : Bool
levelNames : List Name
/-- We use synthetic metavariables as placeholders for pending elaboration steps. -/
inductive SyntheticMVarKind where
/-- Use typeclass resolution to synthesize value for metavariable. -/
| typeClass
/-- Use coercion to synthesize value for the metavariable.
if `f?` is `some f`, we produce an application type mismatch error message.
Otherwise, if `header?` is `some header`, we generate the error `(header ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)`
Otherwise, we generate the error `("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)` -/
| coe (header? : Option String) (expectedType : Expr) (e : Expr) (f? : Option Expr)
/-- Use tactic to synthesize value for metavariable. -/
| tactic (tacticCode : Syntax) (ctx : SavedContext)
/-- Metavariable represents a hole whose elaboration has been postponed. -/
| postponed (ctx : SavedContext)
deriving Inhabited
instance : ToString SyntheticMVarKind where
toString
| .typeClass => "typeclass"
| .coe .. => "coe"
| .tactic .. => "tactic"
| .postponed .. => "postponed"
structure SyntheticMVarDecl where
stx : Syntax
kind : SyntheticMVarKind
deriving Inhabited
/--
We can optionally associate an error context with a metavariable (see `MVarErrorInfo`).
We have three different kinds of error context.
-/
inductive MVarErrorKind where
/-- Metavariable for implicit arguments. `ctx` is the parent application. -/
| implicitArg (ctx : Expr)
/-- Metavariable for explicit holes provided by the user (e.g., `_` and `?m`) -/
| hole
/-- "Custom", `msgData` stores the additional error messages. -/
| custom (msgData : MessageData)
deriving Inhabited
instance : ToString MVarErrorKind where
toString
| .implicitArg _ => "implicitArg"
| .hole => "hole"
| .custom _ => "custom"
/--
We can optionally associate an error context with metavariables.
-/
structure MVarErrorInfo where
mvarId : MVarId
ref : Syntax
kind : MVarErrorKind
argName? : Option Name := none
deriving Inhabited
/--
Nested `let rec` expressions are eagerly lifted by the elaborator.
We store the information necessary for performing the lifting here.
-/
structure LetRecToLift where
ref : Syntax
fvarId : FVarId
attrs : Array Attribute
shortDeclName : Name
declName : Name
lctx : LocalContext
localInstances : LocalInstances
type : Expr
val : Expr
mvarId : MVarId
termination : WF.TerminationHints
deriving Inhabited
/--
State of the `TermElabM` monad.
-/
structure State where
levelNames : List Name := []
syntheticMVars : MVarIdMap SyntheticMVarDecl := {}
pendingMVars : List MVarId := {}
mvarErrorInfos : MVarIdMap MVarErrorInfo := {}
letRecsToLift : List LetRecToLift := []
deriving Inhabited
end Term
namespace Tactic
/--
State of the `TacticM` monad.
-/
structure State where
goals : List MVarId
deriving Inhabited
/--
Snapshots are used to implement the `save` tactic.
This tactic caches the state of the system, and allows us to "replay"
expensive proofs efficiently. This is only relevant implementing the
LSP server.
-/
structure Snapshot where
core : Core.State
meta : Meta.State
term : Term.State
tactic : Tactic.State
stx : Syntax
/--
Key for the cache used to implement the `save` tactic.
-/
structure CacheKey where
mvarId : MVarId -- TODO: should include all goals
pos : String.Pos
deriving BEq, Hashable, Inhabited
/--
Cache for the `save` tactic.
-/
structure Cache where
pre : PHashMap CacheKey Snapshot := {}
post : PHashMap CacheKey Snapshot := {}
deriving Inhabited
end Tactic
namespace Term
structure Context where
declName? : Option Name := none
/--
Map `.auxDecl` local declarations used to encode recursive declarations to their full-names.
-/
auxDeclToFullName : FVarIdMap Name := {}
macroStack : MacroStack := []
/--
When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`.
The function `elabTerm` catches this exception and creates fresh synthetic metavariable `?m`, stores `?m` in
the list of pending synthetic metavariables, and returns `?m`. -/
mayPostpone : Bool := true
/--
When `errToSorry` is set to true, the method `elabTerm` catches
exceptions and converts them into synthetic `sorry`s.
The implementation of choice nodes and overloaded symbols rely on the fact
that when `errToSorry` is set to false for an elaboration function `F`, then
`errToSorry` remains `false` for all elaboration functions invoked by `F`.
That is, it is safe to transition `errToSorry` from `true` to `false`, but
we must not set `errToSorry` to `true` when it is currently set to `false`. -/
errToSorry : Bool := true
/--
When `autoBoundImplicit` is set to true, instead of producing
an "unknown identifier" error for unbound variables, we generate an
internal exception. This exception is caught at `elabBinders` and
`elabTypeWithUnboldImplicit`. Both methods add implicit declarations
for the unbound variable and try again. -/
autoBoundImplicit : Bool := false
autoBoundImplicits : PArray Expr := {}
/--
A name `n` is only eligible to be an auto implicit name if `autoBoundImplicitForbidden n = false`.
We use this predicate to disallow `f` to be considered an auto implicit name in a definition such
as
```
def f : f → Bool := fun _ => true
```
-/
autoBoundImplicitForbidden : Name → Bool := fun _ => false
/-- Map from user name to internal unique name -/
sectionVars : NameMap Name := {}
/-- Map from internal name to fvar -/
sectionFVars : NameMap Expr := {}
/-- Enable/disable implicit lambdas feature. -/
implicitLambda : Bool := true
/-- Heed `elab_as_elim` attribute. -/
heedElabAsElim : Bool := true
/-- Noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/
isNoncomputableSection : Bool := false
/-- When `true` we skip TC failures. We use this option when processing patterns. -/
ignoreTCFailures : Bool := false
/-- `true` when elaborating patterns. It affects how we elaborate named holes. -/
inPattern : Bool := false
/-- Cache for the `save` tactic. It is only `some` in the LSP server. -/
tacticCache? : Option (IO.Ref Tactic.Cache) := none
/--
If `true`, we store in the `Expr` the `Syntax` for recursive applications (i.e., applications
of free variables tagged with `isAuxDecl`). We store the `Syntax` using `mkRecAppWithSyntax`.
We use the `Syntax` object to produce better error messages at `Structural.lean` and `WF.lean`. -/
saveRecAppSyntax : Bool := true
/--
If `holesAsSyntheticOpaque` is `true`, then we mark metavariables associated
with `_`s as `syntheticOpaque` if they do not occur in patterns.
This option is useful when elaborating terms in tactics such as `refine'` where
we want holes there to become new goals. See issue #1681, we have
`refine' (fun x => _)
-/
holesAsSyntheticOpaque : Bool := false
abbrev TermElabM := ReaderT Context $ StateRefT State MetaM
abbrev TermElab := Syntax → Option Expr → TermElabM Expr
/-
Make the compiler generate specialized `pure`/`bind` so we do not have to optimize through the
whole monad stack at every use site. May eventually be covered by `deriving`.
-/
@[always_inline]
instance : Monad TermElabM :=
let i := inferInstanceAs (Monad TermElabM)
{ pure := i.pure, bind := i.bind }
open Meta
instance : Inhabited (TermElabM α) where
default := throw default
/--
Backtrackable state for the `TermElabM` monad.
-/
structure SavedState where
meta : Meta.SavedState
«elab» : State
deriving Nonempty
protected def saveState : TermElabM SavedState :=
return { meta := (← Meta.saveState), «elab» := (← get) }
def SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : TermElabM Unit := do
let traceState ← getTraceState -- We never backtrack trace message
let infoState ← getInfoState -- We also do not backtrack the info nodes when `restoreInfo == false`
s.meta.restore
set s.elab
setTraceState traceState
unless restoreInfo do
setInfoState infoState
/--
Restores full state including sources for unique identifiers. Only intended for incremental reuse
between elaboration runs, not for backtracking within a single run.
-/
def SavedState.restoreFull (s : SavedState) : TermElabM Unit := do
s.meta.restoreFull
set s.elab
instance : MonadBacktrack SavedState TermElabM where
saveState := Term.saveState
restoreState b := b.restore
abbrev TermElabResult (α : Type) := EStateM.Result Exception SavedState α
/--
Execute `x`, save resulting expression and new state.
We remove any `Info` created by `x`.
The info nodes are committed when we execute `applyResult`.
We use `observing` to implement overloaded notation and decls.
We want to save `Info` nodes for the chosen alternative.
-/
def observing (x : TermElabM α) : TermElabM (TermElabResult α) := do
let s ← saveState
try
let e ← x
let sNew ← saveState
s.restore (restoreInfo := true)
return EStateM.Result.ok e sNew
catch
| ex@(.error ..) =>
let sNew ← saveState
s.restore (restoreInfo := true)
return .error ex sNew
| ex@(.internal id _) =>
if id == postponeExceptionId then
s.restore (restoreInfo := true)
throw ex
/--
Apply the result/exception and state captured with `observing`.
We use this method to implement overloaded notation and symbols. -/
def applyResult (result : TermElabResult α) : TermElabM α := do
match result with
| .ok a r => r.restore (restoreInfo := true); return a
| .error ex r => r.restore (restoreInfo := true); throw ex
/--
Execute `x`, but keep state modifications only if `x` did not postpone.
This method is useful to implement elaboration functions that cannot decide whether
they need to postpone or not without updating the state. -/
def commitIfDidNotPostpone (x : TermElabM α) : TermElabM α := do
-- We just reuse the implementation of `observing` and `applyResult`.
let r ← observing x
applyResult r
/--
Return the universe level names explicitly provided by the user.
-/
def getLevelNames : TermElabM (List Name) :=
return (← get).levelNames
/--
Given a free variable `fvar`, return its declaration.
This function panics if `fvar` is not a free variable.
-/
def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do
match (← getLCtx).find? fvar.fvarId! with
| some d => pure d
| none => unreachable!
instance : AddErrorMessageContext TermElabM where
add ref msg := do
let ctx ← read
let ref := getBetterRef ref ctx.macroStack
let msg ← addMessageContext msg
let msg ← addMacroStack msg ctx.macroStack
pure (ref, msg)
/--
Execute `x` without storing `Syntax` for recursive applications. See `saveRecAppSyntax` field at `Context`.
-/
def withoutSavingRecAppSyntax (x : TermElabM α) : TermElabM α :=
withReader (fun ctx => { ctx with saveRecAppSyntax := false }) x
unsafe def mkTermElabAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute TermElab) :=
mkElabAttribute TermElab `builtin_term_elab `term_elab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term" ref
@[implemented_by mkTermElabAttributeUnsafe]
opaque mkTermElabAttribute (ref : Name) : IO (KeyedDeclsAttribute TermElab)
builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermElabAttribute decl_name%
/--
Auxiliary datatype for presenting a Lean lvalue modifier.
We represent an unelaborated lvalue as a `Syntax` (or `Expr`) and `List LVal`.
Example: `a.foo.1` is represented as the `Syntax` `a` and the list
`[LVal.fieldName "foo", LVal.fieldIdx 1]`.
-/
inductive LVal where
| fieldIdx (ref : Syntax) (i : Nat)
/-- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierarchical/composite name.
`ref` is the syntax object representing the field. `fullRef` includes the LHS. -/
| fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (fullRef : Syntax)
def LVal.getRef : LVal → Syntax
| .fieldIdx ref _ => ref
| .fieldName ref .. => ref
def LVal.isFieldName : LVal → Bool
| .fieldName .. => true
| _ => false
instance : ToString LVal where
toString
| .fieldIdx _ i => toString i
| .fieldName _ n .. => n
/-- Return the name of the declaration being elaborated if available. -/
def getDeclName? : TermElabM (Option Name) := return (← read).declName?
/-- Return the list of nested `let rec` declarations that need to be lifted. -/
def getLetRecsToLift : TermElabM (List LetRecToLift) := return (← get).letRecsToLift
/-- Return the declaration of the given metavariable -/
def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := return (← getMCtx).getDecl mvarId
instance : MonadParentDecl TermElabM where
getParentDeclName? := getDeclName?
/-- Execute `withSaveParentDeclInfoContext x` with `declName? := name`. See `getDeclName?`. -/
def withDeclName (name : Name) (x : TermElabM α) : TermElabM α :=
withReader (fun ctx => { ctx with declName? := name }) <| withSaveParentDeclInfoContext x
/-- Update the universe level parameter names. -/
def setLevelNames (levelNames : List Name) : TermElabM Unit :=
modify fun s => { s with levelNames := levelNames }
/-- Execute `x` using `levelNames` as the universe level parameter names. See `getLevelNames`. -/
def withLevelNames (levelNames : List Name) (x : TermElabM α) : TermElabM α := do
let levelNamesSaved ← getLevelNames
setLevelNames levelNames
try x finally setLevelNames levelNamesSaved
/--
Declare an auxiliary local declaration `shortDeclName : type` for elaborating recursive declaration `declName`,
update the mapping `auxDeclToFullName`, and then execute `k`.
-/
def withAuxDecl (shortDeclName : Name) (type : Expr) (declName : Name) (k : Expr → TermElabM α) : TermElabM α :=
withLocalDecl shortDeclName .default (kind := .auxDecl) type fun x =>
withReader (fun ctx => { ctx with auxDeclToFullName := ctx.auxDeclToFullName.insert x.fvarId! declName }) do
k x
def withoutErrToSorryImp (x : TermElabM α) : TermElabM α :=
withReader (fun ctx => { ctx with errToSorry := false }) x
/--
Execute `x` without converting errors (i.e., exceptions) to `sorry` applications.
Recall that when `errToSorry = true`, the method `elabTerm` catches exceptions and converts them into `sorry` applications.
-/
def withoutErrToSorry [MonadFunctorT TermElabM m] : m α → m α :=
monadMap (m := TermElabM) withoutErrToSorryImp
def withoutHeedElabAsElimImp (x : TermElabM α) : TermElabM α :=
withReader (fun ctx => { ctx with heedElabAsElim := false }) x
/--
Execute `x` without heeding the `elab_as_elim` attribute. Useful when there is
no expected type (so `elabAppArgs` would fail), but expect that the user wants
to use such constants.
-/
def withoutHeedElabAsElim [MonadFunctorT TermElabM m] : m α → m α :=
monadMap (m := TermElabM) withoutHeedElabAsElimImp
/--
Execute `x` but discard changes performed at `Term.State` and `Meta.State`.
Recall that the `Environment` and `InfoState` are at `Core.State`. Thus, any updates to it will
be preserved. This method is useful for performing computations where all
metavariable must be resolved or discarded.
The `InfoTree`s are not discarded, however, and wrapped in `InfoTree.Context`
to store their metavariable context. -/
def withoutModifyingElabMetaStateWithInfo (x : TermElabM α) : TermElabM α := do
let s ← get
let sMeta ← getThe Meta.State
try
withSaveInfoContext x
finally
set s
set sMeta
/--
Execute `x` but discard changes performed to the state.
However, the info trees and messages are not discarded. -/
private def withoutModifyingStateWithInfoAndMessagesImpl (x : TermElabM α) : TermElabM α := do
let saved ← saveState
try
withSaveInfoContext x
finally
let saved := { saved with meta.core.infoState := (← getInfoState), meta.core.messages := (← getThe Core.State).messages }
restoreState saved
/-- For testing `TermElabM` methods. The #eval command will sign the error. -/
def throwErrorIfErrors : TermElabM Unit := do
if (← MonadLog.hasErrors) then
throwError "Error(s)"
def traceAtCmdPos (cls : Name) (msg : Unit → MessageData) : TermElabM Unit :=
withRef Syntax.missing <| trace cls msg
def ppGoal (mvarId : MVarId) : TermElabM Format :=
Meta.ppGoal mvarId
open Level (LevelElabM)
def liftLevelM (x : LevelElabM α) : TermElabM α := do
let ctx ← read
let mctx ← getMCtx
let ngen ← getNGen
let lvlCtx : Level.Context := { options := (← getOptions), ref := (← getRef), autoBoundImplicit := ctx.autoBoundImplicit }
match (x lvlCtx).run { ngen := ngen, mctx := mctx, levelNames := (← getLevelNames) } with
| .ok a newS => setMCtx newS.mctx; setNGen newS.ngen; setLevelNames newS.levelNames; pure a
| .error ex _ => throw ex
def elabLevel (stx : Syntax) : TermElabM Level :=
liftLevelM <| Level.elabLevel stx
/-- Elaborate `x` with `stx` on the macro stack -/
def withPushMacroExpansionStack (beforeStx afterStx : Syntax) (x : TermElabM α) : TermElabM α :=
withReader (fun ctx => { ctx with macroStack := { before := beforeStx, after := afterStx } :: ctx.macroStack }) x
/-- Elaborate `x` with `stx` on the macro stack and produce macro expansion info -/
def withMacroExpansion (beforeStx afterStx : Syntax) (x : TermElabM α) : TermElabM α :=
withMacroExpansionInfo beforeStx afterStx do
withPushMacroExpansionStack beforeStx afterStx x
/--
Add the given metavariable to the list of pending synthetic metavariables.
The method `synthesizeSyntheticMVars` is used to process the metavariables on this list. -/
def registerSyntheticMVar (stx : Syntax) (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit := do
modify fun s => { s with syntheticMVars := s.syntheticMVars.insert mvarId { stx, kind }, pendingMVars := mvarId :: s.pendingMVars }
def registerSyntheticMVarWithCurrRef (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit := do
registerSyntheticMVar (← getRef) mvarId kind
def registerMVarErrorInfo (mvarErrorInfo : MVarErrorInfo) : TermElabM Unit :=
modify fun s => { s with mvarErrorInfos := s.mvarErrorInfos.insert mvarErrorInfo.mvarId mvarErrorInfo }
def registerMVarErrorHoleInfo (mvarId : MVarId) (ref : Syntax) : TermElabM Unit :=
registerMVarErrorInfo { mvarId, ref, kind := .hole }
def registerMVarErrorImplicitArgInfo (mvarId : MVarId) (ref : Syntax) (app : Expr) : TermElabM Unit := do
registerMVarErrorInfo { mvarId, ref, kind := .implicitArg app }
def registerMVarErrorCustomInfo (mvarId : MVarId) (ref : Syntax) (msgData : MessageData) : TermElabM Unit := do
registerMVarErrorInfo { mvarId, ref, kind := .custom msgData }
def getMVarErrorInfo? (mvarId : MVarId) : TermElabM (Option MVarErrorInfo) := do
return (← get).mvarErrorInfos.find? mvarId
def registerCustomErrorIfMVar (e : Expr) (ref : Syntax) (msgData : MessageData) : TermElabM Unit :=
match e.getAppFn with
| Expr.mvar mvarId => registerMVarErrorCustomInfo mvarId ref msgData
| _ => pure ()
/--
Auxiliary method for reporting errors of the form "... contains metavariables ...".
This kind of error is thrown, for example, at `Match.lean` where elaboration
cannot continue if there are metavariables in patterns.
We only want to log it if we haven't logged any errors so far. -/
def throwMVarError (m : MessageData) : TermElabM α := do
if (← MonadLog.hasErrors) then
throwAbortTerm
else
throwError m
def MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) (extraMsg? : Option MessageData) : TermElabM Unit := do
match mvarErrorInfo.kind with
| MVarErrorKind.implicitArg app => do
let app ← instantiateMVars app
let msg := addArgName "don't know how to synthesize implicit argument"
let msg := msg ++ m!"{indentExpr app.setAppPPExplicitForExposingMVars}" ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId
logErrorAt mvarErrorInfo.ref (appendExtra msg)
| MVarErrorKind.hole => do
let msg := addArgName "don't know how to synthesize placeholder" " for argument"
let msg := msg ++ Format.line ++ "context:" ++ Format.line ++ MessageData.ofGoal mvarErrorInfo.mvarId
logErrorAt mvarErrorInfo.ref (MessageData.tagged `Elab.synthPlaceholder <| appendExtra msg)
| MVarErrorKind.custom msg =>
logErrorAt mvarErrorInfo.ref (appendExtra msg)
where
/-- Append `mvarErrorInfo` argument name (if available) to the message.
Remark: if the argument name contains macro scopes we do not append it. -/
addArgName (msg : MessageData) (extra : String := "") : MessageData :=
match mvarErrorInfo.argName? with
| none => msg
| some argName => if argName.hasMacroScopes then msg else msg ++ extra ++ m!" '{argName}'"
appendExtra (msg : MessageData) : MessageData :=
match extraMsg? with
| none => msg
| some extraMsg => msg ++ extraMsg
/--
Try to log errors for the unassigned metavariables `pendingMVarIds`.
Return `true` if there were "unfilled holes", and we should "abort" declaration.
TODO: try to fill "all" holes using synthetic "sorry's"
Remark: We only log the "unfilled holes" as new errors if no error has been logged so far. -/
def logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) (extraMsg? : Option MessageData := none) : TermElabM Bool := do
if pendingMVarIds.isEmpty then
return false
else
let hasOtherErrors ← MonadLog.hasErrors
let mut hasNewErrors := false
let mut alreadyVisited : MVarIdSet := {}
let mut errors : Array MVarErrorInfo := #[]
for (_, mvarErrorInfo) in (← get).mvarErrorInfos do
let mvarId := mvarErrorInfo.mvarId
unless alreadyVisited.contains mvarId do
alreadyVisited := alreadyVisited.insert mvarId
/- The metavariable `mvarErrorInfo.mvarId` may have been assigned or
delayed assigned to another metavariable that is unassigned. -/
let mvarDeps ← getMVars (mkMVar mvarId)
if mvarDeps.any pendingMVarIds.contains then do
unless hasOtherErrors do
errors := errors.push mvarErrorInfo
hasNewErrors := true
-- To sort the errors by position use
-- let sortedErrors := errors.qsort fun e₁ e₂ => e₁.ref.getPos?.getD 0 < e₂.ref.getPos?.getD 0
for error in errors do
error.mvarId.withContext do
error.logError extraMsg?
return hasNewErrors
/-- Ensure metavariables registered using `registerMVarErrorInfos` (and used in the given declaration) have been assigned. -/
def ensureNoUnassignedMVars (decl : Declaration) : TermElabM Unit := do
let pendingMVarIds ← getMVarsAtDecl decl
if (← logUnassignedUsingErrorInfos pendingMVarIds) then
throwAbortCommand
/--
Execute `x` without allowing it to postpone elaboration tasks.
That is, `tryPostpone` is a noop. -/
def withoutPostponing (x : TermElabM α) : TermElabM α :=
withReader (fun ctx => { ctx with mayPostpone := false }) x
/-- Creates syntax for `(` <ident> `:` <type> `)` -/
def mkExplicitBinder (ident : Syntax) (type : Syntax) : Syntax :=
mkNode ``Lean.Parser.Term.explicitBinder #[mkAtom "(", mkNullNode #[ident], mkNullNode #[mkAtom ":", type], mkNullNode, mkAtom ")"]
/--
Convert unassigned universe level metavariables into parameters.
The new parameter names are fresh names of the form `u_i` with regard to `ctx.levelNames`, which is updated with the new names. -/
def levelMVarToParam (e : Expr) (except : LMVarId → Bool := fun _ => false) : TermElabM Expr := do
let levelNames ← getLevelNames
let r := (← getMCtx).levelMVarToParam (fun n => levelNames.elem n) except e `u 1
setLevelNames (levelNames ++ r.newParamNames.toList)
setMCtx r.mctx
return r.expr
/--
Auxiliary method for creating fresh binder names.
Do not confuse with the method for creating fresh free/meta variable ids. -/
def mkFreshBinderName [Monad m] [MonadQuotation m] : m Name :=
withFreshMacroScope <| MonadQuotation.addMacroScope `x
/--
Auxiliary method for creating a `Syntax.ident` containing
a fresh name. This method is intended for creating fresh binder names.
It is just a thin layer on top of `mkFreshUserName`. -/
def mkFreshIdent [Monad m] [MonadQuotation m] (ref : Syntax) (canonical := false) : m Ident :=
return mkIdentFrom ref (← mkFreshBinderName) canonical
private def applyAttributesCore
(declName : Name) (attrs : Array Attribute)
(applicationTime? : Option AttributeApplicationTime) : TermElabM Unit := do profileitM Exception "attribute application" (← getOptions) do
for attr in attrs do
withRef attr.stx do withLogging do
let env ← getEnv
match getAttributeImpl env attr.name with
| Except.error errMsg => throwError errMsg
| Except.ok attrImpl =>
let runAttr := attrImpl.add declName attr.stx attr.kind
let runAttr := do
-- not truly an elaborator, but a sensible target for go-to-definition
let elaborator := attrImpl.ref
if (← getInfoState).enabled && (← getEnv).contains elaborator then
withInfoContext (mkInfo := return .ofCommandInfo { elaborator, stx := attr.stx }) do
try runAttr
finally if attr.stx[0].isIdent || attr.stx[0].isAtom then
-- Add an additional node over the leading identifier if there is one to make it look more function-like.
-- Do this last because we want user-created infos to take precedence
pushInfoLeaf <| .ofCommandInfo { elaborator, stx := attr.stx[0] }
else
runAttr
match applicationTime? with
| none => runAttr
| some applicationTime =>
if applicationTime == attrImpl.applicationTime then
runAttr
/-- Apply given attributes **at** a given application time -/
def applyAttributesAt (declName : Name) (attrs : Array Attribute) (applicationTime : AttributeApplicationTime) : TermElabM Unit :=
applyAttributesCore declName attrs applicationTime
def applyAttributes (declName : Name) (attrs : Array Attribute) : TermElabM Unit :=
applyAttributesCore declName attrs none
def mkTypeMismatchError (header? : Option String) (e : Expr) (eType : Expr) (expectedType : Expr) : TermElabM MessageData := do
let header : MessageData := match header? with
| some header => m!"{header} "
| none => m!"type mismatch{indentExpr e}\n"
return m!"{header}{← mkHasTypeButIsExpectedMsg eType expectedType}"
def throwTypeMismatchError (header? : Option String) (expectedType : Expr) (eType : Expr) (e : Expr)
(f? : Option Expr := none) (_extraMsg? : Option MessageData := none) : TermElabM α := do
/-
We ignore `extraMsg?` for now. In all our tests, it contained no useful information. It was
always of the form:
```
failed to synthesize instance
CoeT <eType> <e> <expectedType>
```
We should revisit this decision in the future and decide whether it may contain useful information
or not. -/
let extraMsg := Format.nil
/-
let extraMsg : MessageData := match extraMsg? with
| none => Format.nil
| some extraMsg => Format.line ++ extraMsg;
-/
match f? with
| none => throwError "{← mkTypeMismatchError header? e eType expectedType}{extraMsg}"
| some f => Meta.throwAppTypeMismatch f e
def withoutMacroStackAtErr (x : TermElabM α) : TermElabM α :=
withTheReader Core.Context (fun (ctx : Core.Context) => { ctx with options := pp.macroStack.set ctx.options false }) x
namespace ContainsPendingMVar
abbrev M := MonadCacheT Expr Unit (OptionT MetaM)
/-- See `containsPostponedTerm` -/
partial def visit (e : Expr) : M Unit := do
checkCache e fun _ => do
match e with
| .forallE _ d b _ => visit d; visit b
| .lam _ d b _ => visit d; visit b
| .letE _ t v b _ => visit t; visit v; visit b
| .app f a => visit f; visit a
| .mdata _ b => visit b
| .proj _ _ b => visit b
| .fvar fvarId .. =>
match (← fvarId.getDecl) with
| .cdecl .. => return ()
| .ldecl (value := v) .. => visit v
| .mvar mvarId .. =>
let e' ← instantiateMVars e
if e' != e then
visit e'
else
match (← getDelayedMVarAssignment? mvarId) with
| some d => visit (mkMVar d.mvarIdPending)
| none => failure
| _ => return ()
end ContainsPendingMVar
/-- Return `true` if `e` contains a pending metavariable. Remark: it also visits let-declarations. -/
def containsPendingMVar (e : Expr) : MetaM Bool := do
match (← ContainsPendingMVar.visit e |>.run.run) with
| some _ => return false
| none => return true
/--
Try to synthesize metavariable using type class resolution.
This method assumes the local context and local instances of `instMVar` coincide
with the current local context and local instances.
Return `true` if the instance was synthesized successfully, and `false` if
the instance contains unassigned metavariables that are blocking the type class
resolution procedure. Throw an exception if resolution or assignment irrevocably fails.
-/
def synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := none) : TermElabM Bool := do
let instMVarDecl ← getMVarDecl instMVar
let type := instMVarDecl.type
let type ← instantiateMVars type
let result ← trySynthInstance type maxResultSize?
match result with
| LOption.some val =>
if (← instMVar.isAssigned) then
let oldVal ← instantiateMVars (mkMVar instMVar)
unless (← isDefEq oldVal val) do
if (← containsPendingMVar oldVal <||> containsPendingMVar val) then
/- If `val` or `oldVal` contains metavariables directly or indirectly (e.g., in a let-declaration),
we return `false` to indicate we should try again later. This is very coarse grain since
the metavariable may not be responsible for the failure. We should refine the test in the future if needed.
This check has been added to address dependencies between postponed metavariables. The following
example demonstrates the issue fixed by this test.
```
structure Point where
x : Nat
y : Nat
def Point.compute (p : Point) : Point :=
let p := { p with x := 1 }
let p := { p with y := 0 }
if (p.x - p.y) > p.x then p else p
```
The `isDefEq` test above fails for `Decidable (p.x - p.y ≤ p.x)` when the structure instance assigned to
`p` has not been elaborated yet.
-/
return false -- we will try again later
let oldValType ← inferType oldVal
let valType ← inferType val
unless (← isDefEq oldValType valType) do
throwError "synthesized type class instance type is not definitionally equal to expected type, synthesized{indentExpr val}\nhas type{indentExpr valType}\nexpected{indentExpr oldValType}"
throwError "synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized{indentExpr val}\ninferred{indentExpr oldVal}"
else
unless (← isDefEq (mkMVar instMVar) val) do
throwError "failed to assign synthesized type class instance{indentExpr val}"
return true
| .undef => return false -- we will try later
| .none =>
if (← read).ignoreTCFailures then
return false
else
throwError "failed to synthesize instance{indentExpr type}"
def mkCoe (expectedType : Expr) (e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
withTraceNode `Elab.coe (fun _ => return m!"adding coercion for {e} : {← inferType e} =?= {expectedType}") do
try
withoutMacroStackAtErr do
match ← coerce? e expectedType with
| .some eNew => return eNew
| .none => failure
| .undef =>
let mvarAux ← mkFreshExprMVar expectedType MetavarKind.syntheticOpaque
registerSyntheticMVarWithCurrRef mvarAux.mvarId! (.coe errorMsgHeader? expectedType e f?)
return mvarAux
catch
| .error _ msg => throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f? msg
| _ => throwTypeMismatchError errorMsgHeader? expectedType (← inferType e) e f?
/--
If `expectedType?` is `some t`, then ensures `t` and `eType` are definitionally equal by inserting a coercion if necessary.
Argument `f?` is used only for generating error messages when inserting coercions fails.
-/
def ensureHasType (expectedType? : Option Expr) (e : Expr)
(errorMsgHeader? : Option String := none) (f? : Option Expr := none) : TermElabM Expr := do
let some expectedType := expectedType? | return e
if (← isDefEq (← inferType e) expectedType) then
return e
else
mkCoe expectedType e f? errorMsgHeader?
/--
Create a synthetic sorry for the given expected type. If `expectedType? = none`, then a fresh
metavariable is created to represent the type.
-/
private def mkSyntheticSorryFor (expectedType? : Option Expr) : TermElabM Expr := do
let expectedType ← match expectedType? with
| none => mkFreshTypeMVar
| some expectedType => pure expectedType
mkSyntheticSorry expectedType
/--
Log the given exception, and create a synthetic sorry for representing the failed
elaboration step with exception `ex`.
-/
def exceptionToSorry (ex : Exception) (expectedType? : Option Expr) : TermElabM Expr := do
let syntheticSorry ← mkSyntheticSorryFor expectedType?
logException ex
pure syntheticSorry
/-- If `mayPostpone == true`, throw `Expection.postpone`. -/
def tryPostpone : TermElabM Unit := do
if (← read).mayPostpone then
throwPostpone
/-- Return `true` if `e` reduces (by unfolding only `[reducible]` declarations) to `?m ...` -/
def isMVarApp (e : Expr) : TermElabM Bool :=
return (← whnfR e).getAppFn.isMVar
/-- If `mayPostpone == true` and `e`'s head is a metavariable, throw `Exception.postpone`. -/
def tryPostponeIfMVar (e : Expr) : TermElabM Unit := do
if (← isMVarApp e) then
tryPostpone
/-- If `e? = some e`, then `tryPostponeIfMVar e`, otherwise it is just `tryPostpone`. -/
def tryPostponeIfNoneOrMVar (e? : Option Expr) : TermElabM Unit :=
match e? with
| some e => tryPostponeIfMVar e
| none => tryPostpone
/--
Throws `Exception.postpone`, if `expectedType?` contains unassigned metavariables.
It is a noop if `mayPostpone == false`.
-/
def tryPostponeIfHasMVars? (expectedType? : Option Expr) : TermElabM (Option Expr) := do
tryPostponeIfNoneOrMVar expectedType?
let some expectedType := expectedType? | return none
let expectedType ← instantiateMVars expectedType
if expectedType.hasExprMVar then
tryPostpone
return none
return some expectedType
/--
Throws `Exception.postpone`, if `expectedType?` contains unassigned metavariables.
If `mayPostpone == false`, it throws error `msg`.
-/
def tryPostponeIfHasMVars (expectedType? : Option Expr) (msg : String) : TermElabM Expr := do
let some expectedType ← tryPostponeIfHasMVars? expectedType? |
throwError "{msg}, expected type contains metavariables{indentD expectedType?}"
return expectedType
def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do
tryPostponeIfNoneOrMVar expectedType?
let some expectedType ← pure expectedType?
| throwError "expected type must be known"
x expectedType
/--
Save relevant context for term elaboration postponement.
-/
def saveContext : TermElabM SavedContext :=
return {
macroStack := (← read).macroStack
declName? := (← read).declName?
options := (← getOptions)
openDecls := (← getOpenDecls)
errToSorry := (← read).errToSorry
levelNames := (← get).levelNames
}
/--
Execute `x` with the context saved using `saveContext`.
-/
def withSavedContext (savedCtx : SavedContext) (x : TermElabM α) : TermElabM α := do
withReader (fun ctx => { ctx with declName? := savedCtx.declName?, macroStack := savedCtx.macroStack, errToSorry := savedCtx.errToSorry }) <|
withTheReader Core.Context (fun ctx => { ctx with options := savedCtx.options, openDecls := savedCtx.openDecls }) <|
withLevelNames savedCtx.levelNames x
/--
Delay the elaboration of `stx`, and return a fresh metavariable that works a placeholder.
Remark: the caller is responsible for making sure the info tree is properly updated.
This method is used only at `elabUsingElabFnsAux`.
-/
private def postponeElabTermCore (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
trace[Elab.postpone] "{stx} : {expectedType?}"
let mvar ← mkFreshExprMVar expectedType? MetavarKind.syntheticOpaque
registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed (← saveContext))
return mvar
def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) :=
return (← get).syntheticMVars.find? mvarId
/--
Create an auxiliary annotation to make sure we create an `Info` even if `e` is a metavariable.
See `mkTermInfo`.
We use this function because some elaboration functions elaborate subterms that may not be immediately
part of the resulting term. Example:
```
let_mvar% ?m := b; wait_if_type_mvar% ?m; body
```
If the type of `b` is not known, then `wait_if_type_mvar% ?m; body` is postponed and just returns a fresh
metavariable `?n`. The elaborator for
```
let_mvar% ?m := b; wait_if_type_mvar% ?m; body
```
returns `mkSaveInfoAnnotation ?n` to make sure the info nodes created when elaborating `b` are "saved".
This is a bit hackish, but elaborators like `let_mvar%` are rare.
-/
def mkSaveInfoAnnotation (e : Expr) : Expr :=
if e.isMVar then
mkAnnotation `save_info e
else
e
def isSaveInfoAnnotation? (e : Expr) : Option Expr :=
annotation? `save_info e
partial def removeSaveInfoAnnotation (e : Expr) : Expr :=
match isSaveInfoAnnotation? e with
| some e => removeSaveInfoAnnotation e
| _ => e
/--
Return `some mvarId` if `e` corresponds to a hole that is going to be filled "later" by executing a tactic or resuming elaboration.
We do not save `ofTermInfo` for this kind of node in the `InfoTree`.
-/
def isTacticOrPostponedHole? (e : Expr) : TermElabM (Option MVarId) := do
match e with
| Expr.mvar mvarId =>
match (← getSyntheticMVarDecl? mvarId) with
| some { kind := .tactic .., .. } => return mvarId
| some { kind := .postponed .., .. } => return mvarId
| _ => return none
| _ => pure none
def mkTermInfo (elaborator : Name) (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (isBinder := false) : TermElabM (Sum Info MVarId) := do
match (← isTacticOrPostponedHole? e) with
| some mvarId => return Sum.inr mvarId
| none =>
let e := removeSaveInfoAnnotation e
return Sum.inl <| Info.ofTermInfo { elaborator, lctx := lctx?.getD (← getLCtx), expr := e, stx, expectedType?, isBinder }
/--
Pushes a new leaf node to the info tree associating the expression `e` to the syntax `stx`.
As a result, when the user hovers over `stx` they will see the type of `e`, and if `e`
is a constant they will see the constant's doc string.
* `expectedType?`: the expected type of `e` at the point of elaboration, if available
* `lctx?`: the local context in which to interpret `e` (otherwise it will use `← getLCtx`)
* `elaborator`: a declaration name used as an alternative target for go-to-definition
* `isBinder`: if true, this will be treated as defining `e` (which should be a local constant)
for the purpose of go-to-definition on local variables
* `force`: In patterns, the effect of `addTermInfo` is usually suppressed and replaced
by a `patternWithRef?` annotation which will be turned into a term info on the
post-match-elaboration expression. This flag overrides that behavior and adds the term
info immediately. (See https://github.com/leanprover/lean4/pull/1664.)
-/
def addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none)
(lctx? : Option LocalContext := none) (elaborator := Name.anonymous)
(isBinder := false) (force := false) : TermElabM Expr := do
if (← read).inPattern && !force then
return mkPatternWithRef e stx
else
withInfoContext' (pure ()) (fun _ => mkTermInfo elaborator stx e expectedType? lctx? isBinder) |> discard
return e
def addTermInfo' (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator := Name.anonymous) (isBinder := false) : TermElabM Unit :=
discard <| addTermInfo stx e expectedType? lctx? elaborator isBinder
def withInfoContext' (stx : Syntax) (x : TermElabM Expr) (mkInfo : Expr → TermElabM (Sum Info MVarId)) : TermElabM Expr := do
if (← read).inPattern then
let e ← x