Enough STLC to implement single-step η-reduction

Types2.agda

open import Level using () renaming (suc to lsuc)
open import Data.Empty
open import Data.Nat hiding (compare)
open import Data.Nat.Properties
open import Data.Product
open import Data.Sum
open import Data.Vec
open import Function
open import Relation.Nullary
open import Relation.Nullary.Negation
open import Relation.Binary
open import Relation.Binary.PropositionalEquality hiding ([_])
open StrictTotalOrder strictTotalOrder using (compare)

module Types2 {ℓ Cᵤ} (U : Vec (Set ℓ) Cᵤ) where

  module Helper where
    Fin : ℕ → Set
    Fin n = Σ[ m ∈ ℕ ] m < n

    fsuc : ∀ {n} → Fin n → Fin (suc n)
    fsuc (m , m<n) = (suc m) , (s≤s m<n)

    _at_ : ∀ {a} {A : Set a} {n} → Vec A n → Fin n → A
    []        at (i , ())
    (x₀ ∷ xₛ) at (zero    , i<n)         = x₀
    (x₀ ∷ xₛ) at (suc i-1 , s≤s i-1<n-1) = xₛ at (i-1 , i-1<n-1)

    remove : ∀ {a} {A : Set a} {n} → (i : Fin (suc n)) → (v : Vec A (suc n)) → Vec A n
    remove               (zero    , _)         (v₀ ∷ vₛ) = vₛ
    remove {n = zero}    (suc i-1 , s≤s ())    (v₀ ∷ vₛ)
    remove {n = suc n-1} (suc i-1 , s≤s i-1<n) (v₀ ∷ vₛ) = v₀ ∷ remove (i-1 , i-1<n) vₛ

    remove-at< : ∀ {a} {A : Set a} {n} i j i<n+1 j<n+1 j<n
               → (v : Vec A (suc n)) → j < i
               → remove (i , i<n+1) v at (j , j<n) ≡ v at (j , j<n+1)
    remove-at< zero    j i<n+1 j<n+1 j<n (v₀ ∷ vₛ) ()
    remove-at< {n = zero} (suc i-1) j i<n+1 j<n+1 () (v₀ ∷ vₛ) j<i
    remove-at< {n = suc n-1} (suc i-1) zero (s≤s i-1<n) j<n+1 j<n (v₀ ∷ vₛ) j<i = refl
    remove-at< {n = suc n-1} (suc i-1) (suc j-1) (s≤s i-1<n) (s≤s j-1<n) (s≤s j-1<n-1) (v₀ ∷ vₛ) (s≤s j-1<i-1) = remove-at< i-1 j-1 i-1<n j-1<n j-1<n-1 vₛ j-1<i-1

    ≤-irrel : ∀ {m n} (p q : m ≤ n) → p ≡ q
    ≤-irrel {m = zero} z≤n z≤n = refl
    ≤-irrel {m = suc _} {n = zero} () ()
    ≤-irrel {m = suc _} {n = suc _} (s≤s p) (s≤s q) = cong s≤s (≤-irrel p q)

    <-irrel : ∀ {m n} (p q : m < n) → p ≡ q
    <-irrel = ≤-irrel

    remove-at> : ∀ {a} {A : Set a} {n} i j i<n+1 j+1<n+1 j<n
               → (v : Vec A (suc n)) → suc j > i
               → remove (i , i<n+1) v at (j , j<n) ≡ v at (suc j , j+1<n+1)
    remove-at> zero j i<n+1 (s≤s j<n′) j<n (v₀ ∷ vₛ) j+1>i = cong (λ j<n₁ → vₛ at (j , j<n₁)) (<-irrel j<n j<n′)
    remove-at> {n = zero} (suc i-1) j (s≤s ()) j+1<n+1 j<n (v₀ ∷ vₛ) j+1>i
    remove-at> {n = suc n} (suc i-1) zero (s≤s i-1<n) j+1<n+1 j<n (v₀ ∷ vₛ) (s≤s ())
    remove-at> {n = suc n} (suc i-1) (suc j-1) (s≤s i-1<n) (s≤s j<n) (s≤s j-1<n-1) (v₀ ∷ vₛ) (s≤s j>i-1) = remove-at> i-1 j-1 i-1<n j<n j-1<n-1 vₛ j>i-1

    coerce : ∀ {ℓ} {A B : Set ℓ} → A ≡ B → A → B
    coerce refl x = x

    a<b<c+1 : ∀ {a b c} → a < b → b < suc c → a < c
    a<b<c+1 {a} {b} {c} a<b (s≤s b-1<c) = ≤-trans a<b b-1<c
      where open DecTotalOrder decTotalOrder using () renaming (trans to ≤-trans)

    deMorgan : ∀ {p q} {P : Set p} {Q : Set q} → ¬ (P ⊎ Q) → (¬ P) × (¬ Q)
    deMorgan ¬[p∨q] = (¬[p∨q] ∘ inj₁) , (¬[p∨q] ∘ inj₂)

    decSum : ∀ {p q} {P : Set p} {Q : Set q} → Dec P → Dec Q → Dec (P ⊎ Q)
    decSum (yes p) _       = yes (inj₁ p)
    decSum _       (yes q) = yes (inj₂ q)
    decSum (no ¬p) (no ¬q) = no $ λ
      { (inj₁ p) → contradiction p ¬p
      ; (inj₂ q) → contradiction q ¬q
      }
  open Helper

  infixr 0 _⟶_
  data Type : Set (lsuc ℓ) where
    Prim : Fin Cᵤ → Type
    _⟶_  : Type → Type → Type

  data Expr {n} (Γ : Vec Type n) : Type → Set (lsuc ℓ) where
    Lit : ∀ t → (x : U at t) → Expr Γ (Prim t)
    Var : ∀ v → Expr Γ (Γ at v)
    App : ∀ {τ τ′} → (f : Expr Γ (τ ⟶ τ′)) → (x : Expr Γ τ) → Expr Γ τ′
    Lam : ∀ {τ τ′} → (b : Expr (τ ∷ Γ) τ′) → Expr Γ (τ ⟶ τ′)

  _appears-free-in_ : ∀ {n τ} {Γ : Vec Type n} → (v : Fin n) → (e : Expr Γ τ) → Set
  v appears-free-in Lit t x  = ⊥
  v appears-free-in Var v′   = proj₁ v ≡ proj₁ v′
  v appears-free-in App e e′ = (v appears-free-in e) ⊎ (v appears-free-in e′)
  v appears-free-in Lam e    = fsuc v appears-free-in e

  _appears-free-in?_ : ∀ {n τ} {Γ : Vec Type n} → Decidable (_appears-free-in_ {n} {τ} {Γ})
  v appears-free-in? Lit t x  = no (λ ())
  v appears-free-in? Var v′   = proj₁ v ≟ proj₁ v′
  v appears-free-in? App e e′ = decSum (v appears-free-in? e) (v appears-free-in? e′)
  v appears-free-in? Lam e    = fsuc v appears-free-in? e

  delvar : ∀ {n τ} {Γ : Vec Type (suc n)} → (v : Fin (suc n)) → (e : Expr Γ τ)
         → ¬ (v appears-free-in e) → Expr (remove v Γ) τ
  delvar v (Lit t x) p = Lit t x
  delvar {Γ = Γ} (v , v<n+1) (Var (v′ , v′<n+1)) p with compare v′ v
  ... | tri< v′<v v′≠v v′≯v = coerce (cong (Expr _) (remove-at< v v′ v<n+1 v′<n+1 v′<n Γ v′<v)) (Var (v′ , v′<n))
    where v′<n = a<b<c+1 v′<v v<n+1
  ... | tri≈ v′≮v v′=v v′≯v = contradiction (sym v′=v) p
  ... | tri> v′≮v v′≠v v′>v with v′ | v′<n+1
  ...   | zero     | _          = contradiction v′>v (λ ())
  ...   | suc v′-1 | s≤s v′-1<n = coerce (cong (Expr _) (remove-at> v v′-1 v<n+1 (s≤s v′-1<n) v′-1<n Γ v′>v)) (Var (v′-1 , v′-1<n))
  delvar v (App e e′) p = App (delvar v e (proj₁ (deMorgan p))) (delvar v e′ (proj₂ (deMorgan p)))
  delvar v (Lam e) p = Lam (delvar (fsuc v) e p)

  -- λ x → f x => f
  η-reduce : ∀ {n τ} {Γ : Vec Type n} → Expr Γ τ → Expr Γ τ
  η-reduce (Lam (App e (Var (0 , 0<n+1)))) with (0 , 0<n+1) appears-free-in? e
  ... | no ¬p = delvar (0 , 0<n+1) e ¬p
  ... | yes p = Lam (App e (Var (0 , 0<n+1)))
  η-reduce other = other

  private
    λx→fx : ∀ α β → Expr [ α ⟶ β ] (α ⟶ β)
    λx→fx α β = Lam (App (Var (1 , s≤s (s≤s z≤n))) (Var (0 , (s≤s z≤n))))

    η-test : ∀ α β → η-reduce (λx→fx α β) ≡ Var (0 , s≤s z≤n)
    η-test α β = refl