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