ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.DiscrimTree

Imperfect discrimination trees for indexing data by internal syntax.

Synopsis

value insertDT
value lookupDT
value lookupUnifyDT
data QueryResult
value deleteFromDT

PackageAgda-2.8.0.2
Exports5
LanguageHaskell2010
LicenceMIT
SourceDiscrimTree.hs

valueinsertDT

:: (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.

valuelookupDT

:: (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.

valuelookupUnifyDT

:: (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.

datadata QueryResult a

Constructors

QueryResult
- resultValues :: Set a
- resultBlocker :: Blocker

Instances2Semigroup, Monoid

Ord a => Semigroup (QueryResult a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.DiscrimTree
Ord a => Monoid (QueryResult a)Defined in Agda-2.8.0.2 · Agda.TypeChecking.DiscrimTree

valuedeleteFromDT :: 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.