From e4c9326c00a54e23284dff5f718b9b11975c1f75 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 12 Jul 2019 16:42:25 -0700
Subject: [PATCH] feat(library/init/lean/parser): add `module.lean`

---
 library/init/lean/message.lean        |  5 +-
 library/init/lean/parser/default.lean |  1 +
 library/init/lean/parser/module.lean  | 66 +++++++++++++++++++++++++++
 library/init/lean/parser/parser.lean  |  3 ++
 4 files changed, 72 insertions(+), 3 deletions(-)
 create mode 100644 library/init/lean/parser/module.lean

diff --git a/library/init/lean/message.lean b/library/init/lean/message.lean
index 0ec37f6a6e..e7b89619b0 100644
--- a/library/init/lean/message.lean
+++ b/library/init/lean/message.lean
@@ -40,11 +40,10 @@ end Message
 
 structure MessageLog :=
 -- messages are stored in reverse for efficient append
-(revList : List Message)
+(revList : List Message := [])
 
 namespace MessageLog
-def empty : MessageLog :=
-⟨[]⟩
+def empty : MessageLog := ⟨[]⟩
 
 def add (msg : Message) (log : MessageLog) : MessageLog :=
 ⟨msg :: log.revList⟩
diff --git a/library/init/lean/parser/default.lean b/library/init/lean/parser/default.lean
index fe90655dc3..137a645d36 100644
--- a/library/init/lean/parser/default.lean
+++ b/library/init/lean/parser/default.lean
@@ -8,3 +8,4 @@ import init.lean.parser.parser
 import init.lean.parser.level
 import init.lean.parser.term
 import init.lean.parser.command
+import init.lean.parser.module
diff --git a/library/init/lean/parser/module.lean b/library/init/lean/parser/module.lean
new file mode 100644
index 0000000000..0b9723b1c5
--- /dev/null
+++ b/library/init/lean/parser/module.lean
@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich
+-/
+prelude
+import init.lean.message
+import init.lean.parser.command
+
+namespace Lean
+namespace Parser
+
+namespace Module
+
+def «prelude»  := parser! "prelude"
+def importPath := parser! many (rawCh '.' true) >> ident
+def «import»   := parser! "import " >> many1 importPath
+def header     := parser! optional «prelude» >> many «import»
+
+def tokens : Trie TokenConfig :=
+match header.info.updateTokens {} with
+| Except.ok t    => t
+| Except.error _ => {} -- should be unreachable
+
+end Module
+
+structure ModuleReader :=
+(context  : ParserContext)
+(state    : ParserState)
+(messages : MessageLog := {})
+
+private def checkResult (r : ModuleReader) : Option Syntax × ModuleReader :=
+let s   := r.state;
+match r.state.errorMsg with
+| some msg =>
+  let c   := r.context;
+  let pos := c.fileMap.toPosition s.pos;
+  let msg := { Message . filename := c.filename, pos := pos, text := msg, caption := "parser" };
+  (none, { messages := r.messages.add msg, .. r })
+| none =>
+  let stx := s.stxStack.back;
+  let s   := s.popSyntax;
+  (some stx, { state := s, .. r })
+
+def mkModuleReader (env : Environment) (input : String) (fileName := "<input>") : Option Syntax × ModuleReader :=
+let c := mkParserContext env input fileName;
+let c := { tokens := Module.tokens, .. c };
+let s := mkParserState input;
+let s := whitespace c s;
+let s := Module.header.fn (0:Nat) c s;
+checkResult { context := c, state := s }
+
+namespace ModuleReader
+
+def isEOI (r : ModuleReader) : Bool :=
+r.context.input.atEnd r.state.pos
+
+def nextCommand : ModuleReader → Option Syntax × ModuleReader
+| ⟨c, s, m⟩ :=
+  let s := commandParser.fn (0:Nat) c s;
+  checkResult { context := c, state := s, messages := m }
+
+end ModuleReader
+
+end Parser
+end Lean
diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index b20ade5324..622994fffb 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -495,6 +495,9 @@ private def rawAux {k : ParserKind} (startPos : Nat) (trailingWs : Bool) : Parse
 @[inline] def chFn {k : ParserKind} (c : Char) (trailingWs := false) : ParserFn k :=
 rawFn (fun _ => satisfyFn (fun d => c == d) ("expected '" ++ toString c ++ "'")) trailingWs
 
+def rawCh {k : ParserKind} (c : Char) (trailingWs := false) : Parser k :=
+{ fn := chFn c trailingWs }
+
 def hexDigitFn : BasicParserFn
 | c s :=
   let input := c.input;