HandleExpr

This module provides helpers reflecting Lean Exprs into MRiscX data.

def unwrapWhileCreateLabelmap (e? : Option Lean.Expr) (labelmap : Lean.Expr) : Lean.MetaM Lean.Expr

Fold the optional label expression e? into the running labelmap expression.

Equations

• One or more equations did not get rendered due to their size.
• unwrapWhileCreateLabelmap (some arg) labelmap = pure arg

def getUInt64FromExpr (e : Lean.Expr) : Lean.MetaM UInt64

Evaluate an Expr to the UInt64 it denotes.

Equations

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

def getStrFromExpr (e : Lean.Expr) : Lean.MetaM String

Evaluate an Expr to the String it denotes.

Equations

• getStrFromExpr e = do let e ← Lean.Meta.whnf e match e with | Lean.Expr.lit (Lean.Literal.strVal s) => pure s | x => Lean.throwError (Lean.toMessageData "Expected a string literal")

def getLabelMapFromMapExpr (e : Lean.Expr) : Lean.MetaM LabelMap

Reflect a PMap value from its Expr representation e.

Equations

• getLabelMapFromMapExpr e = getLabelMapFromMapExprAux✝ (exprDepthBound✝ e) e

def getLabelMapFromCodeExpr (e : Lean.Expr) : Lean.MetaM LabelMap

Reflect the LabelMap value out of an Expr of type Code.

Equations

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

def getInstrFromCodeExpr (codeExpr : Lean.Expr) (pc : UInt64) : Lean.MetaM Lean.Expr

Extract an Instr from a Code.mk Expr given a program counter value.

This function takes an Expr of type Code.mk and a program counter (UInt64), and returns the Expr of the Instr at that program counter position.

Equations

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

def getArgsAsUIntsOrThrow (args : Array Lean.Expr) (n : Nat) : Lean.MetaM (List UInt64)

Interpret the first n arguments as UInt64 values, throwing otherwise.

Equations

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

def getTwoUIntFromExprValidated (args : Array Lean.Expr) : Lean.MetaM (UInt64 × UInt64)

Interpret two argument expressions as a pair of UInt64 values.

Equations

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

def getThreeUIntFromExprValidated (args : Array Lean.Expr) : Lean.MetaM (UInt64 × UInt64 × UInt64)

Interpret three argument expressions as a triple of UInt64 values.

Equations

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

def getUIntStringFromExprValidated (args : Array Lean.Expr) : Lean.MetaM (UInt64 × String)

Interpret two argument expressions as a UInt64 and a String.

Equations

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

def getTwoUIntOneStringFromExprValidated (args : Array Lean.Expr) : Lean.MetaM (UInt64 × UInt64 × String)

Interpret three argument expressions as two UInt64 values and a String.

Equations

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

def getInstrFromExpr (e : Lean.Expr) : Lean.MetaM Instr

Reflect the Instr value out of an Expr.

Equations

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

def getInstrMapFromExpr (e : Lean.Expr) : Lean.MetaM InstructionMap

Reflect an InstructionMap value from its Expr representation e.

Equations

• getInstrMapFromExpr e = getInstrMapFromExprAux✝ (exprDepthBound✝ e) e

def getInstrMapFromCodeExpr (e : Lean.Expr) : Lean.MetaM InstructionMap

Reflect the InstructionMap value out of an Expr of type Code.

Equations

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

def getCodeExprFromLambda (e : Lean.Expr) : Lean.MetaM Lean.Expr

Return the actual binding body from a lambda function.

Equations

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

def splitConjDisj (declType : Lean.Expr) : Lean.MetaM (Lean.TSyntax `rcasesPat)

Split a conjunction/disjunction type declType into a matching rcases pattern.

Equations

• splitConjDisj declType = splitConjDisjAux✝ (exprDepthBound✝ declType) declType

def parseSingletonExpr (e : Lean.Expr) : Lean.MetaM UInt64

Evaluate a singleton argument expression to the UInt64 it denotes.

Equations

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