From 01ba75661e957a4725df52e2db4486e265dbe384 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 24 May 2023 20:39:56 -0400
Subject: [PATCH] fix: implement String.toName using decodeNameLit

fixes #2231
---
 src/Init/Meta.lean                 | 36 ++++++++++++++++++------------
 src/Lean/Data/Json/FromToJson.lean |  4 ++--
 src/Lean/Data/Lsp/Internal.lean    |  7 +++---
 src/Lean/Data/Name.lean            |  4 ----
 src/Lean/Data/Options.lean         | 22 ------------------
 5 files changed, 28 insertions(+), 45 deletions(-)

diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean
index f41c4478b6..456c06b9f6 100644
--- a/src/Init/Meta.lean
+++ b/src/Init/Meta.lean
@@ -836,22 +836,30 @@ private partial def splitNameLitAux (ss : Substring) (acc : List Substring) : Li
 def splitNameLit (ss : Substring) : List Substring :=
   splitNameLitAux ss [] |>.reverse
 
+def _root_.Substring.toName (s : Substring) : Name :=
+  match splitNameLitAux s [] with
+  | [] => .anonymous
+  | comps => comps.foldr (init := Name.anonymous)
+    fun comp n =>
+      let comp := comp.toString
+      if isIdBeginEscape comp.front then
+        Name.mkStr n (comp.drop 1 |>.dropRight 1)
+      else if comp.front.isDigit then
+        if let some k := decodeNatLitVal? comp then
+          Name.mkNum n k
+        else
+          unreachable!
+      else
+        Name.mkStr n comp
+
+def _root_.String.toName (s : String) : Name :=
+  s.toSubstring.toName
+
 def decodeNameLit (s : String) : Option Name :=
   if s.get 0 == '`' then
-    match splitNameLitAux (s.toSubstring.drop 1) [] with
-    | [] => none
-    | comps => some <| comps.foldr (init := Name.anonymous)
-      fun comp n =>
-        let comp := comp.toString
-        if isIdBeginEscape comp.front then
-          Name.mkStr n (comp.drop 1 |>.dropRight 1)
-        else if comp.front.isDigit then
-          if let some k := decodeNatLitVal? comp then
-            Name.mkNum n k
-          else
-            unreachable!
-        else
-          Name.mkStr n comp
+    match (s.toSubstring.drop 1).toName with
+    | .anonymous => none
+    | name => some name
   else
     none
 
diff --git a/src/Lean/Data/Json/FromToJson.lean b/src/Lean/Data/Json/FromToJson.lean
index 6c995fed86..913dfa5f81 100644
--- a/src/Lean/Data/Json/FromToJson.lean
+++ b/src/Lean/Data/Json/FromToJson.lean
@@ -81,8 +81,8 @@ instance : FromJson Name where
     if s == "[anonymous]" then
       return Name.anonymous
     else
-      let some n := Syntax.decodeNameLit ("`" ++ s)
-        | throw s!"expected a `Name`, got '{j}'"
+      let n := s.toName
+      if n.isAnonymous then throw s!"expected a `Name`, got '{j}'"
       return n
 
 instance : ToJson Name where
diff --git a/src/Lean/Data/Lsp/Internal.lean b/src/Lean/Data/Lsp/Internal.lean
index d8e3b1cd0a..22bba6e1d9 100644
--- a/src/Lean/Data/Lsp/Internal.lean
+++ b/src/Lean/Data/Lsp/Internal.lean
@@ -34,9 +34,10 @@ def fromString (s : String) : Except String RefIdent := do
   -- See `FromJson Name`
   let name ← match sName with
     | "[anonymous]" => pure Name.anonymous
-    | _ => match Syntax.decodeNameLit ("`" ++ sName) with
-      | some n => pure n
-      | none => throw s!"expected a Name, got {sName}"
+    | _ =>
+      let n := s.toName
+      if n.isAnonymous then throw s!"expected a Name, got {sName}"
+      else pure n
   match sPrefix with
     | "c:" => return RefIdent.const name
     | "f:" => return RefIdent.fvar <| FVarId.mk name
diff --git a/src/Lean/Data/Name.lean b/src/Lean/Data/Name.lean
index 825c3b0ea6..b97a959969 100644
--- a/src/Lean/Data/Name.lean
+++ b/src/Lean/Data/Name.lean
@@ -151,7 +151,3 @@ end Name
 end Lean
 
 open Lean
-
-def String.toName (s : String) : Name :=
-  let ps := s.splitOn ".";
-  ps.foldl (fun n p => Name.mkStr n p.trim) Name.anonymous
diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean
index dbc41f4a2c..0b6525a24a 100644
--- a/src/Lean/Data/Options.lean
+++ b/src/Lean/Data/Options.lean
@@ -62,28 +62,6 @@ def getOptionDescr (name : Name) : IO String := do
   let decl ← getOptionDecl name
   pure decl.descr
 
-def setOptionFromString (opts : Options) (entry : String) : IO Options := do
-  let ps := (entry.splitOn "=").map String.trim
-  let [key, val] ← pure ps | throw $ IO.userError "invalid configuration option entry, it must be of the form '<key> = <value>'"
-  let key := Name.mkSimple key
-  let defValue ← getOptionDefaultValue key
-  match defValue with
-  | DataValue.ofString _ => pure $ opts.setString key val
-  | DataValue.ofBool _   =>
-    if key == `true then pure $ opts.setBool key true
-    else if key == `false then pure $ opts.setBool key false
-    else throw $ IO.userError s!"invalid Bool option value '{val}'"
-  | DataValue.ofName _   => pure $ opts.setName key val.toName
-  | DataValue.ofNat _    =>
-    match val.toNat? with
-    | none   => throw (IO.userError s!"invalid Nat option value '{val}'")
-    | some v => pure $ opts.setNat key v
-  | DataValue.ofInt _    =>
-    match val.toInt? with
-    | none   => throw (IO.userError s!"invalid Int option value '{val}'")
-    | some v => pure $ opts.setInt key v
-  | DataValue.ofSyntax _ => throw (IO.userError s!"invalid Syntax option value")
-
 class MonadOptions (m : Type → Type) where
   getOptions : m Options