twee-lib-2.4.2: An equational theorem prover
Safe HaskellSafe-Inferred
LanguageHaskell2010

Twee.Index

Description

A term index to accelerate matching. An index is a multimap from terms to arbitrary values.

The type of query supported is: given a search term, find all keys such that the search term is an instance of the key, and return the corresponding values.

Synopsis

Documentation

data Index f a Source #

A term index: a multimap from Term f to a.

Instances

Instances details
(Labelled f, Show f, Show a) => Show (Index f a) Source # 
Instance details

Defined in Twee.Index

Methods

showsPrec :: Int -> Index f a -> ShowS #

show :: Index f a -> String #

showList :: [Index f a] -> ShowS #

empty :: Index f a Source #

An empty index.

null :: Index f a -> Bool Source #

Is the index empty?

singleton :: Term f -> a -> Index f a Source #

An index with one entry.

insert :: (Symbolic a, ConstantOf a ~ f) => Term f -> a -> Index f a -> Index f a Source #

Insert an entry into the index.

delete :: (Eq a, Symbolic a, ConstantOf a ~ f) => Term f -> a -> Index f a -> Index f a Source #

Delete an entry from the index.

lookup :: (Has a b, Symbolic b, Has b (TermOf b)) => TermOf b -> Index (ConstantOf b) a -> [b] Source #

Look up a term in the index. Finds all key-value such that the search term is an instance of the key, and returns an instance of the the value which makes the search term exactly equal to the key.

matches :: Term f -> Index f a -> [(Subst f, a)] Source #

Look up a term in the index. Like lookup, but returns the exact value that was inserted into the index, not an instance. Also returns a substitution which when applied to the value gives you the matching instance.

elems :: Index f a -> [a] Source #

Return all elements of the index.

fromList :: (Symbolic a, ConstantOf a ~ f) => [(Term f, a)] -> Index f a Source #

Create an index from a list of items

fromListWith :: (Symbolic a, ConstantOf a ~ f) => (a -> Term f) -> [a] -> Index f a Source #

Create an index from a list of items

invariant :: Index f a -> Bool Source #

Check the invariant of an index. For debugging purposes.