Crash course in scope checking

scopecheck.agda

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')