-- Cons-lists as an ornamentation of natural numbers.

module Examples.List where

open import Prelude.Function
open import Prelude.InverseImage
open import Description
open import Ornament hiding ([]; _∷_)
open import Examples.Nat

open import Data.Unit using (⊤; tt)
open import Data.Product using (Σ; Σ-syntax; _,_)


--------
-- lists

ListOD : Set → OrnDesc ⊤ ! NatD
ListOD A = wrap λ _ → σ ListTag λ { `nil   → ṿ tt
                                  ; `cons  → Δ[ _ ∈ A ] ṿ (ok tt , tt) }

List : Set → Set
List A = μ ⌊ ListOD A ⌋ tt

pattern []       = con (`nil , tt)
pattern _∷_ x xs = con (`cons , x , xs , tt)

infixr  _∷_

length : {A : Set} → List A → Nat
length {A} = forget ⌈ ListOD A ⌉

_++_ : {A : Set} → List A → List A → List A
con (`nil  ,          _) ++ ys = ys
con (`cons , x , xs , _) ++ ys = x ∷ (xs ++ ys)