module univTypes.SubjectReduction.SubjectReduction where

open import Data.Product renaming (_,_ to ⟨_,_⟩)
open import Data.Sum
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; cong; cong₂; module ≡-Reasoning)
open import Data.Fin using (zero; suc) renaming (Fin to 𝔽)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥; ⊥-elim)

open import univTypes.Util.Fin using (zero; suc)
open import univTypes.SubjectReduction.Specification
open import univTypes.SubjectReduction.Inversion using (invert-⊢λ; invert-⊢,; invert-⊢refl)
open import univTypes.SubjectReduction.SubstitutionPreservesTyping using (⊢sub; ⊢sub₁)
open import univTypes.SubjectReduction.ConversionProperties using (≈-sym; ≈σ-sub; ≈σ-sub₁; ≈→≈σ; ↪→≈; ≈-Γ-⊢₁; ≈-trans; ≈-sub; ≈-ren; ≈-refl)

-- Subject Reduction

type-two : ∀ {n} {Γ : Context n} {e : Term n}  {x t}
  → Γ ⊢ e ⦂ ∀[x⦂ x ] t
  → Term _
type-two {t = t} _ = t

subject-reduction : ∀ {n} {Γ : Context n} {e e' t : Term n}
  → Γ ⊢ e ⦂ t
  → e ↪ e'
    ----------
  → Γ ⊢ e' ⦂ t
subject-reduction (⊢-≈ t≈t ⊢e) e↪e' = ⊢-≈ t≈t (subject-reduction ⊢e e↪e')
subject-reduction (⊢-λ ⊢e₁ ⊢e₂) (ξ-λ e₁↪e₁')  = ⊢-λ ⊢e₁ (subject-reduction ⊢e₂ e₁↪e₁')
subject-reduction (⊢-· ⊢e₁ ⊢e₂) (ξ-·₁ e₁↪e₁') = ⊢-· (subject-reduction ⊢e₁ e₁↪e₁') ⊢e₂
subject-reduction (⊢-· ⊢e₁ ⊢e₂) (ξ-·₂ e₂↪e₂') = 
    ⊢-≈ (≈-sym (≈σ-sub {e = type-two ⊢e₁} (≈→≈σ (↪→≈ e₂↪e₂')))) (⊢-· ⊢e₁ (subject-reduction ⊢e₂ e₂↪e₂'))
subject-reduction (⊢-∀ ⊢t ⊢e) (ξ-∀₁ t↪t')     = 
    ⊢-∀ (subject-reduction ⊢t t↪t') (≈-Γ-⊢₁ (↪→≈ t↪t') ⊢e)
subject-reduction (⊢-∀ ⊢e₁ ⊢e₂) (ξ-∀₂ e₁↪e₁') = ⊢-∀ ⊢e₁ (subject-reduction ⊢e₂ e₁↪e₁')
subject-reduction (⊢-· ⊢e₁ ⊢e₂) β-λ with invert-⊢λ ⊢e₁
... | ⟨ t₁' , ⟨ t₂' , ⟨ lvl , ⟨ t₁≈t₁' , ⟨ t₂≈t₂' , ⟨ ⊢t₁' , Γ,t₁'⊢e₁⦂t₂' ⟩ ⟩ ⟩ ⟩ ⟩ ⟩
      = ⊢sub (⊢sub₁ (⊢-≈ t₁≈t₁' ⊢e₂)) ⊢e₁⦂t₂
  where
    ⊢e₁⦂t₂ = ⊢-≈ (≈-sym t₂≈t₂') Γ,t₁'⊢e₁⦂t₂'
subject-reduction (⊢-` x x₁) ()
subject-reduction (⊢-∃ ⊢t₁ t₁⊢t₂) (ξ-∃₁ t₁↪t₁') 
  = ⊢-∃ (subject-reduction ⊢t₁ t₁↪t₁') (≈-Γ-⊢₁ (↪→≈ t₁↪t₁') t₁⊢t₂)
subject-reduction (⊢-∃ ⊢e ⊢e₁) (ξ-∃₂ e↪e') = ⊢-∃ ⊢e (subject-reduction ⊢e₁ e↪e')
subject-reduction (⊢-, {t₂ = t₂} ⊢l ⊢r) (ξ-,₁ l↪l') 
  = ⊢-, (subject-reduction ⊢l l↪l') 
    (⊢-≈ (≈σ-sub₁ {e = t₂} (↪→≈ l↪l')) ⊢r)
-- t₂ [ e₁ ] ≈ t₂ [ e₁' ]
subject-reduction (⊢-, ⊢l ⊢r) (ξ-,₂ r↪r') = ⊢-, ⊢l (subject-reduction ⊢r r↪r')
subject-reduction (⊢-proj₁ ⊢e) β-proj₁ with invert-⊢, ⊢e
... | ⟨ t₁ , ⟨ t₂ , ⟨ t≈t₁ , ⟨ t₃≈t₂ , ⟨ ⊢e' , ⊢e₂ ⟩ ⟩ ⟩ ⟩ ⟩
  = ⊢e'
subject-reduction (⊢-proj₁ ⊢e) (ξ-proj₁ e↪e') = ⊢-proj₁ (subject-reduction ⊢e e↪e')
subject-reduction (⊢-proj₂ {t₂ = t'} ⊢e) β-proj₂ with invert-⊢, ⊢e
... | ⟨ t₁ , ⟨ t₂ , ⟨ t≈t₁ , ⟨ t₃≈t₂ , ⟨ ⊢e' , ⊢e₂ ⟩ ⟩ ⟩ ⟩ ⟩
  = ⊢-≈ (≈σ-sub₁ {e = t'} (mk-≈ _ ↪*-refl (↪*-step β-proj₁ ↪*-refl))) ⊢e₂
subject-reduction (⊢-proj₂ {e = e} {t₂ = t₂} ⊢e) (ξ-proj₂ e↪e')
  = ⊢-≈ (≈-sym (≈σ-sub {e = t₂} (≈→≈σ (↪→≈ (ξ-proj₁ e↪e'))))) (⊢-proj₂ (subject-reduction ⊢e e↪e')) 
subject-reduction (⊢-≡ ⊢e ⊢e₁) (ξ-≡₁ e↪e') = ⊢-≡ (subject-reduction ⊢e e↪e') ⊢e₁
subject-reduction (⊢-≡ ⊢e ⊢e₁) (ξ-≡₂ e↪e') = ⊢-≡ ⊢e (subject-reduction ⊢e₁ e↪e')
subject-reduction (⊢-refl ⊢e) ()
subject-reduction (⊢-subst {t = t} ⊢t ⊢u₁ ⊢u₂ ⊢≈ ⊢t[u₁]) β-subst with invert-⊢refl ⊢≈ 
... | u₁≈u₂
    = ⊢-≈ (≈σ-sub₁ {e = t} u₁≈u₂) ⊢t[u₁]
subject-reduction (⊢-subst {u₁ = u₁} {u₂ = u₂} ⊢t ⊢u₁ ⊢u₂ ⊢≈ ⊢t[u₁]) (ξ-subst₁ t↪t') 
  = ⊢-≈ (≈-sym (≈-sub (0↦ u₂) (↪→≈ t↪t'))) (⊢-subst (subject-reduction ⊢t t↪t') ⊢u₁ ⊢u₂ ⊢≈ (⊢-≈ (≈-sub (0↦ u₁) (↪→≈ t↪t')) ⊢t[u₁]))
subject-reduction (⊢-subst ⊢e ⊢e₁ ⊢e₂ ⊢e₃ ⊢e₄) (ξ-subst₂ e↪e') = ⊢-subst ⊢e ⊢e₁ ⊢e₂ (subject-reduction ⊢e₃ e↪e') ⊢e₄
subject-reduction (⊢-subst ⊢e ⊢e₁ ⊢e₂ ⊢e₃ ⊢e₄) (ξ-subst₃ e↪e') = ⊢-subst ⊢e ⊢e₁ ⊢e₂ ⊢e₃ (subject-reduction ⊢e₄ e↪e')
subject-reduction (⊢-lsuc a) (ξ-lsuc l↪l') = ⊢-lsuc (subject-reduction a l↪l')
subject-reduction (⊢-⊔ a a₁) (ξ-⊔₁ l↪l') = ⊢-⊔ (subject-reduction a l↪l') a₁
subject-reduction (⊢-⊔ a a₁) (ξ-⊔₂ l↪l') = ⊢-⊔ a (subject-reduction a₁ l↪l')
subject-reduction ⊢-Setn (ξ-Setn l↪l') = ⊢-≈ (mk-≈ (`Setn `lsuc _)   ↪*-refl (↪*-step (ξ-Setn (ξ-lsuc l↪l')) ↪*-refl) ) ⊢-Setn
subject-reduction ⊢-Setω (ξ-Setω l↪l') = ⊢-≈ (mk-≈ (`Setω `lsuc _)   ↪*-refl (↪*-step (ξ-Setω (ξ-lsuc l↪l')) ↪*-refl) ) ⊢-Setω