inductive ResolverError : Type

• invalidArgsLen (pos : SourceSpan) (ann : String) (expected nbArgs : ℕ) : ResolverError
• invalidAnnotationType (pos : SourceSpan) (ann expected : String) : ResolverError
• typeParseFailure (pos : SourceSpan) : ResolverError
• expressionParseFailure (pos : SourceSpan) : ResolverError
• invalidMailboxSpecification (pos : SourceSpan) : ResolverError

@[implicit_reducible]

instance instCompilerDiagnosticResolverErrorString : CompilerDiagnostic ResolverError String

Equations

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

inductive Annotation : Type

A subset of general annotations understood by this tool. Each constructor carries its own pos : SourceSpan explicitly rather than using Common/Position.lean's @@/posOf mechanism, which is unsound for nullary constructors such as «@parameter»: they share a single tagged scalar representation, so pointer-identity-based position lookup can't distinguish separate occurrences.

• «@type» (pos : SourceSpan) : SurfaceTLAPlus.Typ → Annotation

  Type information for variables.

• «@mailbox» (pos : SourceSpan) : String → List (SurfaceTLAPlus.Expression (List Annotation)) → Annotation

  Mailbox information for PlusCal processes.

• «@parameter» (pos : SourceSpan) : Annotation

  Functional parameter of a PlusCal process.

@[implicit_reducible]

instance instReprAnnotation : Repr Annotation

Equations

• instReprAnnotation = { reprPrec := instReprAnnotation.repr }

partial def instReprAnnotation.repr : Annotation → ℕ → Std.Format

@[implicit_reducible]

instance instInhabitedAnnotation : Inhabited Annotation

Equations

• instInhabitedAnnotation = { default := instInhabitedAnnotation.default }

partial def instBEqAnnotation.beq : Annotation → Annotation → Bool

@[implicit_reducible]

instance instBEqAnnotation : BEq Annotation

Equations

• instBEqAnnotation = { beq := instBEqAnnotation.beq }

def Annotation.name : Annotation → String

Equations

• (Annotation.«@type» a a_1).name = "@type"
• (Annotation.«@mailbox» a a_1 a_2).name = "@mailbox"
• (Annotation.«@parameter» a).name = "@parameter"

def Annotation.posOf : Annotation → SourceSpan

The position of the comment (group) this annotation was parsed from.

Equations

• (Annotation.«@type» a a_1).posOf = a
• (Annotation.«@mailbox» a a_1 a_2).posOf = a
• (Annotation.«@parameter» a).posOf = a

def resolveAnnotations : SurfaceTLAPlus.Module (SurfacePlusCal.Algorithm (List SurfaceTLAPlus.CommentAnnotation) (SurfaceTLAPlus.Expression (List SurfaceTLAPlus.CommentAnnotation))) (List SurfaceTLAPlus.CommentAnnotation) → Except ResolverError (SurfaceTLAPlus.Module (SurfacePlusCal.Algorithm (List Annotation) (SurfaceTLAPlus.Expression (List Annotation))) (List Annotation))

Equations

• resolveAnnotations = resolveAnnotations'✝