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

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

open import CtxArr2.Context
open import CtxArr2.Term
open import CtxArr2.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 ⟩

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 ∅ ⟩))))