Data.Equality.Matching.Database

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.

Documentation

genericJoin :: forall (l :: Type -> Type). Language l => Database l -> Query l -> [Subst]

Run a conjunctive Query on a Database

Produce the list of valid substitutions from query variables to the query-matching class ids.

newtype Database (lang :: Type -> Type)

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 Operators to IntTries -- each operator has one table represented by an IntTrie

Constructors

DB (Map (Operator lang) IntTrie)

data Query (lang :: Type -> Type)

A conjunctive query to be run on the database

Constructors

Query ![Var] ![Atom lang]

SelectAllQuery !Var

data IntTrie

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.

Constructors

MkIntTrie

Fields

• tkeys :: !IntSet
• trie :: !(IntMap IntTrie)

type Subst = IntMap ClassId

Mapping from Var to ClassId. In a Subst there is only one substitution for each variable

type Var = Int

A variable in a query is identified by an Int. This is much more efficient than using e.g. a String.

As a consequence, patterns also use Int to represent a variable, but we can still have an IsString instance for variable patterns by hashing the string into a unique number.

data Atom (lang :: Type -> Type)

An Atom 𝑅ᵢ(𝑣, 𝑣1, ..., 𝑣𝑘) is defined by the relation 𝑅ᵢ and by the class-ids or variables 𝑣, 𝑣1, ..., 𝑣𝑘. It represents one conjunctive query's body atom.

Constructors

Atom

Fields

• !ClassIdOrVar

  Represents 𝑣

• !(lang ClassIdOrVar)

  Represents 𝑅ᵢ(𝑣1, ..., 𝑣𝑘). Note how 𝑣 isn't included since the arity of the constructor is 𝑘 instead of 𝑘+1.

data ClassIdOrVar

A value which is either a ClassId or a Var

Constructors

CClassId !ClassId

CVar !Var

Instances

Show ClassIdOrVar

Defined in Data.Equality.Matching.Database

Methods

showsPrec :: Int -> ClassIdOrVar -> ShowS

show :: ClassIdOrVar -> String

showList :: [ClassIdOrVar] -> ShowS

Eq ClassIdOrVar

Defined in Data.Equality.Matching.Database

Methods

(==) :: ClassIdOrVar -> ClassIdOrVar -> Bool

(/=) :: ClassIdOrVar -> ClassIdOrVar -> Bool

Ord ClassIdOrVar

Defined in Data.Equality.Matching.Database

Methods

compare :: ClassIdOrVar -> ClassIdOrVar -> Ordering

(<) :: ClassIdOrVar -> ClassIdOrVar -> Bool

(<=) :: ClassIdOrVar -> ClassIdOrVar -> Bool

(>) :: ClassIdOrVar -> ClassIdOrVar -> Bool

(>=) :: ClassIdOrVar -> ClassIdOrVar -> Bool

max :: ClassIdOrVar -> ClassIdOrVar -> ClassIdOrVar

min :: ClassIdOrVar -> ClassIdOrVar -> ClassIdOrVar