Safe Haskell | None |
---|---|
Language | Haskell2010 |
Imperfect discrimination trees for indexing data by internal syntax.
Synopsis
- insertDT :: (Ord a, PrettyTCM a) => Int -> Term -> a -> DiscrimTree a -> TCM (DiscrimTree a)
- lookupDT :: (Ord a, PrettyTCM a) => Term -> DiscrimTree a -> TCM (QueryResult a)
- lookupUnifyDT :: (Ord a, PrettyTCM a) => Term -> DiscrimTree a -> TCM (QueryResult a)
- data QueryResult a = QueryResult {
- resultValues :: Set a
- resultBlocker :: Blocker
- deleteFromDT :: Ord a => DiscrimTree a -> Set a -> DiscrimTree a
Documentation
:: (Ord a, PrettyTCM a) | |
=> Int | Number of variables to consider wildcards, e.g. the number of leading invisible pis in an instance type. |
-> Term | The term to use as a key |
-> a | |
-> DiscrimTree a | |
-> TCM (DiscrimTree a) |
Insert a value into the discrimination tree, turning variables into rigid locals or wildcards depending on the given scope.
lookupDT :: (Ord a, PrettyTCM a) => Term -> DiscrimTree a -> TCM (QueryResult a) Source #
Look up a Term
in the given discrimination tree, treating local
variables as rigid symbols. The returned set is guaranteed to contain
everything that could overlap the given key.
lookupUnifyDT :: (Ord a, PrettyTCM a) => Term -> DiscrimTree a -> TCM (QueryResult a) Source #
Look up a Term
in the given discrimination tree, treating local
variables as wildcards.
data QueryResult a Source #
QueryResult | |
|
Instances
Ord a => Monoid (QueryResult a) Source # | |
Defined in Agda.TypeChecking.DiscrimTree mempty :: QueryResult a mappend :: QueryResult a -> QueryResult a -> QueryResult a mconcat :: [QueryResult a] -> QueryResult a | |
Ord a => Semigroup (QueryResult a) Source # | |
Defined in Agda.TypeChecking.DiscrimTree (<>) :: QueryResult a -> QueryResult a -> QueryResult a # sconcat :: NonEmpty (QueryResult a) -> QueryResult a stimes :: Integral b => b -> QueryResult a -> QueryResult a |
deleteFromDT :: Ord a => DiscrimTree a -> Set a -> DiscrimTree a Source #
Remove a set of values from the discrimination tree. The tree is rebuilt so that cases with no leaves are removed.