{-# OPTIONS --safe #-}
module Core.Examples where
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Nat.Base using (ℕ; zero; suc; _≥‴_; ≤‴-refl; ≤‴-step)
open import Core.Context
open import Core.Term
open import Core.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 0 ∅ A → Term 0 ∅ 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 0 ∅ A → Term 0 ∅ A
eval = iterate 1000 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
test₃ : eval (`let⟨ ∅ ,[ (∅ , `Bool ^ 1) ⊢ `Bool ^ ≤‴-refl ] ⟩ (`let⟨ ∅ ⟩ ⟨ `true ⟩ ⟨ ` S Z `with (∅ , var Z) ⟩) ⟨ `true ⟩) ≡ ⟨ `true ⟩
test₃ = refl
test₄ : eval (`let⟨ ∅ ,[ (∅ , `Bool ^ 1) ⊢ `Bool ^ ≤‴-refl ] ⟩ (`let⟨ ∅ ⟩ ⟨ `true ⟩ ⟨ ` S Z `with (∅ , var Z) ⟩) (`let⟨ ∅ , `Bool ^ 1 ⟩ ⟨ `if ` Z `with ∅ `then `true `else `false ⟩ (`let⟨ ∅ ⟩ ⟨ `false ⟩ ⟨ ` S (S Z) `with (∅ , var (S Z))⟩))) ≡ ⟨ `if `true `then `true `else `false ⟩
test₄ = refl
test₅ : eval (`let⟨ ∅ , `Bool ^ 1 ⟩ ⟨ `if (` Z `with ∅) `then `true `else `false ⟩ (`let⟨ ∅ ⟩ ⟨ `true ⟩ ⟨ ` S Z `with (∅ , var Z) ⟩)) ≡ ⟨ `if `true `then `true `else `false ⟩
test₅ = refl