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 anl (lang :: Type -> Type)

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 anl lang) :| !(RewriteCondition anl lang) infixl 2

Conditional Rewrite

Instances

(forall a. Show a => Show (lang a)) => Show (Rewrite anl lang)

Defined in Data.Equality.Saturation.Rewrites

Methods

showsPrec :: Int -> Rewrite anl lang -> ShowS

show :: Rewrite anl lang -> String

showList :: [Rewrite anl lang] -> ShowS

type RewriteCondition anl (lang :: Type -> Type) = Subst -> EGraph anl 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