Data.Equality.Saturation.Rewrites

Definition of Rewrite and RewriteCondition used to define rewrite rules.

Rewrite rules are applied to all represented expressions in an e-graph every iteration of equality saturation.

Documentation

data Rewrite lang

A rewrite rule that might have conditions for being applied

Example

rewrites :: [Rewrite Expr] -- from Sym.hs
rewrites =
    [ "x"+"y" := "y"+"x"
    , "x"*("y"*"z") := ("x"*"y")*"z"

    , "x"*0 := 0
    , "x"*1 := "x"

    , "a"-"a" := 1 -- cancel sub
    , "a"/"a" := 1 :| is_not_zero "a"
    ]

See the definition of is_not_zero in the documentation for RewriteCondition

Constructors

!(Pattern lang) := !(Pattern lang) infix 3

Trivial Rewrite

!(Rewrite lang) :| !(RewriteCondition lang) infixl 2

Conditional Rewrite

type RewriteCondition lang = Subst -> EGraph lang -> Bool

A rewrite condition. With a substitution from bound variables in the pattern to e-classes and with the e-graph, return True if the condition is satisfied

Example

is_not_zero :: String -> RewriteCondition Expr
is_not_zero v subst egr =
   case lookup v subst of
     Just class_id ->
         egr^._class class_id._data /= Just 0