HoareElaborator

This module provides the elaborator for MRiscX Hoare-triple syntax.

def «term_∧∧_» : Lean.TrailingParserDescr

Notation a₁ ∧∧ a₂ for the conjunction Assertion.And a₁ a₂ of two assertions.

Equations

• «term_∧∧_» = Lean.ParserDescr.trailingNode `«term_∧∧_» 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧∧ ") (Lean.ParserDescr.cat `term 0))

def «term∼_» : Lean.ParserDescr

Notation ∼a for the negation Assertion.Not a of an assertion.

Equations

• «term∼_» = Lean.ParserDescr.node `«term∼_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∼") (Lean.ParserDescr.const `ident))

def processHoareTerm (stx : Lean.Term) : Lean.Elab.TermElabM Lean.Syntax

Preprocess a parsed Hoare condition, expanding assignment chains and binding the implicit state identifier st.

Equations

• processHoareTerm stx = Lean.withFreshMacroScope (processHoareTerm.go stx.raw)

def processHoareTerm.go : Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax

Differentiate between a Hoare assignment and an ordinary term in a pre- or post-condition.

Equations

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

def elabHoareTerm (stx : Lean.Term) : Lean.Elab.TermElabM Lean.Term

Elaborate a Hoare condition into the MState → _ predicate it denotes.

Equations

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

def «term⦃_⦄_1» : Lean.ParserDescr

Notation ⦃t⦄ elaborating a Hoare condition into its state predicate.

Equations

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

def mriscxSyntaxToTerm (stx : Array (Lean.TSyntax `mriscxLabel)) : Lean.Elab.TermElabM (Lean.TSyntax `term)

Some utility function which casts an Array TSyntax mriscxLabel to TSyntax term

Equations

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

def mriscxSpecToTerm (stx : Lean.TSyntax `mriscxInstr) : Lean.Elab.TermElabM (Lean.TSyntax `term)

Some utility function which casts TSyntax mriscxLabel to TSyntax term

Equations

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

def «termHoare__⦃_⦄_↦⟨_|_⟩⦃_⦄End» : Lean.ParserDescr

Hoare-triples for specifications with only one instruction

Equations

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

def term__3 : Lean.ParserDescr

Regular Hoare-triple with concrete MRiscX syntax before the actual triple

Equations

• term__3 = Lean.ParserDescr.node `term__3 1022 (Lean.ParserDescr.cat `hoareTerm 0)

def «term___⦃_⦄_↦⟨_|_⟩⦃_⦄» : Lean.ParserDescr

Define the code beforehand, does not support the usage of variables

Equations

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

def «term___⦃_⦄_↦⟨_|_⟩⦃_⦄_1» : Lean.TrailingParserDescr

To define the code beforehand with some some variables.

Equations

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

def «term___⦃_⦄_↦⟨_|_⟩⦃_⦄_2» : Lean.ParserDescr

Fallback elab if no Labelnames in l, L_w or L_b required

Equations

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

def «term⟦_⟧» : Lean.ParserDescr

Elab of hoare assignment

Equations

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

def «term⟦⟧» : Lean.ParserDescr

Notation ⟦⟧ for the identity assignment, denoting the unchanged state st.

Equations

• «term⟦⟧» = Lean.ParserDescr.node `«term⟦⟧» 1024 (Lean.ParserDescr.symbol "⟦⟧")