{-# OPTIONS --rewriting #-}

module TypeIsos where

import DS
import DSK
import CPS
open import DS-DSK
open import DSK-DS
open import DSK-CPS
open import CPS-DSK
open import DS-CPS
open import CPS-DS

open import Data.Unit
open import Data.Empty
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality


-- DS <-> DSK type translations (knT ∘ embT)
mutual
  knT∘embT≡id : (τ : DSK.Ty) → knT (embT τ) ≡ τ
  knT∘embT≡id DSK.Nat = refl
  knT∘embT≡id DSK.Bol = refl
  knT∘embT≡id (τ₂ DSK.⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)
    rewrite knT∘embT≡id τ₁
          | knT∘embT≡id τ₂
          | knT∘embT≡id α
          | knT∘embT≡id β
          | knMc∘embMc≡id σα
          | knMc∘embMc≡id σβ = refl
  
  knMc∘embMc≡id : (σ : DSK.Mc) → knMc (embMc σ) ≡ σ
  knMc∘embMc≡id DSK.• = refl
  knMc∘embMc≡id (τ DSK.⇨⟨ σα ⟩ α ∷ σβ)
    rewrite knT∘embT≡id τ
          | knT∘embT≡id α
          | knMc∘embMc≡id σα
          | knMc∘embMc≡id σβ = refl

{-# REWRITE knT∘embT≡id #-}
{-# REWRITE knMc∘embMc≡id #-}

kn-id∘emb-id≡id : {τ τ' : DSK.Ty} {σ : DSK.Mc} →
                  (id : DSK.id-cont-type (τ DSK.▷⟨ σ ⟩ τ')) →
                  kn-id-cont-type (emb-id-cont-type id) ≡ id
kn-id∘emb-id≡id {σ = DSK.•} refl = refl
kn-id∘emb-id≡id {σ = τ₁ DSK.⇨⟨ σ₁ ⟩ τ₂ ∷ σ₂} (refl , refl , refl) = refl

{-# REWRITE kn-id∘emb-id≡id #-}


-- DS <-> DSK type translations (embT ∘ knT)
mutual
  embT∘knT≡id : (τ : DS.Ty) → embT (knT τ) ≡ τ
  embT∘knT≡id DS.Nat = refl
  embT∘knT≡id DS.Bol = refl
  embT∘knT≡id (τ₂ DS.⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)
    rewrite embT∘knT≡id τ₁
          | embT∘knT≡id τ₂
          | embT∘knT≡id α
          | embT∘knT≡id β
          | embMc∘knMc≡id σα
          | embMc∘knMc≡id σβ = refl

  embMc∘knMc≡id : (σ : DS.Mc) → embMc (knMc σ) ≡ σ
  embMc∘knMc≡id DS.• = refl
  embMc∘knMc≡id (τ DS.⇨⟨ σα ⟩ α ∷ σβ)
    rewrite embT∘knT≡id τ
          | embT∘knT≡id α
          | embMc∘knMc≡id σα
          | embMc∘knMc≡id σβ = refl

{-# REWRITE embT∘knT≡id #-}
{-# REWRITE embMc∘knMc≡id #-}

emb-id∘kn-id≡id : {τ τ' : DS.Ty} {σ : DS.Mc} →
                  (id : DS.id-cont-type τ σ τ') →
                  emb-id-cont-type (kn-id-cont-type id) ≡ id
emb-id∘kn-id≡id {σ = DS.•} refl = refl
emb-id∘kn-id≡id {σ = τ₁ DS.⇨⟨ σ₁ ⟩ τ₂ ∷ σ₂} (refl , refl , refl) = refl

{-# REWRITE emb-id∘kn-id≡id #-}


-- DSK <-> CPS type translations (cpskT ∘ dskT)
mutual
  cpskT∘dskT≡id : (τ : CPS.Ty) → cpskT (dskT τ) ≡ τ
  cpskT∘dskT≡id CPS.Nat = refl
  cpskT∘dskT≡id CPS.Bol = refl
  cpskT∘dskT≡id (τ₂ CPS.⇒[ τ₁ CPS.⇒ σα ⇒ α ]⇒ σβ ⇒ β)
    rewrite cpskT∘dskT≡id τ₁
          | cpskT∘dskT≡id τ₂
          | cpskT∘dskT≡id α
          | cpskT∘dskT≡id β
          | cpskMc∘dskMc≡id σα
          | cpskMc∘dskMc≡id σβ = refl
  
  cpskMc∘dskMc≡id : (σ : CPS.Mc) → cpskMc (dskMc σ) ≡ σ
  cpskMc∘dskMc≡id CPS.[] = refl
  cpskMc∘dskMc≡id ((τ CPS.⇒ σα ⇒ α) CPS.∷ σβ)
    rewrite cpskT∘dskT≡id τ
          | cpskT∘dskT≡id α
          | cpskMc∘dskMc≡id σα
          | cpskMc∘dskMc≡id σβ = refl

{-# REWRITE cpskT∘dskT≡id #-}
{-# REWRITE cpskMc∘dskMc≡id #-}

cpsk-id∘dsk-id≡id : {τ τ' : CPS.Ty} {σ : CPS.Mc} →
                  (id : CPS.id-cont-type (τ CPS.⇒ σ ⇒ τ')) →
                  cpsk-id-cont-type (dsk-id-cont-type id) ≡ id
cpsk-id∘dsk-id≡id {σ = CPS.[]} refl = refl
cpsk-id∘dsk-id≡id {σ = (τ₁ CPS.⇒ σ₁ ⇒ τ₂) CPS.∷ σ₂} (refl , refl , refl) = refl

{-# REWRITE cpsk-id∘dsk-id≡id #-}

cpskΔ∘dskΔ≡id : (Δ : CPS.Delta) → cpskΔ (dskΔ Δ) ≡ Δ
cpskΔ∘dskΔ≡id (CPS.K (τ CPS.⇒ σ ⇒ α)) = refl
cpskΔ∘dskΔ≡id (CPS.• (γ CPS.⇒ σid ⇒ γ') id) = refl

{-# REWRITE cpskΔ∘dskΔ≡id #-}

cpskΘ∘dskΘ≡id : (Θ : CPS.Theta) → cpskΘ (dskΘ Θ) ≡ Θ
cpskΘ∘dskΘ≡id CPS.G = refl
cpskΘ∘dskΘ≡id (CPS.D Δ) = refl

{-# REWRITE cpskΘ∘dskΘ≡id #-}


-- DSK <-> CPS type translations (dskT ∘ cpskT)
mutual
  dskT∘cpskT≡id : (τ : DSK.Ty) → dskT (cpskT τ) ≡ τ
  dskT∘cpskT≡id DSK.Nat = refl
  dskT∘cpskT≡id DSK.Bol = refl
  dskT∘cpskT≡id (τ₂ DSK.⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)
    rewrite dskT∘cpskT≡id τ₁
          | dskT∘cpskT≡id τ₂
          | dskT∘cpskT≡id α
          | dskT∘cpskT≡id β
          | dskMc∘cpskMc≡id σα
          | dskMc∘cpskMc≡id σβ = refl

  dskMc∘cpskMc≡id : (σ : DSK.Mc) → dskMc (cpskMc σ) ≡ σ
  dskMc∘cpskMc≡id DSK.• = refl
  dskMc∘cpskMc≡id (τ DSK.⇨⟨ σα ⟩ α ∷ σβ)
    rewrite dskT∘cpskT≡id τ
          | dskT∘cpskT≡id α
          | dskMc∘cpskMc≡id σα
          | dskMc∘cpskMc≡id σβ = refl

{-# REWRITE dskT∘cpskT≡id #-}
{-# REWRITE dskMc∘cpskMc≡id #-}

dsk-id∘cpsk-id≡id : {τ τ' : DSK.Ty} {σ : DSK.Mc} →
                  (id : DSK.id-cont-type (τ DSK.▷⟨ σ ⟩ τ')) →
                  dsk-id-cont-type (cpsk-id-cont-type id) ≡ id
dsk-id∘cpsk-id≡id {σ = DSK.•} refl = refl
dsk-id∘cpsk-id≡id {σ = τ₁ DSK.⇨⟨ σ₁ ⟩ τ₂ ∷ σ₂} (refl , refl , refl) = refl

{-# REWRITE dsk-id∘cpsk-id≡id #-}

dskΔ∘cpskΔ≡id : (Δ : DSK.Delta) → dskΔ (cpskΔ Δ) ≡ Δ
dskΔ∘cpskΔ≡id (DSK.K (τ DSK.▷⟨ σ ⟩ α)) = refl
dskΔ∘cpskΔ≡id (DSK.• (γ DSK.▷⟨ σid ⟩ γ') id) = refl

{-# REWRITE dskΔ∘cpskΔ≡id #-}

dskΘ∘cpskΘ≡id : (Θ : DSK.Theta) → dskΘ (cpskΘ Θ) ≡ Θ
dskΘ∘cpskΘ≡id DSK.G = refl
dskΘ∘cpskΘ≡id (DSK.D Δ) = refl

{-# REWRITE dskΘ∘cpskΘ≡id #-}


-- DS <-> CPS type translations (cpsT ∘ dsT)
mutual
  cpsT∘dsT≡id : (τ : CPS.Ty) → cpsT (dsT τ) ≡ τ
  cpsT∘dsT≡id CPS.Nat = refl
  cpsT∘dsT≡id CPS.Bol = refl
  cpsT∘dsT≡id (τ₂ CPS.⇒[ τ₁ CPS.⇒ σα ⇒ α ]⇒ σβ ⇒ β)
    rewrite cpsT∘dsT≡id τ₁
          | cpsT∘dsT≡id τ₂
          | cpsT∘dsT≡id α
          | cpsT∘dsT≡id β
          | cpsMc∘dsMc≡id σα
          | cpsMc∘dsMc≡id σβ = refl
  
  cpsMc∘dsMc≡id : (σ : CPS.Mc) → cpsMc (dsMc σ) ≡ σ
  cpsMc∘dsMc≡id CPS.[] = refl
  cpsMc∘dsMc≡id ((τ CPS.⇒ σα ⇒ α) CPS.∷ σβ)
    rewrite cpsT∘dsT≡id τ
          | cpsT∘dsT≡id α
          | cpsMc∘dsMc≡id σα
          | cpsMc∘dsMc≡id σβ = refl

{-# REWRITE cpsT∘dsT≡id #-}
{-# REWRITE cpsMc∘dsMc≡id #-}

cps-id∘ds-id≡id : {τ τ' : CPS.Ty} {σ : CPS.Mc} →
                  (id : CPS.id-cont-type (τ CPS.⇒ σ ⇒ τ')) →
                  cps-id-cont-type (ds-id-cont-type id) ≡ id
cps-id∘ds-id≡id {σ = CPS.[]} refl = refl
cps-id∘ds-id≡id {σ = (τ₁ CPS.⇒ σ₁ ⇒ τ₂) CPS.∷ σ₂} (refl , refl , refl) = refl

{-# REWRITE cps-id∘ds-id≡id #-}


-- DS <-> CPS type translations (dsT ∘ cpsT)
mutual
  dsT∘cpsT≡id : (τ : DS.Ty) → dsT (cpsT τ) ≡ τ
  dsT∘cpsT≡id DS.Nat = refl
  dsT∘cpsT≡id DS.Bol = refl
  dsT∘cpsT≡id (τ₂ DS.⇒ τ₁ ⟨ σα ⟩ α ⟨ σβ ⟩ β)
    rewrite dsT∘cpsT≡id τ₁
          | dsT∘cpsT≡id τ₂
          | dsT∘cpsT≡id α
          | dsT∘cpsT≡id β
          | dsMc∘cpsMc≡id σα
          | dsMc∘cpsMc≡id σβ = refl

  dsMc∘cpsMc≡id : (σ : DS.Mc) → dsMc (cpsMc σ) ≡ σ
  dsMc∘cpsMc≡id DS.• = refl
  dsMc∘cpsMc≡id (τ DS.⇨⟨ σα ⟩ α ∷ σβ)
    rewrite dsT∘cpsT≡id τ
          | dsT∘cpsT≡id α
          | dsMc∘cpsMc≡id σα
          | dsMc∘cpsMc≡id σβ = refl

{-# REWRITE dsT∘cpsT≡id #-}
{-# REWRITE dsMc∘cpsMc≡id #-}

ds-id∘cps-id≡id : {τ τ' : DS.Ty} {σ : DS.Mc} →
                  (id : DS.id-cont-type τ σ τ') →
                  ds-id-cont-type (cps-id-cont-type id) ≡ id
ds-id∘cps-id≡id {σ = DS.•} refl = refl
ds-id∘cps-id≡id {σ = τ₁ DS.⇨⟨ σ₁ ⟩ τ₂ ∷ σ₂} (refl , refl , refl) = refl

{-# REWRITE ds-id∘cps-id≡id #-}