module Examples.List where

open import Prelude
open import Description
open import Ornament
open import Examples.Nat

open import Data.Unit using (⊤; tt)
open import Data.Bool using (Bool; false; true)
open import Data.Product using (Σ; _,_)


--------
-- lists

ListO : Set → OrnDesc ⊤ ! NatD
ListO A = wrap λ _ → σ Bool λ { false → ∎
                              ; true  → Δ[ _ ∶ A ] ṿ (ok tt) }

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

[] : ∀ {A} → List A
[] = con (false , tt)

_∷_ : ∀ {A} → A → List A → List A
x ∷ xs = con (true , x , xs)

infixr 5 _∷_

length : ∀ {A} → List A → Nat
length {A} = forget ⌈ ListO A ⌉

_++_ : ∀ {A} → List A → List A → List A
con (false , _) ++ ys      = ys
con (true  , x , xs) ++ ys = x ∷ (xs ++ ys)