EvalLabelInHoare

This module provides label resolution inside MRiscX Hoare syntax.

def replaceLabels (stx : Lean.Term) (labels : LabelMap) : Lean.Elab.TermElabM Lean.Syntax

Replace each label name in stx with the program-counter index it maps to.

Equations

• replaceLabels stx labels = Lean.withFreshMacroScope do let __x ← (replaceLabelsGo✝ (syntaxSize✝ stx.raw) stx.raw).run labels match __x with | (newStx, snd) => pure newStx

def replaceLabelsWithCodeExpr (stx : Lean.Term) (e : Lean.Expr) : Lean.Elab.TermElabM Lean.Syntax

Resolve labels in stx using the label map embedded in the code expression e.

Equations

• replaceLabelsWithCodeExpr stx e = if e.isFVar = true then pure stx.raw else do let labels ← liftM (getLabelMapFromCodeExpr e) replaceLabels stx labels

def replaceLabelsWithIdent (stx : Lean.Term) (i : Lean.Ident) : Lean.Elab.TermElabM Lean.Syntax

Resolve labels in stx using the code referred to by identifier i.

Equations

• replaceLabelsWithIdent stx i = do let e ← Lean.Elab.Term.elabTerm i.raw none replaceLabelsWithCodeExpr stx e