Agda-2.8.0: A dependently typed functional programming language and proof assistant

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 => Set a -> DiscrimTree a -> DiscrimTree a

# Documentation

insertDT Source #

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

- resultValues :: Set a
- resultBlocker :: Blocker

#### Instances

Instances details

Ord a => Monoid (QueryResult a) Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree Methods mempty :: QueryResult a Source # mappend :: QueryResult a -> QueryResult a -> QueryResult a Source # mconcat :: [QueryResult a] -> QueryResult a Source #
Ord a => Semigroup (QueryResult a) Source # |
Instance details Defined in Agda.TypeChecking.DiscrimTree Methods (<>) :: QueryResult a -> QueryResult a -> QueryResult a Source # sconcat :: NonEmpty (QueryResult a) -> QueryResult a Source # stimes :: Integral b => b -> QueryResult a -> QueryResult a Source #

deleteFromDT :: Ord a => Set a -> DiscrimTree 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.