{-# OPTIONS --rewriting #-}

module A201801.CMLStandardBidirectionalDerivations-NormalNeutral where

open import A201801.Prelude
open import A201801.Category
open import A201801.List
open import A201801.ListLemmas
open import A201801.AllList
open import A201801.CMLPropositions
open import A201801.CMLStandardDerivations


--------------------------------------------------------------------------------


mutual
  infix  _⊢_normal[_]
  data _⊢_normal[_] : List Assert → Form → List Form → Set
    where
      lam : ∀ {A B Δ Γ} → Δ ⊢ B normal[ Γ , A ]
                        → Δ ⊢ A ⊃ B normal[ Γ ]

      box : ∀ {A Ψ Δ Γ} → Δ ⊢ A valid[ Ψ ]
                        → Δ ⊢ [ Ψ ] A normal[ Γ ]

      letbox : ∀ {A B Ψ Δ Γ} → Δ ⊢ [ Ψ ] A neutral[ Γ ] → Δ , ⟪ Ψ ⊫ A ⟫ ⊢ B normal[ Γ ]
                             → Δ ⊢ B normal[ Γ ]

      use : ∀ {P Δ Γ} → Δ ⊢ ι P neutral[ Γ ]
                      → Δ ⊢ ι P normal[ Γ ]

  infix  _⊢_neutral[_]
  data _⊢_neutral[_] : List Assert → Form → List Form → Set
    where
      var : ∀ {A Δ Γ} → Γ ∋ A
                      → Δ ⊢ A neutral[ Γ ]

      app : ∀ {A B Δ Γ} → Δ ⊢ A ⊃ B neutral[ Γ ] → Δ ⊢ A normal[ Γ ]
                        → Δ ⊢ B neutral[ Γ ]

      mvar : ∀ {A Ψ Δ Γ} → Δ ∋ ⟪ Ψ ⊫ A ⟫ → Δ ⊢ Ψ allnormal[ Γ ]
                         → Δ ⊢ A neutral[ Γ ]

  infix  _⊢_allnormal[_]
  _⊢_allnormal[_] : List Assert → List Form → List Form → Set
  Δ ⊢ Ξ allnormal[ Γ ] = All (\ A → Δ ⊢ A normal[ Γ ]) Ξ


--------------------------------------------------------------------------------


mutual
  renₗ : ∀ {Δ Γ Γ′ A} → Γ′ ⊇ Γ → Δ ⊢ A normal[ Γ ]
                      → Δ ⊢ A normal[ Γ′ ]
  renₗ η (lam 𝒟)      = lam (renₗ (keep η) 𝒟)
  renₗ η (box 𝒟)      = box 𝒟
  renₗ η (letbox 𝒟 ℰ) = letbox (renᵣ η 𝒟) (renₗ η ℰ)
  renₗ η (use 𝒟)      = use (renᵣ η 𝒟)

  rensₗ : ∀ {Δ Γ Γ′ Ξ} → Γ′ ⊇ Γ → Δ ⊢ Ξ allnormal[ Γ ]
                       → Δ ⊢ Ξ allnormal[ Γ′ ]
  rensₗ η ∙       = ∙
  rensₗ η (ξ , 𝒟) = rensₗ η ξ , renₗ η 𝒟

  renᵣ : ∀ {Δ Γ Γ′ A} → Γ′ ⊇ Γ → Δ ⊢ A neutral[ Γ ]
                      → Δ ⊢ A neutral[ Γ′ ]
  renᵣ η (var i)    = var (ren∋ η i)
  renᵣ η (app 𝒟 ℰ)  = app (renᵣ η 𝒟) (renₗ η ℰ)
  renᵣ η (mvar i ψ) = mvar i (rensₗ η ψ)


wkᵣ : ∀ {B Δ Γ A} → Δ ⊢ A neutral[ Γ ]
                  → Δ ⊢ A neutral[ Γ , B ]
wkᵣ 𝒟 = renᵣ (drop id⊇) 𝒟


vzᵣ : ∀ {Δ Γ A} → Δ ⊢ A neutral[ Γ , A ]
vzᵣ = var zero


--------------------------------------------------------------------------------


mutual
  mrenₗ : ∀ {Δ Δ′ Γ A} → Δ′ ⊇ Δ → Δ ⊢ A normal[ Γ ]
                       → Δ′ ⊢ A normal[ Γ ]
  mrenₗ η (lam 𝒟)      = lam (mrenₗ η 𝒟)
  mrenₗ η (box 𝒟)      = box (mren η 𝒟)
  mrenₗ η (letbox 𝒟 ℰ) = letbox (mrenᵣ η 𝒟) (mrenₗ (keep η) ℰ)
  mrenₗ η (use 𝒟)      = use (mrenᵣ η 𝒟)

  mrensₗ : ∀ {Δ Δ′ Γ Ξ} → Δ′ ⊇ Δ → Δ ⊢ Ξ allnormal[ Γ ]
                        → Δ′ ⊢ Ξ allnormal[ Γ ]
  mrensₗ η ∙       = ∙
  mrensₗ η (ξ , 𝒟) = mrensₗ η ξ , mrenₗ η 𝒟

  mrenᵣ : ∀ {Δ Δ′ Γ A} → Δ′ ⊇ Δ → Δ ⊢ A neutral[ Γ ]
                       → Δ′ ⊢ A neutral[ Γ ]
  mrenᵣ η (var i)    = var i
  mrenᵣ η (app 𝒟 ℰ)  = app (mrenᵣ η 𝒟) (mrenₗ η ℰ)
  mrenᵣ η (mvar i ψ) = mvar (ren∋ η i) (mrensₗ η ψ)


mwkₗ : ∀ {B Δ Γ A} → Δ ⊢ A normal[ Γ ]
                   → Δ , B ⊢ A normal[ Γ ]
mwkₗ 𝒟 = mrenₗ (drop id⊇) 𝒟


mwksₗ : ∀ {A Δ Γ Ξ} → Δ ⊢ Ξ allnormal[ Γ ]
                    → Δ , A ⊢ Ξ allnormal[ Γ ]
mwksₗ ξ = maps mwkₗ ξ


mwkᵣ : ∀ {B Δ Γ A} → Δ ⊢ A neutral[ Γ ]
                   → Δ , B ⊢ A neutral[ Γ ]
mwkᵣ 𝒟 = mrenᵣ (drop id⊇) 𝒟


mvzᵣ : ∀ {Δ Γ Ψ A} → Δ ⊢ Ψ allnormal[ Γ ]
                   → Δ , ⟪ Ψ ⊫ A ⟫ ⊢ A neutral[ Γ ]
mvzᵣ ψ = mvar zero (mwksₗ ψ)


xmvzᵣ : ∀ {Δ Δ′ Γ Ψ A} → Δ′ ⊇ Δ , ⟪ Ψ ⊫ A ⟫ → Δ′ ⊢ Ψ allnormal[ Γ ]
                       → Δ′ ⊢ A neutral[ Γ ]
xmvzᵣ η ψ = mvar (ren∋ η zero) ψ


--------------------------------------------------------------------------------


mutual
  denmₗ : ∀ {Δ Γ A} → Δ ⊢ A normal[ Γ ]
                    → Δ ⊢ A valid[ Γ ]
  denmₗ (lam 𝒟)      = lam (denmₗ 𝒟)
  denmₗ (box 𝒟)      = box 𝒟
  denmₗ (letbox 𝒟 ℰ) = letbox (denmᵣ 𝒟) (denmₗ ℰ)
  denmₗ (use 𝒟)      = denmᵣ 𝒟

  denmsₗ : ∀ {Δ Γ Ξ} → Δ ⊢ Ξ allnormal[ Γ ]
                     → Δ ⊢ Ξ allvalid[ Γ ]
  denmsₗ ∙       = ∙
  denmsₗ (ξ , 𝒟) = denmsₗ ξ , denmₗ 𝒟

  denmᵣ : ∀ {Δ Γ A} → Δ ⊢ A neutral[ Γ ]
                    → Δ ⊢ A valid[ Γ ]
  denmᵣ (var i)    = var i
  denmᵣ (app 𝒟 ℰ)  = app (denmᵣ 𝒟) (denmₗ ℰ)
  denmᵣ (mvar i ψ) = mvar i (denmsₗ ψ)


--------------------------------------------------------------------------------