From 0b92195ec8c677c595fb899f836347f531864abc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 21 Apr 2022 10:17:15 -0700 Subject: [PATCH] feat: refine auto bound implicit feature --- RELEASES.md | 15 +++ src/Lean/Elab/Inductive.lean | 49 +++++----- src/Lean/Elab/MutualDef.lean | 93 ++++++++++--------- src/Lean/Elab/Structure.lean | 60 ++++++------ src/Lean/Elab/Term.lean | 25 ++++- tests/lean/autoImplicitForbidden.lean | 23 +++++ .../autoImplicitForbidden.lean.expected.out | 5 + 7 files changed, 168 insertions(+), 102 deletions(-) create mode 100644 tests/lean/autoImplicitForbidden.lean create mode 100644 tests/lean/autoImplicitForbidden.lean.expected.out diff --git a/RELEASES.md b/RELEASES.md index e16c91296a..34d2a0a6a1 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -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 diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index c38d94f541..7e09820c68 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -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 diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index daa8b993e0..91915e1952 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -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 diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index b528e47018..888abf061f 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -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 diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 9558543207..e7fad86bfe 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -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}'" diff --git a/tests/lean/autoImplicitForbidden.lean b/tests/lean/autoImplicitForbidden.lean new file mode 100644 index 0000000000..54b54dca31 --- /dev/null +++ b/tests/lean/autoImplicitForbidden.lean @@ -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 diff --git a/tests/lean/autoImplicitForbidden.lean.expected.out b/tests/lean/autoImplicitForbidden.lean.expected.out new file mode 100644 index 0000000000..33c9afc685 --- /dev/null +++ b/tests/lean/autoImplicitForbidden.lean.expected.out @@ -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'