module stlc.properities where

open import stlc.term

_+++_ : Context → Context → Context
Γ +++ ∅ = Γ
Γ +++ (Δ , A) = (Γ +++ Δ) , A

weaken∋ : ∀ {Γ Γ' A B} → Γ +++ Γ' ∋ B → (Γ , A) +++ Γ' ∋ B
weaken∋ {Γ' = ∅} Z = S Z
weaken∋ {Γ' = ∅} (S x) = S (S x)
weaken∋ {Γ' = Γ' , x₁} Z = Z
weaken∋ {Γ' = Γ' , x₁} (S x) = S weaken∋ x

weaken : ∀ {Γ Γ' A B} → Γ +++ Γ' ⊢ B → (Γ , A) +++ Γ' ⊢ B
weaken ⟨⟩ = ⟨⟩
weaken (` x) = ` (weaken∋ x)
weaken (x , x₁) = weaken x , weaken x₁
weaken (fst x) = fst (weaken x)
weaken (snd x) = snd (weaken x)
weaken {Γ' = Γ'} (ƛ_ {A = A} x) = ƛ weaken {Γ' = Γ' , A} x
weaken (x · x₁) = weaken x · weaken x₁
weaken (`nat x) = `nat x
weaken (inl x) = inl weaken x
weaken (inr x) = inr weaken x
weaken {Γ' = Γ'} (case_inl_inr_ {A = A} {B} x x₁ x₂) = case weaken x inl weaken {Γ' = Γ' , A} x₁ inr weaken {Γ' = Γ' , B} x₂
weaken [] = []
weaken (h ⦂ t) = weaken h ⦂ weaken t
weaken {Γ} (it x r l) = it (weaken x) (weaken {Γ} r) (weaken l)
weaken {Γ} (`let_`in_ {s = s} x x₁) = `let_`in_ {s = s} (weaken x) (weaken {Γ} x₁)
weaken (return {m = m} x) = return {m = m} (weaken x)

exchange∋ : ∀ {Γ Γ' A B C} → (Γ , A , B) +++ Γ' ∋ C → (Γ , B , A) +++ Γ' ∋ C
exchange∋ {Γ' = ∅} Z = S Z
exchange∋ {Γ} {Γ' = ∅} (S x) = weaken∋ {Γ} x
exchange∋ {Γ' = Γ' , x₁} Z = Z
exchange∋ {Γ' = Γ' , x₁} (S x) = S exchange∋ x

exchange : ∀ {Γ Γ' A B C} → (Γ , A , B) +++ Γ' ⊢ C → (Γ , B , A) +++ Γ' ⊢ C
exchange ⟨⟩ = ⟨⟩
exchange (` x) = ` (exchange∋ x)
exchange (x , x₁) = exchange x , exchange x₁
exchange (fst x) = fst (exchange x)
exchange (snd x) = snd (exchange x)
exchange {Γ' = Γ'} (ƛ_ {A = A} x) = ƛ exchange {Γ' = Γ' , A} x
exchange (x · x₁) = exchange x · exchange x₁
exchange (`nat x) = `nat x
exchange (inl x) = inl exchange x
exchange (inr x) = inr exchange x
exchange {Γ' = Γ'} (case_inl_inr_ {A = A} {B} x x₁ x₂) = case exchange x inl exchange {Γ' = Γ' , A} x₁ inr exchange {Γ' = Γ' , B} x₂
exchange [] = []
exchange (h ⦂ t) = exchange h ⦂ exchange t
exchange {Γ' = Γ'} {C = C} (it {A = A} x r l) = it (exchange x) (exchange {Γ' = Γ' , (A × C)} r) (exchange l)
exchange {Γ} {Γ'} (`let_`in_ {A = A} {s = s} x x₁) = `let_`in_ {s = s} (exchange x) (exchange {Γ' = Γ' , A} x₁)
exchange (return {m = m} x) = return {m = m} (exchange x)