Scopecheck.agda

module STLC.Scopecheck (Type : Set) where

open import STLC.Syntax Type as S hiding (Expr; module Expr)
open import STLC.Bound Type
open import Data.Nat hiding (_≟_)
open import Data.Fin
open import Data.Vec using ([]; _∷_; lookup; reverse)
open import Data.String
open import Relation.Nullary.Decidable

appˡ : ∀ {n} {Γ : Binder n} {E E′ F F′} → Γ ⊢ (E · F) ↝ (E′ · F′) → Γ ⊢ E ↝ E′
appˡ (δ · _) = δ

appʳ : ∀ {n} {Γ : Binder n} {E E′ F F′} → Γ ⊢ (E · F) ↝ (E′ · F′) → Γ ⊢ F ↝ F′
appʳ (_ · δ) = δ

open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import STLC.Utils

name-dec : ∀ {n} {Γ : Binder n} {x y : Name} {E : Expr (suc n)} →
           (y ∷ Γ) ⊢ var x ↝ E →
           x ≡ y ⊎ (∃[ E′ ] Γ ⊢ var x ↝ E′)
name-dec var-zero = inj₁ refl
name-dec (var-suc p) = inj₂ (_ , p)

find-name : ∀ {n} → (Γ : Binder n) → (x : Name) → Dec (∃[ E′ ] Γ ⊢ var x ↝ E′)
find-name [] x = no lem
  where
  lem : ∄[ E′ ] [] ⊢ var x ↝ E′
  lem (_ , ())
find-name (y ∷ Γ) x with x ≟ y
find-name (y ∷ Γ) .y | yes refl = yes (var zero , var-zero)
find-name (y ∷ Γ) x | no x≢y with find-name Γ x
find-name (y ∷ Γ) x | no x≢y | yes (var k , δ) = yes (var (suc k) , var-suc {p = fromWitnessFalse x≢y} δ)
find-name (y ∷ Γ) x | no x≢y | yes (lam _ _ , ())
find-name (y ∷ Γ) x | no x≢y | yes (_ · _ , ())
find-name (y ∷ Γ) x | no x≢y | no ¬p = no lem
  where
  lem : ∄[ E′ ] (y ∷ Γ) ⊢ var x ↝ E′
  lem (E′ , δ) with name-dec δ
  lem (E′ , δ) | inj₁ x≡y = x≢y x≡y
  lem (E′ , δ) | inj₂ p = ¬p p

check : ∀ {n} → (Γ : Binder n) → (E : S.Expr) → Dec (∃[ E′ ] Γ ⊢ E ↝ E′)
check Γ (var x) = find-name Γ x
check Γ (lam (x ∶ τ) E) with check (x ∷ Γ) E
check Γ (lam (x ∶ τ) E) | yes (E′ , δ) = yes (lam _ E′ , lam δ)
check Γ (lam (x ∶ τ) E) | no ¬p = no lem
  where
  lem : ∄[ E′ ] Γ ⊢ lam (x ∶ τ) E ↝ E′
  lem (var _ , ())
  lem (_ · _ , ())
  lem (lam .τ E′ , lam δ) = ¬p (E′ , δ)
check Γ (E · F) with check Γ E
check Γ (E · F) | yes (E′ , δ₁) with check Γ F
check Γ (E · F) | yes (E′ , δ₁) | yes (F′ , δ₂) = yes (E′ · F′ , δ₁ · δ₂)
check Γ (E · F) | yes (E′ , δ₁) | no ¬p = no lem
  where
  lem : ∄[ E′ ] Γ ⊢ E · F ↝ E′
  lem (var _ , ())
  lem (lam _ _ , ())
  lem (E₁ · E₂ , δ) = ¬p (E₂ , appʳ δ)
check Γ (E · F) | no ¬p = no lem
  where
  lem : ∄[ E′ ] Γ ⊢ (E · F) ↝ E′
  lem (var _ , ())
  lem (lam _ _ , ())
  lem (E₁ · E₂ , δ) = ¬p (E₁ , appˡ δ)

-- Go from a representation that uses Names to one that uses de Bruijn indices
scope : (E : S.Expr) → {p : True (check [] E)} → Expr 0
scope E {p} = proj₁ (toWitness p)