Skip to content
{{ message }}

Instantly share code, notes, and snippets.

# gergoerdi/ScopeCheckingLC.agda

Created Feb 9, 2017
 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))
to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.