Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
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))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.