{-# OPTIONS --safe #-}
module CtxTyp.Examples where

open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)
open import Data.Nat.Base using (ℕ; zero; suc; _≥‴_; ≤‴-refl; ≤‴-step)
open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂)
open import Function.Base using (id; _∘_)

open import CtxTyp.Context
open import CtxTyp.Term
open import CtxTyp.Reduction

iterate : {A : Set} → ℕ → (A → A) → A → A
iterate zero f x = x
iterate (suc n) f x = f (iterate n f x)

step : Term  ∅ A → Term  ∅ A
step e with progress e
... | p-step {e′ = e′} _ = e′
... | p-value (`λ⟨ Δ ⟩ e) = `λ⟨ Δ ⟩ e
... | p-value `true = `true
... | p-value `false = `false
... | p-value ⟨ e ⟩ = ⟨ e ⟩
... | p-value (`wrap Δ e ve) = `wrap Δ e

eval : Term  ∅ A → Term  ∅ A
eval = iterate  step

test₁ : eval (`if `true `then `true `else `false) ≡ `true
test₁ = refl

test₂ : eval (`let⟨ ∅ ⟩ ⟨ `true ⟩ ⟨ `if (` Z `with ∅) `then `true `else `false ⟩) ≡ ⟨ `if `true `then `true `else `false ⟩
test₂ = refl

-- let < x : [z : Bool |- Bool] . y > = (let < z > = <true> in < x with (z ↦ z) >) in <true> --> <true>
test₃ : eval (`let⟨ ∅ ,[ (∅ , `Bool ^ ) ⊢ `Bool ^ ≤‴-refl ] ⟩ (`let⟨  ∅ ⟩ ⟨ `true ⟩ ⟨ ` S Z `with (∅ , var Z) ⟩) ⟨ `true ⟩) ≡ ⟨ `true ⟩
test₃ = refl

test₄ : eval (`let⟨ ∅ ,[ (∅ , `Bool ^ ) ⊢ `Bool ^ ≤‴-refl ] ⟩ (`let⟨ ∅ ⟩ ⟨ `true ⟩ ⟨ ` S Z `with (∅ , var Z) ⟩) (`let⟨ ∅ , `Bool ^  ⟩ ⟨ `if ` Z `with ∅ `then `true `else `false ⟩ (`let⟨ ∅ ⟩ ⟨ `false ⟩ ⟨ ` S (S Z) `with (∅ , var (S Z))⟩))) ≡ ⟨ `if `true `then `true `else `false ⟩
test₄ = refl

-- let < x : Bool, y > = < if x then true else false > in (let <z> = < true > in < y with x ↦ z >)
test₅ : eval (`let⟨ ∅ , `Bool ^  ⟩ ⟨ `if (` Z `with ∅) `then `true `else `false ⟩ (`let⟨ ∅ ⟩ ⟨ `true ⟩ ⟨ ` S Z `with (∅ , var Z)  ⟩)) ≡ ⟨ `if `true `then `true `else `false ⟩
test₅ = refl

`aif : ∅ ⊢ [ ∅ ⊢ ◯ `Bool ]⇒ ([ ∅ , `Bool ^  ⊢ ◯ `Bool ]⇒ ([ ∅ , `Bool ^  ⊢ ◯ `Bool ]⇒ ◯ `Bool)) ^ 
`aif = `λ⟨ ∅ ⟩ (`λ⟨ ∅ , `Bool ^  ⟩ (`λ⟨ ∅ , `Bool ^  ⟩ 
  `let⟨ ∅ ⟩ (` S (S Z) `with ∅)
  (`let⟨ ∅ , `Bool ^  ⟩ (` S (S (S Z)) `with (∅ , var Z))
  (`let⟨ ∅ , `Bool ^  ⟩ (` S (S (S Z)) `with (∅ , var Z))
    ⟨ (`λ⟨ ∅ ⟩ `if (` Z `with ∅) `then ` S (S Z) `with (∅ , var Z) `else ` S Z `with (∅ , var Z)) · ` S (S Z) `with ∅ ⟩))))

`wrap-to-arr : ∅ , (Δ ▷ A) ⇒ B  ^ n ⊢ [ Δ ⊢ A ]⇒ B ^ n
`wrap-to-arr {Δ = Δ} = `λ⟨ Δ ⟩ ` S Z `with ∅ · `wrap Δ (` (∋-++⁺ˡ (inject₁ Δ) Z) `with lift (∋-++⁺ʳ _))

`arr-to-wrap : ∅ , [ Δ ⊢ A ]⇒ B ^ n ⊢ Δ ▷ A ⇒ B ^ n
`arr-to-wrap {Δ = Δ} = `λ⟨ ∅ ⟩ ` S Z `with ∅ · `letwrap Δ (` (∋-++⁺ˡ (inject₁ Δ) Z) `with ∅) (` Z `with lift (S ∘ ∋-++⁺ʳ _))

-- i.e. pushCirc
◯▷⇒▷◯ : ∀ Δ → ∅ , ◯ (Δ ▷ A) ^ n ⊢ inject₁ Δ ▷ ◯ A ^ n
◯▷⇒▷◯ Δ = `let⟨ ∅ ⟩ (` Z `with ∅) (`wrap (inject₁ Δ) ⟨ `letwrap Δ (` ∋-castˡ (sym (++-inject₁-↾ (inject₁ Δ))) ((∋-++⁺ˡ (inject₁ Δ) Z)) `with ∅) (` Z `with lift (S ∘ ∋-castˡ (sym (++-inject₁-↾ (inject₁ Δ))) ∘ (∋-++⁺ʳ _))) ⟩)

-- i.e. pullCirc
▷◯⇒◯▷ : ∀ Δ → ∅ , inject₁ Δ ▷ ◯ A ^ n ⊢ ◯ (Δ ▷ A) ^ n
▷◯⇒◯▷ Δ = `letwrap (inject₁ Δ) (` Z `with ∅) (`let⟨ inject₁ Δ ⟩ (` (∋-++⁺ˡ (inject₁ (inject₁ Δ)) Z) `with lift (∋-++⁺ʳ _)) ⟨ `wrap Δ (` ∋-++⁺ˡ (inject₁ Δ) Z `with lift (∋-++⁺ʳ _)  ) ⟩ )

subst-to-arr : (σ : Subst (inject₁ Γ) (inject₁ Γ′)) → ∅ ⊢ [ Γ ⊢ A ]⇒ (Γ′ ▷ A) ^ n
subst-to-arr {Γ = Γ} {Γ′ = Γ′} σ = `λ⟨ Γ ⟩ `wrap Γ′ (` ∋-++⁺ˡ _ Z `with renameSubst (∋-++⁺ʳ _) σ)

`letΔwrap-admissable : ∀ Δ
    → (e₁ : Γ ++ inject₁ Δ ⊢ Δ′ ▷ A ^ n)
    → (e₂ : Γ ,[ inject₁ Δ ++ inject₁ Δ′ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n)
      --------------------------------------
    → Γ ⊢ B ^ n
`letΔwrap-admissable {Δ′ = Δ′} Δ e₁ e₂ =
  `letwrap (Δ ++ Δ′)
    (`wrap (Δ ++ Δ′)
      (`letwrap Δ′
        (rename ρ₁ e₁)
        (` Z `with lift (S ∘ ρ₂))))
    (rename ρ₃ e₂)
  where
  ρ₁ : Rename (Γ ++ inject₁ Δ) (Γ ++ inject₁ (Δ ++ Δ′))
  ρ₁ x with ∋-++⁻ (inject₁ Δ) x
  ... | inj₁ xΓ = ∋-++⁺ˡ _ xΓ
  ... | inj₂ xΔ rewrite inject₁-++ {xs = Δ} Δ′ = ∋-++⁺ʳ _ (∋-++⁺ˡ (inject₁ Δ′) xΔ)
  ρ₂ : Rename (inject₁ Δ′) (Γ ++ inject₁ (Δ ++ Δ′))
  ρ₂ x rewrite inject₁-++ {xs = Δ} Δ′ = ∋-++⁺ʳ _ (∋-++⁺ʳ (inject₁ Δ) x)
  ρ₃ : Rename (Γ ,[ inject₁ Δ ++ inject₁ Δ′ ⊢ A ^ ≤‴-refl ]) (Γ ,[ inject₁ (Δ ++ Δ′) ⊢ A ^ ≤‴-refl ])
  ρ₃ x rewrite inject₁-++ {xs = Δ} Δ′ = x