ScopeCheckingLC.agda

module _ where

open import Function using (_∘_)
open import Relation.Binary.PropositionalEquality
open import Relation.Binary
open import Relation.Nullary
open import Data.Empty

-- Untyped lambda calculus, with "weak" names
module _ where
  data Term (name : Set) : Set where
    var : name → Term name
    lam : name → Term name → Term name
    app : Term name → Term name → Term name

-- Scoping rules
module _ where
  data Ctx (A : Set) : Set where
    [] : Ctx A
    _▷_ : Ctx A → A → Ctx A

  data Name {A : Set} : (Γ : Ctx A) → A → Set where
    nz : ∀ {Γ x} → Name (Γ ▷ x) x
    ns : ∀ {Γ x y} → x ≢ y → Name Γ x → Name (Γ ▷ y) x

  data _⊢_ {name : Set} (Γ : Ctx name) : (e : Term name) → Set where
    var : ∀ {n} → Name Γ n → Γ ⊢ var n
    lam : ∀ n {e} → (Γ ▷ n) ⊢ e → Γ ⊢ lam n e
    app : ∀ {f e} → Γ ⊢ f → Γ ⊢ e → Γ ⊢ app f e

-- Scope checking
module Scoping (name : Set) (_≟ₙ_ : Decidable (_≡_ {A = name})) where
  scopeVar : (Γ : Ctx name) → (x : name )→ Dec (Name Γ x)
  scopeVar [] x = no (λ ())
  scopeVar (Γ ▷ y) x with x ≟ₙ y
  scopeVar (Γ ▷ _) x | yes refl = yes nz
  scopeVar (Γ ▷ y) x | no x≢y with scopeVar Γ x
  scopeVar (Γ ▷ y) x | no x≢y | yes v = yes (ns x≢y v)
  scopeVar (Γ ▷ y) x | no x≢y | no ¬v = no (¬v ∘ lemma x≢y)
    where
      lemma : ∀ {x y} → x ≢ y → Name (Γ ▷ y) x → Name Γ x
      lemma y≢x nz = ⊥-elim (y≢x refl)
      lemma y≢x (ns x n) = n

  scope : (Γ : Ctx name) → (e : Term name) → Dec (Γ ⊢ e)
  scope Γ (var x) with scopeVar Γ x
  scope Γ (var x) | yes p = yes (var p)
  scope Γ (var x) | no ¬p = no (¬p ∘ lemma)
    where
      lemma : Γ ⊢ var x → Name Γ x
      lemma (var x) = x
  scope Γ (lam x e) with scope (Γ ▷ x) e
  scope Γ (lam x e) | yes e′ = yes (lam _ e′)
  scope Γ (lam x e) | no ¬prf = no (¬prf ∘ lemma)
    where
      lemma : Γ ⊢ lam x e → (Γ ▷ x) ⊢ e
      lemma (lam _ prf) = prf
  scope Γ (app f e) with scope Γ f
  scope Γ (app f e) | yes f′ with scope Γ e
  scope Γ (app f e) | yes f′ | yes e′ = yes (app f′ e′)
  scope Γ (app f e) | yes f′ | no ¬p = no (¬p ∘ lemma)
    where
      lemma : Γ ⊢ app f e → Γ ⊢ e
      lemma (app f e) = e
  scope Γ (app f e) | no ¬p = no (¬p ∘ lemma)
    where
      lemma : Γ ⊢ app f e → Γ ⊢ f
      lemma (app f e) = f

open import Data.Nat hiding (_≟_)
open import Data.Fin

-- De Bruijn representation: well-scoped by construction
module _ where
  data DBTerm (n : ℕ) : Set where
    var : Fin n → DBTerm n
    lam : DBTerm (suc n) → DBTerm n
    app : DBTerm n → DBTerm n → DBTerm n

-- We can use a proof of well-scopedness (i.e. a derivation of a
-- well-scoped term) to convert to de Bruijn
module _ where
  size : ∀ {A} → Ctx A → ℕ
  size [] = 0
  size (Γ ▷ _) = suc (size Γ)

  index : ∀ {A Γ} {n : A} → Name Γ n → Fin (size Γ)
  index nz = zero
  index (ns _ n) = suc (index n)

  toDB : ∀ {A} {Γ : Ctx A} {e} → Γ ⊢ e → DBTerm (size Γ)
  toDB {Γ = Γ} (var x) = var (index x)
  toDB (lam _ e) = lam (toDB e)
  toDB (app f e) = app (toDB f) (toDB e)

module Example where
  open import Data.String renaming (_≟_ to _≟ₛ_)
  open Scoping String _≟ₛ_
  open import Relation.Nullary.Decidable

  CONST : Term String
  CONST = lam "x" (lam "y" (var "x"))

  CONST′ : DBTerm 0
  CONST′ = toDB (from-yes (scope [] CONST))