From 59acf01bc942a7bb0ccc986ae0ef7811d8e49110 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 8 Feb 2022 12:12:52 -0800 Subject: [PATCH] feat: relax auto-implicit restrictions The new options `relaxedAutoBoundImplicitLocal` can be used to disable this feature. closes #1011 --- RELEASES.md | 2 ++ src/Lean/Elab/AutoBound.lean | 16 +++++++++++----- src/Lean/Elab/Level.lean | 2 +- src/Lean/Elab/Term.lean | 2 +- tests/lean/1011.lean | 5 +++++ tests/lean/1011.lean.expected.out | 1 + tests/lean/autoBoundImplicits1.lean | 2 +- tests/lean/autoBoundImplicits2.lean | 2 +- tests/lean/interactive/533.lean | 1 + tests/lean/interactive/533.lean.expected.out | 2 +- tests/lean/interactive/hoverException.lean | 1 + .../interactive/hoverException.lean.expected.out | 2 +- tests/lean/structSorryBug.lean | 1 + tests/lean/structSorryBug.lean.expected.out | 4 ++-- 14 files changed, 30 insertions(+), 13 deletions(-) create mode 100644 tests/lean/1011.lean create mode 100644 tests/lean/1011.lean.expected.out diff --git a/RELEASES.md b/RELEASES.md index 32c2ed4915..6dc5a6cc4c 100644 --- a/RELEASES.md +++ b/RELEASES.md @@ -21,3 +21,5 @@ theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)] * Various improvements to go-to-definition & find-all-references accuracy. * Auto generated congruence lemmas with support for casts on proofs and `Decidable` instances (see [whishlist](https://github.com/leanprover/lean4/issues/988)). + +* [Relax auto-implicit restrictions](https://github.com/leanprover/lean4/pull/1011). The command `set_option relaxedAutoBoundImplicitLocal false` disables the relaxations. diff --git a/src/Lean/Elab/AutoBound.lean b/src/Lean/Elab/AutoBound.lean index 7331ded00a..6ca3c93434 100644 --- a/src/Lean/Elab/AutoBound.lean +++ b/src/Lean/Elab/AutoBound.lean @@ -11,9 +11,15 @@ namespace Lean.Elab register_builtin_option autoBoundImplicitLocal : Bool := { defValue := true - descr := "Unbound local variables in declaration headers become implicit arguments if they are a lower case or greek letter followed by numeric digits. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}." + descr := "Unbound local variables in declaration headers become implicit arguments. In \"relaxed\" mode (default), any atomic identifier is eligible, otherwise only a lower case or greek letter followed by numeric digits are eligible. For example, `def f (x : Vector α n) : Vector α n :=` automatically introduces the implicit variables {α n}." } +register_builtin_option relaxedAutoBoundImplicitLocal : Bool := { + defValue := true + descr := "When \"relaxed\" mode is enabled, any atomic nonempty identifier is eligible for auto bound implicit locals (see optin `autoBoundImplicitLocal`." + } + + private def isValidAutoBoundSuffix (s : String) : Bool := s.toSubstring.drop 1 |>.all fun c => c.isDigit || isSubScriptAlnum c || c == '_' || c == '\'' @@ -31,14 +37,14 @@ When, we try again, a `x` with a new macro scope is created and this process kee Therefore, we do consider identifier with macro scopes anymore. -/ -def isValidAutoBoundImplicitName (n : Name) : Bool := +def isValidAutoBoundImplicitName (n : Name) (relaxed : Bool) : Bool := match n with - | Name.str Name.anonymous s _ => s.length > 0 && (isGreek s[0] || s[0].isLower) && isValidAutoBoundSuffix s + | Name.str Name.anonymous s _ => s.length > 0 && (relaxed || ((isGreek s[0] || s[0].isLower) && isValidAutoBoundSuffix s)) | _ => false -def isValidAutoBoundLevelName (n : Name) : Bool := +def isValidAutoBoundLevelName (n : Name) (relaxed : Bool) : Bool := match n with - | Name.str Name.anonymous s _ => s.length > 0 && s[0].isLower && isValidAutoBoundSuffix s + | Name.str Name.anonymous s _ => s.length > 0 && (relaxed || (s[0].isLower && isValidAutoBoundSuffix s)) | _ => false end Lean.Elab diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean index 406e7be8d0..cbeb9dd9cf 100644 --- a/src/Lean/Elab/Level.lean +++ b/src/Lean/Elab/Level.lean @@ -72,7 +72,7 @@ partial def elabLevel (stx : Syntax) : LevelElabM Level := withRef stx do else if kind == identKind then let paramName := stx.getId unless (← get).levelNames.contains paramName do - if (← read).autoBoundImplicit && isValidAutoBoundLevelName paramName then + if (← read).autoBoundImplicit && isValidAutoBoundLevelName paramName (relaxedAutoBoundImplicitLocal.get (← read).options) then modify fun s => { s with levelNames := paramName :: s.levelNames } else throwError "unknown universe level '{paramName}'" diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index aa1ab4af62..8c2b4b98fc 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -1418,7 +1418,7 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List Stri throw ex where process (candidates : List (Name × List String)) : TermElabM (List (Expr × List String)) := do if candidates.isEmpty then - if (← read).autoBoundImplicit && isValidAutoBoundImplicitName n then + if (← read).autoBoundImplicit && isValidAutoBoundImplicitName n (relaxedAutoBoundImplicitLocal.get (← getOptions)) then throwAutoBoundImplicitLocal n else throwError "unknown identifier '{Lean.mkConst n}'" diff --git a/tests/lean/1011.lean b/tests/lean/1011.lean new file mode 100644 index 0000000000..2bcd79eceb --- /dev/null +++ b/tests/lean/1011.lean @@ -0,0 +1,5 @@ +def f (x : A) := x + +set_option relaxedAutoBoundImplicitLocal false + +def g (x : A) := x diff --git a/tests/lean/1011.lean.expected.out b/tests/lean/1011.lean.expected.out new file mode 100644 index 0000000000..281d4457e3 --- /dev/null +++ b/tests/lean/1011.lean.expected.out @@ -0,0 +1 @@ +1011.lean:5:11-5:12: error: unknown identifier 'A' diff --git a/tests/lean/autoBoundImplicits1.lean b/tests/lean/autoBoundImplicits1.lean index c512865a59..18f22fdd07 100644 --- a/tests/lean/autoBoundImplicits1.lean +++ b/tests/lean/autoBoundImplicits1.lean @@ -1,5 +1,5 @@ def myid (a : α) := a -- works - +set_option relaxedAutoBoundImplicitLocal false #check myid 10 #check myid true diff --git a/tests/lean/autoBoundImplicits2.lean b/tests/lean/autoBoundImplicits2.lean index 1e5c63b236..50fbab44b1 100644 --- a/tests/lean/autoBoundImplicits2.lean +++ b/tests/lean/autoBoundImplicits2.lean @@ -1,6 +1,6 @@ def f [Add α] (a : α) : α := a + a - +set_option relaxedAutoBoundImplicitLocal false def BV (n : Nat) := { a : Array Bool // a.size = n } def allZero (bv : BV n) : Prop := diff --git a/tests/lean/interactive/533.lean b/tests/lean/interactive/533.lean index e96fe253f3..b247d296ea 100644 --- a/tests/lean/interactive/533.lean +++ b/tests/lean/interactive/533.lean @@ -1,3 +1,4 @@ +set_option relaxedAutoBoundImplicitLocal false inductive Foo where | bar : F --^ textDocument/completion diff --git a/tests/lean/interactive/533.lean.expected.out b/tests/lean/interactive/533.lean.expected.out index 2940ccf971..277babe388 100644 --- a/tests/lean/interactive/533.lean.expected.out +++ b/tests/lean/interactive/533.lean.expected.out @@ -1,5 +1,5 @@ {"textDocument": {"uri": "file://533.lean"}, - "position": {"line": 1, "character": 10}} + "position": {"line": 2, "character": 10}} {"items": [{"label": "False", "kind": 22, "detail": "Prop"}, {"label": "Fin", "kind": 22, "detail": "Nat → Type"}, diff --git a/tests/lean/interactive/hoverException.lean b/tests/lean/interactive/hoverException.lean index 6e56570b65..bf24cf1079 100644 --- a/tests/lean/interactive/hoverException.lean +++ b/tests/lean/interactive/hoverException.lean @@ -1,3 +1,4 @@ +set_option relaxedAutoBoundImplicitLocal false inductive Foo | mk : (a b : Bar) → Foo --^ textDocument/hover diff --git a/tests/lean/interactive/hoverException.lean.expected.out b/tests/lean/interactive/hoverException.lean.expected.out index 311e2c9b53..f692d42901 100644 --- a/tests/lean/interactive/hoverException.lean.expected.out +++ b/tests/lean/interactive/hoverException.lean.expected.out @@ -1,3 +1,3 @@ {"textDocument": {"uri": "file://hoverException.lean"}, - "position": {"line": 1, "character": 14}} + "position": {"line": 2, "character": 14}} null diff --git a/tests/lean/structSorryBug.lean b/tests/lean/structSorryBug.lean index a1113dbcae..fea977b680 100644 --- a/tests/lean/structSorryBug.lean +++ b/tests/lean/structSorryBug.lean @@ -1,3 +1,4 @@ +set_option relaxedAutoBoundImplicitLocal false instance has_arr : HasArr Preorder := { Arr := Function } def foo : Nat := { first := 10 } diff --git a/tests/lean/structSorryBug.lean.expected.out b/tests/lean/structSorryBug.lean.expected.out index efdd6c80b2..59a08396a9 100644 --- a/tests/lean/structSorryBug.lean.expected.out +++ b/tests/lean/structSorryBug.lean.expected.out @@ -1,3 +1,3 @@ -structSorryBug.lean:1:19-1:25: error: unknown identifier 'HasArr' -structSorryBug.lean:3:17-3:32: error: invalid {...} notation, structure type expected +structSorryBug.lean:2:19-2:25: error: unknown identifier 'HasArr' +structSorryBug.lean:4:17-4:32: error: invalid {...} notation, structure type expected Nat