Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Crash course in scope checking
module scope where
import Level as L
open import Data.Nat.Base
open import Data.Vec hiding (_>>=_)
open import Data.Fin.Base
open import Data.String
open import Data.Maybe as Maybe
open import Data.Product as Prod
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Maybe.Categorical
open import Category.Monad
open RawMonad (monad {L.zero})
data Raw : Set where
var : String Raw
lam : String Raw Raw
app : Raw Raw Raw
data Tm n : Set where
var : Fin n Tm n
lam : Tm (suc n) Tm n
app : Tm n Tm n Tm n
Scope : Set
Scope = Vec String
-- resolve a variable name to the corresponding de Bruijn index
-- γ [ k ]= x is an inductive proof that the k-th element in γ is x
resolve : {n} (γ : Scope n) (x : String) Maybe (∃ λ k γ [ k ]= x)
-- if the scope is empty, we can't possibly find the variable
resolve [] x = nothing
-- otherwise we check whether the variable name matches that of the
-- first one in scope
resolve (n ∷ γ) x with n ≟ x
-- if it is the case then we return the zero-th de Bruijn index
... | yes refl = just (zero , here)
... | no ¬p = do
-- otherwise we look for the variable further in the scope
(k , pr) resolve γ x
-- and record we did so by using suc
pure (suc k , there pr)
scopeCheck : {n} Scope n Raw Maybe (Tm n)
scopeCheck γ (var v) = do
-- attempt to resolve v
(k , _) resolve γ v
pure (var k)
scopeCheck γ (lam x b) = do
-- extend the scope with the newly-bound variable
let γ,x = x ∷ γ
-- check the body
b' scopeCheck γ,x b
-- return a λ-expression
pure (lam b')
scopeCheck γ (app f t) = do
--check both the function and its argument in the same scope
f' scopeCheck γ f
t' scopeCheck γ t
-- return the application node
pure (app f' t')
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment