module Uniform.EnvBool
  (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

-- Merging two contexts of the same shape by putting a boolean in
-- front

open import Data.Product as P
open import Function
open import Data.Unit
open import Data.Bool
open import Relation.Binary.PropositionalEquality
open import Level

open import Prelude.Equality

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


mutual

  Bool,  : (Γ Δ : Ctxt) -> same-ctxt-shape Γ Δ -> Ctxt
  Bool, [] [] _ = [] ,σ (λ _ → Bool)
  Bool, (Γ ,σ A) (Δ ,σ B) p = Bool, Γ Δ p ,σ ((λ x → Bool-elim (λ z → (Env (if z then Γ else Δ)) -> Set) A B (proj₁ x) (proj₂ x)) ∘′ EnvBool, Γ Δ p)
  Bool, (Γ ,δ A) (Δ ,δ B) p = Bool, Γ Δ p ,δ ((λ x → Bool-elim (λ z → (Env (if z then Γ else Δ)) -> Set) A B (proj₁ x) (proj₂ x)) ∘′ EnvBool, Γ Δ p)
  Bool, [] (Δ ,σ B) ()
  Bool, [] (Δ ,δ B) ()
  Bool, (Γ ,σ A) [] ()
  Bool, (Γ ,σ A) (Δ ,δ B) ()
  Bool, (Γ ,δ A) [] ()
  Bool, (Γ ,δ A) (Δ ,σ B) ()




  EnvBool, : (Γ Δ : Ctxt) -> (p : same-ctxt-shape Γ Δ) ->
             Env (Bool, Γ Δ p) -> Σ[ x ∈ Bool ] (Env (if x then Γ else Δ))
  EnvBool, [] [] _ (_ , true) = true , (lift tt)
  EnvBool, [] [] _ (_ , false) = false , (lift tt)
  EnvBool, (Γ ,σ A) (Δ ,σ B) p (x , A|B)
   = (proj₁ (EnvBool, Γ Δ p x)) ,
      EnvBool,-withσ Γ A Δ B p (proj₁ (EnvBool, Γ Δ p x))
                     (proj₂ (EnvBool, Γ Δ p x)) x A|B
{- -- handwritten with function, encoding the following:
  EnvBool, (Γ ,σ A) (Δ ,σ B) p (x , A|B) with EnvBool, Γ Δ p x
  ... | true , e = true , e , A|B
  ... | false , e = false , e , A|B
-}
  EnvBool, (Γ ,δ A) (Δ ,δ B) p (x , A|B)
    = (proj₁ (EnvBool, Γ Δ p x)) ,
       EnvBool,-withδ Γ A Δ B p (proj₁ (EnvBool, Γ Δ p x))
                      (proj₂ (EnvBool, Γ Δ p x)) x A|B
{- handwritten with function, encoding the following:
  EnvBool, (Γ ,δ A) (Δ ,δ B) p (x , A|B) with EnvBool, Γ Δ p x
  ... | true , e = true , e , A|B
  ... | false , e = false , e , A|B
-}
  EnvBool, [] (Δ ,σ x) ()
  EnvBool, [] (Δ ,δ x) ()
  EnvBool, (Γ ,σ x) [] ()
  EnvBool, (Γ ,σ x) (Δ ,δ x₁) ()
  EnvBool, (Γ ,δ x) [] ()
  EnvBool, (Γ ,δ x) (Δ ,σ x₁) ()

  EnvBool,-withσ : (Γ : Ctxt) ->
                   (A : Env Γ -> Set) ->
                   (Δ : Ctxt) ->
                   (B : Env Δ -> Set)
                   (p : same-ctxt-shape Γ Δ)
                   (t : Bool) ->
                   (w : Env (if t then Γ else Δ)) ->
                   (e : Env (Bool, Γ Δ p))
                   (A|B  : Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B
                                     t w) ->
                   (Env (if t then Γ ,σ A else Δ ,σ B))
  EnvBool,-withσ Γ A Δ B p true w e A|B = w , A|B
  EnvBool,-withσ Γ A Δ B p false w e A|B = w , A|B

  EnvBool,-withδ : (Γ : Ctxt) ->
                   (A : Env Γ -> Set) ->
                   (Δ : Ctxt) ->
                   (B : Env Δ -> Set)
                   (p : same-ctxt-shape Γ Δ)
                   (t : Bool) ->
                   (w : Env (if t then Γ else Δ)) ->
                   (e : Env (Bool, Γ Δ p)) ->
                   (A|B  : Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B
                                     t w → C) ->
                   (Env (if t then Γ ,δ A else Δ ,δ B))
  EnvBool,-withδ Γ A Δ B p true w e A|B = w , A|B
  EnvBool,-withδ Γ A Δ B p false w e A|B = w , A|B



EnvBool,-withσ-lemma-true : {Γ : Ctxt} ->
                            {A : Env Γ -> Set} ->
                            {γ : IR' (Γ ,σ A)} ->
                            {Δ : Ctxt} ->
                            {B : Env Δ -> Set}
                            {ψ : IR' (Δ ,σ B)} ->
                            {q : same-ctxt-shape Γ Δ}
                            {w : Env (if true then Γ else Δ)} ->
                            {e : Env (Bool, Γ Δ q)} ->
                            (eq : (true , w) ≡ (EnvBool, Γ Δ q e)) ->
                            (h : A w) ->
    Σ[ fst ∈ (Γ ,σ A ≡ (if proj₁ (EnvBool, Γ Δ q e) then Γ ,σ A else Δ ,σ B)) ]
       (proj₁ (subst (λ Γ₁ → (Env Γ₁) × (IR' Γ₁)) fst ((w , h) , γ))
         ≡ EnvBool,-withσ Γ A Δ B q
                          (proj₁ (EnvBool, Γ Δ q e))
                          (proj₂ (EnvBool, Γ Δ q e))
                          e
                          (subst (λ r → Bool-elim
                                         (λ z → Env (if z then Γ else Δ) → Set)
                                         A B
                                         (proj₁ r) (proj₂ r)) eq h))
      × (proj₂ (subst (λ Γ₁ → (Env Γ₁) × (IR' Γ₁)) fst ((w , h) , γ))
         ≡ Bool-elim (λ z → IR' (if z then Γ ,σ A else Δ ,σ B)) γ ψ
                     (proj₁ (EnvBool, Γ Δ q e)))
EnvBool,-withσ-lemma-true {Γ} {Δ = Δ} {q = q} {w} {e} eq h
                                           with (EnvBool, Γ Δ q e) | eq
... | .(true , w) | refl = refl , refl , refl



EnvBool,-withσ-lemma-false : {Γ : Ctxt} ->
                             {A : Env Γ -> Set} ->
                             {γ : IR' (Γ ,σ A)} ->
                             {Δ : Ctxt} ->
                             {B : Env Δ -> Set}
                             {ψ : IR' (Δ ,σ B)} ->
                             {q : same-ctxt-shape Γ Δ}
                             {w : Env (if false then Γ else Δ)} ->
                             {e : Env (Bool, Γ Δ q)} ->
                             (eq : (false , w) ≡ (EnvBool, Γ Δ q e)) ->
                             (h : B w) ->
    Σ[ fst ∈ (Δ ,σ B ≡ (if proj₁ (EnvBool, Γ Δ q e) then Γ ,σ A else Δ ,σ B)) ]
       (proj₁ (subst (λ Γ₁ → (Env Γ₁) × (IR' Γ₁)) fst ((w , h) , ψ))
         ≡ EnvBool,-withσ Γ A Δ B q
                          (proj₁ (EnvBool, Γ Δ q e))
                          (proj₂ (EnvBool, Γ Δ q e))
                          e
                          (subst (λ r → Bool-elim
                                         (λ z → Env (if z then Γ else Δ) → Set)
                                         A B
                                         (proj₁ r) (proj₂ r)) eq h))
      × (proj₂ (subst (λ Γ₁ → (Env Γ₁) × (IR' Γ₁)) fst ((w , h) , ψ))
         ≡ Bool-elim (λ z → IR' (if z then Γ ,σ A else Δ ,σ B)) γ ψ
                     (proj₁ (EnvBool, Γ Δ q e)))
EnvBool,-withσ-lemma-false {Γ} {Δ = Δ} {q = q} {w} {e} eq h
                                              with (EnvBool, Γ Δ q e) | eq
... | .(false , w) | refl = refl , (refl , refl)


EnvBool,-withδ-lemma-true : (Γ : Ctxt) ->
                            (A : Env Γ -> Set) ->
                            (γ : IR' (Γ ,δ A)) ->
                            (Δ : Ctxt) ->
                            (B : Env Δ -> Set)
                            (ψ : IR' (Δ ,δ B)) ->
                            (q : same-ctxt-shape Γ Δ)
                            (w : Env (if true then Γ else Δ)) ->
                            (e : Env (Bool, Γ Δ q)) ->
                            (eq : (true , w) ≡ (EnvBool, Γ Δ q e)) ->
                            (h : A w -> C) ->
                            Σ[ fst ∈ (Γ ,δ A ≡ (if proj₁ (EnvBool, Γ Δ q e) then Γ ,δ A else Δ ,δ B)) ] (proj₁ (subst (λ Γ₁ → (Env Γ₁) × (IR' Γ₁)) fst ((w , h) , γ)) ≡ EnvBool,-withδ Γ A Δ B q (proj₁ (EnvBool, Γ Δ q e)) (proj₂ (EnvBool, Γ Δ q e)) e (subst (λ r → Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B (proj₁ r) (proj₂ r) → C) eq h)) × (proj₂ (subst (λ Γ₁ → (Env Γ₁) × (IR' Γ₁)) fst ((w , h) , γ)) ≡ Bool-elim (λ z → IR' (if z then Γ ,δ A else Δ ,δ B)) γ ψ (proj₁ (EnvBool, Γ Δ q e)))
EnvBool,-withδ-lemma-true Γ A γ Δ B ψ q w e eq h  with (EnvBool, Γ Δ q e) | eq
... | .(true , w) | refl = refl , refl , refl

EnvBool,-withδ-lemma-false : (Γ : Ctxt) ->
                            (A : Env Γ -> Set) ->
                            (γ : IR' (Γ ,δ A)) ->
                            (Δ : Ctxt) ->
                            (B : Env Δ -> Set)
                            (ψ : IR' (Δ ,δ B)) ->
                            (q : same-ctxt-shape Γ Δ)
                            (w : Env (if false then Γ else Δ)) ->
                            (e : Env (Bool, Γ Δ q)) ->
                            (eq : (false , w) ≡ (EnvBool, Γ Δ q e)) ->
                            (h : B w -> C) ->
                            Σ[ fst ∈ (Δ ,δ B ≡ (if proj₁ (EnvBool, Γ Δ q e) then Γ ,δ A else Δ ,δ B)) ] (proj₁ (subst (λ Γ₁ → (Env Γ₁) × (IR' Γ₁)) fst ((w , h) , ψ)) ≡ EnvBool,-withδ Γ A Δ B q (proj₁ (EnvBool, Γ Δ q e)) (proj₂ (EnvBool, Γ Δ q e)) e (subst (λ r → Bool-elim (λ z → Env (if z then Γ else Δ) → Set) A B (proj₁ r) (proj₂ r) → C) eq h)) × (proj₂ (subst (λ Γ₁ → (Env Γ₁) × (IR' Γ₁)) fst ((w , h) , ψ)) ≡ Bool-elim (λ z → IR' (if z then Γ ,δ A else Δ ,δ B)) γ ψ (proj₁ (EnvBool, Γ Δ q e)))
EnvBool,-withδ-lemma-false Γ A γ Δ B ψ q w e eq h  with (EnvBool, Γ Δ q e) | eq
... | .(false , w) | refl = refl , (refl , refl)