Agda.TypeChecking.DiscrimTree

Imperfect discrimination trees for indexing data by internal syntax.

Documentation

insertDT

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 :: forall a. (Ord a, PrettyTCM a) => Term -> DiscrimTree a -> TCM (QueryResult a)

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 :: forall a. (Ord a, PrettyTCM a) => Term -> DiscrimTree a -> TCM (QueryResult a)

Look up a Term in the given discrimination tree, treating local variables as wildcards.

data QueryResult a

Constructors

QueryResult

Fields

• resultValues :: Set a
• resultBlocker :: Blocker

Instances

Ord a => Monoid (QueryResult a)

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)

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

Remove a set of values from the discrimination tree. The tree is rebuilt so that cases with no leaves are removed.