Documentation

Lean.Parser.Module

def Lean.Parser.Module.prelude :

Lean.Parser.Parser

Equations

Lean.Parser.Module.prelude = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "prelude" (some `Lean.Parser.Module.prelude)) (Lean.Parser.leadingNode `Lean.Parser.Module.prelude 1024 (Lean.Parser.symbol "prelude"))

def Lean.Parser.Module.import :

Lean.Parser.Parser

Equations

Lean.Parser.Module.import = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "import" (some `Lean.Parser.Module.import)) (Lean.Parser.leadingNode `Lean.Parser.Module.import 1024 (HAndThen.hAndThen (Lean.Parser.symbol "import ") fun x => HAndThen.hAndThen (Lean.Parser.optional (Lean.Parser.symbol "runtime")) fun x => Lean.Parser.ident))

def Lean.Parser.Module.module :

Lean.Parser.Parser

Equations

Lean.Parser.Module.module = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "module" (some `Lean.Parser.Module.module)) (Lean.Parser.leadingNode `Lean.Parser.Module.module 1024 (HAndThen.hAndThen Lean.Parser.Module.header fun x => Lean.Parser.many (HAndThen.hAndThen Lean.Parser.commandParser fun x => HAndThen.hAndThen Lean.Parser.ppLine fun x => Lean.Parser.ppLine)))

def Lean.Parser.Module.updateTokens (c : Lean.Parser.ParserContext) :

Lean.Parser.ParserContext

Equations

Lean.Parser.Module.updateTokens c = { toInputContext := c.toInputContext, toParserModuleContext := c.toParserModuleContext, prec := c.prec, tokens := match Lean.Parser.addParserTokens c.tokens Lean.Parser.Module.header.info with | Except.ok tables => tables | Except.error x => panicWithPosWithDecl "Lean.Parser.Module" "Lean.Parser.Module.updateTokens" 27 28 "unreachable code has been reached", quotDepth := c.quotDepth, suppressInsideQuot := c.suppressInsideQuot, savedPos? := c.savedPos?, forbiddenTk? := c.forbiddenTk? }

structure Lean.Parser.ModuleParserState :

Type

pos : String.Pos
recovering : Bool

instance Lean.Parser.instInhabitedModuleParserState :

Inhabited Lean.Parser.ModuleParserState

Equations

Lean.Parser.instInhabitedModuleParserState = { default := { pos := default, recovering := default } }

def Lean.Parser.parseHeader (inputCtx : Lean.Parser.InputContext) :

IO (Lean.Syntax × Lean.Parser.ModuleParserState × Lean.MessageLog)

Equations

Lean.Parser.parseHeader inputCtx = do let dummyEnv ← Lean.mkEmptyEnvironment 0 let ctx : Lean.Parser.ParserContext := Lean.Parser.mkParserContext inputCtx { env := dummyEnv, options := { entries := [] }, currNamespace := Lean.Name.anonymous, openDecls := [] } let ctx : Lean.Parser.ParserContext := Lean.Parser.Module.updateTokens ctx let s : Lean.Parser.ParserState := Lean.Parser.mkParserState ctx.toInputContext.input let s : Lean.Parser.ParserState := Lean.Parser.whitespace ctx s let s : Lean.Parser.ParserState := Lean.Parser.Parser.fn Lean.Parser.Module.header ctx s let stx : Lean.Syntax := Array.back s.stxStack match s.errorMsg with | some errorMsg => let msg := Lean.Parser.mkErrorMessage ctx s.pos (toString errorMsg); pure (stx, { pos := s.pos, recovering := true }, Lean.MessageLog.add msg { msgs := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }) | none => pure (stx, { pos := s.pos, recovering := false }, { msgs := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } })

def Lean.Parser.isEOI (s : Lean.Syntax) :

Equations

Lean.Parser.isEOI s = Lean.Syntax.isOfKind s `Lean.Parser.Module.eoi

def Lean.Parser.isExitCommand (s : Lean.Syntax) :

Equations

Lean.Parser.isExitCommand s = Lean.Syntax.isOfKind s `Lean.Parser.Command.exit

def Lean.Parser.topLevelCommandParserFn :

Lean.Parser.ParserFn

Equations

Lean.Parser.topLevelCommandParserFn = Lean.Parser.commandParser.fn

def Lean.Parser.parseCommand (inputCtx : Lean.Parser.InputContext) (pmctx : Lean.Parser.ParserModuleContext) (s : Lean.Parser.ModuleParserState) (messages : Lean.MessageLog) :

Lean.Syntax × Lean.Parser.ModuleParserState × Lean.MessageLog

Equations

Lean.Parser.parseCommand inputCtx pmctx s messages = (fun parse => parse s messages) (Lean.Parser.parseCommand.parse inputCtx pmctx)

partial def Lean.Parser.parseCommand.parse (inputCtx : Lean.Parser.InputContext) (pmctx : Lean.Parser.ParserModuleContext) (s : Lean.Parser.ModuleParserState) (messages : Lean.MessageLog) :

Lean.Syntax × Lean.Parser.ModuleParserState × Lean.MessageLog

def Lean.Parser.testParseModuleAux (env : Lean.Environment) (inputCtx : Lean.Parser.InputContext) (s : Lean.Parser.ModuleParserState) (msgs : Lean.MessageLog) (stxs : Array Lean.Syntax) :

IO (Array Lean.Syntax)

Equations

Lean.Parser.testParseModuleAux env inputCtx s msgs stxs = (fun parse => parse s msgs stxs) (Lean.Parser.testParseModuleAux.parse env inputCtx)

partial def Lean.Parser.testParseModuleAux.parse (env : Lean.Environment) (inputCtx : Lean.Parser.InputContext) (state : Lean.Parser.ModuleParserState) (msgs : Lean.MessageLog) (stxs : Array Lean.Syntax) :

IO (Array Lean.Syntax)

def Lean.Parser.testParseModule (env : Lean.Environment) (fname : String) (contents : String) :

Equations

Lean.Parser.testParseModule env fname contents = let inputCtx := Lean.Parser.mkInputContext contents fname; do let discr ← Lean.Parser.parseHeader inputCtx let x : Lean.Syntax × Lean.Parser.ModuleParserState × Lean.MessageLog := discr match x with | (header, state, messages) => do let cmds ← Lean.Parser.testParseModuleAux env inputCtx state messages #[] let stx : Lean.Syntax := Lean.mkNode `Lean.Parser.Module.module #[header, Lean.mkListNode cmds] pure (Lean.Syntax.updateLeading stx)

def Lean.Parser.testParseFile (env : Lean.Environment) (fname : System.FilePath) :

Equations

Lean.Parser.testParseFile env fname = do let contents ← IO.FS.readFile fname Lean.Parser.testParseModule env fname.toString contents