| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.Equality.Matching
Contents
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 :: forall (l :: Type -> Type). Language l => Database l -> (Query l, Var) -> [Match]
- eGraphToDatabase :: forall (l :: Type -> Type) a. Language l => EGraph a l -> Database l
- data Match = Match {
- matchSubst :: !Subst
- matchClassId :: !ClassId
- compileToQuery :: forall (lang :: Type -> Type). Traversable lang => Pattern lang -> ((Query lang, Var), VarsState)
- data VarsState
- findVarName :: VarsState -> String -> Var
- userPatVars :: VarsState -> [Var]
- module Data.Equality.Matching.Pattern
Documentation
ematch :: forall (l :: Type -> Type). Language l => Database l -> (Query l, Var) -> [Match] Source #
Match a pattern Query, gotten from compileToQuery on a Pattern,
against a Database, which is built 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
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
| |
Compiling a Pattern to a Query
compileToQuery :: forall (lang :: Type -> Type). Traversable lang => Pattern lang -> ((Query lang, Var), VarsState) Source #