{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Eta reduce" #-}

-- | implements a heterogeneous tree ('HTree') indexed by a homogeneous type level tree ('TyTree')
module Data.HTree.Tree
  ( -- * type level tree
    TyTree (..)
  , TyForest

    -- * heterogeneous tree
  , HTree (HLeaf, ..)
  , HForest

    -- * mapping

    -- ** value level
  , hmap
  , hcmap

    -- * type level
  , TreeMap
  , ForestMap

    -- * traversing
  , htraverse
  , hctraverse

    -- *  folding

    -- ** value level
  , hFoldMap
  , hcFoldMap
  , hFlatten

    -- ** type level
  , FlattenTree
  , FlattenForest

    -- * paths into the htree and things you can do with those
  , Path (..)
  , replaceAt

    -- * helpful constraints
  , AllTree
  , AllTreeC
  , AllForest

    -- ** helpers for witnessing the constraints
  , allTopHTree
  , allTopHForest
  )
where

import Data.Functor.Identity (Identity (Identity, runIdentity))
import Data.HTree.Constraint (Dict, withDict, pattern Dict)
import Data.HTree.Families (All, Top, type (++))
import Data.HTree.List (HList (HCons, HNil), hconcat)
import Data.HTree.List qualified as L
import Data.Kind (Constraint, Type)

-- | a type level rose-tree that is only intended to
--   store something of a certain kind, e.g. Type
type TyTree :: forall k. k -> Type
data TyTree k where
  TyNode :: forall a. a -> TyForest a -> TyTree a

-- | a forest of TyTrees
type TyForest :: forall k. k -> Type
type TyForest a = [TyTree a]

-- | a heterogeneous rose tree indexed by a TyTree
type HTree :: forall k. (k -> Type) -> TyTree k -> Type
data HTree f t where
  HNode :: forall f a ts. f a -> HForest f ts -> HTree f ('TyNode a ts)

-- | a pattern synonym for the leaf of an HTree
pattern HLeaf :: forall f a. forall. f a -> HTree f ('TyNode a '[])
pattern $mHLeaf :: forall {r} {a1} {f :: a1 -> Type} {a :: a1}.
HTree @a1 f ('TyNode @a1 a ('[] @(TyTree @Type a1)))
-> (f a -> r) -> ((# #) -> r) -> r
$bHLeaf :: forall {a1} (f :: a1 -> Type) (a :: a1).
f a -> HTree @a1 f ('TyNode @a1 a ('[] @(TyTree @Type a1)))
HLeaf a = HNode a HNil

-- | A forest of heterogeneous rose trees
type HForest :: forall k. (k -> Type) -> TyForest k -> Type
type HForest f ts = HList (HTree f) ts

-- | map a function over an HTree
hmap
  :: forall {k} (f :: k -> Type) (g :: k -> Type) (t :: TyTree k)
   . (forall a. f a -> g a)
  -> HTree f t
  -> HTree g t
hmap :: forall {k} (f :: k -> Type) (g :: k -> Type) (t :: TyTree @Type k).
(forall (a :: k). f a -> g a) -> HTree @k f t -> HTree @k g t
hmap forall (a :: k). f a -> g a
f HTree @k f t
t = Dict (AllTree @k (Top @k) t)
-> (AllTree @k (Top @k) t => HTree @k g t) -> HTree @k g t
forall (c :: Constraint) r. Dict c -> (c => r) -> r
withDict (HTree @k f t -> Dict (AllTree @k (Top @k) t)
forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> Dict (AllTree @k (Top @k) t)
allTopHTree HTree @k f t
t) ((AllTree @k (Top @k) t => HTree @k g t) -> HTree @k g t)
-> (AllTree @k (Top @k) t => HTree @k g t) -> HTree @k g t
forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (f :: k -> Type) (g :: k -> Type)
       (t :: TyTree @Type k).
AllTree @k c t =>
(forall (a :: k). c a => f a -> g a)
-> HTree @k f t -> HTree @k g t
forall (c :: k -> Constraint) (f :: k -> Type) (g :: k -> Type)
       (t :: TyTree @Type k).
AllTree @k c t =>
(forall (a :: k). c a => f a -> g a)
-> HTree @k f t -> HTree @k g t
hcmap @Top @f @g f a -> g a
forall (a :: k). f a -> g a
forall (a :: k). Top @k a => f a -> g a
f HTree @k f t
t

-- | map a function with a constraint over an HTree
hcmap
  :: forall
    {k}
    (c :: k -> Constraint)
    (f :: k -> Type)
    (g :: k -> Type)
    (t :: TyTree k)
   . AllTree c t
  => (forall a. c a => f a -> g a)
  -> HTree f t
  -> HTree g t
hcmap :: forall {k} (c :: k -> Constraint) (f :: k -> Type) (g :: k -> Type)
       (t :: TyTree @Type k).
AllTree @k c t =>
(forall (a :: k). c a => f a -> g a)
-> HTree @k f t -> HTree @k g t
hcmap forall (a :: k). c a => f a -> g a
f = Identity (HTree @k g t) -> HTree @k g t
forall a. Identity a -> a
runIdentity (Identity (HTree @k g t) -> HTree @k g t)
-> (HTree @k f t -> Identity (HTree @k g t))
-> HTree @k f t
-> HTree @k g t
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} (c :: k -> Constraint) (h :: Type -> Type)
       (f :: k -> Type) (g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
forall (c :: k -> Constraint) (h :: Type -> Type) (f :: k -> Type)
       (g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
hctraverse @c @Identity @f @g (g a -> Identity (g a)
forall a. a -> Identity a
Identity (g a -> Identity (g a)) -> (f a -> g a) -> f a -> Identity (g a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> g a
forall (a :: k). c a => f a -> g a
f)

-- | traverse a structure with a function
htraverse
  :: forall
    {k}
    (h :: Type -> Type)
    (f :: k -> Type)
    (g :: k -> Type)
    (t :: TyTree k)
   . Applicative h
  => (forall a. f a -> h (g a))
  -> HTree f t
  -> h (HTree g t)
htraverse :: forall {k} (h :: Type -> Type) (f :: k -> Type) (g :: k -> Type)
       (t :: TyTree @Type k).
Applicative h =>
(forall (a :: k). f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
htraverse forall (a :: k). f a -> h (g a)
f HTree @k f t
t = Dict (AllTree @k (Top @k) t)
-> (AllTree @k (Top @k) t => h (HTree @k g t)) -> h (HTree @k g t)
forall (c :: Constraint) r. Dict c -> (c => r) -> r
withDict (HTree @k f t -> Dict (AllTree @k (Top @k) t)
forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> Dict (AllTree @k (Top @k) t)
allTopHTree HTree @k f t
t) ((AllTree @k (Top @k) t => h (HTree @k g t)) -> h (HTree @k g t))
-> (AllTree @k (Top @k) t => h (HTree @k g t)) -> h (HTree @k g t)
forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (h :: Type -> Type)
       (f :: k -> Type) (g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
forall (c :: k -> Constraint) (h :: Type -> Type) (f :: k -> Type)
       (g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
hctraverse @Top f a -> h (g a)
forall (a :: k). f a -> h (g a)
forall (a :: k). Top @k a => f a -> h (g a)
f HTree @k f t
t

-- | traverse a structure such that a constraint holds; this is the workhorse of mapping and traversing
hctraverse
  :: forall
    {k}
    (c :: k -> Constraint)
    (h :: Type -> Type)
    (f :: k -> Type)
    (g :: k -> Type)
    (t :: TyTree k)
   . (AllTree c t, Applicative h)
  => (forall a. c a => f a -> h (g a))
  -> HTree f t
  -> h (HTree g t)
hctraverse :: forall {k} (c :: k -> Constraint) (h :: Type -> Type)
       (f :: k -> Type) (g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
hctraverse forall (a :: k). c a => f a -> h (g a)
f (HNode f a
x HForest @k f ts
ts) = g a -> HForest @k g ts -> HTree @k g t
g a -> HForest @k g ts -> HTree @k g ('TyNode @k 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 (g a -> HForest @k g ts -> HTree @k g t)
-> h (g a) -> h (HForest @k g ts -> HTree @k g t)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> f a -> h (g a)
forall (a :: k). c a => f a -> h (g a)
f f a
x h (HForest @k g ts -> HTree @k g t)
-> h (HForest @k g ts) -> h (HTree @k g t)
forall a b. h (a -> b) -> h a -> h b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall {k} (c :: k -> Constraint) (t :: Type -> Type)
       (f :: k -> Type) (g :: k -> Type) (xs :: [k]).
(All @k c xs, Applicative t) =>
(forall (a :: k). c a => f a -> t (g a))
-> HList @k f xs -> t (HList @k g xs)
forall (c :: TyTree @Type k -> Constraint) (t :: Type -> Type)
       (f :: TyTree @Type k -> Type) (g :: TyTree @Type k -> Type)
       (xs :: [TyTree @Type k]).
(All @(TyTree @Type k) c xs, Applicative t) =>
(forall (a :: TyTree @Type k). c a => f a -> t (g a))
-> HList @(TyTree @Type k) f xs -> t (HList @(TyTree @Type k) g xs)
L.hctraverse @(AllTreeC c) @h @(HTree f) @(HTree g) (forall {k} (c :: k -> Constraint) (h :: Type -> Type)
       (f :: k -> Type) (g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
forall (c :: k -> Constraint) (h :: Type -> Type) (f :: k -> Type)
       (g :: k -> Type) (t :: TyTree @Type k).
(AllTree @k c t, Applicative h) =>
(forall (a :: k). c a => f a -> h (g a))
-> HTree @k f t -> h (HTree @k g t)
hctraverse @c f a -> h (g a)
forall (a :: k). c a => f a -> h (g a)
f) HForest @k f ts
ts

-- | map a functor over a TyTree
type TreeMap :: forall k l. (k -> l) -> TyTree k -> TyTree l
type family TreeMap f t where
  forall f x. TreeMap f ('TyNode x '[]) = 'TyNode (f x) '[]
  forall f x xs. TreeMap f ('TyNode x xs) = 'TyNode (f x) (ForestMap f xs)

-- | map a functor over a TyForest
type ForestMap :: forall k l. (k -> l) -> TyForest k -> TyForest l
type family ForestMap f t where
  ForestMap _ '[] = '[]
  forall f n ns. ForestMap f (n : ns) = TreeMap f n : ForestMap f ns

-- | monoidally folds down a tree to a single value using a constraint on
--   the element in the wrapping functor, this is similar to 'foldMap'
hcFoldMap
  :: forall
    {k}
    (c :: k -> Constraint)
    (f :: k -> Type)
    (t :: TyTree k)
    (b :: Type)
   . (AllTree c t, Semigroup b)
  => (forall a. c a => f a -> b)
  -> HTree f t
  -> b
hcFoldMap :: forall {k} (c :: k -> Constraint) (f :: k -> Type)
       (t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
hcFoldMap forall (a :: k). c a => f a -> b
f (HNode f a
x HList @(TyTree @Type k) (HTree @k f) ts
HNil) = f a -> b
forall (a :: k). c a => f a -> b
f f a
x
hcFoldMap forall (a :: k). c a => f a -> b
f (HNode f a
x (HTree @k f x
y `HCons` HList @(TyTree @Type k) (HTree @k f) xs
ys)) = forall {k} (c :: k -> Constraint) (f :: k -> Type)
       (t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
forall (c :: k -> Constraint) (f :: k -> Type)
       (t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
hcFoldMap @c f a -> b
forall (a :: k). c a => f a -> b
f HTree @k f x
y b -> b -> b
forall a. Semigroup a => a -> a -> a
<> forall {k} (c :: k -> Constraint) (f :: k -> Type)
       (t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
forall (c :: k -> Constraint) (f :: k -> Type)
       (t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
hcFoldMap @c f a -> b
forall (a :: k). c a => f a -> b
f (f a
-> HList @(TyTree @Type k) (HTree @k f) xs
-> HTree @k f ('TyNode @k a xs)
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 a
x HList @(TyTree @Type k) (HTree @k f) xs
ys)

-- | monoidally folds down a tree to a single value, this is similar to 'foldMap'
hFoldMap
  :: forall
    {k}
    (f :: k -> Type)
    (t :: TyTree k)
    (b :: Type)
   . Semigroup b
  => (forall a. f a -> b)
  -> HTree f t
  -> b
hFoldMap :: forall {k} (f :: k -> Type) (t :: TyTree @Type k) b.
Semigroup b =>
(forall (a :: k). f a -> b) -> HTree @k f t -> b
hFoldMap forall (a :: k). f a -> b
f HTree @k f t
t = Dict (AllTree @k (Top @k) t) -> (AllTree @k (Top @k) t => b) -> b
forall (c :: Constraint) r. Dict c -> (c => r) -> r
withDict (HTree @k f t -> Dict (AllTree @k (Top @k) t)
forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> Dict (AllTree @k (Top @k) t)
allTopHTree HTree @k f t
t) ((AllTree @k (Top @k) t => b) -> b)
-> (AllTree @k (Top @k) t => b) -> b
forall a b. (a -> b) -> a -> b
$ forall {k} (c :: k -> Constraint) (f :: k -> Type)
       (t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
forall (c :: k -> Constraint) (f :: k -> Type)
       (t :: TyTree @Type k) b.
(AllTree @k c t, Semigroup b) =>
(forall (a :: k). c a => f a -> b) -> HTree @k f t -> b
hcFoldMap @Top f a -> b
forall (a :: k). f a -> b
forall (a :: k). Top @k a => f a -> b
f HTree @k f t
t

-- | flatten a heterogeneous tree down to a heterogeneous list
hFlatten
  :: forall
    {k}
    (f :: k -> Type)
    (t :: TyTree k)
   . HTree f t
  -> HList f (FlattenTree t)
hFlatten :: forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> HList @k f (FlattenTree @k t)
hFlatten (HNode f a
x HForest @k f ts
xs) = f a
x f a
-> HList @k f (FlattenForest @k ts)
-> HList @k f ((':) @k a (FlattenForest @k ts))
forall {k} (f :: k -> Type) (x :: k) (xs :: [k]).
f x -> HList @k f xs -> HList @k f ((':) @k x xs)
`HCons` HForest @k f ts -> HList @k f (FlattenForest @k ts)
forall (ts :: TyForest @Type k).
HForest @k f ts -> HList @k f (FlattenForest @k ts)
hflattenForest HForest @k f ts
xs
 where
  hflattenForest :: forall ts. HForest f ts -> HList f (FlattenForest ts)
  hflattenForest :: forall (ts :: TyForest @Type k).
HForest @k f ts -> HList @k f (FlattenForest @k ts)
hflattenForest HList @(TyTree @Type k) (HTree @k f) ts
HNil = HList @k f ('[] @k)
HList @k f (FlattenForest @k ts)
forall {k} (f :: k -> Type). HList @k f ('[] @k)
HNil
  hflattenForest (HTree @k f x
y `HCons` HList @(TyTree @Type k) (HTree @k f) xs
ys) = HTree @k f x -> HList @k f (FlattenTree @k x)
forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> HList @k f (FlattenTree @k t)
hFlatten HTree @k f x
y HList @k f (FlattenTree @k x)
-> HList @k f (FlattenForest @k xs)
-> HList @k f ((++) @k (FlattenTree @k x) (FlattenForest @k xs))
forall {k} (f :: k -> Type) (xs :: [k]) (ys :: [k]).
HList @k f xs -> HList @k f ys -> HList @k f ((++) @k xs ys)
`hconcat` HList @(TyTree @Type k) (HTree @k f) xs
-> HList @k f (FlattenForest @k xs)
forall (ts :: TyForest @Type k).
HForest @k f ts -> HList @k f (FlattenForest @k ts)
hflattenForest HList @(TyTree @Type k) (HTree @k f) xs
ys

-- | a type family that flattens a tree down to a list
type FlattenTree :: forall k. TyTree k -> [k]
type family FlattenTree t where
  forall x xs. FlattenTree ('TyNode x xs) = x : FlattenForest xs

-- | a type family that flattens a forest down to a list
type FlattenForest :: forall k. TyForest k -> [k]
type family FlattenForest f where
  FlattenForest '[] = '[]
  FlattenForest (x : xs) = FlattenTree x ++ FlattenForest xs

-- | a constraint holds for all elements in the tree
type AllTree :: forall k. (k -> Constraint) -> TyTree k -> Constraint
type family AllTree c ts where
  forall c x ts. AllTree c ('TyNode x ts) = (c x, AllForest c ts)

-- | constraint synonym for AllTree
type AllTreeC :: forall k. (k -> Constraint) -> TyTree k -> Constraint
class AllTree c ts => AllTreeC c ts

instance forall c ts. AllTree c ts => AllTreeC c ts

-- | a constraint holds for all elements in the forest
type AllForest :: forall k. (k -> Constraint) -> TyForest k -> Constraint
type family AllForest c t where
  AllForest c xs = All (AllTreeC c) xs

-- | witnesses that for any HTree the constraint AllTree Top always holds
allTopHTree :: forall f t. HTree f t -> Dict (AllTree Top t)
allTopHTree :: forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> Dict (AllTree @k (Top @k) t)
allTopHTree (HNode f a
_ (HForest @k f ts -> Dict (AllForest @k (Top @k) ts)
forall {k} (f :: k -> Type) (t :: TyForest @Type k).
HForest @k f t -> Dict (AllForest @k (Top @k) t)
allTopHForest -> Dict (All @(TyTree @Type k) (AllTreeC @k (Top @k)) ts)
Dict (AllForest @k (Top @k) ts)
Dict)) = Dict (Top @k a, All @(TyTree @Type k) (AllTreeC @k (Top @k)) ts)
Has @Type (Charge @Type (AllTree @k (Top @k) t)) (Proxy @Type) ()
forall (c :: Constraint). c => Dict c
Dict

-- | witnesses that for any HForest the constraint AllForest Top always holds
allTopHForest :: forall f t. HForest f t -> Dict (AllForest Top t)
allTopHForest :: forall {k} (f :: k -> Type) (t :: TyForest @Type k).
HForest @k f t -> Dict (AllForest @k (Top @k) t)
allTopHForest HList @(TyTree @Type k) (HTree @k f) t
HNil = Dict (() :: Constraint)
Has @Type (Charge @Type (AllForest @k (Top @k) t)) (Proxy @Type) ()
forall (c :: Constraint). c => Dict c
Dict
allTopHForest (HCons (HTree @k f x -> Dict (AllTree @k (Top @k) x)
forall {k} (f :: k -> Type) (t :: TyTree @Type k).
HTree @k f t -> Dict (AllTree @k (Top @k) t)
allTopHTree -> Dict (AllTree @k (Top @k) x)
Dict) (HList @(TyTree @Type k) (HTree @k f) xs
-> Dict (AllForest @k (Top @k) xs)
forall {k} (f :: k -> Type) (t :: TyForest @Type k).
HForest @k f t -> Dict (AllForest @k (Top @k) t)
allTopHForest -> Dict (All @(TyTree @Type k) (AllTreeC @k (Top @k)) xs)
Dict (AllForest @k (Top @k) xs)
Dict)) = Dict
  (AllTreeC @k (Top @k) x,
   All @(TyTree @Type k) (AllTreeC @k (Top @k)) xs)
Has @Type (Charge @Type (AllForest @k (Top @k) t)) (Proxy @Type) ()
forall (c :: Constraint). c => Dict c
Dict

-- | replace an element at a certain path.
replaceAt :: Path typ t -> f typ -> HTree f t -> HTree f t
replaceAt :: forall {k} (typ :: k) (t :: TyTree @Type k) (f :: k -> Type).
Path @k typ t -> f typ -> HTree @k f t -> HTree @k f t
replaceAt Path @k typ t
Here f typ
x (HNode f a
_ HForest @k f ts
xs) = f typ -> HForest @k f ts -> HTree @k f ('TyNode @k typ 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 typ
x HForest @k f ts
xs
replaceAt (Deeper Path @k typ t
pt) f typ
x (HNode f a
y (HTree @k f x
t `HCons` HList @(TyTree @Type k) (HTree @k f) xs
ts)) = f a
-> HForest @k f ((':) @(TyTree @Type k) t xs)
-> HTree @k f ('TyNode @k a ((':) @(TyTree @Type k) t xs))
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 a
y (Path @k typ t -> f typ -> HTree @k f t -> HTree @k f t
forall {k} (typ :: k) (t :: TyTree @Type k) (f :: k -> Type).
Path @k typ t -> f typ -> HTree @k f t -> HTree @k f t
replaceAt Path @k typ t
pt f typ
x HTree @k f t
HTree @k f x
t HTree @k f t
-> HList @(TyTree @Type k) (HTree @k f) xs
-> HForest @k f ((':) @(TyTree @Type k) t xs)
forall {k} (f :: k -> Type) (x :: k) (xs :: [k]).
f x -> HList @k f xs -> HList @k f ((':) @k x xs)
`HCons` HList @(TyTree @Type k) (HTree @k f) xs
ts)
replaceAt (Farther Path @k typ ('TyNode @k b ts)
pt) f typ
x (HNode f a
y (HTree @k f x
t `HCons` HList @(TyTree @Type k) (HTree @k f) xs
ts)) = let HNode f b
f a
y' HList @(TyTree @Type k) (HTree @k f) ts
HForest @k f ts
ts' = Path @k typ ('TyNode @k b ts)
-> f typ
-> HTree @k f ('TyNode @k b ts)
-> HTree @k f ('TyNode @k b ts)
forall {k} (typ :: k) (t :: TyTree @Type k) (f :: k -> Type).
Path @k typ t -> f typ -> HTree @k f t -> HTree @k f t
replaceAt Path @k typ ('TyNode @k b ts)
pt f typ
x (f b
-> HList @(TyTree @Type k) (HTree @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
y HList @(TyTree @Type k) (HTree @k f) ts
HList @(TyTree @Type k) (HTree @k f) xs
ts) in f b
-> HForest @k f ((':) @(TyTree @Type k) x ts)
-> HTree @k f ('TyNode @k b ((':) @(TyTree @Type k) x 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
y' (HTree @k f x
t HTree @k f x
-> HList @(TyTree @Type k) (HTree @k f) ts
-> HForest @k f ((':) @(TyTree @Type k) x ts)
forall {k} (f :: k -> Type) (x :: k) (xs :: [k]).
f x -> HList @k f xs -> HList @k f ((':) @k x xs)
`HCons` HList @(TyTree @Type k) (HTree @k f) ts
ts')

-- | provides evidence that an element is in the tree by
--   providing a path to the element
type Path :: forall k. k -> TyTree k -> Type
data Path k t where
  Here :: forall a ts. Path a ('TyNode a ts)
  Deeper :: forall a b t ts. Path a t -> Path a ('TyNode b (t : ts))
  Farther :: forall a b t ts. Path a ('TyNode b ts) -> Path a ('TyNode b (t : ts))

infixr 4 `HNode`

infixr 4 `TyNode`

deriving stock instance (Show (f a), Show (HForest f t)) => Show (HTree f ('TyNode a t))

deriving stock instance (Eq (f a), Eq (HForest f t)) => Eq (HTree f ('TyNode a t))

deriving stock instance Show (Path typ t)

deriving stock instance Eq (Path typ t)