Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Equality.Saturation.Rewrites

Description

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.

Synopsis

data Rewrite anl lang
- = !(Pattern lang) := !(Pattern lang)
- | !(Rewrite anl lang) :| !(RewriteCondition anl lang)
type RewriteCondition anl lang = Subst -> EGraph anl lang -> Bool

Documentation

data Rewrite anl lang Source #

A rewrite rule that might have conditions for being applied

Example

Expand

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

Instances details

Show1 lang => Show (Rewrite anl lang) Source #
Instance details 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 = Subst -> EGraph anl lang -> Bool Source #

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