module Ahmed.LogicalRelations where

open import Data.Empty
open import Data.Unit
open import Data.Bool
open import Data.Nat
open import Data.Fin
open import Data.Product
open import Relation.Nullary using (Dec; yes; no)

data type : Set where
  bool : type
  _-→_ : type → type → type

data ctx : Set where
  nil : ctx
  _,_ : ctx → type → ctx

data var : ctx → type → Set where
  zero : ∀ {Γ τ} → var (Γ , τ) τ
  suc : ∀ {Γ τ₁ τ₂} → var Γ τ₂ → var (Γ , τ₁) τ₂

data term : ctx → type → Set where
  true : ∀ {Γ} → term Γ bool
  false : ∀ {Γ} → term Γ bool
  `_ : ∀ {Γ τ} → var Γ τ → term Γ τ
  λ[_]_ : ∀ {Γ τ₂} → (τ₁ : type) → (e : term (Γ , τ₁) τ₂) → term Γ (τ₁ -→ τ₂)
  _∙_ : ∀ {Γ τ₁ τ₂} → term Γ (τ₁ -→ τ₂) → term Γ τ₁ → term Γ τ₂

length : ctx → ℕ
length nil = zero
length (ctx , _) = suc (length ctx)

extend : ∀ {Γ Δ}
  → (∀ {τ} → var Γ τ → var Δ τ)
  → (∀ {τ₁ τ₂} → var (Γ , τ₂) τ₁ → var (Δ , τ₂) τ₁)
extend ρ zero = zero
extend ρ (suc c) = suc (ρ c)

rename : ∀ {Γ Δ}
  → (∀ {τ} → var Γ τ → var Δ τ)
  → (∀ {τ} → term Γ τ → term Δ τ)
rename ρ true = true
rename ρ false = false
rename ρ (` x) = ` (ρ x)
rename ρ (λ[ τ₁ ] c) = λ[ τ₁ ] rename (extend ρ) c
rename ρ (c ∙ c₁) = rename ρ c ∙ rename ρ c₁

extends : ∀ {Γ Δ}
  → (∀ {τ} → var Γ τ → term Δ τ)
  → (∀ {τ₁ τ₂} → var (Γ , τ₂) τ₁ → term (Δ , τ₂) τ₁)
extends σ zero = ` zero
extends σ (suc x) = rename suc (σ x)

subst : ∀ {Γ Δ}
  → (∀ {τ} → var Γ τ → term Δ τ)
  → (∀ {τ} → term Γ τ → term Δ τ)
subst ρ true = true
subst ρ false = false
subst ρ (` x) = ρ x
subst ρ (λ[ τ₁ ] x) = λ[ τ₁ ] subst (extends ρ) x
subst ρ (x ∙ x₁) = subst ρ x ∙ subst ρ x₁

_[_] : ∀ {Γ τ₁ τ₂} → term (Γ , τ₂) τ₁ → term Γ τ₂ → term Γ τ₁
_[_] {Γ} {τ₁} {τ₂} e e₁ = subst σ e
  where
    σ : ∀ {τ} → var (Γ , τ₂) τ → term Γ τ 
    σ zero = e₁
    σ (suc x) = ` x

data value : ∀ {Γ τ} → term Γ τ → Set where
  true : ∀ {Γ} → value {Γ} true
  false : ∀ {Γ} → value {Γ} false
  λ[_]_ : ∀ {Γ τ₁ τ₂} {e : term (Γ , τ₁) τ₂} → value (λ[ τ₁ ] e)

data step : ∀ {Γ τ} → term Γ τ → term Γ τ → Set where 
  β-λ : ∀ {Γ τ₁ τ₂ v} → (e : term (Γ , τ₁) τ₂) → value v
    → step ((λ[ τ₁ ] e) ∙ v) (e [ v ])