module UVMHS.Lib.TreeNested where

import UVMHS.Core
import UVMHS.Lib.Pretty

data 𝑇A a = 𝑇A
  { forall a. 𝑇A a -> 𝐼 a
vals𝑇A ∷ 𝐼 a
  , forall a. 𝑇A a -> 𝐼 (𝕊 ∧ 𝑇A a)
nest𝑇A ∷ 𝐼 (𝕊 ∧ 𝑇A a)
  } deriving (Int -> 𝑇A a -> ShowS
[𝑇A a] -> ShowS
𝑇A a -> String
(Int -> 𝑇A a -> ShowS)
-> (𝑇A a -> String) -> ([𝑇A a] -> ShowS) -> Show (𝑇A a)
forall a. Show a => Int -> 𝑇A a -> ShowS
forall a. Show a => [𝑇A a] -> ShowS
forall a. Show a => 𝑇A a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> 𝑇A a -> ShowS
showsPrec :: Int -> 𝑇A a -> ShowS
$cshow :: forall a. Show a => 𝑇A a -> String
show :: 𝑇A a -> String
$cshowList :: forall a. Show a => [𝑇A a] -> ShowS
showList :: [𝑇A a] -> ShowS
Show)

instance Null (𝑇A a) where 
  null :: 𝑇A a
null = 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
forall a. 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
𝑇A 𝐼 a
forall a. Null a => a
null 𝐼 (𝕊 ∧ 𝑇A a)
forall a. Null a => a
null
instance Append (𝑇A a) where 
  𝑇A 𝐼 a
m₁ 𝐼 (𝕊 ∧ 𝑇A a)
n₁ ⧺ :: 𝑇A a -> 𝑇A a -> 𝑇A a
⧺ 𝑇A 𝐼 a
m₂ 𝐼 (𝕊 ∧ 𝑇A a)
n₂ = 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
forall a. 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
𝑇A (𝐼 a
m₁ 𝐼 a -> 𝐼 a -> 𝐼 a
forall a. Append a => a -> a -> a
⧺ 𝐼 a
m₂) (𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a) -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
forall a b. (a -> b) -> a -> b
$ 𝐼 (𝕊 ∧ 𝑇A a)
n₁ 𝐼 (𝕊 ∧ 𝑇A a) -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝐼 (𝕊 ∧ 𝑇A a)
forall a. Append a => a -> a -> a
⧺ 𝐼 (𝕊 ∧ 𝑇A a)
n₂
instance Monoid (𝑇A a)

instance Eps (𝑇A a) where 
  eps :: 𝑇A a
eps = 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
forall a. 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
𝑇A 𝐼 a
forall a. Null a => a
null 𝐼 (𝕊 ∧ 𝑇A a)
forall a. Null a => a
null
instance Seq (𝑇A a) where
  𝑇A 𝐼 a
v₁ 𝐼 (𝕊 ∧ 𝑇A a)
n₁ ▷ :: 𝑇A a -> 𝑇A a -> 𝑇A a
▷ 𝑇A 𝐼 a
v₂ 𝐼 (𝕊 ∧ 𝑇A a)
n₂
    | 𝐼 (𝕊 ∧ 𝑇A a) -> 𝔹
forall a t. ToIter a t => t -> 𝔹
isEmpty 𝐼 (𝕊 ∧ 𝑇A a)
n₁ = 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
forall a. 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
𝑇A (𝐼 a
v₁ 𝐼 a -> 𝐼 a -> 𝐼 a
forall a. Append a => a -> a -> a
⧺ 𝐼 a
v₂) 𝐼 (𝕊 ∧ 𝑇A a)
n₂
    | 𝔹
otherwise = 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
forall a. 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
𝑇A 𝐼 a
v₁ (𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a) -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
forall a b. (a -> b) -> a -> b
$ ((𝕊 ∧ 𝑇A a) -> 𝕊 ∧ 𝑇A a) -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝐼 (𝕊 ∧ 𝑇A a)
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map ((𝑇A a -> 𝑇A a) -> (𝕊 ∧ 𝑇A a) -> 𝕊 ∧ 𝑇A a
forall b₁ b₂ a. (b₁ -> b₂) -> (a ∧ b₁) -> a ∧ b₂
mapSnd (𝑇A a -> 𝑇A a -> 𝑇A a
forall a. Seq a => a -> a -> a
▷ 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
forall a. 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
𝑇A 𝐼 a
v₂ 𝐼 (𝕊 ∧ 𝑇A a)
n₂)) 𝐼 (𝕊 ∧ 𝑇A a)
n₁
instance Seqoid (𝑇A a)

fold𝑇AWith ∷ (Monoid b) ⇒ (𝐼 a → b) → (𝕊 → b → b) → 𝑇A a → b
fold𝑇AWith :: forall b a. Monoid b => (𝐼 a -> b) -> (𝕊 -> b -> b) -> 𝑇A a -> b
fold𝑇AWith 𝐼 a -> b
fₗ 𝕊 -> b -> b
fₙ = 𝑇A a -> b
loop
  where 
    loop :: 𝑇A a -> b
loop (𝑇A 𝐼 a
vs 𝐼 (𝕊 ∧ 𝑇A a)
sxs) = [b] -> b
forall a t. (Monoid a, ToIter a t) => t -> a
concat
      [ 𝐼 a -> b
fₗ 𝐼 a
vs
      , 𝐼 b -> b
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 b -> b) -> 𝐼 b -> b
forall a b. (a -> b) -> a -> b
$ 𝐼 (𝕊 ∧ 𝑇A a) -> ((𝕊 ∧ 𝑇A a) -> b) -> 𝐼 b
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn (𝐼 (𝕊 ∧ 𝑇A a) -> 𝐼 (𝕊 ∧ 𝑇A a)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝐼 (𝕊 ∧ 𝑇A a)
sxs) (((𝕊 ∧ 𝑇A a) -> b) -> 𝐼 b) -> ((𝕊 ∧ 𝑇A a) -> b) -> 𝐼 b
forall a b. (a -> b) -> a -> b
$ \ (𝕊
s :* 𝑇A a
xs) →
          𝕊 -> b -> b
fₙ 𝕊
s (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ 𝑇A a -> b
loop 𝑇A a
xs
      ]

fold𝑇AOn ∷ (Monoid b) ⇒ 𝑇A a → (𝐼 a → b) → (𝕊 → b → b) → b
fold𝑇AOn :: forall b a. Monoid b => 𝑇A a -> (𝐼 a -> b) -> (𝕊 -> b -> b) -> b
fold𝑇AOn = ((𝐼 a -> b) -> (𝕊 -> b -> b) -> 𝑇A a -> b)
-> 𝑇A a -> (𝐼 a -> b) -> (𝕊 -> b -> b) -> b
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> d
rotateR (𝐼 a -> b) -> (𝕊 -> b -> b) -> 𝑇A a -> b
forall b a. Monoid b => (𝐼 a -> b) -> (𝕊 -> b -> b) -> 𝑇A a -> b
fold𝑇AWith

key𝑇A ∷ 𝕊 → 𝑇A a → 𝑇A a
key𝑇A :: forall a. 𝕊 -> 𝑇A a -> 𝑇A a
key𝑇A 𝕊
s 𝑇A a
x = 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
forall a. 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
𝑇A 𝐼 a
forall a. Null a => a
null (𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a) -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
forall a b. (a -> b) -> a -> b
$ (𝕊 ∧ 𝑇A a) -> 𝐼 (𝕊 ∧ 𝑇A a)
forall a t. Single a t => a -> t
single ((𝕊 ∧ 𝑇A a) -> 𝐼 (𝕊 ∧ 𝑇A a)) -> (𝕊 ∧ 𝑇A a) -> 𝐼 (𝕊 ∧ 𝑇A a)
forall a b. (a -> b) -> a -> b
$ 𝕊
s 𝕊 -> 𝑇A a -> 𝕊 ∧ 𝑇A a
forall a b. a -> b -> a ∧ b
:* 𝑇A a
x

val𝑇A ∷ a → 𝑇A a
val𝑇A :: forall a. a -> 𝑇A a
val𝑇A a
x = 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
forall a. 𝐼 a -> 𝐼 (𝕊 ∧ 𝑇A a) -> 𝑇A a
𝑇A (a -> 𝐼 a
forall a t. Single a t => a -> t
single a
x) 𝐼 (𝕊 ∧ 𝑇A a)
forall a. Null a => a
null

keys𝑇A ∷ 𝐿 𝕊 → 𝑇A a → 𝑇A a
keys𝑇A :: forall a. 𝐿 𝕊 -> 𝑇A a -> 𝑇A a
keys𝑇A = (𝕊 -> 𝑇A a -> 𝑇A a) -> 𝐿 𝕊 -> 𝑇A a -> 𝑇A a
forall a t b. ToIter a t => (a -> b -> b) -> t -> b -> b
foldrWithOn 𝕊 -> 𝑇A a -> 𝑇A a
forall a. 𝕊 -> 𝑇A a -> 𝑇A a
key𝑇A

instance (Pretty a) ⇒ Pretty (𝑇A a) where
  pretty :: 𝑇A a -> Doc
pretty (𝑇A 𝐼 a
v 𝐼 (𝕊 ∧ 𝑇A a)
n) = 𝐼 Doc -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical (𝐼 Doc -> Doc) -> 𝐼 Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [𝐼 Doc] -> 𝐼 Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat
    [ (a -> Doc) -> 𝐼 a -> 𝐼 Doc
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> Doc
forall a. Pretty a => a -> Doc
pretty 𝐼 a
v
    , 𝐼 (𝕊 ∧ 𝑇A a) -> ((𝕊 ∧ 𝑇A a) -> Doc) -> 𝐼 Doc
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn 𝐼 (𝕊 ∧ 𝑇A a)
n (((𝕊 ∧ 𝑇A a) -> Doc) -> 𝐼 Doc) -> ((𝕊 ∧ 𝑇A a) -> Doc) -> 𝐼 Doc
forall a b. (a -> b) -> a -> b
$ \ (𝕊
k :* 𝑇A a
v') → [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppHorizontal
        [ Color -> Doc -> Doc
ppFG Color
teal (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
ppBD (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString 𝕊
k
        , Doc -> Doc
ppGA (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝑇A a -> Doc
forall a. Pretty a => a -> Doc
pretty 𝑇A a
v'
        ]
    ]

data 𝑇D a = 𝑇D 
  { forall a. 𝑇D a -> 𝐼 a
vals𝑇D ∷ 𝐼 a
  , forall a. 𝑇D a -> 𝕊 ⇰ 𝑇D a
nest𝑇D ∷ 𝕊 ⇰ 𝑇D a
  } deriving (Int -> 𝑇D a -> ShowS
[𝑇D a] -> ShowS
𝑇D a -> String
(Int -> 𝑇D a -> ShowS)
-> (𝑇D a -> String) -> ([𝑇D a] -> ShowS) -> Show (𝑇D a)
forall a. Show a => Int -> 𝑇D a -> ShowS
forall a. Show a => [𝑇D a] -> ShowS
forall a. Show a => 𝑇D a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> 𝑇D a -> ShowS
showsPrec :: Int -> 𝑇D a -> ShowS
$cshow :: forall a. Show a => 𝑇D a -> String
show :: 𝑇D a -> String
$cshowList :: forall a. Show a => [𝑇D a] -> ShowS
showList :: [𝑇D a] -> ShowS
Show)

instance Null (𝑇D a) where 
  null :: 𝑇D a
null = 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
forall a. 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
𝑇D 𝐼 a
forall a. Null a => a
null 𝕊 ⇰ 𝑇D a
forall a. Null a => a
null
instance Append (𝑇D a) where 
  𝑇D 𝐼 a
m₁ 𝕊 ⇰ 𝑇D a
n₁ ⧺ :: 𝑇D a -> 𝑇D a -> 𝑇D a
⧺ 𝑇D 𝐼 a
m₂ 𝕊 ⇰ 𝑇D a
n₂ = 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
forall a. 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
𝑇D (𝐼 a
m₁ 𝐼 a -> 𝐼 a -> 𝐼 a
forall a. Append a => a -> a -> a
⧺ 𝐼 a
m₂) ((𝕊 ⇰ 𝑇D a) -> 𝑇D a) -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
forall a b. (a -> b) -> a -> b
$ 𝕊 ⇰ 𝑇D a
n₁ (𝕊 ⇰ 𝑇D a) -> (𝕊 ⇰ 𝑇D a) -> 𝕊 ⇰ 𝑇D a
forall a. Append a => a -> a -> a
⧺ 𝕊 ⇰ 𝑇D a
n₂
instance Monoid (𝑇D a)

instance Eps (𝑇D a) where 
  eps :: 𝑇D a
eps = 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
forall a. 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
𝑇D 𝐼 a
forall a. Null a => a
null 𝕊 ⇰ 𝑇D a
forall a. Null a => a
null
instance Seq (𝑇D a) where
  𝑇D 𝐼 a
v₁ 𝕊 ⇰ 𝑇D a
n₁ ▷ :: 𝑇D a -> 𝑇D a -> 𝑇D a
▷ 𝑇D 𝐼 a
v₂ 𝕊 ⇰ 𝑇D a
n₂
    | (𝕊 ⇰ 𝑇D a) -> 𝔹
forall a t. ToIter a t => t -> 𝔹
isEmpty 𝕊 ⇰ 𝑇D a
n₁ = 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
forall a. 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
𝑇D (𝐼 a
v₁ 𝐼 a -> 𝐼 a -> 𝐼 a
forall a. Append a => a -> a -> a
⧺ 𝐼 a
v₂) 𝕊 ⇰ 𝑇D a
n₂
    | 𝔹
otherwise = 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
forall a. 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
𝑇D 𝐼 a
v₁ ((𝕊 ⇰ 𝑇D a) -> 𝑇D a) -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
forall a b. (a -> b) -> a -> b
$ (𝑇D a -> 𝑇D a) -> (𝕊 ⇰ 𝑇D a) -> 𝕊 ⇰ 𝑇D a
forall a b. (a -> b) -> (𝕊 ⇰ a) -> 𝕊 ⇰ b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map (𝑇D a -> 𝑇D a -> 𝑇D a
forall a. Seq a => a -> a -> a
▷ 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
forall a. 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
𝑇D 𝐼 a
v₂ 𝕊 ⇰ 𝑇D a
n₂) 𝕊 ⇰ 𝑇D a
n₁
instance Seqoid (𝑇D a)

fold𝑇DWith ∷ (Monoid b) ⇒ (𝐼 a → b) → (𝕊 → b → b) → 𝑇D a → b
fold𝑇DWith :: forall b a. Monoid b => (𝐼 a -> b) -> (𝕊 -> b -> b) -> 𝑇D a -> b
fold𝑇DWith 𝐼 a -> b
fₗ 𝕊 -> b -> b
fₙ = 𝑇D a -> b
loop
  where 
    loop :: 𝑇D a -> b
loop (𝑇D 𝐼 a
vs 𝕊 ⇰ 𝑇D a
sxs) = [b] -> b
forall a t. (Monoid a, ToIter a t) => t -> a
concat
      [ 𝐼 a -> b
fₗ 𝐼 a
vs
      , 𝐼 b -> b
forall a t. (Monoid a, ToIter a t) => t -> a
concat (𝐼 b -> b) -> 𝐼 b -> b
forall a b. (a -> b) -> a -> b
$ 𝐼 (𝕊 ∧ 𝑇D a) -> ((𝕊 ∧ 𝑇D a) -> b) -> 𝐼 b
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn ((𝕊 ⇰ 𝑇D a) -> 𝐼 (𝕊 ∧ 𝑇D a)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕊 ⇰ 𝑇D a
sxs) (((𝕊 ∧ 𝑇D a) -> b) -> 𝐼 b) -> ((𝕊 ∧ 𝑇D a) -> b) -> 𝐼 b
forall a b. (a -> b) -> a -> b
$ \ (𝕊
s :* 𝑇D a
xs) →
          𝕊 -> b -> b
fₙ 𝕊
s (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ 𝑇D a -> b
loop 𝑇D a
xs
      ]

fold𝑇DOn ∷ (Monoid b) ⇒ 𝑇D a → (𝐼 a → b) → (𝕊 → b → b) → b
fold𝑇DOn :: forall b a. Monoid b => 𝑇D a -> (𝐼 a -> b) -> (𝕊 -> b -> b) -> b
fold𝑇DOn = ((𝐼 a -> b) -> (𝕊 -> b -> b) -> 𝑇D a -> b)
-> 𝑇D a -> (𝐼 a -> b) -> (𝕊 -> b -> b) -> b
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> d
rotateR (𝐼 a -> b) -> (𝕊 -> b -> b) -> 𝑇D a -> b
forall b a. Monoid b => (𝐼 a -> b) -> (𝕊 -> b -> b) -> 𝑇D a -> b
fold𝑇DWith

key𝑇D ∷ 𝕊 → 𝑇D a → 𝑇D a
key𝑇D :: forall a. 𝕊 -> 𝑇D a -> 𝑇D a
key𝑇D 𝕊
s 𝑇D a
x = 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
forall a. 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
𝑇D 𝐼 a
forall a. Null a => a
null ((𝕊 ⇰ 𝑇D a) -> 𝑇D a) -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
forall a b. (a -> b) -> a -> b
$ (𝕊 ∧ 𝑇D a) -> 𝕊 ⇰ 𝑇D a
forall a t. Single a t => a -> t
single ((𝕊 ∧ 𝑇D a) -> 𝕊 ⇰ 𝑇D a) -> (𝕊 ∧ 𝑇D a) -> 𝕊 ⇰ 𝑇D a
forall a b. (a -> b) -> a -> b
$ 𝕊
s 𝕊 -> 𝑇D a -> 𝕊 ∧ 𝑇D a
forall a b. a -> b -> a ∧ b
:* 𝑇D a
x

val𝑇D ∷ a → 𝑇D a
val𝑇D :: forall a. a -> 𝑇D a
val𝑇D a
x = 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
forall a. 𝐼 a -> (𝕊 ⇰ 𝑇D a) -> 𝑇D a
𝑇D (a -> 𝐼 a
forall a t. Single a t => a -> t
single a
x) 𝕊 ⇰ 𝑇D a
forall a. Null a => a
null

keys𝑇D ∷ 𝐿 𝕊 → 𝑇D a → 𝑇D a
keys𝑇D :: forall a. 𝐿 𝕊 -> 𝑇D a -> 𝑇D a
keys𝑇D = (𝕊 -> 𝑇D a -> 𝑇D a) -> 𝐿 𝕊 -> 𝑇D a -> 𝑇D a
forall a t b. ToIter a t => (a -> b -> b) -> t -> b -> b
foldrWithOn 𝕊 -> 𝑇D a -> 𝑇D a
forall a. 𝕊 -> 𝑇D a -> 𝑇D a
key𝑇D

instance (Pretty a) ⇒ Pretty (𝑇D a) where
  pretty :: 𝑇D a -> Doc
pretty (𝑇D 𝐼 a
v 𝕊 ⇰ 𝑇D a
n) = 𝐼 Doc -> Doc
forall t. ToIter Doc t => t -> Doc
ppVertical (𝐼 Doc -> Doc) -> 𝐼 Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [𝐼 Doc] -> 𝐼 Doc
forall a t. (Monoid a, ToIter a t) => t -> a
concat
    [ (a -> Doc) -> 𝐼 a -> 𝐼 Doc
forall a b. (a -> b) -> 𝐼 a -> 𝐼 b
forall (t :: * -> *) a b. Functor t => (a -> b) -> t a -> t b
map a -> Doc
forall a. Pretty a => a -> Doc
pretty 𝐼 a
v
    , 𝐼 (𝕊 ∧ 𝑇D a) -> ((𝕊 ∧ 𝑇D a) -> Doc) -> 𝐼 Doc
forall (t :: * -> *) a b. Functor t => t a -> (a -> b) -> t b
mapOn ((𝕊 ⇰ 𝑇D a) -> 𝐼 (𝕊 ∧ 𝑇D a)
forall a t. ToIter a t => t -> 𝐼 a
iter 𝕊 ⇰ 𝑇D a
n) (((𝕊 ∧ 𝑇D a) -> Doc) -> 𝐼 Doc) -> ((𝕊 ∧ 𝑇D a) -> Doc) -> 𝐼 Doc
forall a b. (a -> b) -> a -> b
$ \ (𝕊
k :* 𝑇D a
v') → [Doc] -> Doc
forall t. ToIter Doc t => t -> Doc
ppHorizontal
        [ Color -> Doc -> Doc
ppFG Color
teal (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> Doc
ppBD (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝕊 -> Doc
ppString 𝕊
k
        , Doc -> Doc
ppGA (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ 𝑇D a -> Doc
forall a. Pretty a => a -> Doc
pretty 𝑇D a
v'
        ]
    ]