Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.DiscrimTree

Description

Imperfect discrimination trees for indexing data by internal syntax.

Synopsis

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

Instances

Instances details
Ord a => Monoid (QueryResult a) Source # 
Instance details

Defined in Agda.TypeChecking.DiscrimTree

Ord a => Semigroup (QueryResult a) Source # 
Instance details

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.