module Chapter9.Lift.Examples.Lookup 
         {A : Set}
       where

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

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

open import Chapter2.Logic

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

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

open import Chapter8.Reornament.Examples.List
open import Chapter8.Reornament.Examples.Maybe

open import Chapter9.Functions.Examples.Le
open import Chapter9.FunOrnament.Examples.Lookup
open import Chapter9.Patch.Examples.Lookup

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


βL : (n : Nat) → A →
     Patch {T = μ NatD [ tt ]→ μ BoolD [ tt ]× `⊤} 
           (induction NatD (λ _ → Nat → Bool × Lift ⊤) (λ {i}{xs} → α {i}{xs}) n)
           (μ⁺ (idO NatD) [ inv tt ]→ μ⁺ MaybeO A [ inv tt ]× `⊤) →
     DAlgLift (idO NatD) 
              (λ {i}{xs} → β
                (induction NatD _ (λ {i}{xs} → α {i}{xs}) n)
                {i}{xs}) 
              (μ⁺ MaybeO A [ inv tt ]× `⊤)
βL n a ih {tt , ⟨ zero , lift tt ⟩} {lift tt , lift tt} (lift tt) = 
        liftConstructor (MaybeO A) (a , lift tt) (lift tt) (lift tt)
βL n a ih {tt , ⟨ suc zero , m , lift tt ⟩} 
          {(lift tt , lift tt) , m' , lift tt} 
          ((_ , lift tt) , lift tt) = ih m m'
βL n a ih {tt , ⟨ suc (suc ()) , _ ⟩} {_ , _} _ 


αL : DAlgLift (ListO A) (λ {i}{xs} → α {i}{xs}) 
              (μ⁺ (idO NatD) [ inv tt ]→ μ⁺ MaybeO A [ inv tt ]× `⊤)
αL {tt , ⟨ zero , lift tt ⟩} {lift tt , lift tt} (lift tt) = 
        λ x xs → liftConstructor (MaybeO A) (lift tt) (lift tt) (lift tt)
αL {tt , ⟨ suc zero , n , lift tt ⟩} {(a , lift tt , lift tt) , m , lift tt} (ih , lift tt) = 
       liftInd (idO NatD) 
               {T = μ BoolD [ tt ]× `⊤} 
               {T⁺ = μ⁺ MaybeO A [ inv tt ]× `⊤}
               (λ {i}{xs} → β (induction NatD _ (λ {i}{xs} → α {i}{xs}) n) {i}{xs}) 
               (λ {i}{xs} → βL n a ih {i}{xs})
αL {tt , ⟨ suc (suc ()) , _ ⟩} {_ , _} _


vlookup : Patch _<_ (typeLookup A)
vlookup m m' n vs = liftInd (ListO A) {i = tt}{i⁺ = inv tt} 
                           {T = μ NatD [ tt ]→ μ BoolD [ tt ]× `⊤}
                           {T⁺ = μ⁺ (idO NatD) [ inv tt ]→ 
                                 μ⁺ MaybeO A [ inv tt ]× `⊤} 
                           (λ {i}{xs} → α {i}{xs})
                           (λ{i}{xs} → αL {i}{xs}) n vs m m'

open import Chapter9.Patch.Apply

lookup : ⟦ typeLookup A ⟧FunctionOrn
lookup = patch (typeLookup A) _<_ vlookup