Parser_.TLAPlus

TLAPlusLexer (Array (Located (Token (Located SurfacePlusCal.Token))))

Lex a full module: raw-skip anything before the header and after the footer, tokenizing only what lies between them — both are ignorable junk by TLA⁺'s own rules, and need not lex as valid tokens at all (an unterminated string in a license preamble, say).

Equations

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

Instances For

source

def SurfaceTLAPlus.Lexer.lexModule (s : String) :

Unexpected Char ⊕ Array (Located' (Token (Located' SurfacePlusCal.Token)))

Equations

SurfaceTLAPlus.Lexer.lexModule s = SurfaceTLAPlus.Lexer.runLexer✝ SurfaceTLAPlus.Lexer.lexModule' s

Instances For

source

def SurfaceTLAPlus.Lexer.lexFragment (s : String) :

Unexpected Char ⊕ Array (Located' (Token (Located' SurfacePlusCal.Token)))

Lex an arbitrary TLA⁺ fragment with no module header or footer of its own, tokenizing straight through to the end of input. Parser_/Annotations.lean's parseMailbox re-lexes a bare expression pulled out of a @mailbox comment this way, as opposed to lexModule, which expects a real module's ---- MODULE <name> ---- … ==== structure.

Equations

SurfaceTLAPlus.Lexer.lexFragment s = SurfaceTLAPlus.Lexer.runLexer✝ (Prod.fst <$> Parser.takeUntil Parser.endOfInput (SurfaceTLAPlus.Lexer.lexeme✝ SurfaceTLAPlus.Lexer.lexToken✝)) s

Instances For

source

@[implicit_reducible]

def SurfaceTLAPlus.Parser.instToStringOrdering_parser_ :

ToString Ordering

Equations

SurfaceTLAPlus.Parser.instToStringOrdering_parser_ = { toString := fun (x : Ordering) => match x with | Ordering.lt => "<" | Ordering.eq => "=" | Ordering.gt => ">" }

Instances For

source

inductive SurfaceTLAPlus.Parser.OperatorOrExpression :

Type

prefix : PrefixOperator → OperatorOrExpression
postfix : PostfixOperator → OperatorOrExpression
infix : InfixOperator → OperatorOrExpression
atom : Expression (List CommentAnnotation) → OperatorOrExpression
index : Bool × List (Expression (List CommentAnnotation)) → OperatorOrExpression

Instances For

source

def SurfaceTLAPlus.Parser.instReprOperatorOrExpression.repr :

OperatorOrExpression → ℕ → Std.Format

Equations

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

Instances For

source

@[implicit_reducible]

instance SurfaceTLAPlus.Parser.instReprOperatorOrExpression :

Repr OperatorOrExpression

Equations

SurfaceTLAPlus.Parser.instReprOperatorOrExpression = { reprPrec := SurfaceTLAPlus.Parser.instReprOperatorOrExpression.repr }

source

class SurfaceTLAPlus.Parser.HasPrecedence (α : Type) :

Type

range : α → ℕ × ℕ
wf (x : α) : (range x).1 ≤ (range x).2

Instances

source

@[implicit_reducible]

instance SurfaceTLAPlus.Parser.instHasPrecedenceLocated {α : Type} [HasPrecedence α] :

HasPrecedence (Located α)

Equations

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

source

def SurfaceTLAPlus.Parser.HasPrecedence.conflicts {α β : Type} [HasPrecedence α] [HasPrecedence β] (x : α) (y : β) :

Bool

Returns true if the precedence range of the two operators overlap, false otherwise.

Equations

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

Instances For

source

def SurfaceTLAPlus.Parser.HasPrecedence.blt {α β : Type} [HasPrecedence α] [HasPrecedence β] (x : α) (y : β) :

Bool

Equations

SurfaceTLAPlus.Parser.HasPrecedence.blt x y = decide ((SurfaceTLAPlus.Parser.HasPrecedence.range x).2 < (SurfaceTLAPlus.Parser.HasPrecedence.range y).1)

Instances For

source

@[implicit_reducible]

instance SurfaceTLAPlus.Parser.instHasPrecedencePrefixOperator :

HasPrecedence PrefixOperator

Equations

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

source

@[implicit_reducible]

instance SurfaceTLAPlus.Parser.instHasPrecedencePostfixOperator :

HasPrecedence PostfixOperator

Equations

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

source

@[implicit_reducible]

instance SurfaceTLAPlus.Parser.instHasPrecedenceInfixOperator :

HasPrecedence InfixOperator

Equations

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

source

inductive SurfaceTLAPlus.Parser.Associativity :

Type

Associativity of an infix operator.

left : Associativity
An operator ⊙ is left-associative if x ⊙ y ⊙ z = (x ⊙ y) ⊙ z.
right : Associativity
An operator ⊙ is right-associative if x ⊙ y ⊙ z = x ⊙ (y ⊙ z).
none : Associativity
An operator ⊙ is non-associative if it does not make sense to write x ⊙ y ⊙ z.

Instances For

source

@[implicit_reducible]

instance SurfaceTLAPlus.Parser.instDecidableEqAssociativity :

DecidableEq Associativity

Equations

SurfaceTLAPlus.Parser.instDecidableEqAssociativity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def SurfaceTLAPlus.Parser.TLAPlus.InfixOperator.assoc :

InfixOperator → Associativity

Maps a TLA+ infix operator to its associativity.

Equations

Instances For

source

def SurfaceTLAPlus.Parser.checkConflicts {α : Type u_1} {β γ σ ε : Type} {m : Type → Type u_2} [Monad m] [HasPrecedence β] [HasPrecedence γ] [Parser.Stream σ α] [Parser.Error ε σ α] [ToString β] [ToString γ] (op₁ : β) (op₂ : γ) :

ParserT ε σ α m PUnit.{1}

Equations

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

Instances For

source

def SurfaceTLAPlus.Parser.shuntingYard (input : List OperatorOrExpression) :

TLAPlusParser (Expression (List CommentAnnotation))

A modified Shunting Yard algorithm: also handles prefix/postfix operators and conflicts between precedence ranges.

Equations

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

Instances For

source

partial def SurfaceTLAPlus.Parser.parseExpression (ws : TLAPlusParser PUnit.{1} := pure ()) (inUpdate : Bool := false) :

TLAPlusParser (Expression (List CommentAnnotation))

source

def SurfaceTLAPlus.Parser.parseModule' :

TLAPlusParser (Module (SurfacePlusCal.Algorithm (List CommentAnnotation) (Expression (List CommentAnnotation))) (List CommentAnnotation))

Parse a full module.

Equations

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

Instances For

source

def SurfaceTLAPlus.Parser.parseModule (tokens : Array (Located' (Token (Located' SurfacePlusCal.Token)))) :

DiagT ParserWarning (Unexpected (Token (Located' SurfacePlusCal.Token))) Id (Module (SurfacePlusCal.Algorithm (List CommentAnnotation) (Expression (List CommentAnnotation))) (List CommentAnnotation))

Parse a full module, always pairing any collected ParserWarnings with the result — whether or not parsing itself succeeded, so a warning emitted before a fatal parse error still reaches the caller. A DiagT in all but name (Id base), ascribed that way so Driver/Modules.lean can absorb it directly via DiagT.lift.

.reverse because ParserWarningM accumulates by prepending (Parser_/Common.lean, modify (w :: ·) — O(1) per warning, unlike appending), so its list is newest-first. Every other pass reports through DiagT, whose bind appends, so warnings elsewhere come out in source order; reversing here is what puts the parser's on that same footing.

Equations

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

Instances For

Documentation

Parser_.TLAPlus

A small lexer for TLA⁺ #

Main parser for a single TLA⁺ module #