Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Custom database implemented with trie-maps specialized to run conjunctive queries using a (worst-case optimal) generic join algorithm.
Used in e-matching (Matching
) as described by "Relational
E-Matching" https://arxiv.org/abs/2108.02290.
You probably don't need this module.
Synopsis
- genericJoin :: forall l. Language l => Database l -> Query l -> [Subst]
- newtype Database lang = DB (Map (Operator lang) IntTrie)
- data Query lang
- = Query ![Var] ![Atom lang]
- | SelectAllQuery !Var
- data IntTrie = MkIntTrie {}
- type Subst = IntMap ClassId
- type Var = Int
- data Atom lang = Atom !ClassIdOrVar !(lang ClassIdOrVar)
- data ClassIdOrVar
Documentation
newtype Database lang Source #
The relational representation of an e-graph, as described in section 3.1 of "Relational E-Matching".
Every e-node with symbol ๐ in the e-graph corresponds to a tuple in the relation ๐ ๐ in the database. If ๐ has arity ๐, then ๐ ๐ will have arity ๐ + 1; its first attribute is the e-class id that contains the corresponding e-node , and the remaining attributes are the ๐ children of the ๐ e-node
For every existing symbol in the e-graph the Database
has a table.
In concrete, we map Operator
s to IntTrie
s -- each operator has one table
represented by an IntTrie
A conjunctive query to be run on the database
Query ![Var] ![Atom lang] | |
SelectAllQuery !Var |
An integer triemap that keeps a cache of all keys in at each level.
As described in the paper: Generic join requires two important performance bounds to be met in order for its own run time to meet the AGM bound. First, the intersection [...] must run in ๐ (min(|๐ ๐ .๐ฅ |)) time. Second, the residual relations should be computed in constant time, i.e., computing from the relation ๐ (๐ฅ, ๐ฆ) the relation ๐ (๐ฃ๐ฅ , ๐ฆ) for some ๐ฃ๐ฅ โ ๐ (๐ฅ, ๐ฆ).๐ฅ must take constant time. Both of these can be solved by using tries (sometimes called prefix or suffix trees) as an indexing data structure.
An Atom
๐
แตข(๐ฃ, ๐ฃ1, ..., ๐ฃ๐) is defined by the relation ๐
แตข and by the
class-ids or variables ๐ฃ, ๐ฃ1, ..., ๐ฃ๐. It represents one conjunctive query's body atom.
Atom | |
|
data ClassIdOrVar Source #
Instances
Show ClassIdOrVar Source # | |
Defined in Data.Equality.Matching.Database showsPrec :: Int -> ClassIdOrVar -> ShowS # show :: ClassIdOrVar -> String # showList :: [ClassIdOrVar] -> ShowS # | |
Eq ClassIdOrVar Source # | |
Defined in Data.Equality.Matching.Database (==) :: ClassIdOrVar -> ClassIdOrVar -> Bool # (/=) :: ClassIdOrVar -> ClassIdOrVar -> Bool # | |
Ord ClassIdOrVar Source # | |
Defined in Data.Equality.Matching.Database compare :: ClassIdOrVar -> ClassIdOrVar -> Ordering # (<) :: ClassIdOrVar -> ClassIdOrVar -> Bool # (<=) :: ClassIdOrVar -> ClassIdOrVar -> Bool # (>) :: ClassIdOrVar -> ClassIdOrVar -> Bool # (>=) :: ClassIdOrVar -> ClassIdOrVar -> Bool # max :: ClassIdOrVar -> ClassIdOrVar -> ClassIdOrVar # min :: ClassIdOrVar -> ClassIdOrVar -> ClassIdOrVar # |