Copyright	(c) 2020 Edwin Westbrook
License	BSD3
Maintainer	westbrook@galois.com
Stability	experimental
Portability	GHC
Safe Haskell	None
Language	Haskell2010

Data.Binding.Hobbits.NameSet

Description

Implements sets of Names using Strict. Note that these mappings are strict.

Synopsis

data NameSet k
data SomeName k = forall (a :: k). SomeName (Name a)
empty :: NameSet k
singleton :: Name (a :: k) -> NameSet k
fromList :: [SomeName k] -> NameSet k
toList :: NameSet k -> [SomeName k]
insert :: Name (a :: k) -> NameSet k -> NameSet k
delete :: Name (a :: k) -> NameSet k -> NameSet k
member :: Name (a :: k) -> NameSet k -> Bool
null :: NameSet k -> Bool
size :: NameSet k -> Int
union :: NameSet k -> NameSet k -> NameSet k
unions :: Foldable f => f (NameSet k) -> NameSet k
difference :: NameSet k -> NameSet k -> NameSet k
(\\) :: NameSet k -> NameSet k -> NameSet k
intersection :: NameSet k -> NameSet k -> NameSet k
map :: (forall (a :: k). Name a -> Name a) -> NameSet k -> NameSet k
foldr :: (forall (a :: k). Name a -> r -> r) -> r -> NameSet k -> r
foldl :: (forall (a :: k). r -> Name a -> r) -> r -> NameSet k -> r
liftNameSet :: Mb ctx (NameSet (k :: Type)) -> NameSet k

Documentation

data NameSet k Source #

A set of Names whose types all have kind k

data SomeName k Source #

A Name of some unknown type of kind k

Constructors

forall (a :: k). SomeName (Name a)

Instances

Instances details

NuMatching (SomeName k) Source #
Instance details Defined in Data.Binding.Hobbits.NameSet Methods nuMatchingProof :: MbTypeRepr (SomeName k) Source #

empty :: NameSet k Source #

The empty NameSet

singleton :: Name (a :: k) -> NameSet k Source #

The singleton NameSet

fromList :: [SomeName k] -> NameSet k Source #

Convert a list of names to a NameSet

toList :: NameSet k -> [SomeName k] Source #

Convert a NameSet to a list

insert :: Name (a :: k) -> NameSet k -> NameSet k Source #

Insert a name into a NameSet

delete :: Name (a :: k) -> NameSet k -> NameSet k Source #

Delete a name from a NameSet

member :: Name (a :: k) -> NameSet k -> Bool Source #

Test if a name is in a NameSet

null :: NameSet k -> Bool Source #

Test if a NameSet is empty

size :: NameSet k -> Int Source #

Compute the cardinality of a NameSet

union :: NameSet k -> NameSet k -> NameSet k Source #

Take the union of two NameSets

unions :: Foldable f => f (NameSet k) -> NameSet k Source #

Take the union of a list of NameSets

difference :: NameSet k -> NameSet k -> NameSet k Source #

Take the set of all elements of the first NameSet not in the second

(\\) :: NameSet k -> NameSet k -> NameSet k Source #

Another name for difference

intersection :: NameSet k -> NameSet k -> NameSet k Source #

Take the intersection of two NameSets

map :: (forall (a :: k). Name a -> Name a) -> NameSet k -> NameSet k Source #

Map a function across all elements of a NameSet

foldr :: (forall (a :: k). Name a -> r -> r) -> r -> NameSet k -> r Source #

Perform a right fold of a function across all elements of a NameSet

foldl :: (forall (a :: k). r -> Name a -> r) -> r -> NameSet k -> r Source #

Perform a left fold of a function across all elements of a NameSet

liftNameSet :: Mb ctx (NameSet (k :: Type)) -> NameSet k Source #

Lift a NameSet out of a name-binding by lifting all names not bound by the name-binding and then forming a NameSet from those lifted names