Helpers.hs

module Spec.HTree.Helpers (forgetHTree, forgetHList, liftedWith) where

import Data.Functor.Const (Const (Const, getConst))
import Data.HTree.Existential (Some (MkSome))
import Data.HTree.List (HList (HCons, HNil), hmap)
import Data.HTree.Tree (HTree (HNode))
import Data.Kind (Type)
import Data.Tree (Tree (Node))

forgetHTree :: forall a t. HTree (Const a) t -> Tree a
forgetHTree (HNode x ts) = Node (getConst x) (forgetHList (hmap (Const . forgetHTree) ts))

forgetHList :: forall a l. HList (Const a) l -> [a]
forgetHList HNil = []
forgetHList (HCons x xs) = getConst x : forgetHList xs

liftedWith :: forall {l} (g :: l -> Type) f r. Functor f => f (Some g) -> (forall m. g m -> r) -> f r
liftedWith a f = fmap \case { MkSome b -> f b } a