Data.Equality.Extraction

Given an e-graph representing expressions of our language, we might want to extract, out of all expressions represented by some equivalence class, the best expression (according to a CostFunction) represented by that class

The function extractBest allows us to do exactly that: get the best expression represented in an e-class of an e-graph given a CostFunction

Extraction

extractBest

Arguments

:: forall lang. Language lang

=> EGraph lang

The e-graph out of which we are extracting an expression

-> CostFunction lang

The cost function to define best

-> ClassId

The e-class from which we'll extract the expression

-> Fix lang

The resulting best expression, in its fixed point form.

Extract the best expression from an equivalence class according to a CostFunction

(i, egr) = ...
   i <- represent expr
           ...

bestExpr = extractBest egr depthCost i

For a real example you might want to check out the source code of equalitySaturation'

Cost

type CostFunction l = l Cost -> Cost

A cost function is used to attribute a cost to representations in the e-graph and to extract the best one.

Example

symCost :: Expr Cost -> Cost
symCost = case
    BinOp Integral e1 e2 -> e1 + e2 + 20000
    BinOp Diff e1 e2 -> e1 + e2 + 500
    BinOp x e1 e2 -> e1 + e2 + 3
    UnOp x e1 -> e1 + 30
    Sym _ -> 1
    Const _ -> 1

type Cost = Int

Cost is simply an integer

depthCost :: Language l => CostFunction l

Simple cost function: the deeper the expression, the bigger the cost