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))
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 = (( 1 , λ i → func.out d i ∷ []) , ( (λ i → 0) , λ i → []))