hegg-0.5.0.0: Fast equality saturation in Haskell
Safe HaskellNone
LanguageHaskell2010

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

Documentation

data Rewrite anl (lang :: Type -> Type) 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
(forall a. Show a => Show (lang a)) => 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 :: Type -> Type) = 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