| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.DiscrimTree
Description
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
Arguments
| :: (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 #
Constructors
| QueryResult | |
Fields
| |
Instances
| Ord a => Monoid (QueryResult a) Source # | |
Defined in Agda.TypeChecking.DiscrimTree Methods 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 Methods (<>) :: 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.