feat(library/init/lean/options): add setOptionFromString

We can use this primitive to process command line arguments of the form
`-D <key> = <value>`

TODO: allow users to attach `[init]` to definitions of the form
```
@[init] def foo : IO Unit := ...
```
and avoid the awkward auxiliary constant.

library/init/data/int/basic.lean

@@ -158,3 +158,19 @@ def toNat : Int → Nat
 def natMod (m n : Int) : Nat := (m % n).toNat
 
 end Int
+
+namespace String
+
+def toInt (s : String) : Int :=
+if s.get 0 = '-' then
+ - Int.ofNat (s.foldl (λ n c, n*10 + (c.toNat - '0'.toNat)) 0 1)
+else
+ Int.ofNat s.toNat
+
+def isInt (s : String) : Bool :=
+if s.get 0 = '-' then
+  s.all (λ c, c.isDigit) 1
+else
+  s.isNat
+
+end String

library/init/lean/options.lean

@@ -28,12 +28,38 @@ private constant optionDeclsRef : IO.Ref OptionDecls := default _
 
 def registerOption (name : Name) (decl : OptionDecl) : IO Unit :=
 do decls ← optionDeclsRef.get,
-   when (decls.contains name) $ do {
-     let msg := "invalid option declaration '" ++ toString name ++ "', option already exists",
-     throw msg
-   },
+   when (decls.contains name) $
+     throw $ IO.userError ("invalid option declaration '" ++ toString name ++ "', option already exists"),
    optionDeclsRef.set $ decls.insert name decl
 
 def getOptionDecls : IO OptionDecls := optionDeclsRef.get
 
+def getOptionDecl (name : Name) : IO OptionDecl :=
+do decls ← getOptionDecls,
+   (some decl) ← pure (decls.find name) | throw $ IO.userError ("unknown option '" ++ toString name ++ "'"),
+   pure decl
+
+def getOptionDescr (name : Name) : IO String :=
+do decl ← getOptionDecl name,
+   pure decl.descr
+
+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
+   | DataValue.ofString v := pure $ opts.setString key val
+   | DataValue.ofBool v   :=
+     if key == "true" then pure $ opts.setBool key true
+     else if key == "false" then pure $ opts.setBool key false
+     else throw $ IO.userError ("invalid Bool option value '" ++ val ++ "'")
+   | DataValue.ofName v   := pure $ opts.setName key val.toName
+   | DataValue.ofNat v    := do
+     unless val.isNat $ throw (IO.userError ("invalid Nat option value '" ++ val ++ "'")),
+     pure $ opts.setNat key val.toNat
+   | DataValue.ofInt v    := do
+     unless val.isInt $ throw (IO.userError ("invalid Int option value '" ++ val ++ "'")),
+     pure $ opts.setInt key val.toInt
 end Lean

tests/playground/opts.lean

@@ -0,0 +1,35 @@
+import init.lean.options
+
+open Lean
+
+def initRegopt1 : IO Unit :=
+registerOption `myNatOpt {defValue := DataValue.ofNat 0, descr := "my Nat option" }
+@[init initRegopt1]
+constant regopt1 : Unit := default _
+
+def initRegopt2 : IO Unit :=
+registerOption `myBoolOpt {defValue := DataValue.ofBool true, descr := "my Bool option" }
+@[init initRegopt2]
+constant regopt2 : Unit := default _
+
+def initRegopt3 : IO Unit :=
+registerOption `myStringOpt {defValue := DataValue.ofString "", descr := "my String option" }
+@[init initRegopt3]
+constant regopt3 : Unit := default _
+
+def initRegopt4 : IO Unit :=
+registerOption `myIntOpt {defValue := DataValue.ofInt 0, descr := "my Int option" }
+@[init initRegopt4]
+constant regopt4 : Unit := default _
+
+
+def main : IO Unit :=
+do getOptionDescr `myNatOpt >>= IO.println,
+   getOptionDescr `myBoolOpt >>= IO.println,
+   getOptionDescr `myIntOpt >>= IO.println,
+   let os : Options := {},
+   os ← setOptionFromString os "myNatOpt = 100",
+   IO.println (os.getNat `myNatOpt),
+   os ← setOptionFromString os "myIntOpt = -20",
+   IO.println (os.getInt `myIntOpt),
+   pure ()