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

Data.Equality.Matching

Description

Equality-matching, implemented using a relational database (defined in Database) according to the paper "Relational E-Matching" https://arxiv.org/abs/2108.02290.

Synopsis

Documentation

ematch :: forall (l :: Type -> Type). Language l => Database l -> Pattern l -> [Match] Source #

Match a pattern against a Database, which can be gotten from an EGraph with eGraphToDatabase

Returns a list of matches, one Match for each set of valid substitutions for all variables and the equivalence class in which the pattern was matched.

ematch takes a Database instead of an EGraph because the Database could be constructed only once and shared accross matching.

eGraphToDatabase :: forall (l :: Type -> Type) a. Language l => EGraph a l -> Database l Source #

Convert an e-graph into a database

data Match Source #

Matching a pattern on an e-graph returns the e-class in which the pattern was matched and an e-class substitution for every VariablePattern in the pattern.

Constructors

Match 

compileToQuery :: forall (lang :: Type -> Type). Traversable lang => Pattern lang -> (Query lang, Var) Source #

Compiles a Pattern to a Query and returns the query root variable with it. The root variable's substitutions are the e-classes where the pattern matched