{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | This module implements a search in a typelevel tree
--   and offers a handy interface via @-XOverloaedRecordDot@ and 'GHC.Records.HasField'.
--   We can search in the tree via BFS or DFS.
--   Performance wise this doesn't make a difference, as the search is performed at
--   compile time anyway however, it can change the semantics if the tree contains an
--   element more than once, see the example in 'getElem'.
module Data.HTree.Labeled
  ( -- * Interface

    -- ** Labeled types
    Labeled (..)
  , pattern HNodeL
  , pattern HLeafL
  , type TyNodeL

    -- ** Getting elements
  , getElem
  , getElem'
  , SearchStrategy (..)

    -- ** Reexports
  , HasField (..)
  , Proxy (..)

    -- * Internal
  , HasField' (..)
  , Decide (..)
  , Elem
  , AnyElem
  , getElemWithPath
  )
where

import Data.HTree.Families (Not, type (||))
import Data.HTree.List (HList (HCons, HNil))
import Data.HTree.Tree (HForest, HTree (HNode), Path (Deeper, Farther, Here), TyForest, TyTree (TyNode))
import Data.Kind (Constraint, Type)
import Data.Proxy (Proxy (Proxy))
import GHC.Generics (Generic)
import GHC.Records (HasField (getField))

-- | a type syonym that allows for easy construction of TyTrees that have labeled nodes
type TyNodeL l a = 'TyNode (Labeled l a)

-- | a pattern that allows for direct construction and destruction of nodes with
--   labels
pattern HNodeL :: forall l a f ts. Functor f => f a -> HForest f ts -> HTree f ('TyNode (Labeled l a) ts)
pattern $mHNodeL :: forall {r} {l1} {l :: l1} {a} {f :: Type -> Type}
       {ts :: TyForest @Type Type}.
Functor f =>
HTree @Type f ('TyNode @Type (Labeled @l1 l a) ts)
-> (f a -> HForest @Type f ts -> r) -> ((# #) -> r) -> r
$bHNodeL :: forall {l1} (l :: l1) a (f :: Type -> Type)
       (ts :: TyForest @Type Type).
Functor f =>
f a
-> HForest @Type f ts
-> HTree @Type f ('TyNode @Type (Labeled @l1 l a) ts)
HNodeL x ts <- (HNode (fmap unLabel -> x) ts)
  where
    HNodeL f a
x HForest @Type f ts
ts = f (Labeled @l1 l2 a)
-> HForest @Type f ts
-> HTree @Type f ('TyNode @Type (Labeled @l1 l2 a) ts)
forall {k} (f :: k -> Type) (a :: k) (ts :: TyForest @Type k).
f a -> HForest @k f ts -> HTree @k f ('TyNode @k a ts)
HNode (a -> Labeled @l1 l2 a
forall l (l :: l) a. a -> Labeled @l l a
MkLabeled (a -> Labeled @l1 l2 a) -> f a -> f (Labeled @l1 l2 a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
x) HForest @Type f ts
ts

{-# COMPLETE HNodeL #-}

-- | a labeled HNode Leaf
pattern HLeafL :: forall l a f. Functor f => f a -> HTree f ('TyNode (Labeled l a) '[])
pattern $mHLeafL :: forall {r} {l1} {l :: l1} {a} {f :: Type -> Type}.
Functor f =>
HTree
  @Type
  f
  ('TyNode @Type (Labeled @l1 l a) ('[] @(TyTree @Type Type)))
-> (f a -> r) -> ((# #) -> r) -> r
$bHLeafL :: forall {l1} (l :: l1) a (f :: Type -> Type).
Functor f =>
f a
-> HTree
     @Type
     f
     ('TyNode @Type (Labeled @l1 l a) ('[] @(TyTree @Type Type)))
HLeafL x <- (HNode (fmap unLabel -> x) HNil)
  where
    HLeafL f a
x = f (Labeled @l1 l2 a)
-> HForest @Type f ('[] @(TyTree @Type Type))
-> HTree
     @Type
     f
     ('TyNode @Type (Labeled @l1 l2 a) ('[] @(TyTree @Type Type)))
forall {k} (f :: k -> Type) (a :: k) (ts :: TyForest @Type k).
f a -> HForest @k f ts -> HTree @k f ('TyNode @k a ts)
HNode (a -> Labeled @l1 l2 a
forall l (l :: l) a. a -> Labeled @l l a
MkLabeled (a -> Labeled @l1 l2 a) -> f a -> f (Labeled @l1 l2 a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f a
x) HForest @Type f ('[] @(TyTree @Type Type))
forall {k} (f :: k -> Type). HList @k f ('[] @k)
HNil

-- | a newtype that is labeled with some typelevel tag
type Labeled :: forall l. l -> Type -> Type
newtype Labeled l a = MkLabeled {forall l (l :: l) a. Labeled @l l a -> a
unLabel :: a}
  deriving stock (Int -> Labeled @l l a -> ShowS
[Labeled @l l a] -> ShowS
Labeled @l l a -> String
(Int -> Labeled @l l a -> ShowS)
-> (Labeled @l l a -> String)
-> ([Labeled @l l a] -> ShowS)
-> Show (Labeled @l l a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall l (l :: l) a. Show a => Int -> Labeled @l l a -> ShowS
forall l (l :: l) a. Show a => [Labeled @l l a] -> ShowS
forall l (l :: l) a. Show a => Labeled @l l a -> String
$cshowsPrec :: forall l (l :: l) a. Show a => Int -> Labeled @l l a -> ShowS
showsPrec :: Int -> Labeled @l l a -> ShowS
$cshow :: forall l (l :: l) a. Show a => Labeled @l l a -> String
show :: Labeled @l l a -> String
$cshowList :: forall l (l :: l) a. Show a => [Labeled @l l a] -> ShowS
showList :: [Labeled @l l a] -> ShowS
Show, Labeled @l l a -> Labeled @l l a -> Bool
(Labeled @l l a -> Labeled @l l a -> Bool)
-> (Labeled @l l a -> Labeled @l l a -> Bool)
-> Eq (Labeled @l l a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall l (l :: l) a.
Eq a =>
Labeled @l l a -> Labeled @l l a -> Bool
$c== :: forall l (l :: l) a.
Eq a =>
Labeled @l l a -> Labeled @l l a -> Bool
== :: Labeled @l l a -> Labeled @l l a -> Bool
$c/= :: forall l (l :: l) a.
Eq a =>
Labeled @l l a -> Labeled @l l a -> Bool
/= :: Labeled @l l a -> Labeled @l l a -> Bool
Eq, Eq (Labeled @l l a)
Eq (Labeled @l l a)
-> (Labeled @l l a -> Labeled @l l a -> Ordering)
-> (Labeled @l l a -> Labeled @l l a -> Bool)
-> (Labeled @l l a -> Labeled @l l a -> Bool)
-> (Labeled @l l a -> Labeled @l l a -> Bool)
-> (Labeled @l l a -> Labeled @l l a -> Bool)
-> (Labeled @l l a -> Labeled @l l a -> Labeled @l l a)
-> (Labeled @l l a -> Labeled @l l a -> Labeled @l l a)
-> Ord (Labeled @l l a)
Labeled @l l a -> Labeled @l l a -> Bool
Labeled @l l a -> Labeled @l l a -> Ordering
Labeled @l l a -> Labeled @l l a -> Labeled @l l a
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall {l} {l :: l} {a}. Ord a => Eq (Labeled @l l a)
forall l (l :: l) a.
Ord a =>
Labeled @l l a -> Labeled @l l a -> Bool
forall l (l :: l) a.
Ord a =>
Labeled @l l a -> Labeled @l l a -> Ordering
forall l (l :: l) a.
Ord a =>
Labeled @l l a -> Labeled @l l a -> Labeled @l l a
$ccompare :: forall l (l :: l) a.
Ord a =>
Labeled @l l a -> Labeled @l l a -> Ordering
compare :: Labeled @l l a -> Labeled @l l a -> Ordering
$c< :: forall l (l :: l) a.
Ord a =>
Labeled @l l a -> Labeled @l l a -> Bool
< :: Labeled @l l a -> Labeled @l l a -> Bool
$c<= :: forall l (l :: l) a.
Ord a =>
Labeled @l l a -> Labeled @l l a -> Bool
<= :: Labeled @l l a -> Labeled @l l a -> Bool
$c> :: forall l (l :: l) a.
Ord a =>
Labeled @l l a -> Labeled @l l a -> Bool
> :: Labeled @l l a -> Labeled @l l a -> Bool
$c>= :: forall l (l :: l) a.
Ord a =>
Labeled @l l a -> Labeled @l l a -> Bool
>= :: Labeled @l l a -> Labeled @l l a -> Bool
$cmax :: forall l (l :: l) a.
Ord a =>
Labeled @l l a -> Labeled @l l a -> Labeled @l l a
max :: Labeled @l l a -> Labeled @l l a -> Labeled @l l a
$cmin :: forall l (l :: l) a.
Ord a =>
Labeled @l l a -> Labeled @l l a -> Labeled @l l a
min :: Labeled @l l a -> Labeled @l l a -> Labeled @l l a
Ord, (forall a b. (a -> b) -> Labeled @l l a -> Labeled @l l b)
-> (forall a b. a -> Labeled @l l b -> Labeled @l l a)
-> Functor (Labeled @l l)
forall l (l :: l) a b. a -> Labeled @l l b -> Labeled @l l a
forall l (l :: l) a b. (a -> b) -> Labeled @l l a -> Labeled @l l b
forall a b. a -> Labeled @l l b -> Labeled @l l a
forall a b. (a -> b) -> Labeled @l l a -> Labeled @l l b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall l (l :: l) a b. (a -> b) -> Labeled @l l a -> Labeled @l l b
fmap :: forall a b. (a -> b) -> Labeled @l l a -> Labeled @l l b
$c<$ :: forall l (l :: l) a b. a -> Labeled @l l b -> Labeled @l l a
<$ :: forall a b. a -> Labeled @l l b -> Labeled @l l a
Functor, (forall m. Monoid m => Labeled @l l m -> m)
-> (forall m a. Monoid m => (a -> m) -> Labeled @l l a -> m)
-> (forall m a. Monoid m => (a -> m) -> Labeled @l l a -> m)
-> (forall a b. (a -> b -> b) -> b -> Labeled @l l a -> b)
-> (forall a b. (a -> b -> b) -> b -> Labeled @l l a -> b)
-> (forall b a. (b -> a -> b) -> b -> Labeled @l l a -> b)
-> (forall b a. (b -> a -> b) -> b -> Labeled @l l a -> b)
-> (forall a. (a -> a -> a) -> Labeled @l l a -> a)
-> (forall a. (a -> a -> a) -> Labeled @l l a -> a)
-> (forall a. Labeled @l l a -> [a])
-> (forall a. Labeled @l l a -> Bool)
-> (forall a. Labeled @l l a -> Int)
-> (forall a. Eq a => a -> Labeled @l l a -> Bool)
-> (forall a. Ord a => Labeled @l l a -> a)
-> (forall a. Ord a => Labeled @l l a -> a)
-> (forall a. Num a => Labeled @l l a -> a)
-> (forall a. Num a => Labeled @l l a -> a)
-> Foldable (Labeled @l l)
forall a. Eq a => a -> Labeled @l l a -> Bool
forall a. Num a => Labeled @l l a -> a
forall a. Ord a => Labeled @l l a -> a
forall m. Monoid m => Labeled @l l m -> m
forall a. Labeled @l l a -> Bool
forall a. Labeled @l l a -> Int
forall a. Labeled @l l a -> [a]
forall a. (a -> a -> a) -> Labeled @l l a -> a
forall l (l :: l) a. Eq a => a -> Labeled @l l a -> Bool
forall l (l :: l) a. Num a => Labeled @l l a -> a
forall l (l :: l) a. Ord a => Labeled @l l a -> a
forall l (l :: l) m. Monoid m => Labeled @l l m -> m
forall l (l :: l) a. Labeled @l l a -> Bool
forall l (l :: l) a. Labeled @l l a -> Int
forall l (l :: l) a. Labeled @l l a -> [a]
forall l (l :: l) a. (a -> a -> a) -> Labeled @l l a -> a
forall l (l :: l) m a. Monoid m => (a -> m) -> Labeled @l l a -> m
forall l (l :: l) b a. (b -> a -> b) -> b -> Labeled @l l a -> b
forall l (l :: l) a b. (a -> b -> b) -> b -> Labeled @l l a -> b
forall m a. Monoid m => (a -> m) -> Labeled @l l a -> m
forall b a. (b -> a -> b) -> b -> Labeled @l l a -> b
forall a b. (a -> b -> b) -> b -> Labeled @l l a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall l (l :: l) m. Monoid m => Labeled @l l m -> m
fold :: forall m. Monoid m => Labeled @l l m -> m
$cfoldMap :: forall l (l :: l) m a. Monoid m => (a -> m) -> Labeled @l l a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Labeled @l l a -> m
$cfoldMap' :: forall l (l :: l) m a. Monoid m => (a -> m) -> Labeled @l l a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Labeled @l l a -> m
$cfoldr :: forall l (l :: l) a b. (a -> b -> b) -> b -> Labeled @l l a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Labeled @l l a -> b
$cfoldr' :: forall l (l :: l) a b. (a -> b -> b) -> b -> Labeled @l l a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Labeled @l l a -> b
$cfoldl :: forall l (l :: l) b a. (b -> a -> b) -> b -> Labeled @l l a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Labeled @l l a -> b
$cfoldl' :: forall l (l :: l) b a. (b -> a -> b) -> b -> Labeled @l l a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Labeled @l l a -> b
$cfoldr1 :: forall l (l :: l) a. (a -> a -> a) -> Labeled @l l a -> a
foldr1 :: forall a. (a -> a -> a) -> Labeled @l l a -> a
$cfoldl1 :: forall l (l :: l) a. (a -> a -> a) -> Labeled @l l a -> a
foldl1 :: forall a. (a -> a -> a) -> Labeled @l l a -> a
$ctoList :: forall l (l :: l) a. Labeled @l l a -> [a]
toList :: forall a. Labeled @l l a -> [a]
$cnull :: forall l (l :: l) a. Labeled @l l a -> Bool
null :: forall a. Labeled @l l a -> Bool
$clength :: forall l (l :: l) a. Labeled @l l a -> Int
length :: forall a. Labeled @l l a -> Int
$celem :: forall l (l :: l) a. Eq a => a -> Labeled @l l a -> Bool
elem :: forall a. Eq a => a -> Labeled @l l a -> Bool
$cmaximum :: forall l (l :: l) a. Ord a => Labeled @l l a -> a
maximum :: forall a. Ord a => Labeled @l l a -> a
$cminimum :: forall l (l :: l) a. Ord a => Labeled @l l a -> a
minimum :: forall a. Ord a => Labeled @l l a -> a
$csum :: forall l (l :: l) a. Num a => Labeled @l l a -> a
sum :: forall a. Num a => Labeled @l l a -> a
$cproduct :: forall l (l :: l) a. Num a => Labeled @l l a -> a
product :: forall a. Num a => Labeled @l l a -> a
Foldable, Functor (Labeled @l l)
Foldable (Labeled @l l)
Functor (Labeled @l l)
-> Foldable (Labeled @l l)
-> (forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> Labeled @l l a -> f (Labeled @l l b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    Labeled @l l (f a) -> f (Labeled @l l a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> Labeled @l l a -> m (Labeled @l l b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    Labeled @l l (m a) -> m (Labeled @l l a))
-> Traversable (Labeled @l l)
forall l (l :: l). Functor (Labeled @l l)
forall l (l :: l). Foldable (Labeled @l l)
forall l (l :: l) (m :: Type -> Type) a.
Monad m =>
Labeled @l l (m a) -> m (Labeled @l l a)
forall l (l :: l) (f :: Type -> Type) a.
Applicative f =>
Labeled @l l (f a) -> f (Labeled @l l a)
forall l (l :: l) (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Labeled @l l a -> m (Labeled @l l b)
forall l (l :: l) (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Labeled @l l a -> f (Labeled @l l b)
forall (t :: Type -> Type).
Functor t
-> Foldable t
-> (forall (f :: Type -> Type) a b.
    Applicative f =>
    (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a.
Monad m =>
Labeled @l l (m a) -> m (Labeled @l l a)
forall (f :: Type -> Type) a.
Applicative f =>
Labeled @l l (f a) -> f (Labeled @l l a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Labeled @l l a -> m (Labeled @l l b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Labeled @l l a -> f (Labeled @l l b)
$ctraverse :: forall l (l :: l) (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Labeled @l l a -> f (Labeled @l l b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> Labeled @l l a -> f (Labeled @l l b)
$csequenceA :: forall l (l :: l) (f :: Type -> Type) a.
Applicative f =>
Labeled @l l (f a) -> f (Labeled @l l a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
Labeled @l l (f a) -> f (Labeled @l l a)
$cmapM :: forall l (l :: l) (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Labeled @l l a -> m (Labeled @l l b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> Labeled @l l a -> m (Labeled @l l b)
$csequence :: forall l (l :: l) (m :: Type -> Type) a.
Monad m =>
Labeled @l l (m a) -> m (Labeled @l l a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
Labeled @l l (m a) -> m (Labeled @l l a)
Traversable, (forall x. Labeled @l l a -> Rep (Labeled @l l a) x)
-> (forall x. Rep (Labeled @l l a) x -> Labeled @l l a)
-> Generic (Labeled @l l a)
forall x. Rep (Labeled @l l a) x -> Labeled @l l a
forall x. Labeled @l l a -> Rep (Labeled @l l a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall l (l :: l) a x. Rep (Labeled @l l a) x -> Labeled @l l a
forall l (l :: l) a x. Labeled @l l a -> Rep (Labeled @l l a) x
$cfrom :: forall l (l :: l) a x. Labeled @l l a -> Rep (Labeled @l l a) x
from :: forall x. Labeled @l l a -> Rep (Labeled @l l a) x
$cto :: forall l (l :: l) a x. Rep (Labeled @l l a) x -> Labeled @l l a
to :: forall x. Rep (Labeled @l l a) x -> Labeled @l l a
Generic)

-- | gets an element given a path into the tree
getElemWithPath :: forall typ t f. Path typ t -> HTree f t -> f typ
getElemWithPath :: forall {k} (typ :: k) (t :: TyTree @Type k) (f :: k -> Type).
Path @k typ t -> HTree @k f t -> f typ
getElemWithPath Path @k typ t
Here (HNode f a
e HForest @k f ts
_) = f typ
f a
e
getElemWithPath (Farther Path @k typ ('TyNode @k b ts)
pt) (HNode f a
e (HTree @k f x
_ `HCons` HList @(TyTree @Type k) (HTree @k f) xs
ts)) = Path @k typ ('TyNode @k b ts)
-> HTree @k f ('TyNode @k b ts) -> f typ
forall {k} (typ :: k) (t :: TyTree @Type k) (f :: k -> Type).
Path @k typ t -> HTree @k f t -> f typ
getElemWithPath Path @k typ ('TyNode @k b ts)
pt (f b -> HForest @k f ts -> HTree @k f ('TyNode @k b ts)
forall {k} (f :: k -> Type) (a :: k) (ts :: TyForest @Type k).
f a -> HForest @k f ts -> HTree @k f ('TyNode @k a ts)
HNode f b
f a
e HForest @k f ts
HList @(TyTree @Type k) (HTree @k f) xs
ts)
getElemWithPath (Deeper Path @k typ t1
pt) (HNode f a
_ (HTree @k f x
t `HCons` HList @(TyTree @Type k) (HTree @k f) xs
_)) = Path @k typ t1 -> HTree @k f t1 -> f typ
forall {k} (typ :: k) (t :: TyTree @Type k) (f :: k -> Type).
Path @k typ t -> HTree @k f t -> f typ
getElemWithPath Path @k typ t1
pt HTree @k f t1
HTree @k f x
t

-- | searches a tree for an element and returns that element
getElem' :: forall {proxy} strat typ t f. HasField' (strat :: SearchStrategy) typ t => proxy strat -> HTree f t -> f typ
getElem' :: forall {proxy :: SearchStrategy -> Type} (strat :: SearchStrategy)
       typ (t :: TyTree @Type Type) (f :: Type -> Type).
HasField' strat typ t =>
proxy strat -> HTree @Type f t -> f typ
getElem' proxy strat
_ = Path @Type typ t -> HTree @Type f t -> f typ
forall {k} (typ :: k) (t :: TyTree @Type k) (f :: k -> Type).
Path @k typ t -> HTree @k f t -> f typ
getElemWithPath (forall (strat :: SearchStrategy) typ (t :: TyTree @Type Type)
       {proxy :: SearchStrategy -> Type}.
HasField' strat typ t =>
proxy strat -> Path @Type typ t
evidence @strat @typ @t Proxy @SearchStrategy strat
forall {k} (t :: k). Proxy @k t
Proxy)

-- | searches a tree for an element and returns that element, specialised to 'Labeled' and unwraps
--
-- >>> import Data.Functor.Identity
-- >>> type T = TyNodeL "top" Int [ TyNodeL "inter" Int '[ TyNodeL "foo" Int '[]], TyNodeL "foo" Int '[]]
-- >>> t :: HTree Identity T = 42 `HNodeL` HNodeL 4 (HNodeL 69 HNil `HCons` HNil) `HCons` HNodeL 67 HNil `HCons` HNil
-- >>> getElem @'DFS @"foo" @Int Proxy t
-- Identity 69
-- >>> getElem @'BFS @"foo" @Int Proxy t
-- Identity 67
getElem
  :: forall {proxy} strat l typ t f
   . ( HasField' (strat :: SearchStrategy) (Labeled l typ) t
     , Functor f
     )
  => proxy strat
  -> HTree f t
  -> f typ
getElem :: forall {l} {proxy :: SearchStrategy -> Type}
       (strat :: SearchStrategy) (l :: l) typ (t :: TyTree @Type Type)
       (f :: Type -> Type).
(HasField' strat (Labeled @l l typ) t, Functor f) =>
proxy strat -> HTree @Type f t -> f typ
getElem proxy strat
_ = (Labeled @l l typ -> typ) -> f (Labeled @l l typ) -> f typ
forall a b. (a -> b) -> f a -> f b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap Labeled @l l typ -> typ
forall l (l :: l) a. Labeled @l l a -> a
unLabel (f (Labeled @l l typ) -> f typ)
-> (HTree @Type f t -> f (Labeled @l l typ))
-> HTree @Type f t
-> f typ
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Path @Type (Labeled @l l typ) t
-> HTree @Type f t -> f (Labeled @l l typ)
forall {k} (typ :: k) (t :: TyTree @Type k) (f :: k -> Type).
Path @k typ t -> HTree @k f t -> f typ
getElemWithPath (forall (strat :: SearchStrategy) typ (t :: TyTree @Type Type)
       {proxy :: SearchStrategy -> Type}.
HasField' strat typ t =>
proxy strat -> Path @Type typ t
evidence @strat @(Labeled l typ) @t Proxy @SearchStrategy strat
forall {k} (t :: k). Proxy @k t
Proxy)

-- the default behaviour is a breadth first search
instance (HasField' 'BFS (Labeled l typ) t, Functor f) => HasField l (HTree f t) (f typ) where
  getField :: HTree @Type f t -> f typ
getField = forall {l} {proxy :: SearchStrategy -> Type}
       (strat :: SearchStrategy) (l :: l) typ (t :: TyTree @Type Type)
       (f :: Type -> Type).
(HasField' strat (Labeled @l l typ) t, Functor f) =>
proxy strat -> HTree @Type f t -> f typ
forall (strat :: SearchStrategy) (l :: k) typ
       (t :: TyTree @Type Type) (f :: Type -> Type).
(HasField' strat (Labeled @k l typ) t, Functor f) =>
Proxy @SearchStrategy strat -> HTree @Type f t -> f typ
getElem @'BFS @l @typ @t Proxy @SearchStrategy 'BFS
forall {k} (t :: k). Proxy @k t
Proxy

-- | simple typelevel predicate that tests whether some element is in a tree
type Elem :: forall k. k -> TyTree k -> Bool
type family Elem typ t where
  Elem a ('TyNode a ts) = 'True
  Elem a ('TyNode a' ts) = AnyElem a ts
  Elem a t = 'False

-- | typelevel predicate that tests whether the element is in any of the
--   subtrees
type AnyElem :: forall k. k -> TyForest k -> Bool
type family AnyElem typ ts where
  AnyElem a (t : ts) = Elem a t || AnyElem a ts
  AnyElem a '[] = 'False

-- | the search strategy used in 'HasField'', this is intended to be used only as a DataKind
type SearchStrategy :: Type
data SearchStrategy = DFS | BFS

-- | This is the helper class that creates evidence,
--   it implements a DFS together with Decide
type HasField' :: SearchStrategy -> Type -> TyTree Type -> Constraint
class HasField' strat typ t | strat t -> typ where
  evidence :: forall {proxy}. proxy strat -> Path typ t

-- | Together with HasField' implements a DFS in the tree
type Decide :: SearchStrategy -> Bool -> Type -> TyTree Type -> Constraint
class Decide strat elem typ t | strat t -> typ where
  evidence' :: forall {proxy :: forall k. k -> Type}. proxy strat -> proxy elem -> Path typ t

instance HasField' 'DFS typ ('TyNode typ (t : ts)) where
  evidence :: forall {proxy :: SearchStrategy -> Type}.
proxy 'DFS
-> Path
     @Type typ ('TyNode @Type typ ((':) @(TyTree @Type Type) t ts))
evidence proxy 'DFS
_ = Path @Type typ ('TyNode @Type typ ((':) @(TyTree @Type Type) t ts))
forall {k} (k1 :: k) (ts :: TyForest @Type k).
Path @k k1 ('TyNode @k k1 ts)
Here

instance HasField' 'BFS typ ('TyNode typ (t : ts)) where
  evidence :: forall {proxy :: SearchStrategy -> Type}.
proxy 'BFS
-> Path
     @Type typ ('TyNode @Type typ ((':) @(TyTree @Type Type) t ts))
evidence proxy 'BFS
_ = Path @Type typ ('TyNode @Type typ ((':) @(TyTree @Type Type) t ts))
forall {k} (k1 :: k) (ts :: TyForest @Type k).
Path @k k1 ('TyNode @k k1 ts)
Here

instance HasField' 'DFS typ ('TyNode typ '[]) where
  evidence :: forall {proxy :: SearchStrategy -> Type}.
proxy 'DFS
-> Path @Type typ ('TyNode @Type typ ('[] @(TyTree @Type Type)))
evidence proxy 'DFS
_ = Path @Type typ ('TyNode @Type typ ('[] @(TyTree @Type Type)))
forall {k} (k1 :: k) (ts :: TyForest @Type k).
Path @k k1 ('TyNode @k k1 ts)
Here

instance HasField' 'BFS typ ('TyNode typ '[]) where
  evidence :: forall {proxy :: SearchStrategy -> Type}.
proxy 'BFS
-> Path @Type typ ('TyNode @Type typ ('[] @(TyTree @Type Type)))
evidence proxy 'BFS
_ = Path @Type typ ('TyNode @Type typ ('[] @(TyTree @Type Type)))
forall {k} (k1 :: k) (ts :: TyForest @Type k).
Path @k k1 ('TyNode @k k1 ts)
Here

instance
  {-# OVERLAPPABLE #-}
  Decide
    'BFS
    (AnyElem typ ts)
    typ
    ('TyNode typ' (t : ts))
  => HasField' 'BFS typ ('TyNode typ' (t : ts))
  where
  evidence :: forall {proxy :: SearchStrategy -> Type}.
proxy 'BFS
-> Path
     @Type typ ('TyNode @Type typ' ((':) @(TyTree @Type Type) t ts))
evidence proxy 'BFS
_ = forall (strat :: SearchStrategy) (elem :: Bool) typ
       (t :: TyTree @Type Type) {proxy :: forall k. k -> Type}.
Decide strat elem typ t =>
proxy @SearchStrategy strat -> proxy @Bool elem -> Path @Type typ t
evidence' @'BFS @(AnyElem typ ts) @typ @('TyNode typ' (t : ts)) Proxy @SearchStrategy 'BFS
forall {k} (t :: k). Proxy @k t
Proxy Proxy @Bool (AnyElem @Type typ ts)
forall {k} (t :: k). Proxy @k t
Proxy

instance
  {-# OVERLAPPABLE #-}
  Decide
    'DFS
    (Not (Elem typ t))
    typ
    ('TyNode typ' (t : ts))
  => HasField' 'DFS typ ('TyNode typ' (t : ts))
  where
  evidence :: forall {proxy :: SearchStrategy -> Type}.
proxy 'DFS
-> Path
     @Type typ ('TyNode @Type typ' ((':) @(TyTree @Type Type) t ts))
evidence proxy 'DFS
_ = forall (strat :: SearchStrategy) (elem :: Bool) typ
       (t :: TyTree @Type Type) {proxy :: forall k. k -> Type}.
Decide strat elem typ t =>
proxy @SearchStrategy strat -> proxy @Bool elem -> Path @Type typ t
evidence' @'DFS @(Not (Elem typ t)) @typ @('TyNode typ' (t : ts)) Proxy @SearchStrategy 'DFS
forall {k} (t :: k). Proxy @k t
Proxy Proxy @Bool (Not (Elem @Type typ t))
forall {k} (t :: k). Proxy @k t
Proxy

instance
  HasField' strat typ t
  => Decide strat 'False typ ('TyNode typ' (t : ts'))
  where
  evidence' :: forall {proxy :: forall k. k -> Type}.
proxy @SearchStrategy strat
-> proxy @Bool 'False
-> Path
     @Type typ ('TyNode @Type typ' ((':) @(TyTree @Type Type) t ts'))
evidence' proxy @SearchStrategy strat
_ proxy @Bool 'False
_ = Path @Type typ t
-> Path
     @Type typ ('TyNode @Type typ' ((':) @(TyTree @Type Type) t ts'))
forall {k} (k1 :: k) (b :: k) (t1 :: TyTree @Type k)
       (ts :: TyForest @Type k).
Path @k k1 t1
-> Path @k k1 ('TyNode @k b ((':) @(TyTree @Type k) t1 ts))
Deeper (forall (strat :: SearchStrategy) typ (t :: TyTree @Type Type)
       {proxy :: SearchStrategy -> Type}.
HasField' strat typ t =>
proxy strat -> Path @Type typ t
evidence @strat @typ @t Proxy @SearchStrategy strat
forall {k} (t :: k). Proxy @k t
Proxy)

instance
  HasField' strat typ ('TyNode typ' ts)
  => Decide strat 'True typ ('TyNode typ' (t' : ts))
  where
  evidence' :: forall {proxy :: forall k. k -> Type}.
proxy @SearchStrategy strat
-> proxy @Bool 'True
-> Path
     @Type typ ('TyNode @Type typ' ((':) @(TyTree @Type Type) t' ts))
evidence' proxy @SearchStrategy strat
_ proxy @Bool 'True
_ = Path @Type typ ('TyNode @Type typ' ts)
-> Path
     @Type typ ('TyNode @Type typ' ((':) @(TyTree @Type Type) t' ts))
forall {k} (k1 :: k) (b :: k) (t1 :: TyTree @Type k)
       (ts :: TyForest @Type k).
Path @k k1 ('TyNode @k b ts)
-> Path @k k1 ('TyNode @k b ((':) @(TyTree @Type k) t1 ts))
Farther (forall (strat :: SearchStrategy) typ (t :: TyTree @Type Type)
       {proxy :: SearchStrategy -> Type}.
HasField' strat typ t =>
proxy strat -> Path @Type typ t
evidence @strat @typ @('TyNode typ' ts) Proxy @SearchStrategy strat
forall {k} (t :: k). Proxy @k t
Proxy)

infixr 4 `HNodeL`

infixr 4 `TyNodeL`