| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
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
- ematch :: Language l => Database l -> Pattern l -> [Match]
- eGraphToDatabase :: Language l => EGraph a l -> Database l
- data Match = Match {
- matchSubst :: !Subst
- matchClassId :: !ClassId
- compileToQuery :: Traversable lang => Pattern lang -> (Query lang, Var)
- module Data.Equality.Matching.Pattern
Documentation
ematch :: 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 :: Language l => EGraph a l -> Database l Source #
Convert an e-graph into a database
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
| |
compileToQuery :: Traversable lang => Pattern lang -> (Query lang, Var) Source #