module Description where

open import Prelude

open import Data.Unit using (⊤; tt)
open import Data.Product using (Σ; _,_; _×_)


data RDesc (I : Set) : Set₁ where
  ∎   : RDesc I
  ṿ   : (i : I) → RDesc I
  σ   : (S : Set) (D : S → RDesc I) → RDesc I
  _*_ : (D E : RDesc I) → RDesc I

syntax σ S (λ s → D) = σ[ s ∶ S ] D

⟦_⟧ : ∀ {I} → RDesc I → (I → Set) → Set
⟦ ∎     ⟧ X = ⊤
⟦ ṿ i   ⟧ X = X i
⟦ σ S D ⟧ X = Σ[ s ∶ S ] ⟦ D s ⟧ X
⟦ D * E ⟧ X = ⟦ D ⟧ X × ⟦ E ⟧ X

data Desc (I : Set) : Set₁ where
  wrap : (I → RDesc I) → Desc I

_at_ : ∀ {I} → Desc I → I → RDesc I
(wrap D) at i = D i

Ḟ : ∀ {I} → Desc I → (I → Set) → (I → Set)
Ḟ D X i = ⟦ D at i ⟧ X

_⇒_ : ∀ {I} → (I → Set) → (I → Set) → Set
X ⇒ Y = ∀ {i} → X i → Y i

infixr  _⇒_

data μ {I} (D : Desc I) : I → Set where
  con : Ḟ D (μ D) ⇒ μ D

decon : ∀ {I} {D : Desc I} → μ D ⇒ Ḟ D (μ D)
decon (con xs) = xs

-- fold

mutual

  fold : ∀ {I X} {D : Desc I} → Ḟ D X ⇒ X → μ D ⇒ X
  fold {D = D} φ {i} (con ds) = φ (mapFold D (D at i) φ ds)

  mapFold : ∀ {I} (D : Desc I) (E : RDesc I) → ∀ {X} → (Ḟ D X ⇒ X) → ⟦ E ⟧ (μ D) → ⟦ E ⟧ X
  mapFold D ∎        φ _          = _
  mapFold D (ṿ i)    φ d          = fold φ d
  mapFold D (σ S E)  φ (s , ds)   = s , mapFold D (E s) φ ds
  mapFold D (E * E') φ (ds , ds') = mapFold D E φ ds , mapFold D E' φ ds'

-- induction

All : ∀ {I} (D : RDesc I) {X : I → Set} (P : ∀ {i} → X i → Set) → ⟦ D ⟧ X → Set
All ∎       P _          = ⊤
All (ṿ i)   P x          = P x
All (σ S D) P (s , xs)   = All (D s) P xs
All (D * E) P (xs , xs') = All D P xs × All E P xs'

mutual

  induction : ∀ {I} (D : Desc I) (P : ∀ {i} → μ D i → Set) →
              (∀ {i} (ds : Ḟ D (μ D) i) → All (D at i) P ds → P (con ds)) →
              ∀ {i} (d : μ D i) → P d
  induction D P ih {i} (con ds) = ih ds (everywhereInduction D (D at i) P ih ds)

  everywhereInduction :
    ∀ {I} (D : Desc I) (E : RDesc I)
    (P : ∀ {i} → μ D i → Set) →
    (∀ {i} (ds : Ḟ D (μ D) i) → All (D at i) P ds → P (con ds)) →
    (ds : ⟦ E ⟧ (μ D)) → All E P ds
  everywhereInduction D ∎        P ih _          = _
  everywhereInduction D (ṿ i)    P ih d          = induction D P ih d
  everywhereInduction D (σ S E)  P ih (s , ds)   = everywhereInduction D (E s) P ih ds
  everywhereInduction D (E * E') P ih (ds , ds') = everywhereInduction D E P ih ds ,
                                                   everywhereInduction D E' P ih ds'