{-|
This module contains examples of terms and reductions in λ○▷.
-}

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

open import Data.Nat using (ℕ; zero; suc; _≥‴_; ≤‴-refl; ≤‴-step)
open import Function using (id; _∘_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)

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

-- | Apply a function to a value n times.
iterate : {A : Set} → ℕ → (A → A) → A → A
iterate zero f x = x
iterate (suc n) f x = f (iterate n f x)

-- | Run a single step of reduction.
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

-- | Evaluate a term by repeatedly applying the step function.
eval : Term  ∅ A → Term  ∅ A
eval = iterate  step

-- | (if true then true else false) evaluates to true.
test₁ : eval (`if `true `then `true `else `false) ≡ `true
test₁ = refl

-- | let$ x = <true> in < if x then true else false > evaluates to < if true then true else false >.
test₂ : eval (`let⟨ ∅ ⟩ ⟨ `true ⟩ ⟨ `if (` #  `with ∅) `then `true `else `false ⟩) ≡ ⟨ `if `true `then `true `else `false ⟩
test₂ = refl

{-|
let$ y : (x : [z : bool ⊢ bool] ⊢ bool)  =
  let$ z = <true> in < x with z = z >
in <true>

evaluates to <true>
-}
test₃ : eval (`let⟨ ∅ ,[ (∅ , `Bool ^ ) ⊢ `Bool ^ ≤‴-refl ] ⟩ (`let⟨  ∅ ⟩ ⟨ `true ⟩ ⟨ ` #  `with (∅ , var Z) ⟩) ⟨ `true ⟩) ≡ ⟨ `true ⟩
test₃ = refl

{-|
let$ y : (x : [z : bool ⊢ bool] ⊢ bool)  =
  let$ z = <true> in < x with z = z >
in
  let$ x : (z : bool ⊢ bool) = < if z then true else false > in
  let$ z = <false> in
  <y with x = x>

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

{-|
let$ y : (x : bool ⊢ bool) = <if x then true else false> in
let$ z = <true> in
<y with x = z>

evaluates to <if true then true else false>
-}
test₅ : eval (`let⟨ ∅ , `Bool ^  ⟩ ⟨ `if (` #  `with ∅) `then `true `else `false ⟩ (`let⟨ ∅ ⟩ ⟨ `true ⟩ ⟨ ` #  `with (∅ , var (# ))  ⟩)) ≡ ⟨ `if `true `then `true `else `false ⟩
test₅ = refl

-- | The aif term described in section 2.4.
`aif : ∅ ⊢ [ ∅ ⊢ ◯ `Bool ]⇒ ([ ∅ , `Bool ^  ⊢ ◯ `Bool ]⇒ ([ ∅ , `Bool ^  ⊢ ◯ `Bool ]⇒ ◯ `Bool)) ^ 
`aif = `λ⟨ ∅ ⟩ (`λ⟨ ∅ , `Bool ^  ⟩ (`λ⟨ ∅ , `Bool ^  ⟩ 
  `let⟨ ∅ ⟩ (` L (# ) `with ∅)
  (`let⟨ ∅ , `Bool ^  ⟩ (` (# ) `with (∅ , var (# )))
  (`let⟨ ∅ , `Bool ^  ⟩ (` (# ) `with (∅ , var (# )))
    ⟨ (`λ⟨ ∅ ⟩ `if (` #  `with ∅) `then ` #  `with (∅ , var (# )) `else ` #  `with (∅ , var (# ))) · ` #  `with ∅ ⟩))))

-- | The wrapToArr term described in section 3.
`wrap-to-arr : ∅ , (Δ ▷ A) ⇒ B  ^ n ⊢ [ Δ ⊢ A ]⇒ B ^ n
`wrap-to-arr {Δ = Δ} = `λ⟨ Δ ⟩ ` #  `with ∅ · `wrap Δ (` L (# ) `with lift R)

-- | The arrToWrap term described in section 3.
`arr-to-wrap : ∅ , [ Δ ⊢ A ]⇒ B ^ n ⊢ Δ ▷ A ⇒ B ^ n
`arr-to-wrap {Δ = Δ} = `λ⟨ ∅ ⟩ ` #  `with ∅ · `letwrap Δ (` L (# ) `with ∅) (` (# ) `with lift (S ∘ R))

-- | Pushing a ◯ into a ▷.
◯▷⇒▷◯ : ∀ Δ → ∅ , ◯ (Δ ▷ A) ^ n ⊢ inject₁ Δ ▷ ◯ A ^ n
◯▷⇒▷◯ Δ = `let⟨ ∅ ⟩ (` #  `with ∅) (`wrap (inject₁ Δ) ⟨ `letwrap Δ (` L (# ) `with ∅) (` #  `with lift (S ∘ R ∘ ∋-↾⁺ ∘ ∋-inject₁⁺)) ⟩)

-- | Pulling a ◯ out of a ▷.
▷◯⇒◯▷ : ∀ Δ → ∅ , inject₁ Δ ▷ ◯ A ^ n ⊢ ◯ (Δ ▷ A) ^ n
▷◯⇒◯▷ Δ = `letwrap (inject₁ Δ) (` Z `with ∅) (`let⟨ inject₁ Δ ⟩ (` L (# ) `with lift R) ⟨ `wrap Δ (` L (# )  `with lift R) ⟩ )

-- | Converting a later-stage substitution into a function between unhygienic values.
subst-to-arr : (σ : Subst (inject₁ Γ) (inject₁ Γ′)) → ∅ ⊢ [ Γ ⊢ A ]⇒ (Γ′ ▷ A) ^ n
subst-to-arr {Γ = Γ} {Γ′ = Γ′} σ = `λ⟨ Γ ⟩ `wrap Γ′ (` L (# ) `with renameSubst R σ)

{-|
A variant of the let-wrap rule that allows introducing additional dependencies
in e₁ is admissible:

Γ , Δⁿ⁺¹ ⊢ⁿ e₁ : Δ′ ▷ A
Γ , x : [ Δ, Δ′ ⊢ⁿ A ] ⊢ⁿ e₂ : B
------------------
Γ ⊢ⁿ let_Δ_wrap_Δ′ x = e₁ in e₂ : B
-}
`letΔwrap-admissible : ∀ Δ
    → (e₁ : Γ ++ inject₁ Δ ⊢ Δ′ ▷ A ^ n)
    → (e₂ : Γ ,[ inject₁ Δ ++ inject₁ Δ′ ⊢ A ^ ≤‴-refl ] ⊢ B ^ n)
      --------------------------------------
    → Γ ⊢ B ^ n
`letΔwrap-admissible {Δ′ = Δ′} Δ e₁ e₂ =
  `letwrap (Δ ++ Δ′)
    (`wrap (Δ ++ Δ′)
      (`letwrap Δ′
        (rename ρ₁ e₁)
        (` #  `with lift (S ∘ ρ₂))))
    (rename ρ₃ e₂)
  where
  ρ₁ : Rename (Γ ++ inject₁ Δ) (Γ ++ inject₁ (Δ ++ Δ′))
  ρ₁ (L x) = L x
  ρ₁ (R x) = R (L x)
  ρ₂ : Rename (inject₁ Δ′) (Γ ++ inject₁ (Δ ++ Δ′))
  ρ₂ x = R (R x)
  ρ₃ : Rename (Γ ,[ inject₁ Δ ++ inject₁ Δ′ ⊢ A ^ ≤‴-refl ]) (Γ ,[ inject₁ (Δ ++ Δ′) ⊢ A ^ ≤‴-refl ])
  ρ₃ x = x