open import Data.Product
open import Data.Unit

open import Logic.Logic

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

open import Relation.Binary.PropositionalEquality

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

open import Orn.Ornament

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

open import Orn.Ornament.Examples.Lifting renaming (□h to □ho)


toILift : {I : Set }
          {X : I → Set }
          (D : IDesc  I)
          (P : ∀{i} → X i → Set )
          (xs : ⟦ D ⟧ X) →
          □h D 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)) →
           □h D' (λ t → Q (fold D α t)) xs →
           □h D' Q (Fold.hyps D α D' xs)
□gmap (`var i) xs ih = ih
□gmap `1 xs ih = ih
□gmap (D₁ `× D₂) (xs₁ , xs₂) (ih₁ , ih₂) = 
    □gmap D₁ xs₁ ih₁ , □gmap D₂ xs₂ ih₂
□gmap (`σ n T) (k , xs) ih = □gmap (T k) xs ih
□gmap (`Σ S T) (s , xs) ih = □gmap (T s) xs ih
□gmap (`Π S T) xs ih = λ s → □gmap (T s) (xs s) (ih s)
  

-- Paper: Remark 4.21
-- Typeset: make D α xs = make D^{α} xs
make : ∀{k} → (x : μ D k) → μ algOrnD (k , fold D α x)
make 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 : □h D' (λ {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 α' tt tt = tt , (refl , 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₁) 
                     (□gmap D₁ xs₁ ih₁) , 
                toILift D₂ (λ {k} x → μ algOrnD (k , x)) 
                     (Fold.hyps D α D₂ xs₂)
                     (□gmap D₂ 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)
                     (□gmap (T s) 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)
                     (□gmap (T s) 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))
                           (□gmap (T s) (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 ⟩