From 5b55600e716f0b8259c06104ca4cb2000cefe79d Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 16 Jul 2018 11:15:36 +0200
Subject: [PATCH] feat(library/init/lean/parser/reader/module): `open` command

---
 library/init/lean/parser/reader/basic.lean  | 11 +++++-
 library/init/lean/parser/reader/module.lean | 44 ++++++++++++++++++++-
 library/init/lean/parser/reader/token.lean  |  2 +-
 tests/lean/reader1.lean                     |  5 ++-
 tests/lean/reader1.lean.expected.out        | 22 +++++++++--
 5 files changed, 74 insertions(+), 10 deletions(-)

diff --git a/library/init/lean/parser/reader/basic.lean b/library/init/lean/parser/reader/basic.lean
index 1c0e1da4e8..52711123c8 100644
--- a/library/init/lean/parser/reader/basic.lean
+++ b/library/init/lean/parser/reader/basic.lean
@@ -63,13 +63,17 @@ protected def parse (cfg : reader_config) (s : string) (r : reader) :
 let tokens : list token_config := [⟨"/-", none⟩, ⟨"--", none⟩] in
 r.read.run cfg ⟨r.tokens ++ tokens, ff, []⟩ s
 
-def node (m : macro) (ps : list reader) : reader :=
+namespace combinators
+def node' (m : name) (ps : list reader) : reader :=
 { read := do {
     args ← ps.mmap reader.read,
-    pure $ syntax.node ⟨m.name, args⟩
+    pure $ syntax.node ⟨m, args⟩
   },
   tokens := ps.bind reader.tokens }
 
+def seq := node' name.anonymous
+def node (m : macro) := node' m.name
+
 def many (p : reader) : reader :=
 { p with read := do
     args ← many p.read,
@@ -87,6 +91,9 @@ def optional (p : reader) : reader :=
     | some r := syntax.node ⟨name.anonymous, [r]⟩
     | none   := syntax.node ⟨name.anonymous, []⟩ }
 
+def try (p : reader) : reader :=
+{ p with read := try p.read }
+end combinators
 end reader
 end parser
 end lean
diff --git a/library/init/lean/parser/reader/module.lean b/library/init/lean/parser/reader/module.lean
index 0dcfadf612..43610ab59e 100644
--- a/library/init/lean/parser/reader/module.lean
+++ b/library/init/lean/parser/reader/module.lean
@@ -10,7 +10,7 @@ import init.lean.parser.reader.token
 
 namespace lean.parser
 namespace reader
-open monad_parsec
+open combinators
 
 def «prelude» := {macro . name := `prelude}
 
@@ -28,12 +28,52 @@ def «import» := {macro . name := `import}
 def import.reader : reader :=
 node «import» [keyword "import", many1 import_path.reader]
 
+section commands
+
+def «open» := {macro . name := `open}
+
+def open_export.reader : reader :=
+many1 $ seq [
+  ident,
+  optional $ seq [
+    keyword "as",
+    ident
+  ],
+  optional $ seq [
+    try $ seq [symbol "(", ident],
+    many ident,
+    symbol ")"
+  ],
+  optional $ seq [
+    try $ seq [symbol "(", keyword "renaming"],
+    many1 $ seq [ident, symbol "->", ident],
+    symbol ")"
+  ],
+  optional $ seq [
+    symbol "(",
+    keyword "hiding",
+    many1 ident,
+    symbol ")"
+  ]
+]
+
+def open.reader : reader :=
+node «open» [keyword "open", open_export.reader]
+
+def command.reader :=
+open.reader
+end commands
+
+def «section» := {macro . name := `section}
+
+
 def module := {macro . name := `module}
 
 def module.reader : reader :=
 node module [
   optional prelude.reader,
-  many import.reader
+  many import.reader,
+  many command.reader
 ]
 
 end reader
diff --git a/library/init/lean/parser/reader/token.lean b/library/init/lean/parser/reader/token.lean
index 4ad3f50c78..84ac7c8374 100644
--- a/library/init/lean/parser/reader/token.lean
+++ b/library/init/lean/parser/reader/token.lean
@@ -95,7 +95,7 @@ do tk ← match_token,
          pure $ λ i, syntax.atom ⟨some i, atomic_val.string tk⟩
    -- variable-length token
    | some ⟨tk, some r⟩ := error "not implemented" --str tk *> monad_parsec.lift r
-   | none              := failure
+   | none              := error
 
 def token : read_m syntax :=
 do (r, i) ← with_source_info $
diff --git a/tests/lean/reader1.lean b/tests/lean/reader1.lean
index fbde1b14d5..6cfbe18bbc 100644
--- a/tests/lean/reader1.lean
+++ b/tests/lean/reader1.lean
@@ -18,7 +18,10 @@ match p.parse ⟨⟩ s with
 import ..a b
 import c"
 
+#eval show_result module.reader "open me you"
+#eval show_result module.reader "open me as you (a b c) (renaming a->b c->d) (hiding a b)"
+
 -- slowly progressing...
 #eval do
   s ← io.fs.read_file "../../library/init/core.lean",
-  show_result (many { read := token }) s
+  show_result (combinators.many { read := token }) s
diff --git a/tests/lean/reader1.lean.expected.out b/tests/lean/reader1.lean.expected.out
index 28352792e8..e71f6c115b 100644
--- a/tests/lean/reader1.lean.expected.out
+++ b/tests/lean/reader1.lean.expected.out
@@ -1,15 +1,29 @@
 result: 
-(module [(prelude "prelude")] [])
+(module [(prelude "prelude")] [] [])
 result: 
-(module [] [(import "import" [(import_path [] me)])])
+(module [] [(import "import" [(import_path [] me)])] [])
 error at line 1, column 0:
 unexpected 'i'
-expected "prelude", "import" or end of input
+expected "prelude", "import", "open" or end of input
 result: 
 (module
  [(prelude "prelude")]
  [(import "import" [(import_path ["." "."] a) (import_path [] b)])
- (import "import" [(import_path [] c)])])
+ (import "import" [(import_path [] c)])]
+ [])
+result: 
+(module [] [] [(open "open" [[me [] [] [] []] [you [] [] [] []]])])
+result: 
+(module
+ []
+ []
+ [(open
+ "open"
+ [[me
+ [["as" you]]
+ [[["(" a] [b c] ")"]]
+ [[["(" "renaming"] [[a "->" b] [c "->" d]] ")"]]
+ [["(" "hiding" [a b] ")"]]]])])
 error at line 10, column 9:
 unexpected '`'
 expected end of input