refactor: typed Lean.Option & register_builtin_option macro

src/Lean/Data/KVMap.lean

@@ -144,46 +144,46 @@ instance : BEq KVMap where
   beq := eqv
 
 class Value (α : Type) where
-  defVal : α
-  set    : KVMap → Name → α → KVMap
-  get    : KVMap → Name → α → α
+  toDataValue  : α → DataValue
+  ofDataValue? : DataValue → Option α
 
-export Value (set)
+@[inline] def get? {α : Type} [s : Value α] (m : KVMap) (k : Name) : Option α :=
+  m.find k |>.bind Value.ofDataValue?
 
-@[inline] def get {α : Type} [s : Value α] (m : KVMap) (k : Name) (defVal := s.defVal) : α :=
-  Value.get m k defVal
+@[inline] def get {α : Type} [s : Value α] (m : KVMap) (k : Name) (defVal : α) : α :=
+  m.get? k |>.getD defVal
 
 @[inline] def set {α : Type} [s : Value α] (m : KVMap) (k : Name) (v : α) : KVMap :=
-  Value.set m k v
+  m.insert k (Value.toDataValue v)
 
-instance : Value Bool := {
-  defVal := false,
-  set := setBool,
-  get := fun k n v => getBool k n v
-}
+instance : Value Bool where
+  toDataValue  := DataValue.ofBool
+  ofDataValue?
+    | DataValue.ofBool b => some b
+    | _                  => none
 
-instance : Value Nat := {
-  defVal := 0,
-  set := setNat,
-  get := fun k n v => getNat k n v
-}
+instance : Value Nat where
+  toDataValue  := DataValue.ofNat
+  ofDataValue?
+    | DataValue.ofNat n => some n
+    | _                 => none
 
-instance : Value Int := {
-  defVal := 0,
-  set := setInt,
-  get := fun k n v => getInt k n v
-}
+instance : Value Int where
+  toDataValue  := DataValue.ofInt
+  ofDataValue?
+    | DataValue.ofInt i => some i
+    | _                 => none
 
-instance : Value Name := {
-  defVal := Name.anonymous,
-  set := setName,
-  get := fun k n v => getName k n v
-}
+instance : Value Name where
+  toDataValue  := DataValue.ofName
+  ofDataValue?
+    | DataValue.ofName n => some n
+    | _                  => none
 
-instance : Value String := {
-  defVal := "",
-  set := setString,
-  get := fun k n v => getString k n v
-}
+instance : Value String where
+  toDataValue  := DataValue.ofString
+  ofDataValue?
+    | DataValue.ofString n => some n
+    | _                    => none
 
 end Lean.KVMap

src/Lean/Data/Options.lean

@@ -115,4 +115,35 @@ def getNatOption (k : Name) (defValue := 0) : m Nat := do
   let opts ← getOptions
   pure $ opts.getNat k defValue
 
+
+/-- A strongly-typed reference to an option. -/
+protected structure Option (α : Type) where
+  name     : Name
+  defValue : α
+  deriving Inhabited
+
+namespace Option
+
+protected structure Decl (α : Type) where
+  defValue : α
+  group    : String := ""
+  descr    : String := ""
+
+protected def get [KVMap.Value α] (opts : Options) (opt : Lean.Option α) : α :=
+  opts.get opt.name opt.defValue
+
+protected def set [KVMap.Value α] (opts : Options) (opt : Lean.Option α) (val: α) : Options :=
+  opts.set opt.name val
+
+protected def register [KVMap.Value α] (name : Name) (decl : Lean.Option.Decl α) : IO (Lean.Option α) := do
+  registerOption name { defValue := KVMap.Value.toDataValue decl.defValue, group := decl.group, descr := decl.descr }
+  return { name := name, defValue := decl.defValue }
+
+macro "register_builtin_option" name:ident " : " type:term " := " decl:term : command => `(
+  def initFn : IO (Lean.Option $type) :=
+    Lean.Option.register $(quote name.getId) $decl
+  @[builtinInit initFn] constant $name : Lean.Option $type)
+
+end Option
+
 end Lean

src/Lean/Elab/AutoBound.lean

@@ -9,16 +9,11 @@ import Lean.Data.Options
 
 namespace Lean.Elab
 
-builtin_initialize
-  registerOption `autoBoundImplicitLocal {
+register_builtin_option autoBoundImplicitLocal : Bool := {
     defValue := true
-    group    := ""
-    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 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}."
   }
 
-def getAutoBoundImplicitLocalOption (opts : Options) : Bool :=
-  opts.get `autoBoundImplicitLocal true
-
 private def allNumeral (s : Substring) : Bool :=
   s.all fun c => c.isDigit || isNumericSubscript c
 

src/Lean/Elab/Term.lean

@@ -324,9 +324,9 @@ def withLevelNames {α} (levelNames : List Name) (x : TermElabM α) : TermElabM
 def withoutErrToSorry {α} (x : TermElabM α) : TermElabM α :=
   withReader (fun ctx => { ctx with errToSorry := false }) x
 
-/-- Execute `x` with `autoBoundImplicit = (options.get `autoBoundImplicitLocal) && flag` -/
+/-- Execute `x` with `autoBoundImplicit := (autoBoundImplicitLocal.get options) && flag` -/
 def withAutoBoundImplicitLocal {α} (x : TermElabM α) (flag := true) : TermElabM α := do
-  let flag := getAutoBoundImplicitLocalOption (← getOptions) && flag
+  let flag := autoBoundImplicitLocal.get (← getOptions) && flag
   withReader (fun ctx => { ctx with autoBoundImplicit := flag, autoBoundImplicits := {} }) x
 
 /-- For testing `TermElabM` methods. The #eval command will sign the error. -/