From d354dc437c368ba0779e3fa4c31bd5573ee99755 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 11 Jul 2019 17:13:22 -0700
Subject: [PATCH] feat(library/init/lean/parser/command): add `declaration`
 draft

---
 library/init/lean/parser/command.lean | 16 ++++++++++++++--
 tests/playground/cmdparsertest1.lean  | 24 ++++++++++++++++++++++++
 2 files changed, 38 insertions(+), 2 deletions(-)
 create mode 100644 tests/playground/cmdparsertest1.lean

diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean
index 8139bb003f..3ad7b9debf 100644
--- a/library/init/lean/parser/command.lean
+++ b/library/init/lean/parser/command.lean
@@ -37,14 +37,26 @@ def «noncomputable»  := parser! "noncomputable"
 def «unsafe»         := parser! "unsafe"
 def declModifiers    := parser! optional docComment >> optional «attributes» >> optional visibility >> optional «noncomputable» >> optional «unsafe»
 def declId           := parser! ident >> optional (".{" >> sepBy1 ident ", " >> "}")
-def declSig          := parser! many1 Term.bracktedBinder >> Term.typeSpec
-def optDeclSig       := parser! many1 Term.bracktedBinder >> Term.optType
+def declSig          := parser! many Term.bracktedBinder >> Term.typeSpec
+def optDeclSig       := parser! many Term.bracktedBinder >> Term.optType
 def declValSimple    := parser! " := " >> termParser
 def declValEqns      := parser! many1Indent Term.equation "equations must be indented"
 def declVal          := declValSimple <|> declValEqns
 def «def»            := parser! "def " >> declId >> optDeclSig >> declVal
 def «theorem»        := parser! "theorem " >> declId >> declSig >> declVal
 
+def declaration      := declModifiers >> («def» <|> «theorem»)
+
+/- TODO: remove this hack by improving how we compute `Parser.info.firstTokens` -/
+def declTokens := ["/--", "@[", "private", "protected", "noncomputable", "unsafe", "def", "theorem"]
+
+@[builtinCommandParser] def declEntry : Parser :=
+{ info := {
+    firstTokens := FirstTokens.tokens $ declTokens.map $ fun tk => { val := tk },
+    .. declaration.info
+  },
+  fn   := declaration.fn }
+
 end Command
 
 end Parser
diff --git a/tests/playground/cmdparsertest1.lean b/tests/playground/cmdparsertest1.lean
new file mode 100644
index 0000000000..22038acfa9
--- /dev/null
+++ b/tests/playground/cmdparsertest1.lean
@@ -0,0 +1,24 @@
+import init.lean.parser.command
+open Lean
+open Lean.Parser
+
+def testParser (input : String) : IO Unit :=
+do
+env ← mkEmptyEnvironment;
+cmdPTables ← builtinCommandParsingTable.get;
+stx ← IO.ofExcept $ runParser env cmdPTables input "<input>" "command";
+IO.println stx
+
+def test (is : List String) : IO Unit :=
+is.mfor $ fun input => do
+  IO.println input;
+  testParser input
+
+def main (xs : List String) : IO Unit :=
+do
+test [
+"@[inline] def x := 2",
+"protected def length.{u} {α : Type u} : List α → Nat
+  | [] := 0
+  | (a::as) := 1 + length as"
+]