The main types user around the egg interface.

def CvxLean.EggTree : Type

An intermediate structure to represent problems as trees of strings.

Equations

• CvxLean.EggTree = CvxLean.Tree String String

instance CvxLean.instInhabitedEggTree : Inhabited CvxLean.EggTree

Equations

• CvxLean.instInhabitedEggTree = { default := CvxLean.Tree.leaf "" }

def CvxLean.EggOCTree : Type

A more refined EggTree, split by its objective function and components.

Equations

• CvxLean.EggOCTree = CvxLean.OC (String × CvxLean.EggTree)

inductive CvxLean.EggTreeOpArgTag : Type

Helper structure to keep track of the arguments, some of which may be pre-determined, when translating from atom trees to trees with constructors in the egg language.

• arg: CvxLean.EggTreeOpArgTag
• val: String → CvxLean.EggTreeOpArgTag

structure CvxLean.EggMinimization : Type

Once EggTree is flattened into S-expressions, it can be turned into an EggMinimization. This is what will by JSONified and sent to egg. It is split into objective functions and constraints, with their tag. Note that egg builds one problem term from this. However, it is useful to keep track of the names of the components so that when egg comes back with a sequence of rewrites it can easily indicate the location of the rewrite.

• objFun : String
• constrs : List (String × String)

structure CvxLean.EggDomain : Type

This encodes an interval, used for e-class analysis. For example ⟨"0", "1", "-inf", "8"⟩ is how the interval (-∞, 8] would be encoded.

• hi : String
• lo : String
• hi_open : String
• lo_open : String

structure CvxLean.EggDomainIdentified : Type

Every EggDomain is infered from a constraint named constraintName, and it corresponds to a variable or parameter named varOrParamName. This structure keeps track of that.

• constraintName : String
• varOrParamName : String
• domain : CvxLean.EggDomain

def CvxLean.EggOCTreeExtended : Type

An EggOCTree with also the domain information.

Equations

• CvxLean.EggOCTreeExtended = (CvxLean.EggOCTree × Array CvxLean.EggDomainIdentified)

structure CvxLean.EggRequest : Type

A request consists of an EggMinimization and a list of domains per variable (or parameter).

• probName : String
• domains : List (String × CvxLean.EggDomain)
• target : CvxLean.EggMinimization

inductive CvxLean.EggRewriteDirection : Type

Recall that, in egg, rewrites can be forward or backward (in the response).

• Forward: CvxLean.EggRewriteDirection
• Backward: CvxLean.EggRewriteDirection

instance CvxLean.instInhabitedEggRewriteDirection : Inhabited CvxLean.EggRewriteDirection

Equations

• CvxLean.instInhabitedEggRewriteDirection = { default := CvxLean.EggRewriteDirection.Forward }

instance CvxLean.instDecidableEqEggRewriteDirection : DecidableEq CvxLean.EggRewriteDirection

Equations

• CvxLean.instDecidableEqEggRewriteDirection x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

structure CvxLean.EggRewrite : Type

A rewrite returned by egg.

• rewriteName : String

  This is the name of the lemma used for rewriting.

• direction : CvxLean.EggRewriteDirection

  Forward or backward.

• location : String

  The name of the constraint or "objFun".

• subexprFrom : String

  Source sub-expression.

• subexprTo : String

  Target sub-expression.

• expectedTerm : String

  The context expression with a "?" in place of the sub-expression. For example, if we are rewriting x + (y + z) into x + (z + y), the expected term would be x + ?, with subexprFrom set to y + z and subexprTo set to z + y.