From 4380d4a9dad2c453da7d14533e6941be7eac1295 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 16 Dec 2020 23:15:25 +0100 Subject: [PATCH] feat: parser: store options & pass to `evalConst` --- src/Lean/Elab/Frontend.lean | 2 +- src/Lean/Parser/Basic.lean | 5 +++-- src/Lean/Parser/Extension.lean | 2 +- src/Lean/Parser/Module.lean | 4 ++-- src/Lean/PrettyPrinter/Formatter.lean | 11 ++++++++--- src/Lean/Server/Snapshots.lean | 2 +- stage0/src/library/compiler/ir_interpreter.cpp | 2 +- 7 files changed, 17 insertions(+), 11 deletions(-) diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean index df70a9ef3d..52d8dda5cf 100644 --- a/src/Lean/Elab/Frontend.lean +++ b/src/Lean/Elab/Frontend.lean @@ -50,7 +50,7 @@ def processCommand : FrontendM Bool := do let ictx ← getInputContext let pstate ← getParserState let scope := cmdState.scopes.head! - let pmctx := { env := cmdState.env, currNamespace := scope.currNamespace, openDecls := scope.openDecls } + let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } let pos := ictx.fileMap.toPosition pstate.pos match profileit "parsing" pos fun _ => Parser.parseCommand ictx pmctx pstate cmdState.messages with | (cmd, ps, messages) => diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean index f3b6572312..01de5caf48 100644 --- a/src/Lean/Parser/Basic.lean +++ b/src/Lean/Parser/Basic.lean @@ -121,6 +121,7 @@ structure InputContext where /-- Input context derived from elaboration of previous commands. -/ structure ParserModuleContext where env : Environment + options : Options -- for name lookup currNamespace : Name := Name.anonymous openDecls : List OpenDecl := [] @@ -1704,8 +1705,8 @@ def categoryParserOfStack (offset : Nat) (prec : Nat := 0) : Parser := { fn := fun c s => categoryParserOfStackFn offset { c with prec := prec } s } unsafe def evalParserConstUnsafe (declName : Name) : ParserFn := fun ctx s => - match ctx.env.evalConstCheck Parser {} `Lean.Parser.Parser declName <|> - ctx.env.evalConstCheck Parser {} `Lean.Parser.TrailingParser declName with + match ctx.env.evalConstCheck Parser ctx.options `Lean.Parser.Parser declName <|> + ctx.env.evalConstCheck Parser ctx.options `Lean.Parser.TrailingParser declName with | Except.ok p => p.fn ctx s | Except.error e => s.mkUnexpectedError s!"error running parser {declName}: {e}" diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 8d9329da77..00e3d12251 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -407,7 +407,7 @@ def mkParserState (input : String) : ParserState := /- convenience function for testing -/ def runParserCategory (env : Environment) (catName : Name) (input : String) (fileName := "") : Except String Syntax := - let c := mkParserContext (mkInputContext input fileName) { env := env } + let c := mkParserContext (mkInputContext input fileName) { env := env, options := {} } let s := mkParserState input let s := whitespace c s let s := categoryParserFnImpl catName c s diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean index 32f651d031..bb045607ad 100644 --- a/src/Lean/Parser/Module.lean +++ b/src/Lean/Parser/Module.lean @@ -39,7 +39,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 inputCtx { env := dummyEnv } + let ctx := mkParserContext inputCtx { env := dummyEnv, options := {} } let ctx := Module.updateTokens ctx let s := mkParserState ctx.input let s := whitespace ctx s @@ -107,7 +107,7 @@ partial def parseCommand (inputCtx : InputContext) (pmctx : ParserModuleContext) 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 inputCtx { env := env } state msgs with + match parseCommand inputCtx { env := env, options := {} } state msgs with | (stx, state, msgs) => if isEOI stx then if msgs.isEmpty then diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 2a6b45cc10..9cda686758 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -236,9 +236,14 @@ def trailingNode.formatter (k : SyntaxNodeKind) (_ : Nat) (p : Formatter) : Form categoryParser.formatter `foo def parseToken (s : String) : FormatterM ParserState := do - let ctx ← read - let env ← getEnv - pure $ Parser.tokenFn { input := s, fileName := "", fileMap := FileMap.ofString "", prec := 0, env := env, tokens := ctx.table } (Parser.mkParserState s) + Parser.tokenFn { + input := s, + fileName := "", + fileMap := FileMap.ofString "", + prec := 0, + env := ← getEnv, + options := ← getOptions, + tokens := (← read).table } (Parser.mkParserState s) def pushTokenCore (tk : String) : FormatterM Unit := do if tk.toSubstring.dropRightWhile (fun s => s == ' ') == tk.toSubstring then diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index c31cb6c674..53dcd501d6 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/src/Lean/Server/Snapshots.lean @@ -80,7 +80,7 @@ def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot Mess let inputCtx := Parser.mkInputContext contents ""; let cmdState := snap.toCmdState; let scope := cmdState.scopes.head! - let pmctx := { env := cmdState.env, currNamespace := scope.currNamespace, openDecls := scope.openDecls } + let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls } let (cmdStx, cmdParserState, msgLog) := Parser.parseCommand inputCtx pmctx snap.mpState snap.msgLog; let cmdPos := cmdStx.getHeadInfo.get!.pos.get!; -- TODO(WN): always `some`? diff --git a/stage0/src/library/compiler/ir_interpreter.cpp b/stage0/src/library/compiler/ir_interpreter.cpp index 5fde882707..c00e44e935 100644 --- a/stage0/src/library/compiler/ir_interpreter.cpp +++ b/stage0/src/library/compiler/ir_interpreter.cpp @@ -48,7 +48,7 @@ functions, which have a (relatively) homogeneous ABI that we can use without run #include "util/option_declarations.h" #ifndef LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE -#if LEAN_IS_STAGE0 == 1 +#if false // We already set `-Dinterpreter.prefer_native=false` in stdlib.make, but also set it here as a default when we use stage 0 in the editor #define LEAN_DEFAULT_INTERPRETER_PREFER_NATIVE false #else