General.agda

open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Product
module _ where

----------------------------------------------------------------------

data Desc (I : Set) : Set₁ where
  `ι : I → Desc I
  `δ : I → Desc I → Desc I
  `σ : (A : Set) (D : A → Desc I) → Desc I

⟦_⟧ : {I : Set} (D : Desc I) (X : I → Set) → Set
⟦ `ι i ⟧ X = ⊤
⟦ `δ i D ⟧ X = X i × ⟦ D ⟧ X
⟦ `σ A D ⟧ X = Σ A λ a → ⟦ D a ⟧ X

idx : {I : Set} (D : Desc I) (X : I → Set) (xs : ⟦ D ⟧ X) → I
idx (`ι i) X u = i
idx (`δ i D) X (x , xs) = idx D X xs
idx (`σ A D) X (a , xs) = idx (D a) X xs

data μ {I : Set} (D : Desc I) : I → Set where
  init : (xs : ⟦ D ⟧ (μ D)) → μ D (idx D (μ D) xs)

----------------------------------------------------------------------

module PropVec where
  VecD : Set → Desc ℕ
  VecD A = `σ Bool λ b → if b
    then `ι zero
    else `σ ℕ λ n → `σ A λ _ → `δ n (`ι (suc n))

  Vec : Set → ℕ → Set
  Vec A n = μ (VecD A) n

  nil : (A : Set) → Vec A zero
  nil A = init (true , tt)

  cons : (A : Set) (n : ℕ) → A → Vec A n → Vec A (suc n)
  cons A n a xs = init (false , n , a , xs , tt)

-- idx
-- (if proj₁ xs then `ι zero else
--  `σ ℕ (λ n → `σ A (λ _ → `δ n (`ι (suc n)))))
-- (μ (VecD A)) (proj₂ xs)
-- != suc n of type ℕ
-- when checking that the pattern init (false , n , a , ys , tt) has
-- type μ (VecD A) (suc n)
  tail : {A : Set} {n : ℕ} → Vec A (suc n) → Vec A n
  tail (init (false , n , a , ys , tt)) = ys

----------------------------------------------------------------------

GeneralHack.agda

open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality
module _ where

----------------------------------------------------------------------

data Desc (I : Set) : Set₁ where
  `ι : I → Desc I
  `δ : I → Desc I → Desc I
  `σ : (A : Set) (D : A → Desc I) → Desc I

⟦_⟧ : {I : Set} (D : Desc I) (X : I → Set) → Set
⟦ `ι i ⟧ X = ⊤
⟦ `δ i D ⟧ X = X i × ⟦ D ⟧ X
⟦ `σ A D ⟧ X = Σ A λ a → ⟦ D a ⟧ X

idx : {I : Set} (D : Desc I) (X : I → Set) (xs : ⟦ D ⟧ X) → I
idx (`ι i) X u = i
idx (`δ i D) X (x , xs) = idx D X xs
idx (`σ A D) X (a , xs) = idx (D a) X xs

data μ {I : Set} (D : Desc I) (i : I) : Set where
  init : (xs : ⟦ D ⟧ (μ D)) (q : idx D (μ D) xs ≡ i) → μ D i

----------------------------------------------------------------------

module PropVec where
  VecD : Set → Desc ℕ
  VecD A = `σ Bool λ b → if b
    then `ι zero
    else `σ ℕ λ n → `σ A λ _ → `δ n (`ι (suc n))

  Vec : Set → ℕ → Set
  Vec A n = μ (VecD A) n

  nil : (A : Set) → Vec A zero
  nil A = init (true , tt) refl

  cons : (A : Set) (n : ℕ) → A → Vec A n → Vec A (suc n)
  cons A n a xs = init (false , n , a , xs , tt) refl

  tail : {A : Set} {n : ℕ} → Vec A (suc n) → Vec A n
  tail (init (true , xs) ())
  tail (init (false , n , a , xs , tt) refl) = xs

----------------------------------------------------------------------