open import Level 

open import Data.Product
open import Data.Unit

open import Chapter2.Logic

open import Chapter5.IDesc
open import Chapter5.IDesc.Fixpoint
open import Chapter5.IDesc.InitialAlgebra
open import Chapter5.IDesc.Induction
open import Chapter5.IDesc.Lifting

open import Relation.Binary.PropositionalEquality

module Chapter8.AlgebraicOrnament.Make
           {ℓ : Level}
           {K : Set ℓ}
           {X : K → Set ℓ}
           (D : func ℓ K K)
           (α : ⟦ D ⟧func X ⇒ X) where

open import Chapter8.Ornament

import Chapter8.AlgebraicOrnament
open Chapter8.AlgebraicOrnament.Func D α
open Chapter8.AlgebraicOrnament hiding (algOrnD)

open import Chapter8.Ornament.Examples.Lifting renaming ([_]^h to [_]^ho)


toILift : {I : Set ℓ}
          {X : I → Set ℓ}
          (D : IDesc ℓ I)
          (P : ∀{i} → X i → Set ℓ)
          (xs : ⟦ D ⟧ X) →
          [ D ]^h P xs → 
          ⟦ (⟦ [_]^ho {L = I} D xs ⟧Orn) ⟧ 
            (λ ix → P {proj₁ ix} (proj₂ ix))
toILift (`var i) P xs ih = ih
toILift `1 P xs ih = ih
toILift (D₁ `× D₂) P (xs₁ , xs₂) (ih₁ , ih₂) = 
  toILift D₁ P xs₁ ih₁ , toILift D₂ P xs₂ ih₂
toILift (`σ n T) P (k , xs) ih = toILift (T k) P xs ih
toILift (`Σ S T) P (s , xs) ih = toILift (T s) P xs ih
toILift (`Π S T) P xs ih = λ s → toILift (T s) P (xs s) (ih s)

-- This generalizes (slightly, but not fully) [_]^map:
[_]^gmap : (D' : IDesc ℓ K)
           {Q : ∀{i} → X i → Set ℓ}
           {α : ∀{i} → ⟦ func.out D i ⟧ X → X i}
           (xs : ⟦ D' ⟧ (μ D)) →
           [ D' ]^h (λ t → Q (fold D α t)) xs →
           [ D' ]^h Q (Fold.hyps D α D' xs)
[ `var i ]^gmap xs ih = ih
[ `1 ]^gmap xs ih = ih
[ D₁ `× D₂ ]^gmap (xs₁ , xs₂) (ih₁ , ih₂) = 
    [ D₁ ]^gmap xs₁ ih₁ , [ D₂ ]^gmap xs₂ ih₂
[ `σ n T ]^gmap (k , xs) ih = [ T k ]^gmap xs ih
[ `Σ S T ]^gmap (s , xs) ih = [ T s ]^gmap xs ih
[ `Π S T ]^gmap xs ih = λ s → [ T s ]^gmap (xs s) (ih s)
  
makeAlg : ∀{k} → (x : μ D k) → μ algOrnD (k , fold D α x)
makeAlg x = induction D (λ {k} x → μ algOrnD (k , fold D α x)) step x
        where step' : (k : K)
                      (D' : IDesc ℓ K)
                      (α' : ⟦ D' ⟧ X → X k)
                      (xs : ⟦ D' ⟧ (μ D))
                      (ih : [ D' ]^h (λ {k} x → μ algOrnD (k , fold D α x)) xs) →
                      ⟦ Desc.algOrnD k (α' (Fold.hyps D α D' xs))  D' α' ⟧ (μ algOrnD)

              step' k (`var i) α' xs ih = Fold.fold D α xs , 
                                          refl , ih
              step' k `1 α' (lift tt) (lift tt) = (lift tt) , (refl , (lift tt))
              step' k (D₁ `× D₂) α' (xs₁ , xs₂) (ih₁ , ih₂) = 
                ( Fold.hyps D α D₁ xs₁ , Fold.hyps D α D₂ xs₂) , 
                refl , 
                toILift D₁ (λ {k} x → μ algOrnD (k , x)) 
                     (Fold.hyps D α D₁ xs₁) 
                     ([ D₁ ]^gmap xs₁ ih₁) , 
                toILift D₂ (λ {k} x → μ algOrnD (k , x)) 
                     (Fold.hyps D α D₂ xs₂)
                     ([ D₂ ]^gmap xs₂ ih₂) 
              step' k (`σ n T) α' (s , xs) ih = 
                (s , Fold.hyps D α (T s) xs) , 
                refl , 
                toILift (T s) (λ {k} x → μ algOrnD (k , x)) 
                     (Fold.hyps D α (T s) xs)
                     ([ T s ]^gmap xs ih)
              step' k (`Σ S T) α' (s , xs) ih = 
                (s , (Fold.hyps D α (T s) xs)) ,
                refl , 
                toILift (T s) (λ {k} x → μ algOrnD (k , x)) 
                     (Fold.hyps D α (T s) xs)
                     ([ T s ]^gmap xs ih)
              step' k (`Π S T) α' xs ih = 
                (λ s → Fold.hyps D α (T s) (xs s)) , 
                refl , 
                λ s → toILift (T s) 
                           (λ {k₁} x₁ → μ algOrnD (k₁ , x₁))
                           (Fold.hyps D α (T s) (xs s))
                           ([ T s ]^gmap (xs s) (ih s))

              step : DAlg D (λ {k} x → μ algOrnD (k , fold D α x))
              step {k}{xs} x = ⟨ step' k (func.out D k) (α {k}) xs x ⟩