{-# OPTIONS --rewriting #-}

module A201801.STLCStandardDerivations where

open import A201801.Prelude
open import A201801.Category
open import A201801.Fin
open import A201801.Vec
open import A201801.VecLemmas
open import A201801.AllVec
open import A201801.STLCTypes
open import A201801.STLCStandardTerms


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


infix  ⊢_⦂_valid[_]
data ⊢_⦂_valid[_] : ∀ {g} → Term g → Type → Types g → Set
  where
    var : ∀ {A g I} → {Γ : Types g}
                    → Γ ∋⟨ I ⟩ A
                    → ⊢ VAR I ⦂ A valid[ Γ ]

    lam : ∀ {A B g M} → {Γ : Types g}
                      → ⊢ M ⦂ B valid[ Γ , A ]
                      → ⊢ LAM M ⦂ A ⊃ B valid[ Γ ]

    app : ∀ {A B g M N} → {Γ : Types g}
                        → ⊢ M ⦂ A ⊃ B valid[ Γ ] → ⊢ N ⦂ A valid[ Γ ]
                        → ⊢ APP M N ⦂ B valid[ Γ ]


infix  ⊢_⦂_allvalid[_]
⊢_⦂_allvalid[_] : ∀ {g n} → Terms g n → Types n → Types g → Set
⊢ τ ⦂ Ξ allvalid[ Γ ] = All (\ { (M , A) → ⊢ M ⦂ A valid[ Γ ] }) (zip τ Ξ)


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


ren : ∀ {g g′ e M A} → {Γ : Types g} {Γ′ : Types g′}
                     → Γ′ ⊇⟨ e ⟩ Γ → ⊢ M ⦂ A valid[ Γ ]
                     → ⊢ REN e M ⦂ A valid[ Γ′ ]
ren η (var i)   = var (ren∋ η i)
ren η (lam 𝒟)   = lam (ren (keep η) 𝒟)
ren η (app 𝒟 ℰ) = app (ren η 𝒟) (ren η ℰ)


rens : ∀ {g g′ e n} → {Γ : Types g} {Γ′ : Types g′}
                       {τ : Terms g n} {Ξ : Types n}
                    → Γ′ ⊇⟨ e ⟩ Γ → ⊢ τ ⦂ Ξ allvalid[ Γ ]
                    → ⊢ RENS e τ ⦂ Ξ allvalid[ Γ′ ]
rens {τ = ∙}     {∙}     η ∙       = ∙
rens {τ = τ , M} {Ξ , A} η (ξ , 𝒟) = rens η ξ , ren η 𝒟


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


wk : ∀ {B g M A} → {Γ : Types g}
                 → ⊢ M ⦂ A valid[ Γ ]
                 → ⊢ WK M ⦂ A valid[ Γ , B ]
wk 𝒟 = ren (drop id⊇) 𝒟


wks : ∀ {g n A} → {Γ : Types g} {τ : Terms g n} {Ξ : Types n}
                → ⊢ τ ⦂ Ξ allvalid[ Γ ]
                → ⊢ WKS τ ⦂ Ξ allvalid[ Γ , A ]
wks ξ = rens (drop id⊇) ξ


vz : ∀ {g A} → {Γ : Types g}
             → ⊢ VZ ⦂ A valid[ Γ , A ]
vz = var zero


lifts : ∀ {g n A} → {Γ : Types g} {τ : Terms g n} {Ξ : Types n}
                  → ⊢ τ ⦂ Ξ allvalid[ Γ ]
                  → ⊢ LIFTS τ ⦂ Ξ , A allvalid[ Γ , A ]
lifts ξ = wks ξ , vz


vars : ∀ {g g′ e} → {Γ : Types g} {Γ′ : Types g′}
                  → Γ′ ⊇⟨ e ⟩ Γ
                  → ⊢ VARS e ⦂ Γ allvalid[ Γ′ ]
vars done     = ∙
vars (drop η) = wks (vars η)
vars (keep η) = lifts (vars η)


ids : ∀ {g} → {Γ : Types g}
            → ⊢ IDS ⦂ Γ allvalid[ Γ ]
ids = vars id⊇


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


sub : ∀ {g n M A} → {Γ : Types g} {τ : Terms g n} {Ξ : Types n}
                  → ⊢ τ ⦂ Ξ allvalid[ Γ ] → ⊢ M ⦂ A valid[ Ξ ]
                  → ⊢ SUB τ M ⦂ A valid[ Γ ]
sub ξ (var i)   = get ξ (zip∋₂ i)
sub ξ (lam 𝒟)   = lam (sub (lifts ξ) 𝒟)
sub ξ (app 𝒟 ℰ) = app (sub ξ 𝒟) (sub ξ ℰ)


subs : ∀ {g n m} → {Γ : Types g} {τ : Terms g n} {Ξ : Types n}
                    {υ : Terms n m}  {Ψ : Types m}
                 → ⊢ τ ⦂ Ξ allvalid[ Γ ] → ⊢ υ ⦂ Ψ allvalid[ Ξ ]
                 → ⊢ SUBS τ υ ⦂ Ψ allvalid[ Γ ]
subs {υ = ∙}     {∙}     ξ ∙       = ∙
subs {υ = υ , M} {Ψ , A} ξ (ψ , 𝒟) = subs ξ ψ , sub ξ 𝒟


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


unlam : ∀ {g M A B} → {Γ : Types g}
                    → ⊢ M ⦂ A ⊃ B valid[ Γ ]
                    → ⊢ UNLAM M ⦂ B valid[ Γ , A ]
unlam 𝒟 = app (wk 𝒟) vz


cut : ∀ {g M N A B} → {Γ : Types g}
                    → ⊢ M ⦂ A valid[ Γ ] → ⊢ N ⦂ B valid[ Γ , A ]
                    → ⊢ CUT M N ⦂ B valid[ Γ ]
cut 𝒟 ℰ = sub (ids , 𝒟) ℰ


pseudocut : ∀ {g M N A B} → {Γ : Types g}
                          → ⊢ M ⦂ A valid[ Γ ] → ⊢ N ⦂ B valid[ Γ , A ]
                          → ⊢ PSEUDOCUT M N ⦂ B valid[ Γ ]
pseudocut 𝒟 ℰ = app (lam ℰ) 𝒟


pseudosub : ∀ {g n M A} → {Γ : Types g} {τ : Terms g n} {Ξ : Types n}
                        → ⊢ τ ⦂ Ξ allvalid[ Γ ] → ⊢ M ⦂ A valid[ Ξ ]
                        → ⊢ PSEUDOSUB τ M ⦂ A valid[ Γ ]
pseudosub {τ = ∙}     {∙}     ∙       𝒟 = ren bot⊇ 𝒟
pseudosub {τ = τ , M} {Ξ , B} (ξ , 𝒞) 𝒟 = app (pseudosub ξ (lam 𝒟)) 𝒞


exch : ∀ {g M A B C} → {Γ : Types g}
                     → ⊢ M ⦂ C valid[ (Γ , A) , B ]
                     → ⊢ EXCH M ⦂ C valid[ (Γ , B) , A ]
exch 𝒟 = app (app (wk (wk (lam (lam 𝒟)))) vz) (wk vz)


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