module Chapter5.IDesc.Tagged where

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

open import Data.Nat hiding (_⊔_)
open import Data.Fin hiding (lift) renaming (_+_ to _F+_)
open import Data.Vec
open import Data.Product

open import Chapter5.IDesc


tagDesc : ∀(ℓ : Level){k} → Set k → Set (k ⊔ (sucL ℓ))
tagDesc ℓ {k} I = Tags I × iTags I
  where
    Tags : Set k → Set (k ⊔ (sucL ℓ))
    Tags I = Σ[ n ∈ ℕ ] (I → Vec (IDesc ℓ I) n)

    iTags : Set k → Set (k ⊔ (sucL ℓ))
    iTags I = Σ[ f ∈ (I → ℕ) ] ((i : I) → Vec (IDesc ℓ I) (f i))

-- TODO: Must be part of the stdlib
private
  ⟨_∣_⟩ : ∀{ℓ}{A : Set ℓ}{m n} → (Fin m → A) → (Fin n → A) → Fin (m + n) → A
  ⟨_∣_⟩ {A = A} {m = m}{n = n} f g k = help m f k
    where help : (m : ℕ) → (Fin m → A) → Fin (m + n) → A
          help zero f k = g k
          help (suc m) f zero = f zero
          help (suc m) f (suc k) = help m (f ∘ suc) k

toDesc : ∀{ℓ k}{I : Set k} → tagDesc ℓ I → func ℓ I I 
toDesc ((n , ds) , (f , ids)) =
       func.mk λ i → 
         `Σ (Lift (Fin (n + f i)))
            λ { (lift k) → 
                ⟨ (flip lookup) (ds i) ∣ (flip lookup) (ids i) ⟩ k }

toTagged : ∀{ℓ k}{I : Set k} → func ℓ I I → tagDesc ℓ I
toTagged d = ((  , λ i → func.out d i ∷ []) , ( (λ i → ) , λ i → []))