module Chapter9.Lift.Examples.Head 
         (A : Set)
       where

open import Level hiding (zero ; suc)

open import Data.Unit
open import Data.Fin hiding (fold ; lift)
open import Data.Product

open import Chapter2.Logic

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.InitialAlgebra
open import Chapter5.IDesc.Examples.Bool
open import Chapter5.IDesc.Examples.Nat 

open import Chapter8.Ornament
open import Chapter8.Ornament.Examples.List
open import Chapter8.Ornament.Examples.Maybe

open import Chapter9.Functions
open import Chapter9.FunOrnament
open import Chapter9.Patch
open import Chapter9.Lift.Fold
open import Chapter9.Lift.Constructor

typeIsSuc : Type _
typeIsSuc = μ NatD [ tt ]→ μ BoolD [ tt  `⊤

α : Alg NatD  _  Bool × Lift )
α {tt} (zero , lift tt) = false , lift tt
α {tt} (suc zero , _) = true , lift tt
α {tt} (suc (suc ()) , _)

isSuc :  typeIsSuc ⟧Type
isSuc = fold NatD α
  

typeHead : FunctionOrn typeIsSuc
typeHead = μ⁺ ListO A [ inv tt ]→ 
             μ⁺ MaybeO A [ inv tt  `⊤

αL : AlgLift (ListO A) α (μ⁺ MaybeO A [ inv tt  `⊤)
αL {tt ,  zero , lift tt } xs = liftConstructor (MaybeO A) (lift tt) (lift tt) (lift tt)
αL {tt ,  suc zero , n } ((a , _) , xs) = liftConstructor ((MaybeO A)) (a , lift tt) (lift tt) (lift tt)
αL {tt ,  suc (suc ()) , _ } _

vhead : Patch isSuc typeHead
vhead = liftAlg (ListO A)  {T⁺ = μ⁺ MaybeO A [ inv tt  `⊤} α  {i}  αL {i})

open import Chapter9.Patch.Apply

head :  typeHead ⟧FunctionOrn
head = patch typeHead isSuc vhead

{-
private
  module Test where

    open import Relation.Binary.PropositionalEquality

    test-head-nil : head nil ≡ (nothing , tt)
    test-head-nil = refl

-}