module UVMHS.Lib.TreeAnnote where

import UVMHS.Core

import qualified Prelude as HS

-- This file contains two datastructures for annotated trees. The first is
-- straightforward to understand based on its datatype definition. The second
-- “virtual” one never constructs the full tree, and is equivalent to the first
-- “vanilla” one.

class Annote i a | a → i where
  annote ∷ i → a → a

-------------
-- VANILLA --
-------------

data 𝑇 i a =
    N𝑇
  | B𝑇 (𝑇 i a) (𝑇 i a)
  | L𝑇 a
  | A𝑇 i (𝑇 i a)

fold𝑇With ∷ (Monoid b) ⇒ (a → b) → (i → b → b) → 𝑇 i a → b
fold𝑇With :: forall b a i. Monoid b => (a -> b) -> (i -> b -> b) -> 𝑇 i a -> b
fold𝑇With a -> b
fₗ i -> b -> b
fₐ = 𝑇 i a -> b
loop
  where 
    loop :: 𝑇 i a -> b
loop = \case
      𝑇 i a
N𝑇 → b
forall a. Null a => a
null
      B𝑇 𝑇 i a
xs 𝑇 i a
ys → 𝑇 i a -> b
loop 𝑇 i a
xs b -> b -> b
forall a. Append a => a -> a -> a
⧺ 𝑇 i a -> b
loop 𝑇 i a
ys
      L𝑇 a
x → a -> b
fₗ a
x
      A𝑇 i
i 𝑇 i a
xs → i -> b -> b
fₐ i
i (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ 𝑇 i a -> b
loop 𝑇 i a
xs

fold𝑇On ∷ (Monoid b) ⇒ 𝑇 i a → (a → b) → (i → b → b) → b
fold𝑇On :: forall b i a. Monoid b => 𝑇 i a -> (a -> b) -> (i -> b -> b) -> b
fold𝑇On = ((a -> b) -> (i -> b -> b) -> 𝑇 i a -> b)
-> 𝑇 i a -> (a -> b) -> (i -> b -> b) -> b
forall a b c d. (a -> b -> c -> d) -> c -> a -> b -> d
rotateR (a -> b) -> (i -> b -> b) -> 𝑇 i a -> b
forall b a i. Monoid b => (a -> b) -> (i -> b -> b) -> 𝑇 i a -> b
fold𝑇With

instance Null (𝑇 i a) where null :: 𝑇 i a
null = 𝑇 i a
forall i a. 𝑇 i a
N𝑇
instance Append (𝑇 i a) where ⧺ :: 𝑇 i a -> 𝑇 i a -> 𝑇 i a
(⧺) = 𝑇 i a -> 𝑇 i a -> 𝑇 i a
forall i a. 𝑇 i a -> 𝑇 i a -> 𝑇 i a
B𝑇
instance Monoid (𝑇 i a)

instance Single a (𝑇 i a) where single :: a -> 𝑇 i a
single = a -> 𝑇 i a
forall i a. a -> 𝑇 i a
L𝑇
instance Annote i (𝑇 i a) where annote :: i -> 𝑇 i a -> 𝑇 i a
annote = i -> 𝑇 i a -> 𝑇 i a
forall i a. i -> 𝑇 i a -> 𝑇 i a
A𝑇

instance Functor (𝑇 i) where map :: forall a b. (a -> b) -> 𝑇 i a -> 𝑇 i b
map a -> b
f = (a -> 𝑇 i b) -> (i -> 𝑇 i b -> 𝑇 i b) -> 𝑇 i a -> 𝑇 i b
forall b a i. Monoid b => (a -> b) -> (i -> b -> b) -> 𝑇 i a -> b
fold𝑇With (b -> 𝑇 i b
forall i a. a -> 𝑇 i a
L𝑇 (b -> 𝑇 i b) -> (a -> b) -> a -> 𝑇 i b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> b
f) i -> 𝑇 i b -> 𝑇 i b
forall i a. Annote i a => i -> a -> a
annote

-------------
-- VIRTUAL --
-------------

data 𝑇V i a = 𝑇V 
  { forall i a.
𝑇V i a -> forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b
un𝑇V ∷ ∀ b. (Monoid b) 
              ⇒ (a → b) 
              → (i → b → b) 
              → b 
  }

fold𝑇VOn ∷ (Monoid b) ⇒ 𝑇V i a → (a → b) → (i → b → b) → b
fold𝑇VOn :: forall b i a. Monoid b => 𝑇V i a -> (a -> b) -> (i -> b -> b) -> b
fold𝑇VOn 𝑇V i a
xs = 𝑇V i a -> forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b
forall i a.
𝑇V i a -> forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b
un𝑇V 𝑇V i a
xs

fold𝑇VWith ∷ (Monoid b) ⇒ (a → b) → (i → b → b) → 𝑇V i a → b
fold𝑇VWith :: forall b a i. Monoid b => (a -> b) -> (i -> b -> b) -> 𝑇V i a -> b
fold𝑇VWith = (𝑇V i a -> (a -> b) -> (i -> b -> b) -> b)
-> (a -> b) -> (i -> b -> b) -> 𝑇V i a -> b
forall a b c d. (a -> b -> c -> d) -> b -> c -> a -> d
rotateL 𝑇V i a -> (a -> b) -> (i -> b -> b) -> b
forall b i a. Monoid b => 𝑇V i a -> (a -> b) -> (i -> b -> b) -> b
fold𝑇VOn

null𝑇V ∷ 𝑇V i a
null𝑇V :: forall i a. 𝑇V i a
null𝑇V = (forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
forall i a.
(forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
𝑇V ((forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a)
-> (forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b
_fₑ i -> b -> b
_fₐ → b
forall a. Null a => a
null

append𝑇V ∷ 𝑇V i a → 𝑇V i a → 𝑇V i a
append𝑇V :: forall i a. 𝑇V i a -> 𝑇V i a -> 𝑇V i a
append𝑇V (𝑇V forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b
g₁) (𝑇V forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b
g₂) = (forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
forall i a.
(forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
𝑇V ((forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a)
-> (forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b
fₑ i -> b -> b
fₐ →
  (a -> b) -> (i -> b -> b) -> b
forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b
g₁ a -> b
fₑ i -> b -> b
fₐ b -> b -> b
forall a. Append a => a -> a -> a
⧺ (a -> b) -> (i -> b -> b) -> b
forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b
g₂ a -> b
fₑ i -> b -> b
fₐ

single𝑇V ∷ a → 𝑇V i a
single𝑇V :: forall a i. a -> 𝑇V i a
single𝑇V a
e = (forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
forall i a.
(forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
𝑇V ((forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a)
-> (forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b
fₑ i -> b -> b
_fₐ → a -> b
fₑ a
e

annote𝑇V ∷ i → 𝑇V i a → 𝑇V i a
annote𝑇V :: forall i a. i -> 𝑇V i a -> 𝑇V i a
annote𝑇V i
i (𝑇V forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b
g) = (forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
forall i a.
(forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
𝑇V ((forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a)
-> (forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
forall a b. (a -> b) -> a -> b
HS.$ \ a -> b
fₑ i -> b -> b
fₐ → i -> b -> b
fₐ i
i (b -> b) -> b -> b
forall a b. (a -> b) -> a -> b
$ (a -> b) -> (i -> b -> b) -> b
forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b
g a -> b
fₑ i -> b -> b
fₐ

map𝑇V ∷ (i → j) → (a → b) → 𝑇V i a → 𝑇V j b
map𝑇V :: forall i j a b. (i -> j) -> (a -> b) -> 𝑇V i a -> 𝑇V j b
map𝑇V i -> j
f a -> b
g (𝑇V forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b
h) = (forall b. Monoid b => (b -> b) -> (j -> b -> b) -> b) -> 𝑇V j b
forall i a.
(forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b) -> 𝑇V i a
𝑇V ((forall b. Monoid b => (b -> b) -> (j -> b -> b) -> b) -> 𝑇V j b)
-> (forall b. Monoid b => (b -> b) -> (j -> b -> b) -> b) -> 𝑇V j b
forall a b. (a -> b) -> a -> b
HS.$ \ b -> b
fₑ j -> b -> b
fₐ → (a -> b) -> (i -> b -> b) -> b
forall b. Monoid b => (a -> b) -> (i -> b -> b) -> b
h (b -> b
fₑ (b -> b) -> (a -> b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ a -> b
g) ((i -> b -> b) -> b) -> (i -> b -> b) -> b
forall a b. (a -> b) -> a -> b
$ j -> b -> b
fₐ (j -> b -> b) -> (i -> j) -> i -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
∘ i -> j
f

instance Null (𝑇V i a) where null :: 𝑇V i a
null = 𝑇V i a
forall i a. 𝑇V i a
null𝑇V
instance Append (𝑇V i a) where ⧺ :: 𝑇V i a -> 𝑇V i a -> 𝑇V i a
(⧺) = 𝑇V i a -> 𝑇V i a -> 𝑇V i a
forall i a. 𝑇V i a -> 𝑇V i a -> 𝑇V i a
append𝑇V
instance Monoid (𝑇V i a)

instance Single a (𝑇V i a) where single :: a -> 𝑇V i a
single = a -> 𝑇V i a
forall a i. a -> 𝑇V i a
single𝑇V
instance Annote i (𝑇V i a) where annote :: i -> 𝑇V i a -> 𝑇V i a
annote = i -> 𝑇V i a -> 𝑇V i a
forall i a. i -> 𝑇V i a -> 𝑇V i a
annote𝑇V

instance Functor (𝑇V i) where map :: forall a b. (a -> b) -> 𝑇V i a -> 𝑇V i b
map = (i -> i) -> (a -> b) -> 𝑇V i a -> 𝑇V i b
forall i j a b. (i -> j) -> (a -> b) -> 𝑇V i a -> 𝑇V j b
map𝑇V i -> i
forall a. a -> a
id