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

feat: refine auto bound implicit feature

Browse source
This commit is contained in:
Leonardo de Moura 2022-04-21 10:17:15 -07:00
parent d81c124479
commit 0b92195ec8
7 changed files with 168 additions and 102 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
RELEASES.md
View file

@ -1,6 +1,21 @@
Unreleased
---------
* Refine auto bound implicit feature. It does not consider anymore unbound variables that have the same
name of a declaration being defined. Example:
```lean
def f : f → Bool := -- Error at second `f`
fun _ => true
inductive Foo : List Foo → Type -- Error at second `Foo`
| x : Foo []
```
Before this refinement, the declarations above would be accepted and the
second `f` and `Foo` would be treated as auto implicit variables. That is,
`f : {f : Sort u} → f → Bool`, and
`Foo : {Foo : Type u} → List Foo → Type`.
* Fix syntax hightlighting for recursive declarations. Example
```lean
inductive List (α : Type u) where

49
src/Lean/Elab/Inductive.lean
View file

@ -67,31 +67,32 @@ structure ElabHeaderResult where
type : Expr
deriving Inhabited
private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : Array ElabHeaderResult) : TermElabM (Array ElabHeaderResult) := do
if h : i < views.size then
let view := views.get ⟨i, h⟩
let acc ← Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
match view.type? with
| none =>
let u ← mkFreshLevelMVar
let type := mkSort u
Term.synthesizeSyntheticMVarsNoPostponing
Term.addAutoBoundImplicits' params type fun params type => do
pure <| acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
| some typeStx =>
let (type, numImplicitIndices) ← Term.withAutoBoundImplicit do
let type ← Term.elabType typeStx
unless (← isTypeFormerType type) do
throwErrorAt typeStx "invalid inductive type, resultant type is not a sort"
private partial def elabHeaderAux (views : Array InductiveView) (i : Nat) (acc : Array ElabHeaderResult) : TermElabM (Array ElabHeaderResult) :=
Term.withAutoBoundImplicitForbiddenPred (fun n => views.any (·.shortDeclName == n)) do
if h : i < views.size then
let view := views.get ⟨i, h⟩
let acc ← Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
match view.type? with
| none =>
let u ← mkFreshLevelMVar
let type := mkSort u
Term.synthesizeSyntheticMVarsNoPostponing
let indices ← Term.addAutoBoundImplicits #[]
return (← mkForallFVars indices type, indices.size)
Term.addAutoBoundImplicits' params type fun params type => do
trace[Elab.inductive] "header params: {params}, type: {type}"
pure <| acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
elabHeaderAux views (i+1) acc
else
pure acc
Term.addAutoBoundImplicits' params type fun params type => do
pure <| acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
| some typeStx =>
let (type, numImplicitIndices) ← Term.withAutoBoundImplicit do
let type ← Term.elabType typeStx
unless (← isTypeFormerType type) do
throwErrorAt typeStx "invalid inductive type, resultant type is not a sort"
Term.synthesizeSyntheticMVarsNoPostponing
let indices ← Term.addAutoBoundImplicits #[]
return (← mkForallFVars indices type, indices.size)
Term.addAutoBoundImplicits' params type fun params type => do
trace[Elab.inductive] "header params: {params}, type: {type}"
pure <| acc.push { lctx := (← getLCtx), localInsts := (← getLocalInstances), params, type, view }
elabHeaderAux views (i+1) acc
else
pure acc
private def checkNumParams (rs : Array ElabHeaderResult) : TermElabM Nat := do
let numParams := rs[0].params.size

93
src/Lean/Elab/MutualDef.lean
View file

@ -99,51 +99,54 @@ private def getPendindMVarErrorMessage (views : Array DefView) : String :=
"\nwhen the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed"
private def elabHeaders (views : Array DefView) : TermElabM (Array DefViewElabHeader) := do
let mut headers := #[]
for view in views do
let newHeader ← withRef view.ref do
let ⟨shortDeclName, declName, levelNames⟩ ← Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
addDeclarationRanges declName view.ref
applyAttributesAt declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration
withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
elabBindersEx view.binders.getArgs fun xs => do
let refForElabFunType := view.value
let type ← match view.type? with
| some typeStx =>
let type ← elabType typeStx
registerFailedToInferDefTypeInfo type typeStx
pure type
| none =>
let hole := mkHole refForElabFunType
let type ← elabType hole
trace[Elab.definition] ">> type: {type}\n{type.mvarId!}"
registerFailedToInferDefTypeInfo type refForElabFunType
pure type
Term.synthesizeSyntheticMVarsNoPostponing
let (binderIds, xs) := xs.unzip
let xs ← addAutoBoundImplicits xs
let type ← mkForallFVars' xs type
let type ← instantiateMVars type
let levelNames ← getLevelNames
if view.type?.isSome then
let pendingMVarIds ← getMVars type
discard <| logUnassignedUsingErrorInfos pendingMVarIds <|
getPendindMVarErrorMessage views
let newHeader := {
ref := view.ref,
modifiers := view.modifiers,
kind := view.kind,
shortDeclName := shortDeclName,
declName := declName,
levelNames := levelNames,
binderIds := binderIds,
numParams := xs.size,
type := type,
valueStx := view.value : DefViewElabHeader }
check headers newHeader
return newHeader
headers := headers.push newHeader
pure headers
let expandedDeclIds ← views.mapM fun view => withRef view.ref do
Term.expandDeclId (← getCurrNamespace) (← getLevelNames) view.declId view.modifiers
withAutoBoundImplicitForbiddenPred (fun n => expandedDeclIds.any (·.shortName == n)) do
let mut headers := #[]
for view in views, ⟨shortDeclName, declName, levelNames⟩ in expandedDeclIds do
let newHeader ← withRef view.ref do
addDeclarationRanges declName view.ref
applyAttributesAt declName view.modifiers.attrs AttributeApplicationTime.beforeElaboration
withDeclName declName <| withAutoBoundImplicit <| withLevelNames levelNames <|
elabBindersEx view.binders.getArgs fun xs => do
let refForElabFunType := view.value
let type ← match view.type? with
| some typeStx =>
let type ← elabType typeStx
registerFailedToInferDefTypeInfo type typeStx
pure type
| none =>
let hole := mkHole refForElabFunType
let type ← elabType hole
trace[Elab.definition] ">> type: {type}\n{type.mvarId!}"
registerFailedToInferDefTypeInfo type refForElabFunType
pure type
Term.synthesizeSyntheticMVarsNoPostponing
let (binderIds, xs) := xs.unzip
-- TODO: add forbidden predicate using `shortDeclName` from `views`
let xs ← addAutoBoundImplicits xs
let type ← mkForallFVars' xs type
let type ← instantiateMVars type
let levelNames ← getLevelNames
if view.type?.isSome then
let pendingMVarIds ← getMVars type
discard <| logUnassignedUsingErrorInfos pendingMVarIds <|
getPendindMVarErrorMessage views
let newHeader := {
ref := view.ref,
modifiers := view.modifiers,
kind := view.kind,
shortDeclName := shortDeclName,
declName := declName,
levelNames := levelNames,
binderIds := binderIds,
numParams := xs.size,
type := type,
valueStx := view.value : DefViewElabHeader }
check headers newHeader
return newHeader
headers := headers.push newHeader
return headers
private partial def withFunLocalDecls {α} (headers : Array DefViewElabHeader) (k : Array Expr → TermElabM α) : TermElabM α :=
let rec loop (i : Nat) (fvars : Array Expr) := do

60
src/Lean/Elab/Structure.lean
View file

@ -485,14 +485,15 @@ where
else
k infos copiedParents
private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr × Option Expr) := do
Term.withAutoBoundImplicit <| Term.elabBinders view.binders.getArgs fun params => do
private def elabFieldTypeValue (view : StructFieldView) : TermElabM (Option Expr × Option Expr) :=
Term.withAutoBoundImplicit <| Term.withAutoBoundImplicitForbiddenPred (fun n => view.name == n) <| Term.elabBinders view.binders.getArgs fun params => do
match view.type? with
| none =>
match view.value? with
| none => return (none, none)
| some valStx =>
Term.synthesizeSyntheticMVarsNoPostponing
-- TODO: add forbidden predicate using `shortDeclName` from `view`
let params ← Term.addAutoBoundImplicits params
let value ← Term.elabTerm valStx none
let value ← mkLambdaFVars params value
@ -867,33 +868,34 @@ def elabStructure (modifiers : Modifiers) (stx : Syntax) : CommandElabM Unit :=
runTermElabM none fun scopeVars => do
let scopeLevelNames ← Term.getLevelNames
let ⟨name, declName, allUserLevelNames⟩ ← Elab.expandDeclId (← getCurrNamespace) scopeLevelNames declId modifiers
addDeclarationRanges declName stx
Term.withDeclName declName do
let ctor ← expandCtor stx modifiers declName
let fields ← expandFields stx modifiers declName
Term.withLevelNames allUserLevelNames <| Term.withAutoBoundImplicit <|
Term.elabBinders params fun params => do
Term.synthesizeSyntheticMVarsNoPostponing
let params ← Term.addAutoBoundImplicits params
let allUserLevelNames ← Term.getLevelNames
elabStructureView {
ref := stx
modifiers
scopeLevelNames
allUserLevelNames
declName
isClass
scopeVars
params
parents
type
ctor
fields
}
unless isClass do
mkSizeOfInstances declName
mkInjectiveTheorems declName
return declName
Term.withAutoBoundImplicitForbiddenPred (fun n => name == n) do
addDeclarationRanges declName stx
Term.withDeclName declName do
let ctor ← expandCtor stx modifiers declName
let fields ← expandFields stx modifiers declName
Term.withLevelNames allUserLevelNames <| Term.withAutoBoundImplicit <|
Term.elabBinders params fun params => do
Term.synthesizeSyntheticMVarsNoPostponing
let params ← Term.addAutoBoundImplicits params
let allUserLevelNames ← Term.getLevelNames
elabStructureView {
ref := stx
modifiers
scopeLevelNames
allUserLevelNames
declName
isClass
scopeVars
params
parents
type
ctor
fields
}
unless isClass do
mkSizeOfInstances declName
mkInjectiveTheorems declName
return declName
derivingClassViews.forM fun view => view.applyHandlers #[declName]
builtin_initialize registerTraceClass `Elab.structure

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

@ -138,11 +138,13 @@ structure Context where
fileMap : FileMap
declName? : Option Name := none
macroStack : MacroStack := []
/- When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`.
/--
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
/--
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
@ -150,13 +152,23 @@ structure Context where
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
/--
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 : Std.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 -/
@ -1374,6 +1386,9 @@ partial def withAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
def withoutAutoBoundImplicit (k : TermElabM α) : TermElabM α := do
withReader (fun ctx => { ctx with autoBoundImplicit := false, autoBoundImplicits := {} }) k
partial def withAutoBoundImplicitForbiddenPred (p : Name → Bool) (x : TermElabM α) : TermElabM α := do
withReader (fun ctx => { ctx with autoBoundImplicitForbidden := fun n => p n || ctx.autoBoundImplicitForbidden n }) x
/--
Collect unassigned metavariables in `type` that are not already in `init` and not satisfying `except`.
-/
@ -1525,7 +1540,9 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List Stri
process preresolved
where process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do
if candidates.isEmpty then
if (← read).autoBoundImplicit && isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) then
if (← read).autoBoundImplicit &&
!(← read).autoBoundImplicitForbidden n &&
isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) then
throwAutoBoundImplicitLocal n
else
throwError "unknown identifier '{Lean.mkConst n}'"

23
tests/lean/autoImplicitForbidden.lean Normal file
View file

@ -0,0 +1,23 @@
def f : f → Bool := -- Error at second `f`
fun _ => true
mutual
def g : h → Bool := -- Error at `h`, `h` is not eligible to be an auto implicit because of the mutual block
fun _ => true
def h := List Nat
end
structure Bla (x : List Bla) where -- Error at second `Foo`
val : Nat
inductive Foo : List Foo -> Type -- Error at second `Foo`
| x : Foo []
mutual
inductive Ex1 : Ex2 → Type -- Error at `Ex2`
inductive Ex2 : Type
end

5
tests/lean/autoImplicitForbidden.lean.expected.out Normal file
View file

@ -0,0 +1,5 @@
autoImplicitForbidden.lean:1:8-1:9: error: unknown identifier 'f'
autoImplicitForbidden.lean:6:10-6:11: error: unknown identifier 'h'
autoImplicitForbidden.lean:13:24-13:27: error: unknown identifier 'Bla'
autoImplicitForbidden.lean:16:21-16:24: error: unknown identifier 'Foo'
autoImplicitForbidden.lean:20:18-20:21: error: unknown identifier 'Ex2'