MetaData

The Imperative dialect has a mechanism to store metadata in each of its constructs. Metadata can be used to track both syntactic facts obtained during translation from the source program to this dialect (e.g., line and column numbers), or semantic facts derived during analyses (e.g., global variables implicitly modified by a language construct).

inductive Imperative.MetaDataElem.Field (P : PureExpr) : Type

A metadata field, which can be either a variable or an arbitrary string label.

For now, we only track the variables modified by a construct, but we will expand this in the future.

• var {P : PureExpr} (v : P.Ident) : Field P

  Metadata indexed by a Strata variable.

• label {P : PureExpr} (l : String) : Field P

  Metadata indexed by an arbitrary label.

def Imperative.MetaDataElem.Field.beq {P : PureExpr} [BEq P.Ident] (f1 f2 : Field P) : Bool

Equations

• (Imperative.MetaDataElem.Field.var v1).beq (Imperative.MetaDataElem.Field.var v2) = (v1 == v2)
• (Imperative.MetaDataElem.Field.label l1).beq (Imperative.MetaDataElem.Field.label l2) = (l1 == l2)
• f1.beq f2 = false

instance Imperative.instBEqField {P : PureExpr} [BEq P.Ident] : BEq (MetaDataElem.Field P)

Equations

• Imperative.instBEqField = { beq := fun (f1 f2 : Imperative.MetaDataElem.Field P) => f1.beq f2 }

theorem Imperative.MetaDataElem.Field.beq_eq {P : PureExpr} [DecidableEq P.Ident] (f1 f2 : Field P) : f1.beq f2 = true ↔ f1 = f2

instance Imperative.instDecidableEqField {P : PureExpr} [DecidableEq P.Ident] : DecidableEq (MetaDataElem.Field P)

Equations

• Imperative.instDecidableEqField = beq_eq_DecidableEq Imperative.MetaDataElem.Field.beq ⋯

instance Imperative.instToFormatField {P : PureExpr} [Std.ToFormat P.Ident] : Std.ToFormat (MetaDataElem.Field P)

Equations

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

instance Imperative.instReprField {P : PureExpr} [Repr P.Ident] : Repr (MetaDataElem.Field P)

Equations

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

inductive Imperative.MetaDataElem.Value (P : PureExpr) : Type

A metadata value, which can be either an expression, a message, or a fileRange

• expr {P : PureExpr} (e : P.Expr) : Value P

  Metadata value in the form of a structured expression.

• msg {P : PureExpr} (s : String) : Value P

  Metadata value in the form of an arbitrary string.

• fileRange {P : PureExpr} (r : Strata.FileRange) : Value P

  Metadata value in the form of a fileRange.

• switch {P : PureExpr} (b : Bool) : Value P

  Metadata value in the form of a boolean switch.

instance Imperative.instToFormatValue {P : PureExpr} [Std.ToFormat P.Expr] : Std.ToFormat (MetaDataElem.Value P)

Equations

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

instance Imperative.instReprValue {P : PureExpr} [Repr P.Expr] : Repr (MetaDataElem.Value P)

Equations

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

def Imperative.MetaDataElem.Value.beq {P : PureExpr} [BEq P.Expr] (v1 v2 : Value P) : Bool

Equations

• (Imperative.MetaDataElem.Value.expr e1).beq (Imperative.MetaDataElem.Value.expr e2) = (e1 == e2)
• (Imperative.MetaDataElem.Value.msg m1).beq (Imperative.MetaDataElem.Value.msg m2) = (m1 == m2)
• (Imperative.MetaDataElem.Value.fileRange r1).beq (Imperative.MetaDataElem.Value.fileRange r2) = (r1 == r2)
• (Imperative.MetaDataElem.Value.switch b1).beq (Imperative.MetaDataElem.Value.switch b2) = (b1 == b2)
• v1.beq v2 = false

instance Imperative.instBEqValue {P : PureExpr} [BEq P.Expr] : BEq (MetaDataElem.Value P)

Equations

• Imperative.instBEqValue = { beq := fun (v1 v2 : Imperative.MetaDataElem.Value P) => v1.beq v2 }

theorem Imperative.MetaDataElem.Value.beq_eq {P : PureExpr} [DecidableEq P.Expr] (v1 v2 : Value P) : v1.beq v2 = true ↔ v1 = v2

instance Imperative.instDecidableEqValue {P : PureExpr} [DecidableEq P.Expr] : DecidableEq (MetaDataElem.Value P)

Equations

• Imperative.instDecidableEqValue = beq_eq_DecidableEq Imperative.MetaDataElem.Value.beq ⋯

structure Imperative.MetaDataElem (P : PureExpr) : Type

A metadata element

• fld : Field P

  The field or key used to identify the metadata.

• value : Value P

  The value of the metadata.

@[reducible, inline]

abbrev Imperative.MetaData (P : PureExpr) : Type

Metadata is an array of tagged elements.

Equations

• Imperative.MetaData P = Array (Imperative.MetaDataElem P)

def Imperative.MetaData.empty {P : PureExpr} : MetaData P

Equations

• Imperative.MetaData.empty = #[]

def Imperative.MetaData.pushElem {P : PureExpr} (md : MetaData P) (fld : MetaDataElem.Field P) (value : MetaDataElem.Value P) : MetaData P

Push a new metadata element.

Equations

• md.pushElem fld value = Array.push md { fld := fld, value := value }

def Imperative.MetaData.eraseElem {P : PureExpr} [BEq P.Ident] (md : MetaData P) (fld : MetaDataElem.Field P) : MetaData P

Remove the first metadata element with tag fld.

Equations

• md.eraseElem fld = Array.eraseP md fun (e : Imperative.MetaDataElem P) => e.fld == fld

def Imperative.MetaData.findElem {P : PureExpr} [BEq P.Ident] (md : MetaData P) (fld : MetaDataElem.Field P) : Option (MetaDataElem P)

Retrieve the first metadata element with tag fld.

Equations

• md.findElem fld = Array.find? (fun (e : Imperative.MetaDataElem P) => e.fld == fld) md

def Imperative.MetaDataElem.beq {P : PureExpr} [DecidableEq P.Ident] [DecidableEq P.Expr] (e1 e2 : MetaDataElem P) : Bool

Equations

• e1.beq e2 = (e1.fld.beq e2.fld && e1.value.beq e2.value)

theorem Imperative.MetaDataElem.beq_eq {P : PureExpr} [DecidableEq P.Ident] [DecidableEq P.Expr] (e1 e2 : MetaDataElem P) : e1.beq e2 = true ↔ e1 = e2

instance Imperative.instDecidableEqMetaDataElem {P : PureExpr} [DecidableEq P.Ident] [DecidableEq P.Expr] : DecidableEq (MetaDataElem P)

Equations

• Imperative.instDecidableEqMetaDataElem = beq_eq_DecidableEq Imperative.MetaDataElem.beq ⋯

instance Imperative.instToFormatMetaDataElemOfFieldOfValue {P : PureExpr} [Std.ToFormat (MetaDataElem.Field P)] [Std.ToFormat (MetaDataElem.Value P)] : Std.ToFormat (MetaDataElem P)

Equations

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

instance Imperative.instToFormatMetaDataOfMetaDataElem {P : PureExpr} [Std.ToFormat (MetaDataElem P)] : Std.ToFormat (MetaData P)

Equations

• Imperative.instToFormatMetaDataOfMetaDataElem = { format := fun (md : Imperative.MetaData P) => if Array.isEmpty md = true then Std.format "" else Std.format md ++ Std.format " " }

instance Imperative.instReprMetaDataElem {P : PureExpr} [Repr P.Expr] [Repr P.Ident] : Repr (MetaDataElem P)

Equations

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

Common metadata fields

@[reducible, match_pattern, inline]

abbrev Imperative.MetaData.message {P : PureExpr} : MetaDataElem.Field P

Equations

• Imperative.MetaData.message = Imperative.MetaDataElem.Field.label "message"

@[reducible, match_pattern, inline]

abbrev Imperative.MetaData.fileRange {P : PureExpr} : MetaDataElem.Field P

Equations

• Imperative.MetaData.fileRange = Imperative.MetaDataElem.Field.label "fileRange"

@[reducible, match_pattern, inline]

abbrev Imperative.MetaData.reachCheck {P : PureExpr} : MetaDataElem.Field P

Equations

• Imperative.MetaData.reachCheck = Imperative.MetaDataElem.Field.label "reachCheck"

@[reducible, match_pattern, inline]

abbrev Imperative.MetaData.fullCheck {P : PureExpr} : MetaDataElem.Field P

Equations

• Imperative.MetaData.fullCheck = Imperative.MetaDataElem.Field.label "fullCheck"

@[reducible, match_pattern, inline]

abbrev Imperative.MetaData.validityCheck {P : PureExpr} : MetaDataElem.Field P

Equations

• Imperative.MetaData.validityCheck = Imperative.MetaDataElem.Field.label "validityCheck"

@[reducible, match_pattern, inline]

abbrev Imperative.MetaData.satisfiabilityCheck {P : PureExpr} : MetaDataElem.Field P

Equations

• Imperative.MetaData.satisfiabilityCheck = Imperative.MetaDataElem.Field.label "satisfiabilityCheck"

def Imperative.MetaData.hasReachCheck {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Bool

Equations

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

def Imperative.MetaData.hasFullCheck {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Bool

Equations

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

def Imperative.MetaData.hasValidityCheck {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Bool

Equations

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

def Imperative.MetaData.hasSatisfiabilityCheck {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Bool

Equations

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

def Imperative.getFileRange {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Option Strata.FileRange

Equations

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

def Imperative.MetaData.toDiagnostic {P : PureExpr} [BEq P.Ident] (md : MetaData P) (msg : String) (type : Strata.DiagnosticType := Strata.DiagnosticType.UserError) : Strata.DiagnosticModel

Create a DiagnosticModel from metadata and a message. Uses the file range from metadata if available, otherwise uses a default location.

Equations

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

def Imperative.MetaData.toDiagnosticF {P : PureExpr} [BEq P.Ident] (md : MetaData P) (msg : Std.Format) (type : Strata.DiagnosticType := Strata.DiagnosticType.UserError) : Strata.DiagnosticModel

Create a DiagnosticModel from metadata and a Format message.

Equations

• md.toDiagnosticF msg type = md.toDiagnostic (toString msg) type

def Imperative.MetaData.formatFileRangeD {P : PureExpr} [BEq P.Ident] (md : MetaData P) (fileMap : Option Lean.FileMap := none) (includeEnd? : Bool := false) : Std.Format

Get the file range from metadata as a DiagnosticModel (for formatting). This is a compatibility function that formats the file range using byte offsets. For proper line/column display, use toDiagnostic and format with a FileMap at the top level.

Equations

• md.formatFileRangeD fileMap includeEnd? = match Imperative.getFileRange md with | some fr => fr.format fileMap includeEnd? | none => Std.format ""

def Imperative.MetaData.relatedFileRange {P : PureExpr} : MetaDataElem.Field P

Metadata field for a related file range (e.g., the original assertion location when the primary file range points to the call site after inlining). There can be multiple relatedFileRange fields in a single metadata due to multiple levels of inlining.

Equations

• Imperative.MetaData.relatedFileRange = Imperative.MetaDataElem.Field.label "relatedFileRange"

def Imperative.getRelatedFileRanges {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Array Strata.FileRange

Get all related file ranges from metadata, in order. The returned array's order is determined by the call stack: the innermost (most deeply inlined) call comes first.

Equations

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

def Imperative.MetaData.eraseAllElems {P : PureExpr} [BEq P.Ident] (md : MetaData P) (fld : MetaDataElem.Field P) : MetaData P

Remove all metadata elements with the given field.

Equations

• md.eraseAllElems fld = Array.filter (fun (e : Imperative.MetaDataElem P) => !e.fld == fld) md

def Imperative.MetaData.setCallSiteFileRange {P : PureExpr} [BEq P.Ident] (md callSiteRange : MetaData P) : MetaData P

Replace the primary file range with a new one, shifting existing related file ranges and prepending the old primary range.

Equations

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

def Imperative.MetaData.propertyType {P : PureExpr} : MetaDataElem.Field P

Metadata field for property type classification (e.g., "divisionByZero").

Equations

• Imperative.MetaData.propertyType = Imperative.MetaDataElem.Field.label "propertyType"

def Imperative.MetaData.divisionByZero : String

Metadata value for division-by-zero property type classification.

Equations

• Imperative.MetaData.divisionByZero = "divisionByZero"

def Imperative.MetaData.getPropertyType {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Option String

Read the property type classification from metadata, if present.

Equations

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

def Imperative.MetaData.propertySummary {P : PureExpr} : MetaDataElem.Field P

Metadata field for property summaries attached to assert/requires/ensures clauses.

Equations

• Imperative.MetaData.propertySummary = Imperative.MetaDataElem.Field.label "propertySummary"

def Imperative.MetaData.getPropertySummary {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Option String

Read the property summary from metadata, if present.

Equations

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

def Imperative.MetaData.withPropertySummary {P : PureExpr} (md : MetaData P) (msg : String) : MetaData P

Push a property summary into metadata.

Equations

• md.withPropertySummary msg = md.pushElem Imperative.MetaData.propertySummary (Imperative.MetaDataElem.Value.msg msg)