refactor(library/init/lean): add init/lean/parser/identifier

library/init/lean/parser/identifier.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.char.basic
+import init.data.char.basic init.lean.parser.parser
 
 namespace lean
 
@@ -37,4 +37,23 @@ c = id_begin_escape
 def is_id_end_escape (c : char) : bool :=
 c = id_end_escape
 
+namespace parser
+
+def id_part_default : parser string :=
+do c ← satisfy is_id_first,
+   take_while_cont is_id_rest (to_string c)
+
+def id_part_escaped : parser string :=
+ch id_begin_escape >> take_until1 is_id_end_escape <* ch id_end_escape
+
+def id_part : parser string :=
+cond is_id_begin_escape
+  id_part_escaped
+  id_part_default
+
+def identifier : parser name :=
+(try $ do s  ← id_part,
+       foldl name.mk_string (mk_simple_name s) (ch '.' >> id_part)) <?> "identifier"
+
+end parser
 end lean

library/init/lean/parser/parser.lean

@@ -9,7 +9,7 @@ https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/parsec-paper
 -/
 prelude
 import init.data.to_string init.data.string.basic init.data.list.basic init.control.except
-import init.data.repr init.lean.name init.lean.char
+import init.data.repr init.lean.name
 namespace lean
 namespace parser
 @[reducible] def position : Type := nat
@@ -427,23 +427,5 @@ run (p <* eoi) s fname
 def parse_with_left_over (p : parser α) (s : string) (fname := "") : except message (α × iterator) :=
 run (prod.mk <$> p <*> left_over) s fname
 
-/- Lean specific parsers -/
-
-def id_part_default : parser string :=
-do c ← satisfy is_id_first,
-   take_while_cont is_id_rest (to_string c)
-
-def id_part_escaped : parser string :=
-ch id_begin_escape >> take_until1 is_id_end_escape <* ch id_end_escape
-
-def id_part : parser string :=
-cond is_id_begin_escape
-  id_part_escaped
-  id_part_default
-
-def identifier : parser name :=
-(try $ do s  ← id_part,
-       foldl name.mk_string (mk_simple_name s) (ch '.' >> id_part)) <?> "identifier"
-
 end parser
 end lean

tests/lean/parser1.lean

@@ -1,4 +1,4 @@
-import system.io init.lean.parser.parser
+import system.io init.lean.parser.identifier
 open lean.parser
 
 def test {α} [decidable_eq α] (p : parser α) (s : string) (e : α) : io unit :=