def StrataDDM.Parser.TokenTable.addParser (tt : Lean.Parser.TokenTable) (p : Parser) : Lean.Parser.TokenTable

Equations

• StrataDDM.Parser.TokenTable.addParser tt p = List.foldl (fun (tt : Lean.Parser.TokenTable) (t : String) => Lean.Data.Trie.insert tt t t) tt (p.info.collectTokens [])

def StrataDDM.Parser.stringInputContext (fileName : System.FilePath) (contents : String) : InputContext

Create an input context from a string.

Equations

• StrataDDM.Parser.stringInputContext fileName contents = { inputString := contents, fileName := fileName.toString, fileMap := Lean.FileMap.ofString contents, endPos_valid := ⋯ }

def StrataDDM.Parser.strataIsIdFirst (c : Char) : Bool

The characters an identifier may begin with. With strataIsIdRest, this is the alphabet the lexer accepts unquoted.

Equations

• StrataDDM.Parser.strataIsIdFirst c = (c.isAlpha || c == '_' || c == '$')

def StrataDDM.Parser.strataIsIdRest (c : Char) : Bool

The characters an identifier may continue with. Wider than strataIsIdFirst, and note it admits ', so a primed name such as x' lexes bare.

Equations

• StrataDDM.Parser.strataIsIdRest c = (c.isAlphanum || c == '_' || c == '\'' || c == '.' || c == '?' || c == '!' || c == '$' || c == '@')

def StrataDDM.Parser.charLitFnAux (startPos : String.Pos.Raw) : Lean.Parser.ParserFn

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.identFnAux (startPos : String.Pos.Raw) (tk : Option Lean.Parser.Token) : Lean.Parser.ParserFn

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.decimalNumberFn (startPos : String.Pos.Raw) (c : Lean.Parser.ParserContext) : Lean.Parser.ParserState → Lean.Parser.ParserState

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.binNumberFn (startPos : String.Pos.Raw) : Lean.Parser.ParserFn

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.octalNumberFn (startPos : String.Pos.Raw) : Lean.Parser.ParserFn

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.isHexDigit (c : Char) : Bool

Equations

• StrataDDM.Parser.isHexDigit c = (decide ('0' ≤ c) && decide (c ≤ '9') || decide ('a' ≤ c) && decide (c ≤ 'f') || decide ('A' ≤ c) && decide (c ≤ 'F'))

def StrataDDM.Parser.hexNumberFn (startPos : String.Pos.Raw) : Lean.Parser.ParserFn

Equations

• StrataDDM.Parser.hexNumberFn startPos c s = StrataDDM.Parser.mkNodeToken✝ Lean.numLitKind startPos c (StrataDDM.Parser.takeDigitsFn✝ StrataDDM.Parser.isHexDigit "hexadecimal number" true c s)

def StrataDDM.Parser.numberFnAux : Lean.Parser.ParserFn

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev StrataDDM.Parser.bytesLitKind : Lean.SyntaxNodeKind

Equations

• StrataDDM.Parser.bytesLitKind = `bytes

def StrataDDM.Parser.parseByteContent (startPos : String.Pos.Raw) : Lean.Parser.ParserFn

Equations

• One or more equations did not get rendered due to their size.

partial def StrataDDM.Parser.strLitFnAux (startPos : String.Pos.Raw) : Lean.Parser.ParserFn

def StrataDDM.Parser.tokenFn (expected : List String := []) : Lean.Parser.ParserFn

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.expectTokenFn (k : Lean.SyntaxNodeKind) (desc : String) : Lean.Parser.ParserFn

Parses a token and asserts the result is of the given kind. desc is used in error messages as the token kind.

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.satisfySymbolFn (p : String → Bool) (expected : List String) : Lean.Parser.ParserFn

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.symbolFnAux (sym errorMsg : String) : Lean.Parser.ParserFn

Equations

• StrataDDM.Parser.symbolFnAux sym errorMsg = StrataDDM.Parser.satisfySymbolFn (fun (s : String) => s == sym) [errorMsg]

def StrataDDM.Parser.symbolFn (sym : String) : Lean.Parser.ParserFn

Equations

• StrataDDM.Parser.symbolFn sym = StrataDDM.Parser.symbolFnAux sym ("'" ++ sym ++ "'")

def StrataDDM.Parser.symbolNoAntiquot (sym : String) : Parser

Equations

• StrataDDM.Parser.symbolNoAntiquot sym = { info := Lean.Parser.symbolInfo sym, fn := StrataDDM.Parser.symbolFn sym }

def StrataDDM.Parser.identifier : Parser

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.numLit : Parser

Equations

• StrataDDM.Parser.numLit = { info := Lean.Parser.mkAtomicInfo "num", fn := StrataDDM.Parser.expectTokenFn Lean.numLitKind "numeral" }

def StrataDDM.Parser.byteArray : Parser

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.decimalLit : Parser

Equations

• StrataDDM.Parser.decimalLit = { info := Lean.Parser.mkAtomicInfo "scientific", fn := StrataDDM.Parser.expectTokenFn Lean.scientificLitKind "scientific number" }

def StrataDDM.Parser.strLit : Parser

Equations

• StrataDDM.Parser.strLit = { info := Lean.Parser.mkAtomicInfo "str", fn := StrataDDM.Parser.expectTokenFn Lean.strLitKind "string literal" }

def StrataDDM.Parser.identName (nm : QualifiedIdent) : Lean.Name

Equations

• StrataDDM.Parser.identName nm = (Lean.Name.anonymous.str nm.dialect).str nm.name

def StrataDDM.Parser.peekTokenAux (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState × Except Lean.Parser.ParserState Lean.Syntax

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.peekToken (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState × Except Lean.Parser.ParserState Lean.Syntax

Equations

• StrataDDM.Parser.peekToken c s = if (s.cache.tokenCache.startPos == s.pos) = true then (s, Except.ok s.cache.tokenCache.token) else StrataDDM.Parser.peekTokenAux c s

def StrataDDM.Parser.indexed {α : Type} (map : Lean.Parser.TokenMap α) (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) (behavior : Lean.Parser.LeadingIdentBehavior) : Lean.Parser.ParserState × List α

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.longestMatchMkResult (startSize : Nat) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

Equations

• StrataDDM.Parser.longestMatchMkResult startSize s = if s.stackSize > startSize + 1 then s.mkNode Lean.choiceKind startSize else s

def StrataDDM.Parser.longestMatchFnAux (left? : Option Lean.Syntax) (startSize startLhsPrec : Nat) (startPos : String.Pos.Raw) (prevPrio : Nat) (ps : List (Parser × Nat)) : Lean.Parser.ParserFn

Equations

• StrataDDM.Parser.longestMatchFnAux left? startSize startLhsPrec startPos prevPrio ps = StrataDDM.Parser.longestMatchFnAux.parse✝ left? startSize startLhsPrec startPos prevPrio ps

def StrataDDM.Parser.longestMatchFn (left? : Option Lean.Syntax) : List (Parser × Nat) → Lean.Parser.ParserFn

Equations

• One or more equations did not get rendered due to their size.
• StrataDDM.Parser.longestMatchFn left? [] = fun (x : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) => s.mkError "longestMatch: empty list"
• StrataDDM.Parser.longestMatchFn left? [p] = fun (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) => Lean.Parser.runLongestMatchParser left? s.lhsPrec p.fst.fn c s

def StrataDDM.Parser.leadingParserAux (cat : QualifiedIdent) (tables : Lean.Parser.PrattParsingTables) (behavior : Lean.Parser.LeadingIdentBehavior) : Lean.Parser.ParserFn

Equations

• One or more equations did not get rendered due to their size.

partial def StrataDDM.Parser.trailingLoop (cat : QualifiedIdent) (tables : Lean.Parser.PrattParsingTables) (c : Lean.Parser.ParserContext) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

def StrataDDM.Parser.prattParser (cat : QualifiedIdent) (tables : Lean.Parser.PrattParsingTables) (behavior : Lean.Parser.LeadingIdentBehavior) : Lean.Parser.ParserFn

Implements a variant of Pratt's algorithm. In Pratt's algorithms tokens have a right and left binding power. In our implementation, parsers have precedence instead. This method selects a parser (or more, via longestMatchFn) from leadingTable based on the current token. Note that the unindexed leadingParsers parsers are also tried. We have the unidexed leadingParsers because some parsers do not have a "first token". Example:

syntax term:51 "≤" ident "<" term "|" term : index

Example, in principle, the set of first tokens for this parser is any token that can start a term, but this set is always changing. Thus, this parsing rule is stored as an unindexed leading parser at leadingParsers. After processing the leading parser, we chain with parsers from trailingTable/trailingParsers that have precedence at least c.prec where c is the ParsingContext. Recall that c.prec is set by categoryParser.

Note that in the original Pratt's algorithm, precedences are only checked before calling trailing parsers. In our implementation, leading and trailing parsers check the precedence. We claim our algorithm is more flexible, modular and easier to understand.

antiquotParser should be a mkAntiquot parser (or always fail) and is tried before all other parsers. It should not be added to the regular leading parsers because it would heavily overlap with antiquotation parsers nested inside them.

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.dynamicParser (cat : QualifiedIdent) : Parser

Equations

• One or more equations did not get rendered due to their size.

inductive StrataDDM.Parser.LhsRec : Type

Describes the atoms in a pattern to identify left-recusive syntax.

• isLeading (atoms : List SyntaxDefAtom) : LhsRec

  This atom is not left-recursive and uses the seq atoms.

• isTrailing (minArgPrec : Nat) (remaining : List SyntaxDefAtom) : LhsRec

  This atom is left-recursive The initial argument must have precedence ≥ prec. The remaining syntax is given.

• invalid (message : StrataFormat) : LhsRec

  Classification failed with message

@[implicit_reducible]

instance StrataDDM.Parser.instInhabitedLhsRec : Inhabited LhsRec

Equations

• StrataDDM.Parser.instInhabitedLhsRec = { default := StrataDDM.Parser.instInhabitedLhsRec.default }

def StrataDDM.Parser.instInhabitedLhsRec.default : LhsRec

Equations

• StrataDDM.Parser.instInhabitedLhsRec.default = StrataDDM.Parser.LhsRec.isLeading default

structure StrataDDM.Parser.DeclParser : Type

Information about a parser.

• category : QualifiedIdent
• outerPrec : Nat
• isLeading : Bool
• parser : Parser

class StrataDDM.Parser.ParsingContext : Type

• fixedParsers : Std.HashMap QualifiedIdent Parser

@[implicit_reducible]

instance StrataDDM.Parser.instInhabitedParsingContext : Inhabited ParsingContext

Equations

• StrataDDM.Parser.instInhabitedParsingContext = { default := { } }

@[reducible]

def StrataDDM.Parser.ParsingContext.add (ctx : ParsingContext) (cat : QualifiedIdent) (p : Parser) : ParsingContext

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.ParsingContext.atomCatParser (ctx : ParsingContext) (cat : QualifiedIdent) : Parser

Parser function for given syntax category

Equations

• ctx.atomCatParser cat = match StrataDDM.Parser.ParsingContext.fixedParsers[cat]? with | some p => p | x => StrataDDM.Parser.dynamicParser cat

def StrataDDM.Parser.ParsingContext.manyParser (p : Parser) : Parser

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.ParsingContext.many1Parser (p : Parser) : Parser

Equations

• One or more equations did not get rendered due to their size.

partial def StrataDDM.Parser.ParsingContext.catParser (ctx : ParsingContext) (cat : SyntaxCat) (metadata : Metadata := ∅) : Except SyntaxCat Parser

Parser function for given syntax category

def StrataDDM.Parser.ParsingContext.opSyntaxParser (ctx : ParsingContext) (category ident : QualifiedIdent) (argDecls : ArgDecls) (opStx : SyntaxDef) : Except StrataFormat DeclParser

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.ParsingContext.fnDeclParser (ctx : ParsingContext) (dialect : DialectName) (decl : FunctionDecl) : Except StrataFormat DeclParser

Equations

• ctx.fnDeclParser dialect decl = ctx.opSyntaxParser { dialect := "Init", name := "Expr" } { dialect := dialect, name := decl.name } decl.argDecls decl.syntaxDef

def StrataDDM.Parser.ParsingContext.opDeclParser (ctx : ParsingContext) (dialect : DialectName) (decl : OpDecl) : Except StrataFormat DeclParser

Equations

• ctx.opDeclParser dialect decl = ctx.opSyntaxParser decl.category { dialect := dialect, name := decl.name } decl.argDecls decl.syntaxDef

def StrataDDM.Parser.ParsingContext.mkDialectParsers (ctx : ParsingContext) (d : Dialect) : Except StrataFormat (Array DeclParser)

Equations

• One or more equations did not get rendered due to their size.

def StrataDDM.Parser.runCatParser (tokenTable : Lean.Parser.TokenTable) (parsingTableMap : PrattParsingTableMap) (leanEnv : Lean.Environment) (inputContext : InputContext) (pos stopPos : String.Pos.Raw) (cat : QualifiedIdent) : Lean.Parser.ParserState

Equations

• One or more equations did not get rendered due to their size.