module Uniform.Shape
  (C : Set1)
  (HomC : C -> C -> Set)
  (idC : (c : C) -> HomC c c)
  (_∘C_ : {a b c : C} -> HomC b c -> HomC a b -> HomC a c)
  where

-- Definitions and lemmas relating the shape of a uniform code


open import Data.Unit
open import Data.Empty
open import Function

import Uniform.posIR
open Uniform.posIR C HomC idC _∘C_


same-shape : {Γ Δ : Ctxt} -> IR' Γ -> IR' Δ -> Set
same-shape (ι c) (ι d) = ⊤
same-shape (ι c) (σ B ψ) = ⊥
same-shape (ι c) (δ B ψ ψ→) = ⊥
same-shape (σ A γ) (ι d) = ⊥
same-shape (σ A γ) (σ B ψ) = same-shape γ ψ
same-shape (σ A γ) (δ B ψ ψ→) = ⊥
same-shape (δ A γ γ→) (ι d) = ⊥
same-shape (δ A γ γ→) (σ B ψ) = ⊥
same-shape (δ A γ γ→) (δ B ψ ψ→) = same-shape γ ψ


refl-shape : {Γ : Ctxt} -> (γ : IR' Γ) -> same-shape γ γ
refl-shape (ι c) = _
refl-shape (σ A γ) = refl-shape γ
refl-shape (δ A γ γ→) = refl-shape γ

trans-shape : {Γ Γ' Γ'' : Ctxt} -> {γ : IR' Γ}{γ' : IR' Γ'}{γ'' : IR' Γ''} ->
              same-shape γ γ' -> same-shape γ' γ'' -> same-shape γ γ''
trans-shape {γ = ι c} {ι d} {ι e} _ _ = tt
trans-shape {γ = ι c} {ι d} {σ C γ''} p ()
trans-shape {γ = ι c} {ι d} {δ V γ'' γ''→} p ()
trans-shape {γ = ι c} {σ B γ'} () q
trans-shape {γ = ι c} {δ B γ' γ'→} () q
trans-shape {γ = σ A γ} {ι d} () q
trans-shape {γ = σ A γ} {σ B γ'} {ι e} p ()
trans-shape {γ = σ A γ} {σ B γ'} {σ C γ''} p q = trans-shape {γ = γ} p q
trans-shape {γ = σ A γ} {σ B γ'} {δ C γ'' γ''→} p ()
trans-shape {γ = σ A γ} {δ B γ' γ'→} () q
trans-shape {γ = δ A γ γ→} {ι d} () q
trans-shape {γ = δ A γ γ→} {σ B γ'} () q
trans-shape {γ = δ A γ γ→} {δ B γ' γ'→} {ι e} p ()
trans-shape {γ = δ A γ γ→} {δ B γ' γ'→} {σ C γ''} p ()
trans-shape {γ = δ A γ γ→} {δ B γ' γ'→} {δ C γ'' γ''→} p q
  = trans-shape {γ = γ} p q

sym-shape : {Γ Δ : Ctxt} -> {γ : IR' Γ}{ψ : IR' Δ} ->
            same-shape γ ψ -> same-shape ψ γ
sym-shape {γ = ι c} {ι d} _ = tt
sym-shape {γ = ι c} {σ B ψ} ()
sym-shape {γ = ι c} {δ B ψ ψ→} ()
sym-shape {γ = σ A γ} {ι d} ()
sym-shape {γ = σ A γ} {σ B ψ} p = sym-shape {γ = γ} p
sym-shape {γ = σ A γ} {δ B ψ ψ→} ()
sym-shape {γ = δ A γ γ→} {ι d} ()
sym-shape {γ = δ A γ γ→} {σ B ψ} ()
sym-shape {γ = δ A γ γ→} {δ B ψ ψ→} p = sym-shape {γ = γ} p


IRcMor-preserves-shape : ∀ {Γ Δ Γ' Δ'} ->
                         {f : Env Γ -> Env Δ}{f' : Env Γ' -> Env Δ'} ->
                         (γ : IR' Δ) -> (γ' : IR' Δ') ->
                         same-shape γ γ' ->
                         same-shape {Γ} {Γ'} (IRcMor f γ) (IRcMor f' γ')
IRcMor-preserves-shape (ι c) (ι d) p = p
IRcMor-preserves-shape (ι c) (σ B ψ) ()
IRcMor-preserves-shape (ι c) (δ B ψ ψ→) ()
IRcMor-preserves-shape (σ A γ) (ι d) ()
IRcMor-preserves-shape (σ A γ) (σ B ψ) p = IRcMor-preserves-shape γ ψ p
IRcMor-preserves-shape (σ A γ) (δ B ψ ψ→) ()
IRcMor-preserves-shape (δ A γ γ→) (ι d) ()
IRcMor-preserves-shape (δ A γ γ→) (σ B ψ) ()
IRcMor-preserves-shape (δ A γ γ→) (δ B ψ ψ→) p = IRcMor-preserves-shape γ ψ p

IRcMor-same-shape : ∀ {Γ Δ} ->
                   {f : Env Γ -> Env Δ}
                   (γ : IR' Δ) ->
                   same-shape {Δ} {Γ} γ (IRcMor f γ)
IRcMor-same-shape (ι c) = tt
IRcMor-same-shape (σ A γ) = IRcMor-same-shape γ
IRcMor-same-shape (δ A γ γ→) = IRcMor-same-shape γ

mutual
  pad₀ : {Γ Δ : Ctxt} -> IR' Γ -> IR' Δ -> IR' Γ
  pad₀ (ι c) (ι d) = ι c
  pad₀ (ι c) (σ B ψ) = σ (λ _ → ⊤) (pad₀ (IRwkσ (ι c)) ψ)
  pad₀ (ι c) (δ B ψ ψ→)
    = δ (λ _ → ⊥) (pad₀ (IRwkδ (ι c)) ψ)
                  (λ _ → pad₀-mor  {ψ = ψ} (ι→ι (idC _)))
  pad₀ {Γ} {Δ} (σ A γ) (ι d) = σ A (pad₀ {Γ ,σ A} {Δ} γ (ι d))
  pad₀ (σ A γ) (σ B ψ) = σ A (pad₀ γ ψ)
  pad₀ (σ A γ) (δ B ψ ψ→) = σ A  (pad₀ γ (δ B ψ ψ→))
  pad₀ {Γ} {Δ} (δ A γ γ→) (ι d)
    = δ A (pad₀ {Γ ,δ A} {Δ} γ (ι d)) (pad₀-mor ∘ γ→)
  pad₀ (δ A γ γ→) (σ B ψ) = δ A (pad₀ γ (σ B ψ)) (pad₀-mor ∘ γ→)
  pad₀ (δ A γ γ→) (δ B ψ ψ→) = δ A (pad₀ γ ψ) (pad₀-mor ∘ γ→)

  pad₀-mor : {Γ Γ' Δ : Ctxt} ->
             {γ : IR' Γ}{γ' : IR' Γ'}{ψ : IR' Δ} 
             {e : Env Γ}{e' : Env Γ'} -> 
             Hom' e e' γ γ' -> 
             Hom' e e' (pad₀ γ ψ) (pad₀ γ' ψ)
  pad₀-mor {ψ = ι c'} (ι→ι f) = ι→ι f
  pad₀-mor {ψ = ι c'} (σ→σ f g) = σ→σ f (pad₀-mor ∘ g)
  pad₀-mor {ψ = ι c'} (δ→δ f g) = δ→δ f (pad₀-mor ∘ g)
  pad₀-mor {ψ = σ B ψ} (ι→ι f) = σ→σ id (λ _ → pad₀-mor {ψ = ψ} (ι→ι f))
  pad₀-mor {ψ = σ B ψ} (σ→σ f g) = σ→σ f (pad₀-mor ∘ g)
  pad₀-mor {ψ = σ B ψ} (δ→δ f g) = δ→δ f (pad₀-mor ∘ g)
  pad₀-mor {ψ = δ B ψ ψ→} (ι→ι f) = δ→δ id (λ _ → pad₀-mor {ψ = ψ} (ι→ι f))
  pad₀-mor {ψ = δ B ψ ψ→} (σ→σ f g) = σ→σ f (pad₀-mor ∘ g)
  pad₀-mor {ψ = δ B ψ ψ→} (δ→δ f g) = δ→δ f (pad₀-mor ∘ g)

mutual

  pad₁ : {Γ Δ : Ctxt} -> IR' Γ -> IR' Δ -> IR' Δ
  pad₁ (ι c) (ι d) = ι d
  pad₁ {Γ} {Δ} (ι c) (σ B ψ) = σ B (pad₁ {Γ} (ι c) ψ)
  pad₁ {Γ} {Δ} (ι c) (δ B ψ ψ→)
    = δ B (pad₁ {Γ} {Δ ,δ B} (ι c) ψ) (pad₁-mor {γ = ι c} ∘ ψ→)
  pad₁ (σ A γ) (ι d) = σ (λ _ → ⊤) (pad₁ γ (IRwkσ (ι d)))
  pad₁ (σ A γ) (σ B ψ) = σ B (pad₁ γ ψ)
  pad₁ (σ A γ) (δ B ψ ψ→) = σ (λ _ → ⊤) (pad₁ γ (IRwkσ (δ B ψ ψ→)))
  pad₁ (δ A γ γ→) (ι d)
   = δ (λ _ → ⊥) (pad₁ γ (IRwkδ (ι d))) 
                 (λ _ → pad₁-mor {γ = γ} (ι→ι (idC _)))
  pad₁ (δ A γ γ→) (σ B ψ)
   = δ (λ _ → ⊥) (pad₁ γ (IRwkδ (σ B ψ)))
                 (λ _ → pad₁-mor {γ = γ} (HomcMor _ _ (idIR' (σ B ψ))))
  pad₁ (δ A γ γ→) (δ B ψ ψ→) = δ B (pad₁ γ ψ) (pad₁-mor {γ = γ} ∘ ψ→)

  pad₁-mor : {Γ Δ Δ' : Ctxt} ->
             {γ : IR' Γ}{ψ : IR' Δ}{ψ' : IR' Δ'} 
             {e : Env Δ}{e' : Env Δ'} -> 
             Hom' e e' ψ ψ' -> 
             Hom' e e' (pad₁ γ ψ) (pad₁ γ ψ')
  pad₁-mor {γ = ι c} (ι→ι f) = ι→ι f
  pad₁-mor {γ = ι c} (σ→σ f g) = σ→σ f (pad₁-mor {γ = ι c} ∘ g)
  pad₁-mor {γ = ι c} (δ→δ f g) = δ→δ f (pad₁-mor {γ = ι c} ∘ g)
  pad₁-mor {γ = σ A γ} (ι→ι f) = σ→σ id (λ _ → pad₁-mor {γ = γ} (ι→ι f))
  pad₁-mor {γ = σ A γ} (σ→σ f g) = σ→σ f (pad₁-mor {γ = γ} ∘ g)
  pad₁-mor {γ = σ A γ} (δ→δ f g)
    = σ→σ id (λ _ → pad₁-mor {γ = γ} (δ→δ f (HomcMor _ _ ∘ g)))
  pad₁-mor {γ = δ A γ γ→} (ι→ι f) = δ→δ id (λ _ → pad₁-mor {γ = γ} (ι→ι f))
  pad₁-mor {γ = δ A γ γ→} (σ→σ f g)
    = δ→δ id (λ _ → pad₁-mor {γ = γ} (HomcMor _ _ (σ→σ f g)))
  pad₁-mor {γ = δ A γ γ→} (δ→δ f g) = δ→δ f (pad₁-mor {γ = γ} ∘ g)

pad₀-preserves-shape :  {Γ Γ' Δ : Ctxt} ->
                        (γ : IR' Γ) -> (γ' : IR' Γ') -> (ψ : IR' Δ) -> 
                        same-shape γ γ' -> same-shape (pad₀ γ ψ) (pad₀ γ' ψ)
pad₀-preserves-shape (ι c) (ι d) (ι e) _ = tt
pad₀-preserves-shape (ι c) (ι d) (σ C ψ) _
 = pad₀-preserves-shape (IRwkσ (ι c)) (IRwkσ (ι d)) ψ tt
pad₀-preserves-shape (ι c) (ι d) (δ C ψ ψ→) _
 =  pad₀-preserves-shape (IRwkδ (ι c)) (IRwkδ (ι d)) ψ tt
pad₀-preserves-shape (ι c) (σ B γ') ψ ()
pad₀-preserves-shape (ι c) (δ B γ' γ'→) ψ ()
pad₀-preserves-shape (σ A γ) (ι d) ψ ()
pad₀-preserves-shape (σ A γ) (σ B γ') (ι e) p = pad₀-preserves-shape γ γ' _ p
pad₀-preserves-shape (σ A γ) (σ B γ') (σ C ψ) p = pad₀-preserves-shape γ γ' _ p
pad₀-preserves-shape (σ A γ) (σ B γ') (δ C ψ ψ→) p
 = pad₀-preserves-shape γ γ' _ p
pad₀-preserves-shape (σ A γ) (δ B γ' γ'→) ψ ()
pad₀-preserves-shape (δ A γ γ→) (ι d) ψ ()
pad₀-preserves-shape (δ A γ γ→) (σ B γ') ψ ()
pad₀-preserves-shape (δ A γ γ→) (δ B γ' γ'→) (ι e) p
 = pad₀-preserves-shape γ γ' _ p
pad₀-preserves-shape (δ A γ γ→) (δ B γ' γ'→) (σ C ψ) p
 = pad₀-preserves-shape γ γ' _ p
pad₀-preserves-shape (δ A γ γ→) (δ B γ' γ'→) (δ C ψ ψ→) p
 = pad₀-preserves-shape γ γ' _ p



pad₁-preserves-shape :  {Γ Δ Δ' : Ctxt} ->
                        (γ : IR' Γ) -> (ψ : IR' Δ) -> (ψ' : IR' Δ') -> 
                        same-shape ψ ψ' -> same-shape (pad₁ γ ψ) (pad₁ γ ψ')
pad₁-preserves-shape (ι c) (ι d) (ι e) _ = tt
pad₁-preserves-shape (σ A γ) (ι d) (ι e) p = pad₁-preserves-shape γ _ _ p
pad₁-preserves-shape (δ A γ γ→) (ι d) (ι e) p = pad₁-preserves-shape γ _ _ p
pad₁-preserves-shape γ (ι d) (σ C ψ') ()
pad₁-preserves-shape γ (ι d) (δ C ψ' ψ'→) ()
pad₁-preserves-shape γ (σ B ψ) (ι e) ()
pad₁-preserves-shape (ι c) (σ B ψ) (σ C ψ') p
  = pad₁-preserves-shape (ι c) ψ ψ' p
pad₁-preserves-shape (σ A γ) (σ B ψ) (σ C ψ') p = pad₁-preserves-shape γ ψ ψ' p
pad₁-preserves-shape (δ A γ γ→) (σ B ψ) (σ C ψ') p
  = pad₁-preserves-shape γ _ _ (IRcMor-preserves-shape ψ ψ' p)
pad₁-preserves-shape γ (σ B ψ) (δ C ψ' ψ'→) ()
pad₁-preserves-shape γ (δ B ψ ψ→) (ι e) ()
pad₁-preserves-shape γ (δ B ψ ψ→) (σ C ψ') ()
pad₁-preserves-shape (ι c) (δ B ψ ψ→) (δ C₁ ψ' ψ'→) p
  = pad₁-preserves-shape (ι c) ψ ψ' p
pad₁-preserves-shape (σ A γ) (δ B ψ ψ→) (δ C₁ ψ' ψ'→) p
  = pad₁-preserves-shape γ _ _ (IRcMor-preserves-shape ψ ψ' p)
pad₁-preserves-shape (δ A γ γ→) (δ B ψ ψ→) (δ C₁ ψ' ψ'→) p
  = pad₁-preserves-shape γ ψ ψ' p

padded-same-shape : {Γ Δ : Ctxt} -> (γ : IR' Γ) -> (ψ : IR' Δ) ->
             same-shape (pad₀ γ ψ) (pad₁ γ ψ)
padded-same-shape (ι c) (ι d) = tt
padded-same-shape (ι c) (σ B ψ)
 = trans-shape {γ = pad₀ (IRwkσ (ι c)) ψ}
               (pad₀-preserves-shape (IRwkσ (ι c)) (ι c) ψ tt)
               (padded-same-shape (ι c) ψ)
padded-same-shape (ι c) (δ B ψ ψ→)
 = trans-shape {γ = pad₀ (IRwkδ (ι c)) ψ}
               (pad₀-preserves-shape (IRwkδ (ι c)) (ι c) ψ tt)
               (padded-same-shape (ι c) ψ)
padded-same-shape (σ A γ) (ι d)
 = trans-shape {γ = pad₀ γ (ι d)}
               (padded-same-shape γ (ι d))
               (pad₁-preserves-shape γ (ι d) (IRwkσ (ι d)) tt)
padded-same-shape (σ A γ) (σ B ψ) = padded-same-shape γ ψ
padded-same-shape (σ A γ) (δ B ψ ψ→)
 = trans-shape {γ = pad₀ γ (δ B ψ ψ→)}
               (padded-same-shape γ (δ B ψ ψ→))
               (pad₁-preserves-shape γ (δ B ψ ψ→) (IRwkσ (δ B ψ ψ→))
                                      (IRcMor-same-shape ψ))
padded-same-shape (δ A γ γ→) (ι d)
 = trans-shape {γ = pad₀ γ (ι d)}
               (padded-same-shape γ (ι d))
               (pad₁-preserves-shape γ (ι d) (IRwkδ (ι d)) tt)
padded-same-shape (δ A γ γ→) (σ B ψ)
  = trans-shape {γ = pad₀ γ (σ B ψ)}
                (padded-same-shape γ (σ B ψ))
                (pad₁-preserves-shape γ _ _ (IRcMor-same-shape ψ))
padded-same-shape (δ A γ γ→) (δ B ψ ψ→) = padded-same-shape γ ψ



same-ctxt-shape : Ctxt -> Ctxt -> Set
same-ctxt-shape [] [] = ⊤
same-ctxt-shape [] (Δ ,σ B) = ⊥
same-ctxt-shape [] (Δ ,δ B) = ⊥
same-ctxt-shape (Γ ,σ A) [] = ⊥
same-ctxt-shape (Γ ,σ A) (Δ ,σ B) = same-ctxt-shape Γ Δ
same-ctxt-shape (Γ ,σ A) (Δ ,δ B) = ⊥
same-ctxt-shape (Γ ,δ A) [] = ⊥
same-ctxt-shape (Γ ,δ A) (Δ ,σ B) = ⊥
same-ctxt-shape (Γ ,δ A) (Δ ,δ B) = same-ctxt-shape Γ Δ