-- 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
      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


    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
      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 γ