module Uniform.Constructions.Pi
  where

-- This module implements a "uniform pi" for uniform IR+(Set^op) codes.
-- As a special case, we get a code K → γ for exponentiation with
-- a set K.


open import Data.Product as P
open import Function

import Prelude
open Prelude Set (λ A B → B -> A) (λ c → id) (λ f g → g ∘ f)



import Uniform.posIR
open Uniform.posIR Set (λ A B → B -> A)
                   (λ c → id) (λ f g → g ∘ f)

import Uniform.Shape
open Uniform.Shape Set (λ A B → B -> A) (λ c → id) (λ f g → g ∘ f)


private
  C : Set1
  C = Set
  
  HomC : Set -> Set -> Set
  HomC = (λ A B → B -> A)


-- inversion for IR morphisms
extractι→ι : {Γ Δ : Ctxt}{e : Env Γ}{e' : Env Δ} -> 
                     {c : Env Γ -> C}{c' : Env Δ -> C} ->
                     Hom' {Γ} {Δ} e e' (ι c) (ι c') -> HomC (c e) (c' e')
extractι→ι (ι→ι g) = g

extractσ→σ : ∀ {Γ Δ A B γ γ'}-> {e : Env Γ}{e' : Env Δ} -> 
              Hom' {Γ} {Δ} e e' (σ A γ) (σ B γ') ->
              Σ[ f ∈ (A e -> B e')] ((x : A e) -> Hom' (e , x) (e' , f x) γ γ')
extractσ→σ (σ→σ f g) = f , g

extractδ→δ : ∀ {Γ Δ e e' A B γ γ'} ->
              {γ→ : ∀ {e}{f g : A e -> C} -> ((a : A e) -> HomC (f a) (g a)) ->
                  Hom' {Γ ,δ A} {Γ ,δ A} (e , f) (e , g) γ γ} ->
              {γ'→ : ∀ {e f g} -> ((a : B e) -> HomC (f a) (g a)) ->
                  Hom' {Δ ,δ B} {Δ ,δ B} (e , f) (e , g) γ' γ'} ->
              Hom' {Γ} {Δ} e e' (δ A γ γ→) (δ B γ' γ'→) ->
              Σ[ f ∈ (B e' -> A e) ]
                  ((h : A e -> C) -> Hom' (e , h) (e' , h ∘ f) γ γ')
extractδ→δ (δ→δ f g) = f , g



mutual
  {-# TERMINATING #-} -- IRcMor preserves structure, but Agda can't see it;
                      -- could use sized types to fix this
  _⇒_ : {Γ : Ctxt} -> (K : Env Γ -> Set) -> IR' (Γ ,σ K) -> IR' Γ
  K ⇒ (ι c) = ι (λ e → Σ[ x ∈ (K e) ] (c (e , x))) 
  K ⇒ (σ A γ) = σ (λ e → (x : K e) -> A (e , x))
                  ((K ∘ proj₁) ⇒  (IRcMor (λ x → let y = proj₁ (proj₁ x)
                                                     f = proj₂ (proj₁ x)
                                                     k = proj₂ x
                                                 in (y , k) , f k ) γ))
  K ⇒ (δ A γ γ→)
   = δ (λ e → Σ[ x ∈ K e ] A (e , x))
       ((K ∘ proj₁) ⇒ IRcMor (λ x → let y = proj₁ (proj₁ x)
                                        F = proj₂ (proj₁ x)
                                        k = proj₂ x
                                    in (y , k) , λ a → F (k , a)) γ)
       (λ {e} {f} {g} η → ⇒-mor (K ∘ proj₁) (K ∘ proj₁) id _ _ (refl-shape (IRcMor _ γ)) (λ {k} → HomcMor _ _ (γ→ (λ a → η (k , a)))) )

  ⇒-mor : {Γ Δ : Ctxt} ->
           (K : Env Γ -> Set) ->
           (K' : Env Δ -> Set) ->
           {e : Env Γ}{e' : Env Δ} ->
           (h : K' e' -> K e) ->
           (γ : IR' (Γ ,σ K))(γ' : IR' (Δ ,σ K')) ->
           same-shape γ γ' ->
           ({k : K' e'} -> Hom' (e , h k) (e' , k) γ γ') ->
           Hom' e e' (K ⇒ γ) (K' ⇒ γ')
  ⇒-mor K K' h (ι c) (ι c') p f = ι→ι (P.map h (λ {k} → extractι→ι (f {k})))
  ⇒-mor K K' h (ι x) (σ A γ') () f 
  ⇒-mor K K' h (ι x) (δ A γ' γ→) () f
  ⇒-mor K K' h (σ A γ) (ι x) () f
  ⇒-mor K K' h (σ A γ) (σ B γ') p f = σ→σ (λ g k → proj₁ (extractσ→σ (f {k})) (g (h k))) (λ g → ⇒-mor (K ∘ proj₁) (K' ∘ proj₁) h (IRcMor _ γ) (IRcMor _ γ') (IRcMor-preserves-shape γ γ' p) (λ {k} → HomcMor _ _ (proj₂ (extractσ→σ (f {k})) (g (h k)))))
  ⇒-mor K K' h (σ A γ) (δ A₁ γ' γ→) () f
  ⇒-mor K K' h (δ A γ γ→) (ι x) () f
  ⇒-mor K K' h (δ A γ γ→) (σ A₁ γ') () f
  ⇒-mor K K' h (δ A γ γ→) (δ A₁ γ' γ→₁) p f = δ→δ (P.map h (λ {x} → proj₁ (extractδ→δ (f {x})))) (λ g → ⇒-mor (K ∘ proj₁) (K' ∘ proj₁) h _ _ (IRcMor-preserves-shape γ γ' p) (λ {k} → HomcMor _ _ (proj₂ (extractδ→δ (f {k})) (λ a → g ((h k) , a)))))