feat: name resolution during parsing

src/Lean/Elab/Frontend.lean

@@ -49,8 +49,10 @@ def processCommand : FrontendM Bool := do
   let cmdState ← getCommandState
   let ictx ← getInputContext
   let pstate ← getParserState
+  let scope := cmdState.scopes.head!
+  let pmctx := { env := cmdState.env, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
   let pos := ictx.fileMap.toPosition pstate.pos
-  match profileit "parsing" pos fun _ => Parser.parseCommand cmdState.env ictx pstate cmdState.messages with
+  match profileit "parsing" pos fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with
   | (cmd, ps, messages) =>
     modify fun s => { s with commands := s.commands.push cmd }
     setParserState ps

src/Lean/Parser/Basic.lean

@@ -62,6 +62,7 @@ import Lean.Environment
 import Lean.Attributes
 import Lean.Message
 import Lean.Compiler.InitAttr
+import Lean.ResolveName
 
 namespace Lean
 
@@ -120,15 +121,24 @@ instance : Inhabited InputContext := ⟨{
   input := "", fileName := "", fileMap := arbitrary
 }⟩
 
-structure ParserContext extends InputContext where
+/-- Input context derived from elaboration of previous commands. -/
+structure ParserModuleContext where
+  env           : Environment
+  -- for name lookup
+  currNamespace : Name := Name.anonymous
+  openDecls     : List OpenDecl := []
+
+structure ParserContext extends InputContext, ParserModuleContext where
   prec               : Nat
-  env                : Environment
   tokens             : TokenTable
   insideQuot         : Bool := false
   suppressInsideQuot : Bool := false
   savedPos?          : Option String.Pos := none
   forbiddenTk?       : Option Token := none
 
+def ParserContext.resolveName (ctx : ParserContext) (id : Name) : List (Name × List String) :=
+  ResolveName.resolveGlobalName ctx.env ctx.currNamespace ctx.openDecls id
+
 structure Error where
   unexpected : String := ""
   expected : List String := []

src/Lean/Parser/Extension.lean

@@ -422,11 +422,11 @@ def mkInputContext (input : String) (fileName : String) : InputContext := {
   fileMap  := input.toFileMap
 }
 
-def mkParserContext (env : Environment) (ctx : InputContext) : ParserContext := {
-  prec           := 0,
-  toInputContext := ctx,
-  env            := env,
-  tokens         := getTokenTable env
+def mkParserContext (ictx : InputContext) (pmctx : ParserModuleContext) : ParserContext := {
+  prec                  := 0,
+  toInputContext        := ictx,
+  toParserModuleContext := pmctx,
+  tokens                := getTokenTable pmctx.env
 }
 
 def mkParserState (input : String) : ParserState :=
@@ -434,7 +434,7 @@ def mkParserState (input : String) : ParserState :=
 
 /- convenience function for testing -/
 def runParserCategory (env : Environment) (catName : Name) (input : String) (fileName := "<input>") : Except String Syntax :=
-  let c := mkParserContext env (mkInputContext input fileName)
+  let c := mkParserContext (mkInputContext input fileName) { env := env }
   let s := mkParserState input
   let s := whitespace c s
   let s := categoryParserFnImpl catName c s

src/Lean/Parser/Module.lean

@@ -40,7 +40,7 @@ private def mkErrorMessage (c : ParserContext) (pos : String.Pos) (errorMsg : St
 
 def parseHeader (inputCtx : InputContext) : IO (Syntax × ModuleParserState × MessageLog) := do
   let dummyEnv ← mkEmptyEnvironment
-  let ctx := mkParserContext dummyEnv inputCtx
+  let ctx := mkParserContext inputCtx { env := dummyEnv }
   let ctx := Module.updateTokens ctx
   let s   := mkParserState ctx.input
   let s   := whitespace ctx s
@@ -76,13 +76,13 @@ def topLevelCommandParserFn : ParserFn :=
     (andthenFn (lookaheadFn termParser.fn) (errorFn "expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term"))
     false /- do not merge errors -/
 
-partial def parseCommand (env : Environment) (inputCtx : InputContext) (s : ModuleParserState) (messages : MessageLog) : Syntax × ModuleParserState × MessageLog :=
+partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext) (s : ModuleParserState) (messages : MessageLog) : Syntax × ModuleParserState × MessageLog :=
   let rec parse (s : ModuleParserState) (messages : MessageLog) :=
     let { pos := pos, recovering := recovering } := s
     if inputCtx.input.atEnd pos then
       (mkEOI pos, s, messages)
     else
-      let c   := mkParserContext env inputCtx
+      let c   := mkParserContext inputCtx pmctx
       let s   := { cache := initCacheForInput c.input, pos := pos : ParserState }
       let s   := whitespace c s
       let s   := topLevelCommandParserFn c s
@@ -104,29 +104,11 @@ partial def parseCommand (env : Environment) (inputCtx : InputContext) (s : Modu
           -- (stx, { pos := pos, recovering := true }, messages)
   parse s messages
 
-private partial def testModuleParserAux (env : Environment) (inputCtx : InputContext) (displayStx : Bool) (s : ModuleParserState) (messages : MessageLog) : IO Bool :=
-  let rec loop (s : ModuleParserState) (messages : MessageLog) := do
-    match parseCommand env inputCtx s messages with
-    | (stx, s, messages) =>
-      if isEOI stx || isExitCommand stx then
-        messages.forM fun msg => msg.toString >>= IO.println
-        pure (!messages.hasErrors)
-      else
-        if displayStx then IO.println stx
-        loop s messages
-  loop s messages
+-- only useful for testing since most Lean files cannot be parsed without elaboration
 
-@[export lean_test_module_parser]
-def testModuleParser (env : Environment) (input : String) (fileName := "<input>") (displayStx := false) : IO Bool :=
-  timeit (fileName ++ " parser") do
-    let inputCtx           := mkInputContext input fileName
-    let (stx, s, messages) ← parseHeader inputCtx
-    if displayStx then IO.println stx
-    testModuleParserAux env inputCtx displayStx s messages
-
-partial def parseModuleAux (env : Environment) (inputCtx : InputContext) (s : ModuleParserState) (msgs : MessageLog) (stxs  : Array Syntax) : IO (Array Syntax) :=
+partial def testParseModuleAux (env : Environment) (inputCtx : InputContext) (s : ModuleParserState) (msgs : MessageLog) (stxs  : Array Syntax) : IO (Array Syntax) :=
   let rec parse (state : ModuleParserState) (msgs : MessageLog) (stxs : Array Syntax) :=
-    match parseCommand env inputCtx state msgs with
+    match parseCommand inputCtx { env := env } state msgs with
     | (stx, state, msgs) =>
       if isEOI stx then
         if msgs.isEmpty then
@@ -138,17 +120,17 @@ partial def parseModuleAux (env : Environment) (inputCtx : InputContext) (s : Mo
         parse state msgs (stxs.push stx)
   parse s msgs stxs
 
-def parseModule (env : Environment) (fname contents : String) : IO Syntax := do
+def testParseModule (env : Environment) (fname contents : String) : IO Syntax := do
   let fname ← IO.realPath fname
   let inputCtx := mkInputContext contents fname
   let (header, state, messages) ← parseHeader inputCtx
-  let cmds ← parseModuleAux env inputCtx state messages #[]
+  let cmds ← testParseModuleAux env inputCtx state messages #[]
   let stx := Syntax.node `Lean.Parser.Module.module #[header, mkListNode cmds]
   pure stx.updateLeading
 
-def parseFile (env : Environment) (fname : String) : IO Syntax := do
+def testParseFile (env : Environment) (fname : String) : IO Syntax := do
   let contents ← IO.FS.readFile fname
-  parseModule env fname contents
+  testParseModule env fname contents
 
 end Parser
 end Lean

src/Lean/Server/Snapshots.lean

@@ -78,8 +78,11 @@ through the file. -/
 -- isServer? conditionals and not be worth it due to how short it is.
 def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot MessageLog) := do
   let inputCtx := Parser.mkInputContext contents "<input>";
+  let cmdState := snap.toCmdState;
+  let scope := cmdState.scopes.head!
+  let pmctx := { env := cmdState.env, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
   let (cmdStx, cmdParserState, msgLog) :=
-    Parser.parseCommand snap.env inputCtx snap.mpState snap.msgLog;
+    Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog;
   let cmdPos := cmdStx.getHeadInfo.get!.pos.get!; -- TODO(WN): always `some`?
   if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then
     pure $ Sum.inr msgLog

src/shell/lean.cpp

@@ -332,11 +332,6 @@ public:
 };
 
 namespace lean {
-extern "C" object* lean_test_module_parser(object* env, object* input, object* filename, uint8 displayCtx, object* w);
-bool test_module_parser(environment const & env, std::string const & input, std::string const & filename) {
-    return get_io_scalar_result<bool>(lean_test_module_parser(env.to_obj_arg(), mk_string(input), mk_string(filename), false, io_mk_world()));
-}
-
 typedef list_ref<object_ref> messages;
 typedef object_ref module_stx;
 extern "C" object * lean_run_frontend(object * input, object * opts, object * filename, object * main_module_name, object * w);

tests/lean/Reformat.lean

@@ -12,10 +12,10 @@ let (debug, f) : Bool × String := match args with
   | [f]       => (false, f)
   | _         => panic! "usage: file [-d]"
 let env ← mkEmptyEnvironment
-let stx ← Lean.Parser.parseFile env args.head!
+let stx ← Lean.Parser.testParseFile env args.head!
 let (f, _) ← (tryFinally (PrettyPrinter.ppModule stx) printTraces).toIO { options := Options.empty.setBool `trace.PrettyPrinter.format debug } { env := env }
 IO.print f
-let stx' ← Lean.Parser.parseModule env args.head! (toString f)
+let stx' ← Lean.Parser.testParseModule env args.head! (toString f)
 if stx' != stx then
   let stx := stx.getArg 1
   let stx' := stx'.getArg 1

tests/lean/run/Reparen.lean

@@ -23,7 +23,7 @@ let (debug, f) : Bool × String := match args with
   | [f]       => (false, f)
   | _         => panic! "usage: file [-d]";
 let env ← mkEmptyEnvironment;
-let stx ← Lean.Parser.parseFile env args.head!;
+let stx ← Lean.Parser.testParseFile env args.head!;
 let header := stx.getArg 0;
 let some s ← pure header.reprint | throw $ IO.userError "header reprint failed";
 IO.print s;

tests/lean/run/parsePrelude.lean

@@ -1,4 +1,3 @@
-#lang lean4
 import Lean.Parser
 
 def test : IO Unit :=
@@ -6,7 +5,7 @@ if System.Platform.isWindows then
   pure () -- TODO investigate why the following doesn't work on Windows
 else do
   let env ← Lean.mkEmptyEnvironment;
-  Lean.Parser.parseFile env (System.mkFilePath ["..", "..", "..", "src", "Init", "Prelude.lean"]);
+  Lean.Parser.testParseFile env (System.mkFilePath ["..", "..", "..", "src", "Init", "Prelude.lean"]);
   IO.println "done"
 
 #eval test