{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}
module Data.HTree.Labeled
(
Labeled (..)
, pattern HNodeL
, pattern HLeafL
, type TyNodeL
, getElem
, getElem'
, SearchStrategy (..)
, HasField (..)
, Proxy (..)
, 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))
type TyNodeL l a = 'TyNode (Labeled l a)
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 #-}
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
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)
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
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)
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)
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
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
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
type SearchStrategy :: Type
data SearchStrategy = DFS | BFS
type HasField' :: SearchStrategy -> Type -> TyTree Type -> Constraint
class HasField' strat typ t | strat t -> typ where
evidence :: forall {proxy}. proxy strat -> Path typ t
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`