793 lines
34 KiB
Text
793 lines
34 KiB
Text
/-
|
||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Leonardo de Moura
|
||
-/
|
||
prelude
|
||
import Lean.Elab.Quotation.Precheck
|
||
import Lean.Elab.Term
|
||
import Lean.Elab.BindersUtil
|
||
import Lean.Elab.SyntheticMVars
|
||
import Lean.Elab.PreDefinition.TerminationHint
|
||
|
||
namespace Lean.Elab.Term
|
||
open Meta
|
||
open Lean.Parser.Term
|
||
open TSyntax.Compat
|
||
|
||
/--
|
||
Given syntax of the forms
|
||
a) (`:` term)?
|
||
b) `:` term
|
||
return `term` if it is present, or a hole if not. -/
|
||
private def expandBinderType (ref : Syntax) (stx : Syntax) : Syntax :=
|
||
if stx.getNumArgs == 0 then
|
||
mkHole ref
|
||
else
|
||
stx[1]
|
||
|
||
/-- Given syntax of the form `ident <|> hole`, return `ident`. If `hole`, then we create a new anonymous name. -/
|
||
private def expandBinderIdent (stx : Syntax) : TermElabM Syntax :=
|
||
match stx with
|
||
| `(_) => mkFreshIdent stx (canonical := true)
|
||
| _ => pure stx
|
||
|
||
/-- Given syntax of the form `(ident >> " : ")?`, return `ident`, or a new instance name. -/
|
||
private def expandOptIdent (stx : Syntax) : TermElabM Syntax := do
|
||
if stx.isNone then
|
||
let id ← withFreshMacroScope <| MonadQuotation.addMacroScope `inst
|
||
return mkIdentFrom stx id
|
||
else
|
||
return stx[0]
|
||
|
||
/-- Auxiliary datatype for elaborating binders. -/
|
||
structure BinderView where
|
||
/--
|
||
Position information provider for the Info Tree.
|
||
We currently do not track binder "macro expansion" steps in the info tree.
|
||
For example, suppose we expand a `_` into a fresh identifier. The fresh identifier
|
||
has synthetic position since it was not written by the user, and we would not get
|
||
hover information for the `_` because we also don't have this macro expansion step
|
||
stored in the info tree. Thus, we store the original `Syntax` in `ref`, and use
|
||
it when storing the binder information in the info tree.
|
||
|
||
Potential better solution: add a binder syntax category, an extensible `elabBinder`
|
||
(like we have `elabTerm`), and perform all macro expansion steps at `elabBinder` and
|
||
record them in the infro tree.
|
||
-/
|
||
ref : Syntax
|
||
id : Syntax
|
||
type : Syntax
|
||
bi : BinderInfo
|
||
|
||
/--
|
||
Determines the local declaration kind depending on the variable name.
|
||
|
||
The `__x` in `let __x := 42; body` gets kind `.implDetail`.
|
||
-/
|
||
def kindOfBinderName (binderName : Name) : LocalDeclKind :=
|
||
if binderName.isImplementationDetail then
|
||
.implDetail
|
||
else
|
||
.default
|
||
|
||
partial def quoteAutoTactic : Syntax → CoreM Expr
|
||
| .ident _ _ val preresolved =>
|
||
return mkApp4 (.const ``Syntax.ident [])
|
||
(.const ``SourceInfo.none [])
|
||
(.app (.const ``String.toSubstring []) (mkStrLit (toString val)))
|
||
(toExpr val)
|
||
(toExpr preresolved)
|
||
| stx@(.node _ k args) => do
|
||
if stx.isAntiquot then
|
||
throwErrorAt stx "invalid auto tactic, antiquotation is not allowed"
|
||
else
|
||
let ty := .const ``Syntax []
|
||
let mut quotedArgs := mkApp (.const ``Array.empty [.zero]) ty
|
||
for arg in args do
|
||
if k == nullKind && (arg.isAntiquotSuffixSplice || arg.isAntiquotSplice) then
|
||
throwErrorAt arg "invalid auto tactic, antiquotation is not allowed"
|
||
else
|
||
let quotedArg ← quoteAutoTactic arg
|
||
quotedArgs := mkApp3 (.const ``Array.push [.zero]) ty quotedArgs quotedArg
|
||
return mkApp3 (.const ``Syntax.node []) (.const ``SourceInfo.none []) (toExpr k) quotedArgs
|
||
| .atom _ val => return .app (.const ``mkAtom []) (toExpr val)
|
||
| .missing => throwError "invalid auto tactic, tactic is missing"
|
||
|
||
def declareTacticSyntax (tactic : Syntax) : TermElabM Name :=
|
||
withFreshMacroScope do
|
||
let name ← MonadQuotation.addMacroScope ((← getEnv).asyncPrefix?.getD .anonymous ++ `_auto)
|
||
let type := Lean.mkConst `Lean.Syntax
|
||
let value ← quoteAutoTactic tactic
|
||
trace[Elab.autoParam] value
|
||
let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := .opaque,
|
||
safety := DefinitionSafety.safe }
|
||
addDecl decl
|
||
compileDecl decl
|
||
return name
|
||
|
||
/--
|
||
Expand `optional (binderTactic <|> binderDefault)`
|
||
```
|
||
def binderTactic := leading_parser " := " >> " by " >> tacticParser
|
||
def binderDefault := leading_parser " := " >> termParser
|
||
```
|
||
-/
|
||
private def expandBinderModifier (type : Syntax) (optBinderModifier : Syntax) : TermElabM Syntax := do
|
||
if optBinderModifier.isNone then
|
||
return type
|
||
else
|
||
let modifier := optBinderModifier[0]
|
||
let kind := modifier.getKind
|
||
if kind == `Lean.Parser.Term.binderDefault then
|
||
let defaultVal := modifier[1]
|
||
`(optParam $type $defaultVal)
|
||
else if kind == `Lean.Parser.Term.binderTactic then
|
||
let tac := modifier[2]
|
||
let name ← declareTacticSyntax tac
|
||
`(autoParam $type $(mkIdentFrom tac name))
|
||
else
|
||
throwUnsupportedSyntax
|
||
|
||
private def getBinderIds (ids : Syntax) : TermElabM (Array Syntax) :=
|
||
ids.getArgs.mapM fun id =>
|
||
let k := id.getKind
|
||
if k == identKind || k == `Lean.Parser.Term.hole then
|
||
return id
|
||
else
|
||
throwErrorAt id "identifier or `_` expected"
|
||
|
||
/--
|
||
Convert `stx` into an array of `BinderView`s.
|
||
`stx` must be an identifier, `_`, `explicitBinder`, `implicitBinder`, `strictImplicitBinder`, or `instBinder`.
|
||
-/
|
||
private def toBinderViews (stx : Syntax) : TermElabM (Array BinderView) := do
|
||
let k := stx.getKind
|
||
if stx.isIdent || k == ``hole then
|
||
-- binderIdent
|
||
return #[{ ref := stx, id := (← expandBinderIdent stx), type := mkHole stx, bi := .default }]
|
||
else if k == ``Lean.Parser.Term.explicitBinder then
|
||
-- `(` binderIdent+ binderType (binderDefault <|> binderTactic)? `)`
|
||
let ids ← getBinderIds stx[1]
|
||
let type := stx[2]
|
||
let optModifier := stx[3]
|
||
ids.mapM fun id => do pure { ref := id, id := (← expandBinderIdent id), type := (← expandBinderModifier (expandBinderType id type) optModifier), bi := .default }
|
||
else if k == ``Lean.Parser.Term.implicitBinder then
|
||
-- `{` binderIdent+ binderType `}`
|
||
let ids ← getBinderIds stx[1]
|
||
let type := stx[2]
|
||
ids.mapM fun id => do pure { ref := id, id := (← expandBinderIdent id), type := expandBinderType id type, bi := .implicit }
|
||
else if k == ``Lean.Parser.Term.strictImplicitBinder then
|
||
-- `⦃` binderIdent+ binderType `⦄`
|
||
let ids ← getBinderIds stx[1]
|
||
let type := stx[2]
|
||
ids.mapM fun id => do pure { ref := id, id := (← expandBinderIdent id), type := expandBinderType id type, bi := .strictImplicit }
|
||
else if k == ``Lean.Parser.Term.instBinder then
|
||
-- `[` optIdent type `]`
|
||
let id ← expandOptIdent stx[1]
|
||
let type := stx[2]
|
||
return #[ { ref := id, id := id, type := type, bi := .instImplicit } ]
|
||
else
|
||
throwUnsupportedSyntax
|
||
|
||
private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : TermElabM Unit := do
|
||
registerCustomErrorIfMVar type ref "failed to infer binder type"
|
||
registerLevelMVarErrorExprInfo type ref m!"failed to infer universe levels in binder type"
|
||
|
||
def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit :=
|
||
addTermInfo' (isBinder := true) stx fvar
|
||
|
||
private def ensureAtomicBinderName (binderView : BinderView) : TermElabM Unit :=
|
||
let n := binderView.id.getId.eraseMacroScopes
|
||
unless n.isAtomic do
|
||
throwErrorAt binderView.id "invalid binder name '{n}', it must be atomic"
|
||
|
||
register_builtin_option checkBinderAnnotations : Bool := {
|
||
defValue := true
|
||
descr := "check whether type is a class instance whenever the binder annotation `[...]` is used"
|
||
}
|
||
|
||
/-- Throw an error if `type` is not a valid local instance. -/
|
||
private partial def checkLocalInstanceParameters (type : Expr) : TermElabM Unit := do
|
||
let .forallE n d b bi ← whnf type | return ()
|
||
-- We allow instance arguments so that local instances of the form
|
||
-- `variable [∀ (a : α) [P a], Q a]`
|
||
-- are accepted, per https://github.com/leanprover/lean4/issues/2311
|
||
if bi != .instImplicit && !b.hasLooseBVar 0 then
|
||
throwError "invalid parametric local instance, parameter with type{indentExpr d}\ndoes not have forward dependencies, type class resolution cannot use this kind of local instance because it will not be able to infer a value for this parameter."
|
||
withLocalDecl n bi d fun x => checkLocalInstanceParameters (b.instantiate1 x)
|
||
|
||
private partial def elabBinderViews (binderViews : Array BinderView) (fvars : Array (Syntax × Expr)) (k : Array (Syntax × Expr) → TermElabM α)
|
||
: TermElabM α :=
|
||
let rec loop (i : Nat) (fvars : Array (Syntax × Expr)) : TermElabM α := do
|
||
if h : i < binderViews.size then
|
||
let binderView := binderViews[i]
|
||
ensureAtomicBinderName binderView
|
||
let type ← elabType binderView.type
|
||
registerFailedToInferBinderTypeInfo type binderView.type
|
||
if binderView.bi.isInstImplicit && checkBinderAnnotations.get (← getOptions) then
|
||
unless (← isClass? type).isSome do
|
||
throwErrorAt binderView.type "invalid binder annotation, type is not a class instance{indentExpr type}\nuse the command `set_option checkBinderAnnotations false` to disable the check"
|
||
withRef binderView.type <| checkLocalInstanceParameters type
|
||
let id := binderView.id.getId
|
||
let kind := kindOfBinderName id
|
||
withLocalDecl id binderView.bi type (kind := kind) fun fvar => do
|
||
addLocalVarInfo binderView.ref fvar
|
||
loop (i+1) (fvars.push (binderView.id, fvar))
|
||
else
|
||
k fvars
|
||
loop 0 fvars
|
||
|
||
private partial def elabBindersAux (binders : Array Syntax) (k : Array (Syntax × Expr) → TermElabM α) : TermElabM α :=
|
||
let rec loop (i : Nat) (fvars : Array (Syntax × Expr)) : TermElabM α := do
|
||
if h : i < binders.size then
|
||
let binderViews ← toBinderViews binders[i]
|
||
elabBinderViews binderViews fvars <| loop (i+1)
|
||
else
|
||
k fvars
|
||
loop 0 #[]
|
||
|
||
/--
|
||
Like `elabBinders`, but also pass syntax node per binder.
|
||
`elabBinders(Ex)` automatically adds binder info nodes for the produced fvars, but storing the syntax nodes
|
||
might be necessary when later adding the same binders back to the local context so that info nodes can
|
||
manually be added for the new fvars; see `MutualDef` for an example. -/
|
||
def elabBindersEx (binders : Array Syntax) (k : Array (Syntax × Expr) → TermElabM α) : TermElabM α :=
|
||
universeConstraintsCheckpoint do
|
||
if binders.isEmpty then
|
||
k #[]
|
||
else
|
||
elabBindersAux binders k
|
||
|
||
/--
|
||
Elaborate the given binders (i.e., `Syntax` objects for `bracketedBinder`),
|
||
update the local context, set of local instances, reset instance cache (if needed), and then
|
||
execute `k` with the updated context.
|
||
The local context will only be included inside `k`.
|
||
|
||
For example, suppose you have binders `[(a : α), (b : β a)]`, then the elaborator will
|
||
create two new free variables `a` and `b`, push these to the context and pass to `k #[a,b]`.
|
||
-/
|
||
def elabBinders (binders : Array Syntax) (k : Array Expr → TermElabM α) : TermElabM α :=
|
||
elabBindersEx binders (fun fvars => k (fvars.map (·.2)))
|
||
|
||
/-- Same as `elabBinder` with a single binder.-/
|
||
def elabBinder (binder : Syntax) (x : Expr → TermElabM α) : TermElabM α :=
|
||
elabBinders #[binder] fun fvars => x fvars[0]!
|
||
|
||
/-- If `binder` is a `_` or an identifier, return a `bracketedBinder` using `type` otherwise throw an exception. -/
|
||
def expandSimpleBinderWithType (type : Term) (binder : Syntax) : MacroM Syntax :=
|
||
if binder.isOfKind ``hole || binder.isIdent then
|
||
`(bracketedBinderF| ($binder : $type))
|
||
else
|
||
Macro.throwErrorAt type "unexpected type ascription"
|
||
|
||
@[builtin_macro Lean.Parser.Term.forall] def expandForall : Macro
|
||
| `(forall $binders* : $ty, $term) => do
|
||
let binders ← binders.mapM (expandSimpleBinderWithType ty)
|
||
`(forall $binders*, $term)
|
||
| _ => Macro.throwUnsupported
|
||
|
||
@[builtin_term_elab «forall»] def elabForall : TermElab := fun stx _ =>
|
||
match stx with
|
||
| `(forall $binders*, $term) =>
|
||
elabBinders binders fun xs => do
|
||
let e ← elabType term
|
||
mkForallFVars xs e
|
||
| _ => throwUnsupportedSyntax
|
||
|
||
open Lean.Elab.Term.Quotation in
|
||
@[builtin_quot_precheck Lean.Parser.Term.arrow] def precheckArrow : Precheck
|
||
| `($dom:term -> $rng) => do
|
||
precheck dom
|
||
precheck rng
|
||
| _ => throwUnsupportedSyntax
|
||
|
||
@[builtin_term_elab arrow] def elabArrow : TermElab := fun stx _ =>
|
||
match stx with
|
||
| `($dom:term -> $rng) => do
|
||
-- elaborate independently from each other
|
||
let dom ← elabType dom
|
||
let rng ← elabType rng
|
||
return mkForall (← MonadQuotation.addMacroScope `a) BinderInfo.default dom rng
|
||
| _ => throwUnsupportedSyntax
|
||
|
||
/--
|
||
The dependent arrow. `(x : α) → β` is equivalent to `∀ x : α, β`, but we usually
|
||
reserve the latter for propositions. Also written as `Π x : α, β` (the "Pi-type")
|
||
in the literature. -/
|
||
@[builtin_term_elab depArrow] def elabDepArrow : TermElab := fun stx _ =>
|
||
-- bracketedBinder `->` term
|
||
let binder := stx[0]
|
||
let term := stx[2]
|
||
elabBinders #[binder] fun xs => do
|
||
mkForallFVars xs (← elabType term)
|
||
|
||
/--
|
||
Auxiliary functions for converting `id_1 ... id_n` application into `#[id_1, ..., id_m]`
|
||
It is used at `expandFunBinders`. -/
|
||
private partial def getFunBinderIds? (stx : Syntax) : OptionT MacroM (Array Syntax) :=
|
||
let convertElem (stx : Term) : OptionT MacroM Syntax :=
|
||
match stx with
|
||
| `(_) =>
|
||
/-
|
||
We used to use `mkFreshIdent` here,
|
||
but it prevented us from obtaining hover info for `_` because the
|
||
fresh identifier would have a synthetic position, and synthetic positions
|
||
are ignored by the LSP server.
|
||
See comment at `BinderView.ref` for additional details.
|
||
-/
|
||
return stx
|
||
| `($_:ident) => return stx
|
||
| _ => failure
|
||
match stx with
|
||
| `($f $args*) => do
|
||
let mut acc := #[].push (← convertElem f)
|
||
for arg in args do
|
||
acc := acc.push (← convertElem arg)
|
||
return acc
|
||
| _ =>
|
||
return #[].push (← convertElem stx)
|
||
|
||
/--
|
||
Auxiliary function for expanding `fun` notation binders. Recall that `fun` parser is defined as
|
||
```
|
||
def funBinder : Parser := implicitBinder <|> instBinder <|> termParser maxPrec
|
||
leading_parser unicodeSymbol "λ" "fun" >> many1 funBinder >> "=>" >> termParser
|
||
```
|
||
to allow notation such as `fun (a, b) => a + b`, where `(a, b)` should be treated as a pattern.
|
||
The result is a pair `(explicitBinders, newBody)`, where `explicitBinders` is syntax of the form
|
||
```
|
||
`(` ident `:` term `)`
|
||
```
|
||
which can be elaborated using `elabBinders`, and `newBody` is the updated `body` syntax.
|
||
We update the `body` syntax when expanding the pattern notation.
|
||
Example: `fun (a, b) => a + b` expands into `fun _a_1 => match _a_1 with | (a, b) => a + b`.
|
||
See local function `processAsPattern` at `expandFunBindersAux`.
|
||
|
||
The resulting `Bool` is true if a pattern was found. We use it "mark" a macro expansion. -/
|
||
partial def expandFunBinders (binders : Array Syntax) (body : Syntax) : MacroM (Array Syntax × Syntax × Bool) :=
|
||
let rec loop (body : Syntax) (i : Nat) (newBinders : Array Syntax) := do
|
||
if h : i < binders.size then
|
||
let binder := binders[i]
|
||
let processAsPattern : Unit → MacroM (Array Syntax × Syntax × Bool) := fun _ => do
|
||
let pattern := binder
|
||
let major ← mkFreshIdent binder
|
||
let (binders, newBody, _) ← loop body (i+1) (newBinders.push $ mkExplicitBinder major (mkHole binder))
|
||
let newBody ← `(match $major:ident with | $pattern => $newBody)
|
||
pure (binders, newBody, true)
|
||
match binder.getKind with
|
||
| ``Lean.Parser.Term.implicitBinder
|
||
| ``Lean.Parser.Term.strictImplicitBinder
|
||
| ``Lean.Parser.Term.instBinder
|
||
| ``Lean.Parser.Term.explicitBinder
|
||
| ``Lean.Parser.Term.hole | `ident => loop body (i+1) (newBinders.push binder)
|
||
| ``Lean.Parser.Term.paren =>
|
||
let term := binder[1]
|
||
match (← getFunBinderIds? term) with
|
||
| some idents =>
|
||
-- `fun (x ...) ...` ~> `fun (x : _) ...`
|
||
-- Interpret `(x ...)` as sequence of binders instead of pattern only if none of the idents
|
||
-- are defined in the global scope. Technically, it would be sufficient to only check the
|
||
-- first ident to be sure that the syntax cannot possibly be a valid pattern. However, for
|
||
-- consistency we apply the same check to all idents so that the possibility of shadowing
|
||
-- a global decl is identical for all of them.
|
||
if (← idents.allM fun ident => return List.isEmpty (← Macro.resolveGlobalName ident.getId)) then
|
||
loop body (i+1) (newBinders ++ idents.map (mkExplicitBinder · (mkHole binder)))
|
||
else
|
||
processAsPattern ()
|
||
| none => processAsPattern ()
|
||
| ``Lean.Parser.Term.typeAscription =>
|
||
let term := binder[1]
|
||
let type := binder[3].getOptional?.getD (mkHole binder)
|
||
match (← getFunBinderIds? term) with
|
||
| some idents => loop body (i+1) (newBinders ++ idents.map (fun ident => mkExplicitBinder ident type))
|
||
| none => processAsPattern ()
|
||
| _ => processAsPattern ()
|
||
else
|
||
pure (newBinders, body, false)
|
||
loop body 0 #[]
|
||
|
||
namespace FunBinders
|
||
|
||
structure State where
|
||
fvars : Array Expr := #[]
|
||
lctx : LocalContext
|
||
localInsts : LocalInstances
|
||
expectedType? : Option Expr := none
|
||
|
||
private def propagateExpectedType (fvar : Expr) (fvarType : Expr) (s : State) : TermElabM State := do
|
||
match s.expectedType? with
|
||
| none => pure s
|
||
| some expectedType =>
|
||
let expectedType ← whnfForall expectedType
|
||
match expectedType with
|
||
| .forallE _ d b _ =>
|
||
discard <| isDefEq fvarType d
|
||
let b := b.instantiate1 fvar
|
||
return { s with expectedType? := some b }
|
||
| _ =>
|
||
return { s with expectedType? := none }
|
||
|
||
private partial def elabFunBinderViews (binderViews : Array BinderView) (i : Nat) (s : State) : TermElabM State := do
|
||
if h : i < binderViews.size then
|
||
let binderView := binderViews[i]
|
||
ensureAtomicBinderName binderView
|
||
withRef binderView.type <| withLCtx s.lctx s.localInsts do
|
||
let type ← elabType binderView.type
|
||
registerFailedToInferBinderTypeInfo type binderView.type
|
||
let fvarId ← mkFreshFVarId
|
||
let fvar := mkFVar fvarId
|
||
let s := { s with fvars := s.fvars.push fvar }
|
||
let id := binderView.id.getId
|
||
let kind := kindOfBinderName id
|
||
/-
|
||
We do **not** want to support default and auto arguments in lambda abstractions.
|
||
Example: `fun (x : Nat := 10) => x+1`.
|
||
We do not believe this is an useful feature, and it would complicate the logic here.
|
||
-/
|
||
let lctx := s.lctx.mkLocalDecl fvarId id type binderView.bi kind
|
||
addTermInfo' (lctx? := some lctx) (isBinder := true) binderView.ref fvar
|
||
let s ← withRef binderView.id <| propagateExpectedType fvar type s
|
||
let s := { s with lctx }
|
||
match ← isClass? type, kind with
|
||
| some className, .default =>
|
||
let localInsts := s.localInsts.push { className, fvar := mkFVar fvarId }
|
||
elabFunBinderViews binderViews (i+1) { s with localInsts }
|
||
| _, _ => elabFunBinderViews binderViews (i+1) s
|
||
else
|
||
pure s
|
||
|
||
partial def elabFunBindersAux (binders : Array Syntax) (i : Nat) (s : State) : TermElabM State := do
|
||
if h : i < binders.size then
|
||
let binderViews ← toBinderViews binders[i]
|
||
let s ← elabFunBinderViews binderViews 0 s
|
||
elabFunBindersAux binders (i+1) s
|
||
else
|
||
pure s
|
||
|
||
end FunBinders
|
||
|
||
def elabFunBinders (binders : Array Syntax) (expectedType? : Option Expr) (x : Array Expr → Option Expr → TermElabM α) : TermElabM α :=
|
||
if binders.isEmpty then
|
||
x #[] expectedType?
|
||
else do
|
||
let lctx ← getLCtx
|
||
let localInsts ← getLocalInstances
|
||
let s ← FunBinders.elabFunBindersAux binders 0 { lctx, localInsts, expectedType? }
|
||
withLCtx s.lctx s.localInsts do
|
||
x s.fvars s.expectedType?
|
||
|
||
def expandWhereDecls (whereDecls : Syntax) (body : Syntax) : MacroM Syntax :=
|
||
match whereDecls with
|
||
| `(whereDecls|where $[$decls:letRecDecl];*) => `(let rec $decls:letRecDecl,*; $body)
|
||
| _ => Macro.throwUnsupported
|
||
|
||
def expandWhereDeclsOpt (whereDeclsOpt : Syntax) (body : Syntax) : MacroM Syntax :=
|
||
if whereDeclsOpt.isNone then
|
||
return body
|
||
else
|
||
expandWhereDecls whereDeclsOpt[0] body
|
||
|
||
/--
|
||
Helper function for `expandMatchAltsIntoMatch`.
|
||
-/
|
||
private def expandMatchAltsIntoMatchAux (matchAlts : Syntax) (isTactic : Bool) (useExplicit : Bool) : Nat → Array Syntax → Array Ident → MacroM Syntax
|
||
| 0, discrs, xs => do
|
||
if isTactic then
|
||
`(tactic|match $[$discrs:term],* with $matchAlts:matchAlts)
|
||
else
|
||
let stx ← `(match $[$discrs:term],* with $matchAlts:matchAlts)
|
||
clearInMatch stx xs
|
||
| n+1, discrs, xs => withFreshMacroScope do
|
||
let x ← `(x) -- If this were implementation-detail, the `contradiction` tactic used by match would not find it.
|
||
let d ← `(@$x:ident)
|
||
let body ← expandMatchAltsIntoMatchAux matchAlts isTactic useExplicit n (discrs.push d) (xs.push x)
|
||
if isTactic then
|
||
`(tactic| intro $x:term; $body:tactic)
|
||
else if useExplicit then
|
||
`(@fun $x => $body)
|
||
else
|
||
`(fun $x => $body)
|
||
|
||
/--
|
||
Expand `matchAlts` syntax into a full `match`-expression.
|
||
Example:
|
||
```
|
||
| 0, true => alt_1
|
||
| i, _ => alt_2
|
||
```
|
||
expands into (for tactic == false)
|
||
```
|
||
fun x_1 x_2 =>
|
||
match @x_1, @x_2 with
|
||
| 0, true => alt_1
|
||
| i, _ => alt_2
|
||
```
|
||
and (for tactic == true)
|
||
```
|
||
intro x_1; intro x_2;
|
||
match @x_1, @x_2 with
|
||
| 0, true => alt_1
|
||
| i, _ => alt_2
|
||
```
|
||
|
||
If `useExplicit = true`, we add a `@` before `fun` to disable implicit lambdas. We disable them when processing `let` and `let rec` declarations
|
||
to make sure the behavior is consistent with top-level declarations where we can write
|
||
```
|
||
def f : {α : Type} → α → α
|
||
| _, a => a
|
||
```
|
||
We use `useExplicit = false` when we are elaborating the `fun | ... => ... | ...` notation. See issue #1132.
|
||
If `@fun` is used with this notation, the we set `useExplicit = true`.
|
||
We also use `useExplicit = false` when processing `instance ... where` notation declarations. The motivation is to have compact declarations such as
|
||
```
|
||
instance [Alternative m] : MonadLiftT Option m where
|
||
monadLift -- We don't want to provide the implicit arguments of `monadLift` here. One should use `monadLift := @fun ...` if they want to provide them.
|
||
| some a => pure a
|
||
| none => failure
|
||
```
|
||
|
||
Remark: we add `@` at discriminants to make sure we don't consume implicit arguments, and to make the behavior consistent with `fun`.
|
||
Example:
|
||
```
|
||
inductive T : Type 1 :=
|
||
| mkT : (forall {a : Type}, a -> a) -> T
|
||
|
||
def makeT (f : forall {a : Type}, a -> a) : T :=
|
||
mkT f
|
||
|
||
def makeT' : (forall {a : Type}, a -> a) -> T
|
||
| f => mkT f
|
||
```
|
||
The two definitions should be elaborated without errors and be equivalent.
|
||
-/
|
||
def expandMatchAltsIntoMatch (ref : Syntax) (matchAlts : Syntax) (useExplicit := true) : MacroM Syntax :=
|
||
withRef ref <| expandMatchAltsIntoMatchAux matchAlts (isTactic := false) (useExplicit := useExplicit) (getMatchAltsNumPatterns matchAlts) #[] #[]
|
||
|
||
def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM Syntax :=
|
||
withRef ref <| expandMatchAltsIntoMatchAux matchAlts (isTactic := true) (useExplicit := false) (getMatchAltsNumPatterns matchAlts) #[] #[]
|
||
|
||
/--
|
||
Similar to `expandMatchAltsIntoMatch`, but supports an optional `where` clause.
|
||
|
||
Expand `matchAltsWhereDecls` into `let rec` + `match`-expression.
|
||
Example
|
||
```
|
||
| 0, true => ... f 0 ...
|
||
| i, _ => ... f i + g i ...
|
||
where
|
||
f x := g x + 1
|
||
|
||
g : Nat → Nat
|
||
| 0 => 1
|
||
| x+1 => f x
|
||
```
|
||
expands into
|
||
```
|
||
fux x_1 x_2 =>
|
||
let rec
|
||
f x := g x + 1,
|
||
g : Nat → Nat
|
||
| 0 => 1
|
||
| x+1 => f x
|
||
match x_1, x_2 with
|
||
| 0, true => ... f 0 ...
|
||
| i, _ => ... f i + g i ...
|
||
```
|
||
-/
|
||
def expandMatchAltsWhereDecls (matchAltsWhereDecls : Syntax) : MacroM Syntax :=
|
||
let matchAlts := matchAltsWhereDecls[0]
|
||
-- matchAltsWhereDecls[1] is the termination hints, collected elsewhere
|
||
let whereDeclsOpt := matchAltsWhereDecls[2]
|
||
let rec loop (i : Nat) (discrs : Array Syntax) : MacroM Syntax :=
|
||
match i with
|
||
| 0 => do
|
||
let matchStx ← `(match $[@$discrs:term],* with $matchAlts:matchAlts)
|
||
let matchStx ← clearInMatch matchStx discrs
|
||
if whereDeclsOpt.isNone then
|
||
return matchStx
|
||
else
|
||
expandWhereDeclsOpt whereDeclsOpt matchStx
|
||
| n+1 => withFreshMacroScope do
|
||
let body ← loop n (discrs.push (← `(x)))
|
||
`(@fun x => $body)
|
||
loop (getMatchAltsNumPatterns matchAlts) #[]
|
||
|
||
@[builtin_macro Parser.Term.fun] partial def expandFun : Macro
|
||
| `(fun $binders* : $ty => $body) => do
|
||
let binders ← binders.mapM (expandSimpleBinderWithType ty)
|
||
`(fun $binders* => $body)
|
||
| `(fun $binders* => $body) => do -- if there is a type ascription, we assume all binders are already simple
|
||
let (binders, body, expandedPattern) ← expandFunBinders binders body
|
||
if expandedPattern then
|
||
`(fun $binders* => $body)
|
||
else
|
||
Macro.throwUnsupported
|
||
| stx@`(fun $m:matchAlts) => expandMatchAltsIntoMatch stx m (useExplicit := false)
|
||
| _ => Macro.throwUnsupported
|
||
|
||
@[builtin_macro Parser.Term.explicit] partial def expandExplicitFun : Macro := fun stx =>
|
||
match stx with
|
||
| `(@fun $m:matchAlts) => expandMatchAltsIntoMatch stx[1] m (useExplicit := true)
|
||
| _ => Macro.throwUnsupported
|
||
|
||
open Lean.Elab.Term.Quotation in
|
||
@[builtin_quot_precheck Lean.Parser.Term.fun] def precheckFun : Precheck
|
||
| `(fun $binders* $[: $ty?]? => $body) => do
|
||
let (binders, body, _) ← liftMacroM <| expandFunBinders binders body
|
||
let mut ids := #[]
|
||
for b in binders do
|
||
for v in ← toBinderViews b do
|
||
Quotation.withNewLocals ids <| precheck v.type
|
||
ids := ids.push v.id.getId
|
||
Quotation.withNewLocals ids <| precheck body
|
||
| _ => throwUnsupportedSyntax
|
||
|
||
@[builtin_term_elab «fun»] partial def elabFun : TermElab := fun stx expectedType? =>
|
||
match stx with
|
||
| `(fun $binders* => $body) => do
|
||
-- We can assume all `match` binders have been iteratively expanded by the above macro here, though
|
||
-- we still need to call `expandFunBinders` once to obtain `binders` in a normal form
|
||
-- expected by `elabFunBinder`.
|
||
let (binders, body, _) ← liftMacroM <| expandFunBinders binders body
|
||
elabFunBinders binders expectedType? fun xs expectedType? => do
|
||
/- We ensure the expectedType here since it will force coercions to be applied if needed.
|
||
If we just use `elabTerm`, then we will need to a coercion `Coe (α → β) (α → δ)` whenever there is a coercion `Coe β δ`,
|
||
and another instance for the dependent version. -/
|
||
let e ← elabTermEnsuringType body expectedType?
|
||
mkLambdaFVars xs e
|
||
| _ => throwUnsupportedSyntax
|
||
|
||
/-- If `useLetExpr` is true, then a kernel let-expression `let x : type := val; body` is created.
|
||
Otherwise, we create a term of the form `letFun val (fun (x : type) => body)`
|
||
|
||
The default elaboration order is `binders`, `typeStx`, `valStx`, and `body`.
|
||
If `elabBodyFirst == true`, then we use the order `binders`, `typeStx`, `body`, and `valStx`. -/
|
||
def elabLetDeclAux (id : Syntax) (binders : Array Syntax) (typeStx : Syntax) (valStx : Syntax) (body : Syntax)
|
||
(expectedType? : Option Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) (usedLetOnly : Bool) : TermElabM Expr := do
|
||
let (type, val, binders) ← elabBindersEx binders fun xs => do
|
||
let (binders, fvars) := xs.unzip
|
||
/-
|
||
We use `withSynthesize` to ensure that any postponed elaboration problem
|
||
and nested tactics in `type` are resolved before elaborating `val`.
|
||
Resolved: we want to avoid synthetic opaque metavariables in `type`.
|
||
Recall that this kind of metavariable is non-assignable, and `isDefEq`
|
||
may waste a lot of time unfolding declarations before failing.
|
||
See issue #4051 for an example.
|
||
|
||
Here is the analysis for issue #4051.
|
||
- Given `have x : type := value; body`, we were previously elaborating `value` even
|
||
if `type` contained postponed elaboration problems.
|
||
- Moreover, the metavariables in `type` corresponding to postponed elaboration
|
||
problems cannot be assigned by `isDefEq` since the elaborator is supposed to assign them.
|
||
- Then, when checking whether type of `value` is definitionally equal to `type`,
|
||
a very long-time was spent unfolding a bunch of declarations before it failed.
|
||
In #4051, it was unfolding `Array.swaps` which is defined by well-founded recursion.
|
||
After the failure, the elaborator inserted a postponed coercion
|
||
that would be resolved later as soon as the types don't have unassigned metavariables.
|
||
|
||
We use `postpone := .partial` to allow type class (TC) resolution problems to be postponed
|
||
Recall that TC resolution does **not** produce synthetic opaque metavariables.
|
||
-/
|
||
let type ← withSynthesize (postpone := .partial) <| elabType typeStx
|
||
let letMsg := if useLetExpr then "let" else "have"
|
||
registerCustomErrorIfMVar type typeStx m!"failed to infer '{letMsg}' declaration type"
|
||
registerLevelMVarErrorExprInfo type typeStx m!"failed to infer universe levels in '{letMsg}' declaration type"
|
||
if elabBodyFirst then
|
||
let type ← mkForallFVars fvars type
|
||
let val ← mkFreshExprMVar type
|
||
pure (type, val, binders)
|
||
else
|
||
let val ← elabTermEnsuringType valStx type
|
||
let type ← mkForallFVars fvars type
|
||
/- By default `mkLambdaFVars` and `mkLetFVars` create binders only for let-declarations that are actually used
|
||
in the body. This generates counterintuitive behavior in the elaborator since users will not be notified
|
||
about holes such as
|
||
```
|
||
def ex : Nat :=
|
||
let x := _
|
||
42
|
||
```
|
||
-/
|
||
let val ← mkLambdaFVars fvars val (usedLetOnly := false)
|
||
pure (type, val, binders)
|
||
let kind := kindOfBinderName id.getId
|
||
trace[Elab.let.decl] "{id.getId} : {type} := {val}"
|
||
let result ← if useLetExpr then
|
||
withLetDecl id.getId (kind := kind) type val fun x => do
|
||
addLocalVarInfo id x
|
||
let body ← elabTermEnsuringType body expectedType?
|
||
let body ← instantiateMVars body
|
||
mkLetFVars #[x] body (usedLetOnly := usedLetOnly)
|
||
else
|
||
withLocalDecl id.getId (kind := kind) .default type fun x => do
|
||
addLocalVarInfo id x
|
||
let body ← elabTermEnsuringType body expectedType?
|
||
let body ← instantiateMVars body
|
||
mkLetFun x val body
|
||
if elabBodyFirst then
|
||
forallBoundedTelescope type binders.size fun xs type => do
|
||
-- the original `fvars` from above are gone, so add back info manually
|
||
for b in binders, x in xs do
|
||
addLocalVarInfo b x
|
||
let valResult ← elabTermEnsuringType valStx type
|
||
let valResult ← mkLambdaFVars xs valResult (usedLetOnly := false)
|
||
unless (← isDefEq val valResult) do
|
||
throwError "unexpected error when elaborating 'let'"
|
||
pure result
|
||
|
||
structure LetIdDeclView where
|
||
id : Syntax
|
||
binders : Array Syntax
|
||
type : Syntax
|
||
value : Syntax
|
||
|
||
def mkLetIdDeclView (letIdDecl : Syntax) : LetIdDeclView :=
|
||
-- `letIdDecl` is of the form `binderIdent >> many bracketedBinder >> optType >> " := " >> termParser
|
||
let id := letIdDecl[0]
|
||
let binders := letIdDecl[1].getArgs
|
||
let optType := letIdDecl[2]
|
||
let type := expandOptType id optType
|
||
let value := letIdDecl[4]
|
||
{ id, binders, type, value }
|
||
|
||
def expandLetEqnsDecl (letDecl : Syntax) (useExplicit := true) : MacroM Syntax := do
|
||
let ref := letDecl
|
||
let matchAlts := letDecl[3]
|
||
let val ← expandMatchAltsIntoMatch ref matchAlts (useExplicit := useExplicit)
|
||
return mkNode `Lean.Parser.Term.letIdDecl #[letDecl[0], letDecl[1], letDecl[2], mkAtomFrom ref " := ", val]
|
||
|
||
def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : Bool) (elabBodyFirst : Bool) (usedLetOnly : Bool) : TermElabM Expr := do
|
||
let letDecl := stx[1][0]
|
||
let body := stx[3]
|
||
if letDecl.getKind == ``Lean.Parser.Term.letIdDecl then
|
||
let { id, binders, type, value } := mkLetIdDeclView letDecl
|
||
let id ← if id.isIdent then pure id else mkFreshIdent id (canonical := true)
|
||
elabLetDeclAux id binders type value body expectedType? useLetExpr elabBodyFirst usedLetOnly
|
||
else if letDecl.getKind == ``Lean.Parser.Term.letPatDecl then
|
||
-- node `Lean.Parser.Term.letPatDecl $ try (termParser >> pushNone >> optType >> " := ") >> termParser
|
||
if elabBodyFirst then
|
||
throwError "'let_delayed' with patterns is not allowed"
|
||
let pat := letDecl[0]
|
||
let optType := letDecl[2]
|
||
let val := letDecl[4]
|
||
if pat.getKind == ``Parser.Term.hole then
|
||
-- `let _ := ...` should not be treated as a `letIdDecl`
|
||
let id ← mkFreshIdent pat (canonical := true)
|
||
let type := expandOptType id optType
|
||
elabLetDeclAux id #[] type val body expectedType? useLetExpr elabBodyFirst usedLetOnly
|
||
else
|
||
-- We are currently treating `let_fun` and `let` the same way when patterns are used.
|
||
let stxNew ← if optType.isNone then
|
||
`(match $val:term with | $pat => $body)
|
||
else
|
||
let type := optType[0][1]
|
||
`(match ($val:term : $type) with | $pat => $body)
|
||
withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
|
||
else if letDecl.getKind == ``Lean.Parser.Term.letEqnsDecl then
|
||
let letDeclIdNew ← liftMacroM <| expandLetEqnsDecl letDecl
|
||
let declNew := stx[1].setArg 0 letDeclIdNew
|
||
let stxNew := stx.setArg 1 declNew
|
||
withMacroExpansion stx stxNew <| elabTerm stxNew expectedType?
|
||
else
|
||
throwUnsupportedSyntax
|
||
|
||
@[builtin_term_elab «let»] def elabLetDecl : TermElab :=
|
||
fun stx expectedType? => elabLetDeclCore stx expectedType? (useLetExpr := true) (elabBodyFirst := false) (usedLetOnly := false)
|
||
|
||
@[builtin_term_elab «let_fun»] def elabLetFunDecl : TermElab :=
|
||
fun stx expectedType? => elabLetDeclCore stx expectedType? (useLetExpr := false) (elabBodyFirst := false) (usedLetOnly := false)
|
||
|
||
@[builtin_term_elab «let_delayed»] def elabLetDelayedDecl : TermElab :=
|
||
fun stx expectedType? => elabLetDeclCore stx expectedType? (useLetExpr := true) (elabBodyFirst := true) (usedLetOnly := false)
|
||
|
||
@[builtin_term_elab «let_tmp»] def elabLetTmpDecl : TermElab :=
|
||
fun stx expectedType? => elabLetDeclCore stx expectedType? (useLetExpr := true) (elabBodyFirst := false) (usedLetOnly := true)
|
||
|
||
builtin_initialize
|
||
registerTraceClass `Elab.let
|
||
registerTraceClass `Elab.let.decl
|
||
registerTraceClass `Elab.autoParam
|
||
|
||
end Lean.Elab.Term
|