module Chapter5.IDesc.Examples.Vec where open import Level renaming ( zero to zeroL ; suc to sucL ) open import Data.Unit open import Data.Nat open import Data.Fin hiding (lift) open import Data.Vec renaming (Vec to VecNative) open import Data.Product open import Relation.Binary.PropositionalEquality open import Chapter5.IDesc open import Chapter5.IDesc.Fixpoint open import Chapter5.IDesc.Tagged module Compute where VecD : (A : Set) → func zeroL ℕ ℕ VecD A = func.mk (λ { zero → `1 ; (suc n) → `Σ A λ _ → `var n `× `1 }) Vec : (A : Set) → ℕ → Set Vec A = μ (VecD A) nil : ∀{A} → Vec A 0 nil = ⟨ lift tt ⟩ cons : ∀{A n} → A → Vec A n → Vec A (suc n) cons a xs = ⟨ a , xs , lift tt ⟩ module Constraint where VecD : (A : Set) → func zeroL ℕ ℕ VecD A = func.mk (λ n → `Σ (Fin 2) λ { zero → `Σ (n ≡ 0) λ _ → `1 ; (suc zero) → `Σ A λ _ → `Σ ℕ λ m → `Σ (n ≡ suc m) λ _ → `var m `× `1 ; (suc (suc ())) } ) Vec : (A : Set) → ℕ → Set Vec A = μ (VecD A) nil : ∀{A} → Vec A 0 nil = ⟨ zero , refl , lift tt ⟩ cons : ∀{A n} → A → Vec A n → Vec A (suc n) cons a xs = ⟨ suc zero , a , _ , refl , xs , lift tt ⟩ module TaggedCompute where VecD : (A : Set) → tagDesc zeroL ℕ VecD A = (0 , λ n → []) , (λ { zero → 1 ; (suc n) → 1 }) , (λ { zero → `1 ∷ [] ; (suc n) → (`Σ A λ _ → `var n `× `1) ∷ [] }) Vec : (A : Set) → ℕ → Set Vec A = μ (toDesc (VecD A)) nil : ∀{A} → Vec A 0 nil = ⟨ lift zero , lift tt ⟩ cons : ∀{A n} → A → Vec A n → Vec A (suc n) cons a xs = ⟨ lift zero , a , xs , lift tt ⟩ module TaggedConstraint where VecD : (A : Set) → tagDesc zeroL ℕ VecD A = (2 , λ n → (`Σ (n ≡ 0) λ _ → `1) ∷ (`Σ A λ _ → `Σ ℕ λ m → `Σ (n ≡ suc m) λ _ → `var m `× `1) ∷ []) , ((λ n → 0) , λ n → []) Vec : (A : Set) → ℕ → Set Vec A = μ (toDesc (VecD A)) nil : ∀{A} → Vec A 0 nil = ⟨ lift zero , refl , lift tt ⟩ cons : ∀{A n} → A → Vec A n → Vec A (suc n) cons a xs = ⟨ lift (suc zero) , a , _ , refl , xs , lift tt ⟩