module Chapter8.Ornament where

open import Level
  renaming ( zero to zeroL 
           ; suc to sucL )
open import Function

open import Data.Nat hiding (_⊔_)
open import Data.Fin

open import Chapter2.Logic

open import Chapter5.IDesc 

data Orn {ℓ k}{I K : Set k}(u : I → K) : IDesc ℓ K → Set (sucL ℓ ⊔ k) where
  -- Insert
  insert : ∀{D} → (S : Set ℓ)(D⁺ : S → Orn u D) → Orn u D

  -- Refine
  `var : ∀{i} → (i⁻¹ : u ⁻¹ i) → Orn u (`var i)
  
  -- Copy
  `1 : Orn u `1
  _`×_ : ∀{D D'} → (D⁺ : Orn u D)(D'⁺ : Orn u D') → Orn u (D `× D')
  `σ : ∀{n T} → (T⁺ : (k : Fin n) → Orn u (T k)) → Orn u (`σ n T)
  `Σ : ∀{S T} → (T⁺ : (s : S) → Orn u (T s)) → Orn u (`Σ S T)
  `Π : ∀{S T} → (T⁺ : (s : S) → Orn u (T s)) → Orn u (`Π S T)

  -- Delete
  deleteΣ : ∀{S T} → (s : S)
                     (T⁺ : Orn u (T s))  →
                    Orn u (`Σ S T)
  deleteσ : ∀{n T} → (k : Fin n)
                     (T⁺ : Orn u (T k))  →
                    Orn u (`σ n T)

⟦_⟧Orn : ∀{ℓ k}{I K : Set k}{u}{D : IDesc ℓ I} → Orn u D → IDesc ℓ K
⟦ `1 ⟧Orn = `1
⟦ T⁺ `× T'⁺ ⟧Orn = ⟦ T⁺ ⟧Orn `× ⟦ T'⁺ ⟧Orn 
⟦ `σ {n} T⁺ ⟧Orn = `σ n ((λ D → ⟦ D ⟧Orn) ∘ T⁺)
⟦ `Σ {S} T⁺ ⟧Orn = `Σ S ((λ D → ⟦ D ⟧Orn) ∘ T⁺)
⟦ `Π {S} T⁺ ⟧Orn = `Π S ((λ D → ⟦ D ⟧Orn) ∘ T⁺)
⟦ `var (inv i⁺) ⟧Orn = `var i⁺
⟦ insert S D⁺ ⟧Orn = `Σ S (λ s → ⟦ D⁺ s ⟧Orn)
⟦ deleteΣ s T⁺ ⟧Orn = ⟦ T⁺ ⟧Orn 
⟦ deleteσ k T⁺ ⟧Orn = ⟦ T⁺ ⟧Orn  

-- Help the unification engine by keeping things folded.
record orn {ℓ k : Level}{I J K L : Set k}(D : func ℓ K L)(u : I → K)(v : J → L) : Set (k ⊔ sucL ℓ) where
  constructor mk
  field 
    out : (j : J) → Orn u (func.out D (v j))

{-
orn : ∀ {I J K L : Set}(D : func K L)(u : I → K)(v : J → L) → Set₁
orn {J = J} D u v = (j : J) → Orn u (func.out D (v j))
-}

⟦_⟧orn : ∀{ℓ k}{I J K L : Set k}{D : func ℓ K L}{u : I → K}{v : J → L}  → 
        orn D u v → func ℓ I J
⟦ o ⟧orn = func.mk λ j → ⟦ orn.out o j ⟧Orn