------------------------------------------------------------------------
-- Eating, based on Agda 1 code from Peter Hancock
------------------------------------------------------------------------

module Eating where

open import Coinduction
open import Data.Product
open import Data.Unit

data WC {S : Set} (C R : S → Set) (X : Set) : Set where
  wc : ∀ {s} (c : C s) (meal : R s → X) → WC C R X

module Neighbourhoods (S : Set) (P : S → Set) where

  record Inf : Set where
    field
      head : S
      tail : P head → ∞ Inf

  open Inf public

  unfold : (C : Set) → (C → ∃ λ s → P s → C) → C → Inf
  unfold C g seed = record
    { head = proj₁ gs
    ; tail = λ p → ♯ unfold C g (proj₂ gs p)
    }
    where gs = g seed

  mutual

    data S⋆ : Set where
      start : S⋆
      grow  : ∀ s⋆ (growth : P⋆ s⋆ → S) → S⋆

    P⋆ : S⋆ → Set
    P⋆ start           = ⊤
    P⋆ (grow _ growth) = ∃ λ p⋆ → P (growth p⋆)

module DiscreteEating (S : Set) (P : S → Set) (B : Set) where
  open Neighbourhoods S P

  data Bar (s⋆ : S⋆) : Set where
    wr : (b : B) → Bar s⋆
    rd : (ingest : (k : P⋆ s⋆ → S) → Bar (grow s⋆ k)) → Bar s⋆

  eat : ∀ {s⋆} → Bar s⋆ → (P⋆ s⋆ → Inf) → B
  eat (wr b)      meal = b
  eat (rd ingest) meal = eat (ingest λ h → head (meal h))
                             (λ h → ♭ (tail (meal (proj₁ h)) (proj₂ h)))

module GeneralEating (S : Set) (P : S → Set) (Q : Set) (R : Q → Set) where
  open Neighbourhoods Q R using (grow; unfold)
                          renaming (S⋆ to Q⋆; P⋆ to R⋆; Inf to N)
  open Neighbourhoods S P using (S⋆; P⋆; grow; head; tail)
                          renaming (Inf to M)

  data Bar (B : S⋆ → Set) (s⋆ : S⋆) : Set where
    wr : (b : B s⋆) → Bar B s⋆
    rd : (ingest : (k : P⋆ s⋆ → S) → Bar B (grow s⋆ k)) → Bar B s⋆

  eat : ∀ {B s⋆} → Bar B s⋆ → (P⋆ s⋆ → M) → WC B P⋆ M
  eat (wr b)      meal = wc b meal
  eat (rd ingest) meal = eat (ingest (λ h → head (meal h)))
                             (λ h → ♭ (tail (meal (proj₁ h)) (proj₂ h)))

  record Pos (q⋆ : Q⋆) (s⋆ : S⋆) : Set where
    field
      out : Bar (λ s⋆ → ∃ λ τ → ∞ (Pos (grow q⋆ τ) s⋆)) s⋆

  open Pos public

  Carrier : Set
  Carrier = ∃ λ q⋆ → WC (Pos q⋆) P⋆ M × R⋆ q⋆

  γ : Carrier → ∃ λ q → R q → Carrier
  γ (q⋆ , wc cc m , r) with eat (out cc) m
  γ (q⋆ , wc cc m , r) | wc (τ , b) meal =
    (τ r , λ r′ → (grow q⋆ τ , wc (♭ b) meal , r , r′))

  eat∞ : Carrier → N
  eat∞ = unfold Carrier γ