feat(library/init/lean): improving options

@kha It will be awesome to automate the following idiom with a macro :)
```
def defIndent  := 4
def getIndent (o : Options) : Nat   := o.get `format.indent defIndent
@[init] def indentOption : IO Unit :=
registerOption `format.indent { defValue := defIndent, group := "format", descr := "indentation" }
```

library/init/lean/format.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.control.except init.control.reader init.control.state
+import init.lean.options
 universes u v
 
 namespace Lean
@@ -77,9 +77,6 @@ def be : Nat → Nat → String → List (Nat × Format) → String
   let r := merge w (spaceUptoLine f₁ w) (spaceUptoLine' z w) in
   if r.exceeded then be w k out ((i, f₂)::z) else be w k out ((i, f₁)::z)
 
-def pretty (f : Format) (w : Nat := 80) : String :=
-be w 0 "" [(0, f)]
-
 @[inline] def bracket (l : String) (f : Format) (r : String) : Format :=
 group (nest l.length $ l ++ f ++ r)
 
@@ -89,6 +86,25 @@ bracket "(" f ")"
 @[inline] def sbracket (f : Format) : Format :=
 bracket "[" f "]"
 
+def defIndent  := 4
+def defUnicode := true
+def defWidth   := 120
+
+def getWidth (o : Options) : Nat    := o.get `format.width  defWidth
+def getIndent (o : Options) : Nat   := o.get `format.indent defIndent
+def getUnicode (o : Options) : Bool := o.get `format.unicode defUnicode
+
+@[init] def indentOption : IO Unit :=
+registerOption `format.indent { defValue := defIndent, group := "format", descr := "indentation" }
+@[init] def unicodeOption : IO Unit :=
+registerOption `format.unicode { defValue := defUnicode, group := "format", descr := "unicode characters" }
+@[init] def widthOption : IO Unit :=
+registerOption `format.width { defValue := defWidth, group := "format", descr := "line width" }
+
+def pretty (f : Format) (o : Options := {}) : String :=
+let w := getWidth o in
+be w 0 "" [(0, f)]
+
 end Format
 
 open Lean.Format
@@ -133,13 +149,12 @@ instance listHasToFormat {α : Type u} [HasToFormat α] : HasToFormat (List α)
 instance prodHasToFormat {α : Type u} {β : Type v} [HasToFormat α] [HasToFormat β] : HasToFormat (Prod α β) :=
 ⟨λ ⟨a, b⟩, paren $ toFormat a ++ "," ++ line ++ toFormat b⟩
 
-instance natHasToFormat : HasToFormat Nat    := ⟨λ n, toString n⟩
+instance natHasToFormat : HasToFormat Nat       := ⟨λ n, toString n⟩
 instance uint16HasToFormat : HasToFormat UInt16 := ⟨λ n, toString n⟩
 instance uint32HasToFormat : HasToFormat UInt32 := ⟨λ n, toString n⟩
 instance uint64HasToFormat : HasToFormat UInt64 := ⟨λ n, toString n⟩
-instance usizeHasToFormat : HasToFormat USize := ⟨λ n, toString n⟩
-
-instance formatHasToString : HasToString Format := ⟨pretty⟩
+instance usizeHasToFormat : HasToFormat USize   := ⟨λ n, toString n⟩
+instance nameHasToFormat : HasToFormat Name     := ⟨λ n, n.toString⟩
 
 protected def Format.repr : Format → Format
 | nil := "Format.nil"
@@ -149,6 +164,9 @@ protected def Format.repr : Format → Format
 | (compose b f₁ f₂) := paren $ "Format.compose " ++ repr b ++ line ++ Format.repr f₁ ++ line ++ Format.repr f₂
 | (choice f₁ f₂) := paren $ "Format.choice" ++ line ++ Format.repr f₁ ++ line ++ Format.repr f₂
 
+
+instance formatHasToString : HasToString Format := ⟨Format.pretty⟩
+
 instance : HasRepr Format := ⟨Format.pretty ∘ Format.repr⟩
 
 end Lean

library/init/lean/kvmap.lean

@@ -10,9 +10,9 @@ namespace Lean
 
 inductive DataValue
 | ofString (v : String)
-| ofNat    (v : Nat)
 | ofBool   (v : Bool)
 | ofName   (v : Name)
+| ofNat    (v : Nat)
 | ofInt    (v : Int)
 
 def DataValue.beq : DataValue → DataValue → Bool
@@ -23,6 +23,12 @@ def DataValue.beq : DataValue → DataValue → Bool
 
 instance DataValue.HasBeq : HasBeq DataValue := ⟨DataValue.beq⟩
 
+instance string2DataValue : HasCoe String DataValue := ⟨DataValue.ofString⟩
+instance bool2DataValue   : HasCoe Bool DataValue   := ⟨DataValue.ofBool⟩
+instance name2DataValue   : HasCoe Name DataValue   := ⟨DataValue.ofName⟩
+instance nat2DataValue    : HasCoe Nat DataValue    := ⟨DataValue.ofNat⟩
+instance int2DataValue    : HasCoe Int DataValue    := ⟨DataValue.ofInt⟩
+
 /- Remark: we do not use RBMap here because we need to manipulate KVMap objects in
    C++ and RBMap is implemented in Lean. So, we use just a List until we can
    generate C++ code from Lean code. -/
@@ -47,30 +53,30 @@ def insert : KVMap → Name → DataValue → KVMap
 def contains (m : KVMap) (n : Name) : Bool :=
 (m.find n).isSome
 
-def getString (m : KVMap) (k : Name) : Option String :=
+def getString (m : KVMap) (k : Name) (defVal := "") : String :=
 match m.find k with
-| some (DataValue.ofString v) := some v
-| _                             := none
+| some (DataValue.ofString v) := v
+| _                           := defVal
 
-def getNat (m : KVMap) (k : Name) : Option Nat :=
+def getNat (m : KVMap) (k : Name) (defVal := 0) : Nat :=
 match m.find k with
-| some (DataValue.ofNat v) := some v
-| _                          := none
+| some (DataValue.ofNat v) := v
+| _                        := defVal
 
-def getInt (m : KVMap) (k : Name) : Option Int :=
+def getInt (m : KVMap) (k : Name) (defVal : Int := 0) : Int :=
 match m.find k with
-| some (DataValue.ofInt v) := some v
-| _                        := none
+| some (DataValue.ofInt v) := v
+| _                        := defVal
 
-def getBool (m : KVMap) (k : Name) : Option Bool :=
+def getBool (m : KVMap) (k : Name) (defVal := false) : Bool :=
 match m.find k with
-| some (DataValue.ofBool v) := some v
-| _                           := none
+| some (DataValue.ofBool v) := v
+| _                         := defVal
 
-def getName (m : KVMap) (k : Name) : Option Name :=
+def getName (m : KVMap) (k : Name) (defVal := Name.anonymous) : Name :=
 match m.find k with
-| some (DataValue.ofName v) := some v
-| _                           := none
+| some (DataValue.ofName v) := v
+| _                         := defVal
 
 def setString (m : KVMap) (k : Name) (v : String) : KVMap :=
 m.insert k (DataValue.ofString v)
@@ -99,5 +105,30 @@ subset m₁ m₂ && subset m₂ m₁
 
 instance : HasBeq KVMap := ⟨eqv⟩
 
+class isKVMapVal (α : Type) :=
+(defVal : α)
+(set    : KVMap → Name → α → KVMap)
+(get    : KVMap → Name → α → α)
+
+export isKVMapVal (set)
+
+@[inline] def get {α : Type} [isKVMapVal α] (m : KVMap) (k : Name) (defVal := isKVMapVal.defVal α) : α :=
+isKVMapVal.get m k defVal
+
+instance boolVal : isKVMapVal Bool :=
+{ defVal := false, set := setBool, get := λ k n v, getBool k n v }
+
+instance natVal : isKVMapVal Nat :=
+{ defVal := 0, set := setNat, get := λ k n v, getNat k n v }
+
+instance intVal : isKVMapVal Int :=
+{ defVal := 0, set := setInt, get := λ k n v, getInt k n v }
+
+instance nameVal : isKVMapVal Name :=
+{ defVal := Name.anonymous, set := setName, get := λ k n v, getName k n v }
+
+instance stringVal : isKVMapVal String :=
+{ defVal := "", set := setString, get := λ k n v, getString k n v }
+
 end KVMap
 end Lean

library/init/lean/level.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.name init.data.option.basic
+import init.data.option.basic init.lean.name init.lean.format
 
 namespace Lean
 
@@ -80,8 +80,8 @@ inductive Result
 | leaf      : Format → Result
 | num       : Nat → Result
 | offset    : Result → Nat → Result
-| maxNode  : List Result → Result
-| imaxNode : List Result → Result
+| maxNode   : List Result → Result
+| imaxNode  : List Result → Result
 
 def Result.succ : Result → Result
 | (Result.offset f k) := Result.offset f (k+1)

library/init/lean/name.lean

@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 -/
 prelude
 import init.data.string.basic init.coe init.data.uint init.data.tostring
-import init.lean.format init.data.hashable init.data.rbmap init.data.rbtree
+import init.data.hashable init.data.rbmap init.data.rbtree
 namespace Lean
 
 inductive Name
@@ -138,9 +138,6 @@ toStringWithSep "."
 instance : HasToString Name :=
 ⟨Name.toString⟩
 
-instance : HasToFormat Name :=
-⟨λ n, n.toString⟩
-
 theorem mkStringNeMkStringOfNePrefix {p₁ : Name} (s₁ : String) {p₂ : Name} (s₂ : String) : p₁ ≠ p₂ → mkString p₁ s₁ ≠ mkString p₂ s₂ :=
 λ h₁ h₂, Name.noConfusion h₂ (λ h _, absurd h h₁)
 

library/init/lean/options.lean

@@ -9,6 +9,7 @@ import init.lean.kvmap init.io init.control.combinators init.data.tostring
 namespace Lean
 
 def Options := KVMap
+
 namespace Options
 def empty : Options  := {KVMap .}
 instance : HasEmptyc Options := ⟨empty⟩
@@ -16,6 +17,7 @@ end Options
 
 structure OptionDecl :=
 (defValue : DataValue)
+(group    : String := "")
 (descr    : String := "")
 
 def OptionDecls := NameMap OptionDecl
@@ -39,6 +41,10 @@ do decls ← getOptionDecls,
    (some decl) ← pure (decls.find name) | throw $ IO.userError ("unknown option '" ++ toString name ++ "'"),
    pure decl
 
+def getOptionDefaulValue (name : Name) : IO DataValue :=
+do decl ← getOptionDecl name,
+   pure decl.defValue
+
 def getOptionDescr (name : Name) : IO String :=
 do decl ← getOptionDecl name,
    pure decl.descr
@@ -46,10 +52,8 @@ do decl ← getOptionDecl name,
 def setOptionFromString (opts : Options) (entry : String) : IO Options :=
 do let ps := (entry.split "=").map String.trim,
    [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form '<key> = <value>'",
-   let key := key.toName,
-   decls ← getOptionDecls,
-   (some decl) ← pure (decls.find key) | throw $ IO.userError ("unknown option '" ++ toString key ++ "'"),
-   match decl.defValue with
+   defValue ← getOptionDefaulValue key.toName,
+   match defValue with
    | DataValue.ofString v := pure $ opts.setString key val
    | DataValue.ofBool v   :=
      if key == "true" then pure $ opts.setBool key true
@@ -62,4 +66,5 @@ do let ps := (entry.split "=").map String.trim,
    | DataValue.ofInt v    := do
      unless val.isInt $ throw (IO.userError ("invalid Int option value '" ++ val ++ "'")),
      pure $ opts.setInt key val.toInt
+
 end Lean

library/init/lean/parser/parsec.lean

@@ -10,6 +10,7 @@ https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/Parsec-paper
 prelude
 import init.data.tostring init.data.string.basic init.data.list.basic init.control.except
 import init.data.repr init.lean.name init.data.dlist init.control.monadfail init.control.combinators
+import init.lean.format
 
 namespace Lean
 namespace Parser

library/init/lean/parser/rec.lean

@@ -6,7 +6,7 @@ Author: Sebastian Ullrich
 Recursion monad transformer
 -/
 prelude
-import init.lean.parser.parsec init.fix
+import init.control.reader init.lean.parser.parsec init.fix
 
 namespace Lean.Parser
 

library/init/lean/parser/trie.lean

@@ -55,7 +55,7 @@ private def toStringAux {α : Type} : Trie α → List Format
   toFormat (repr c) :: (Format.group $ Format.nest 2 $ flip Format.joinSep Format.line $ toStringAux t) :: Fs) []
 
 instance {α : Type} : HasToString (Trie α) :=
-⟨λ t, (flip Format.joinSep Format.line $ toStringAux t).pretty 0⟩
+⟨λ t, (flip Format.joinSep Format.line $ toStringAux t).pretty⟩
 end Trie
 
 end Parser

library/init/lean/trace.lean

@@ -50,7 +50,7 @@ traceCtx cls msg (pure () : m Unit)
 instance (m) [Monad m] : MonadTracer (TraceT m) :=
 { traceRoot := λ α pos cls msg ctx, do {
     st ← get,
-    if st.opts.getBool cls = some true then do {
+    if st.opts.getBool cls = true then do {
       modify $ λ st, {curPos := pos, curTraces := [], ..st},
       a ← ctx.get,
       modify $ λ (st : TraceState), {roots := st.roots.insert pos ⟨msg, st.curTraces⟩, ..st},
@@ -62,7 +62,7 @@ instance (m) [Monad m] : MonadTracer (TraceT m) :=
     -- tracing enabled?
     some _ ← pure st.curPos | ctx.get,
     -- Trace class enabled?
-    if st.opts.getBool cls = some true then do {
+    if st.opts.getBool cls = true then do {
       set {curTraces := [], ..st},
       a ← ctx.get,
       modify $ λ (st' : TraceState), {curTraces := st.curTraces ++ [⟨msg, st'.curTraces⟩], ..st'},