HoareAssignmentElab

This module provides elaboration of MRiscX Hoare assignment chains.

def replaceKeywords (stx : Lean.Term) (curState : Lean.TSyntax `term) : Lean.Elab.TermElabM Lean.Syntax

Traverse stx and replace the keyword notations (x[..], mem[..], labels[..], ⸨pc⸩, ⸨terminated⸩) by the corresponding MState function calls on curState.

Equations

• replaceKeywords stx curState = replaceKeywordsAux✝ (assignmentSyntaxSize✝ stx.raw) curState stx.raw

def getHoareAssignmentArray (stx : Lean.TSyntax `hoareAssignmentChain) (curArr : Array (Lean.TSyntax `hoareAssignment)) : Lean.Elab.TermElabM (Array (Lean.TSyntax `hoareAssignment))

Collect every assignment in the ⟦⟧ chain stx into a single array.

Equations

• getHoareAssignmentArray stx curArr = getHoareAssignmentArrayAux✝ (assignmentSyntaxSize✝ stx.raw) stx curArr

def foldTermArray (element : Lean.TSyntax `hoareAssignment) (curTerm : Lean.TSyntax `term) : Lean.Elab.TermElabM (Lean.TSyntax `term)

Fold a single Hoare assignment onto the accumulated state-update term, turning it into the corresponding MState mutation.

Equations

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

def generateHoareAssignmentSyntax (stx : Lean.TSyntax `hoareAssignmentChain) : Lean.Elab.TermElabM Lean.Syntax

Construct the final state-update lambda term from a chain of Hoare assignments.

Equations

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