max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: docstrings for src/Lean/Elab/Term.lean

Browse source
This commit is contained in:
Leonardo de Moura 2022-06-30 19:01:11 -07:00
parent 14260f454b
commit d1f966fa6d
1 changed files with 117 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

141
src/Lean/Elab/Term.lean
View file

@ -38,17 +38,18 @@ structure SavedContext where
/-- We use synthetic metavariables as placeholders for pending elaboration steps. -/
inductive SyntheticMVarKind where
-- typeclass instance search
| typeClass
/- Similar to typeClass, but error messages are different.
| /-- Use typeclass resolution to synthesize value for metavariable. -/
typeClass
| /--
Similar to `typeClass`, but error messages are different.
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) (eNew : Expr) (expectedType : Expr) (eType : Expr) (e : Expr) (f? : Option Expr)
-- tactic block execution
| tactic (tacticCode : Syntax) (ctx : SavedContext)
-- `elabTerm` call that threw `Exception.postpone` (input is stored at `SyntheticMVarDecl.ref`)
| postponed (ctx : SavedContext)
coe (header? : Option String) (eNew : Expr) (expectedType : Expr) (eType : 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)
instance : ToString SyntheticMVarKind where
toString
@ -62,10 +63,17 @@ structure SyntheticMVarDecl where
stx : Syntax
kind : SyntheticMVarKind
/--
We can optionally associate an error context with a metavariable (see `MVarErrorInfo`).
We have three different kinds of error context.
-/
inductive MVarErrorKind where
| implicitArg (ctx : Expr)
| hole
| custom (msgData : MessageData)
| /-- 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
@ -74,6 +82,9 @@ instance : ToString MVarErrorKind where
| MVarErrorKind.hole => "hole"
| MVarErrorKind.custom _ => "custom"
/--
We can optionally associate an error context with metavariables.
-/
structure MVarErrorInfo where
mvarId : MVarId
ref : Syntax
@ -81,6 +92,10 @@ structure MVarErrorInfo where
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
@ -94,6 +109,9 @@ structure LetRecToLift where
mvarId : MVarId
deriving Inhabited
/--
State of the `TermElabM` monad.
-/
structure State where
levelNames : List Name := []
syntheticMVars : List SyntheticMVarDecl := []
@ -106,10 +124,19 @@ 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
@ -118,11 +145,17 @@ structure Snapshot where
stx : Syntax
deriving Inhabited
/--
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 : Std.PHashMap CacheKey Snapshot := {}
post : Std.PHashMap CacheKey Snapshot := {}
@ -178,6 +211,7 @@ structure Context where
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`.
@ -196,6 +230,9 @@ open Meta
instance : Inhabited (TermElabM α) where
default := throw default
/--
Backtrackable state for the `TermElabM` monad.
-/
structure SavedState where
meta : Meta.SavedState
«elab» : State
@ -263,9 +300,16 @@ def commitIfDidNotPostpone (x : TermElabM α) : TermElabM α := do
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
@ -352,23 +396,35 @@ instance : ToString LVal where
| LVal.fieldName _ n .. => n
| LVal.getOp _ idx => "[" ++ toString idx ++ "]"
/-- 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 `true` if the give metavariable is already assigned. -/
def isExprMVarAssigned (mvarId : MVarId) : TermElabM Bool := return (← getMCtx).isExprAssigned mvarId
/-- Return the declaration of the given metavariable -/
def getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl := return (← getMCtx).getDecl mvarId
/-- Assign `mvarId := val`. It assumes `mvarId` it a valid universe level metavariable id. -/
def assignLevelMVar (mvarId : MVarId) (val : Level) : TermElabM Unit := modifyThe Meta.State fun s => { s with mctx := s.mctx.assignLevel mvarId val }
/-- Execute `x` with `declName? := name`. See `getDeclName? -/
def withDeclName (name : Name) (x : TermElabM α) : TermElabM α :=
withReader (fun ctx => { ctx with declName? := name }) 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
/--
Execute `x` without converting errors (i.e., exceptions) to `sorry` applications.
Recall that when `errToSorry = true`, the method `elabTerm` catches exceptions and convert them into `sorry` applications.
-/
def withoutErrToSorry (x : TermElabM α) : TermElabM α :=
withReader (fun ctx => { ctx with errToSorry := false }) x
@ -636,12 +692,14 @@ def containsPendingMVar (e : Expr) : TermElabM Bool := do
| 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. -/
/--
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
@ -701,9 +759,10 @@ register_builtin_option maxCoeSize : Nat := {
def synthesizeCoeInstMVarCore (instMVar : MVarId) : TermElabM Bool := do
synthesizeInstMVarCore instMVar (some (maxCoeSize.get (← getOptions)))
/-
The coercion from `α` to `Thunk α` cannot be implemented using an instance because it would
eagerly evaluate `e` -/
/--
The coercion from `α` to `Thunk α` cannot be implemented using an instance because it would
eagerly evaluate `e`
-/
def tryCoeThunk? (expectedType : Expr) (eType : Expr) (e : Expr) : TermElabM (Option Expr) := do
match expectedType with
| Expr.app (Expr.const ``Thunk u _) arg _ =>
@ -750,13 +809,15 @@ private def tryCoe (errorMsgHeader? : Option String) (expectedType : Expr) (eTyp
| some r => return r
| none => mkCoe expectedType eType e f? errorMsgHeader?
/-- Return `some (m, α)` if `type` can be reduced to an application of the form `m α` using `[reducible]` transparency. -/
def isTypeApp? (type : Expr) : TermElabM (Option (Expr × Expr)) := do
let type ← withReducible <| whnf type
match type with
| Expr.app m α _ => return some ((← instantiateMVars m), (← instantiateMVars α))
| _ => return none
def synthesizeInst (type : Expr) : TermElabM Expr := do
/-- Helper method used to implement auto-lift and coercions -/
private def synthesizeInst (type : Expr) : TermElabM Expr := do
let type ← instantiateMVars type
match (← trySynthInstance type) with
| LOption.some val => return val
@ -764,11 +825,15 @@ def synthesizeInst (type : Expr) : TermElabM Expr := do
| LOption.undef => throwError "failed to synthesize instance{indentExpr type}"
| LOption.none => throwError "failed to synthesize instance{indentExpr type}"
/--
Return `true` if `type` is of the form `m α` where `m` is a `Monad`.
Note that we reduce `type` using transparency `[reducible]`.
-/
def isMonadApp (type : Expr) : TermElabM Bool := do
let some (m, _) ← isTypeApp? type | return false
return (← isMonad? m) |>.isSome
/-
/--
Try coercions and monad lifts to make sure `e` has type `expectedType`.
If `expectedType` is of the form `n β`, we try monad lifts and other extensions.
@ -892,12 +957,20 @@ def ensureHasType (expectedType? : Option Expr) (e : Expr) (errorMsgHeader? : Op
let eType ← inferType e
ensureHasTypeAux expectedType? eType e none 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 an 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
@ -914,11 +987,16 @@ def tryPostponeIfMVar (e : Expr) : TermElabM Unit := do
if e.getAppFn.isMVar 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
@ -928,11 +1006,18 @@ def tryPostponeIfHasMVars? (expectedType? : Option Expr) : TermElabM (Option Exp
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
/--
Save relevant context for term elaboration postponement.
-/
def saveContext : TermElabM SavedContext :=
return {
macroStack := (← read).macroStack
@ -943,6 +1028,9 @@ def saveContext : TermElabM SavedContext :=
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 }) <|
@ -1293,6 +1381,11 @@ def adaptExpander (exp : Syntax → TermElabM Syntax) : TermElab := fun stx expe
let stx' ← exp stx
withMacroExpansion stx stx' <| elabTerm stx' expectedType?
/--
Create a new metavariable with the given type, and try to synthesize it.
It type class resolution cannot be executed (e.g., it is stuck because of metavariables in `type`),
register metavariable as a pending one.
-/
def mkInstMVar (type : Expr) : TermElabM Expr := do
let mvar ← mkFreshExprMVar type MetavarKind.synthetic
let mvarId := mvar.mvarId!
@ -1300,7 +1393,7 @@ def mkInstMVar (type : Expr) : TermElabM Expr := do
registerSyntheticMVarWithCurrRef mvarId SyntheticMVarKind.typeClass
return mvar
/-
/--
Relevant definitions:
```
class CoeSort (α : Sort u) (β : outParam (Sort v))
@ -1481,7 +1574,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
| _ => none
return loop view.name []
/- Return true iff `stx` is a `Syntax.ident`, and it is a local variable. -/
/-- Return true iff `stx` is a `Syntax.ident`, and it is a local variable. -/
def isLocalIdent? (stx : Syntax) : TermElabM (Option Expr) :=
match stx with
| Syntax.ident _ _ val _ => do