Call the egg sub-process and get a list of rewrites

This file defines the runEggRequest function, which is used to call the egg sub-process. Some pre-processing is necessary to encode domains and minimization problems into the JSON. Also, some post-processing is needed to parse the JSON response.

Taken from /

def Lean.Json.getStr! (j : Lean.Json) : String

Equations

• j.getStr! = match j with | Lean.Json.str a => a | x => ""

def Lean.Json.getArr! (j : Lean.Json) : Array Lean.Json

Equations

• j.getArr! = match j with | Lean.Json.arr a => a | x => #[]

def MetaM.ofExcept {ε : Type u_1} {α : Type} [ToString ε] : Except ε α → Lean.MetaM α

Equations

• MetaM.ofExcept e = match e with | Except.error msg => Lean.throwError ((Lean.MessageData.ofFormat ∘ Std.format) (toString msg)) | Except.ok x => pure x

instance CvxLean.instMonadExceptOfStringMetaM_cvxLean : MonadExceptOf String Lean.MetaM

Equations

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

def CvxLean.surroundQuotes (s : String) : String

Equations

• CvxLean.surroundQuotes s = "\"" ++ s ++ "\""

def CvxLean.EggMinimization.toJson (e : CvxLean.EggMinimization) : String

JSONify an EggMinimization. NOTE: Tuples are lists of two elements.

Equations

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

def CvxLean.EggDomain.toJson (e : CvxLean.EggDomain) : String

Equations

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

def CvxLean.EggRequest.toJson (e : CvxLean.EggRequest) : String

JSONify an EggRequest. NOTE: Tuples are lists of two elements.

Equations

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

def CvxLean.EggRewriteDirection.toString : CvxLean.EggRewriteDirection → String

Equations

• x.toString = match x with | CvxLean.EggRewriteDirection.Forward => "fwd" | CvxLean.EggRewriteDirection.Backward => "bwd"

instance CvxLean.instToStringEggRewriteDirection : ToString CvxLean.EggRewriteDirection

Equations

• CvxLean.instToStringEggRewriteDirection = { toString := CvxLean.EggRewriteDirection.toString }

def CvxLean.EggRewrite.toString (e : CvxLean.EggRewrite) : String

Equations

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

instance CvxLean.instToStringEggRewrite : ToString CvxLean.EggRewrite

Equations

• CvxLean.instToStringEggRewrite = { toString := CvxLean.EggRewrite.toString }

def CvxLean.runEggRequestRaw (requestJson : String) : Lean.MetaM String

Call the egg sub-process by runnning the executable egg-pre-dcp/utils/egg-pre-dcp, generated by running lake build EggPreDCP. The input is passed via standard input.

Equations

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

def CvxLean.parseEggResponse (responseString : String) : Lean.MetaM (Lean.HashMap String (Array CvxLean.EggRewrite))

Read egg's output and trun it into an array of EggRewrites.

Equations

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

def CvxLean.runEggRequest (request : CvxLean.EggRequest) : Lean.MetaM (Lean.HashMap String (Array CvxLean.EggRewrite))

Run request to egg and parse the output to get an array of rewrites, if successful.

Equations

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