DelabHoare

This module provides delaborators for MRiscX Hoare triples.

def MRiscX.annotateStateFns (e : Lean.Expr) : Lean.Expr

Annotate applications of the MState accessor functions in e so that the delaborator can pretty-print them with the dedicated Hoare-state notation.

Equations

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

def MRiscX.termToIdent (t : Lean.Term) : Option (Lean.TSyntax `ident)

Reinterpret a term as an identifier syntax, if it is one.

Equations

• MRiscX.termToIdent t = if t.raw.isIdent = true then some { raw := t.raw } else none

def MRiscX.extractStringFromTerm (t : Lean.Term) : Option (Lean.TSyntax `ident)

Extract the string literal carried by t as an identifier, if t is one.

Equations

• MRiscX.extractStringFromTerm t = match t.raw.isStrLit? with | some s => some (Lean.mkIdent (Lean.Name.mkSimple s)) | x => none

def MRiscX.termToMriscxSyntax (t : Lean.Term) : Option (Lean.TSyntax `mriscxSyntax)

Reinterpret a term as a parsed MRiscX assembly block, if it has that kind.

Equations

• MRiscX.termToMriscxSyntax t = if (t.raw.getKind == `mriscxSyntaxBlock) = true then some { raw := t.raw } else none

def MRiscX.hoareTermToTerm (t : Lean.TSyntax `hoareTerm) : Lean.PrettyPrinter.Delaborator.DelabM Lean.Term

Coerce a parsed Hoare term back into a plain term during delaboration.

Equations

• MRiscX.hoareTermToTerm t = pure { raw := t.raw }

def MRiscX.stateFnsDelab : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for the annotated MState accessor functions, rendering them with the dedicated Hoare-state notation (x[_], mem[_], ⸨pc⸩, ...).

Equations

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

def MRiscX.hasNestedLambdaBody (e : Lean.Expr) : Bool

Whether e is a lambda whose body is itself headed by a lambda.

Equations

• MRiscX.hasNestedLambdaBody e = if e.isLambda = true then e.bindingBody!.getAppFn.isLambda else false

def MRiscX.mkAssertionAtN (n : ℕ) (stName : Lean.Name) (withAnnotatedBody : Lean.PrettyPrinter.Delaborator.Delab → Lean.PrettyPrinter.Delaborator.Delab) : Lean.PrettyPrinter.Delaborator.DelabM Lean.Term

Delaborate the assertion stored at argument position n of a Hoare triple, threading the bound state name stName and an annotated-body transformer.

Equations

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

def MRiscX.hoareTripleDelab : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for hoareTripleUp, rendering it with the surface Hoare-triple notation ⦃P⦄ l ↦ ⟨L_w | L_b⟩ ⦃Q⦄.

Equations

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

def MRiscX.isOnlyStateIdent (s : Lean.TSyntax `term) : Bool

Whether the term s is exactly the bound state identifier st.

Equations

• MRiscX.isOnlyStateIdent s = if s.raw.matchesIdent `st = true then true else have __discr := s; false

def MRiscX.IncPcUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander rendering MState.incPc applications with the pc++ assignment notation.

Equations

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

def MRiscX.AddRegUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander rendering MState.addRegister applications with the x[_] ← _ notation.

Equations

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

def MRiscX.AddMemUnexpander : Lean.PrettyPrinter.Unexpander

Unexpander rendering MState.addMemory applications with the mem[_] ← _ notation.

Equations

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