-- |
-- Module      : ScopeCheck
-- Description : Scope checking the Untyped lambda calculus
-- Stability   : experimental
--
-- This module demonstrates a translation from unscoped to well-scoped terms

module ScopeCheck where

import Rebound
import Rebound.Bind.Single
import Data.Maybe (fromJust)
import LC qualified
import Rebound.Lib

-- | Named representation for the untyped lambda calculus
-- The type parameter 'a' is the variable type
data Exp (a :: Type) where
  Var :: a -> Exp a
  Lam :: a -> Exp a -> Exp a
  App :: Exp a -> Exp a -> Exp a

-- | Convert a named expression to deBruijn indices, checking to make
-- sure that the expression is well scoped
scopeCheck :: (Eq a) => Exp a -> Maybe (LC.Exp Z)
scopeCheck = to []
  where
    to :: (Eq a) => [(a, Fin n)] -> Exp a -> Maybe (LC.Exp n)
    to vs (Var v) = do
      x <- lookup v vs
      return $ LC.Var x
    to vs (Lam v b) = do
      b' <- to ((v, FZ) : map (fmap FS) vs) b
      return $ LC.Lam (bind b')
    to vs (App f a) = do
      f' <- to vs f
      a' <- to vs a
      return $ LC.App f' a'


----------------------------------------------
-- Examples
----------------------------------------------

-- | Identity function
idExp :: Exp String
idExp = Lam "x" (Var "x")

-- | "True"
trueExp :: Exp String
trueExp = Lam "x" (Lam "y" (Var "x"))

-- | An ill-scoped term (`y` is never bound)
illScoped :: Exp String
illScoped = Lam "x" (Var "y")

-- >>> scopeCheck idExp
-- Just (λ. 0)

-- >>> scopeCheck trueExp
-- Just (λ. (λ. 1))

-- >>> scopeCheck illScoped
-- Nothing