Data.Equality.Matching

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

Documentation

ematch :: Language l => Database l -> Pattern l -> [Match]

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 :: Language l => EGraph a l -> Database l

Convert an e-graph into a database

data Match

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

Fields

• matchSubst :: !Subst
• matchClassId :: !ClassId

compileToQuery :: Traversable lang => Pattern lang -> (Query lang, Var)

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

module Data.Equality.Matching.Pattern