feat(library/init/lean/parser/reader/module): open command

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

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

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 $

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

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