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.

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)
• 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

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

Equations

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

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) : Strata.DiagnosticModel

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

Equations

• md.toDiagnostic msg = match Imperative.getFileRange md with | some fr => Strata.DiagnosticModel.withRange fr (Std.Format.text msg) | none => Strata.DiagnosticModel.fromMessage msg

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

Create a DiagnosticModel from metadata and a Format message.

Equations

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

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 ""