{-# OPTIONS --no-termination-check #-}

module Hyper.Monadic.Example where

open import Prelude
open import Data.Maybe
open import Data.Maybe.Properties

module _ {a : Level} where
  open import Hyper.Monadic {𝑀 = Maybe} (maybeMonad {a = a}) public

open import Data.List
infixr  _&_
record Tree (A : Type a) : Type a where
  inductive; pattern
  constructor _&_
  field
    root : A
    children : List (Tree A)

open Tree

tree : Tree ℕ
tree
  =
     &
      (  &
          (  &
              (   & []
              ∷  & []
              ∷ [])
          ∷  & []
          ∷ [])
      ∷  & []
      ∷  &
          (  &
              (  & []
              ∷  & []
              ∷ [])
          ∷  & []
          ∷ [])
      ∷ [])

run⟨_⟩ : A → A ↬ A → A
run⟨ b ⟩ x = x · maybe b run⟨ b ⟩

𝔼 : A ↬ A
𝔼 · k = k nothing

𝔽 : Maybe (A ↬ A) → A ↬ A
𝔽 = fromMaybe 𝔼

foldE : (A → B → B) → List A → B → B
foldE f = flip (foldr f)

bfs : Tree A → List A
bfs t = run⟨ [] ⟩ (f t 𝔼)
  where
  f : Tree A → (List A ↬ List A) → (List A ↬ List A)
  f (t & ts) fw · bw = t ∷ (fw · bw ∘ just ∘ foldE f ts ∘ 𝔽)

_ : bfs tree ≡ ( ⋯ )
_ = refl