-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Type-level sets
--   
--   Please see the README on GitHub at
--   <a>https://github.com/isovector/type-sets#readme</a>
@package type-sets
@version 0.1.0.0

module Type.Set

-- | A binary search tree. When <tt>-XDataKinds</tt> is turned on, this
--   becomes the backbone of the type-level set.
--   
--   <pre>
--   &gt;&gt;&gt; type MySet = Insert Bool (Insert String (Insert (Maybe Int) 'Empty))
--   </pre>
data TypeSet a
Empty :: TypeSet a
Branch :: a -> TypeSet a -> TypeSet a -> TypeSet a

-- | <i>O(log n)</i>. Determine membership in the 'TypeSet.'
type family Member (t :: k) (bst :: TypeSet k) :: Bool

-- | <i>O(log n)</i>. Insert an element into the <a>TypeSet</a>.
type family Insert (t :: k) (bst :: TypeSet k) :: TypeSet k

-- | <i>O(log n)</i>. Remove an element from the <a>TypeSet</a>.
type family Remove (t :: k) (bst :: TypeSet k) :: TypeSet k

-- | <i>O(m log n)</i> for <tt>Merge m n</tt>; put your smaller set on the
--   left side. Merge two <a>TypeSet</a>s together.
type family Merge (small :: TypeSet k) (big :: TypeSet k) :: TypeSet k

-- | <i>O(log n)</i>. Compute a <tt>[<a>Side</a>]</tt> which finds the
--   desired element in the tree. The result of this can be passed to
--   <a>Follow</a> in order to look up the same element again later.
type family Locate (t :: k) (bst :: TypeSet k) :: [Side]

-- | <i>O(log n)</i>. Follow the result of a <a>Locate</a> to get a
--   particular element in the tree.
type family Follow (ss :: [Side]) (bst :: TypeSet k) :: k

-- | Either left or right down a path.
data Side
L :: Side
R :: Side
instance GHC.Show.Show Type.Set.Side
instance GHC.Classes.Ord Type.Set.Side
instance GHC.Classes.Eq Type.Set.Side

module Type.Set.Variant

-- | A <a>Variant</a> is like an <a>Either</a>, except that it can store
--   any of the types contained in the <a>TypeSet</a>. You can use
--   <a>toVariant</a> to construct one, and <a>fromVariant</a> to pattern
--   match it out.
data Variant (v :: TypeSet *)
[Variant] :: SSide ss -> Follow ss v -> Variant v

-- | A proof that the set <tt>bst</tt> contains type <tt>t</tt>.
class Has t bst

-- | Inject a <tt>t</tt> into a <a>Variant</a>.
toVariant :: Has t bst => t -> Variant bst

-- | Attempt to project a <a>Variant</a> into <tt>t</tt>. This might fail,
--   because there is no guarantee that the <a>Variant</a> <i>actually
--   contains</i> <tt>t</tt>.
--   
--   You can use <a>decompRoot</a> instead of this function if you'd like a
--   proof that the <a>Variant</a> doesn't contain <tt>t</tt> in the case
--   of failure.
fromVariant :: Has t bst => Variant bst -> Maybe t

-- | Like <a>fromVariant</a>, but decomposes the <a>Variant</a> into its
--   left and right branches, depending on where <tt>t</tt> is.
decompRoot :: Variant ( 'Branch t lbst rbst) -> Split t lbst rbst
data Split t lbst rbst
Root :: t -> Split t lbst rbst
LSplit :: Variant lbst -> Split t lbst rbst
RSplit :: Variant rbst -> Split t lbst rbst

-- | Weaken a <a>Variant</a> so that it can contain something else.
weaken :: forall t bst. Variant bst -> Variant (Insert t bst)

-- | A proof that inserting into a <tt>bst</tt> doesn't affect the position
--   of anything already in the tree.
proveFollowInsert :: Follow ss (Insert t bst) :~: Follow ss bst

-- | Singletons for <a>Side</a>s.
data SSide (ss :: [Side])
[SNil] :: SSide '[]
[SL] :: SSide ss -> SSide ( 'L : ss)
[SR] :: SSide ss -> SSide ( 'R : ss)

-- | Get a singleton for a list of <a>Side</a>s.
class FromSides (ss :: [Side])
fromSides :: FromSides ss => SSide ss
instance (Type.Set.Follow (Type.Set.Locate t bst) bst Data.Type.Equality.~ t, Type.Set.Variant.FromSides (Type.Set.Locate t bst)) => Type.Set.Variant.Has t bst
instance Type.Set.Variant.FromSides '[]
instance Type.Set.Variant.FromSides ss => Type.Set.Variant.FromSides ('Type.Set.L : ss)
instance Type.Set.Variant.FromSides ss => Type.Set.Variant.FromSides ('Type.Set.R : ss)
instance Data.Type.Equality.TestEquality Type.Set.Variant.SSide