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 anl lang cost. (Language lang, Ord cost)

=> EGraph anl lang

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

-> CostFunction lang cost

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 cost = l cost -> cost

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

The cost function is polymorphic over the type used for the cost, however cost must instance Ord in order for the defined CostFunction to fulfill its purpose. That's why we have an Ord cost constraint in equalitySaturation and extractBest

Example

symCost :: Expr Int -> Int
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

depthCost :: Language l => CostFunction l Int

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