module Chapter8.Ornament.Examples.Maybe where

open import Level 
  renaming ( zero to zeroL
           ; suc to sucL )
open import Function

open import Data.Unit
open import Data.Nat
open import Data.Fin hiding (lift)
open import Data.Product

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint

open import Chapter5.IDesc.Examples.Bool

open import Chapter8.Ornament


MaybeO : Set → orn BoolD id id 
MaybeO A = orn.mk (λ _ → 
           `σ (λ { zero → insert A (λ _ → `1) 
                 ; (suc zero) → `1
                 ; (suc (suc ())) }))

Maybe : Set → Set
Maybe A = μ ⟦ MaybeO A ⟧orn tt

just : ∀{A} → A → Maybe A
just a = ⟨ zero , a , lift tt ⟩

nothing : ∀{A} → Maybe A
nothing = ⟨ suc zero , lift tt ⟩