-- This module contains an enumeration of well scoped lambda terms

{-#LANGUAGE DeriveDataTypeable#-}
import Test.Feat
import Test.Feat.Enumerate
import Test.Feat.Access
import Data.MemoCombinators(bits) -- From package data-memocombinators


-- De Bruijn style lambda calculus
data Lam = Lam Lam
         | App Lam Lam
         | Var Integer
         deriving (Show,Eq,Ord, Typeable)


enumLamPair :: Integer -> Enumerate (Lam,Lam)
enumLamPair = bits enumLamPair' where
  enumLamPair' n = (,) <$> enumLam n <*> enumLam n

enumLam :: Integer -> Enumerate Lam
enumLam = bits enumLam' where
  enumLam' n = 
    let e = consts $
         [ App <$> e <*> e
         , fmap Lam $ enumLam (n+1)
         , fromParts [Finite n Var]
         ] 
    in e 

instance Enumerable Lam where
  enumerate = noOptim $ enumLam 0



test n = take n $ values :: [(Integer,[Lam])]