module Chapter8.Ornament.Examples.Vec where open import Level hiding (suc) renaming (zero to zeroL) open import Function open import Data.Empty open import Data.Unit open import Data.Nat open import Data.Fin hiding (lift) open import Data.Product open import Relation.Binary.PropositionalEquality open import Chapter2.Logic import Chapter4.Desc.Examples.List as Desc open import Chapter5.IDesc open import Chapter5.IDesc.Fixpoint open import Chapter5.IDesc.Examples.ToIDesc open import Chapter8.Ornament u : ℕ → ⊤ u _ = tt ListD : Set → func zeroL ⊤ ⊤ ListD A = func.mk λ _ → toIDesc (Desc.ListD A) module Constraint {A : Set} where VecO : orn (ListD A) u u VecO = orn.mk λ n → `Σ {S = Fin 2} λ { zero → insert (0 ≡ n) λ _ → `1 ; (suc zero) → insert ℕ λ m → insert (suc m ≡ n) λ _ → `Σ λ _ → `var (inv m) `× `1 ; (suc (suc ())) } Vec : ℕ → Set Vec = μ ⟦ VecO ⟧orn nil : Vec 0 nil = ⟨ zero , refl , lift tt ⟩ cons : ∀{n} → A → Vec n → Vec (suc n) cons {n} a xs = ⟨ suc zero , n , refl , a , xs , lift tt ⟩ module Compute {A : Set} where VecO : orn (ListD A) u u VecO = orn.mk λ { zero → deleteΣ zero `1 ; (suc n) → deleteΣ (suc zero) (`Σ λ _ → `var (inv n) `× `1) } Vec : ℕ → Set Vec = μ ⟦ VecO ⟧orn nil : Vec 0 nil = ⟨ lift tt ⟩ cons : ∀{n} → A → Vec n → Vec (suc n) cons a xs = ⟨ a , xs , lift tt ⟩