twee-lib-2.1.1: An equational theorem prover

Safe HaskellNone
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

Show a => Show (Index f a) Source # 

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 :: Term f -> a -> Index f a -> Index f a Source #

Insert an entry into the index.

delete :: Eq a => 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 :: Has a (Term f) => 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.

approxMatches :: Term f -> Index f a -> [a] Source #

Look up a term in the index, possibly returning spurious extra results.

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

Return all elements of the index.