content: {-# LANGUAGE DeriveGeneric, DeriveDataTypeable #-}
  module PropOpenClose (test_openClose) where
  
  import Control.Applicative (Applicative(..), (<$>))
  import Data.Monoid (Any(..))
  import Data.Typeable (Typeable)
  import GHC.Generics (Generic)
  
  import Test.QuickCheck
  import Test.Tasty (testGroup, TestTree)
  import Test.Tasty.QuickCheck (testProperty)
  
  import Unbound.Generics.LocallyNameless
  import Unbound.Generics.LocallyNameless.Internal.Fold (foldMapOf, toListOf)
  
  import AlphaProperties
  
  
  -- Wrapper around 'Name a' that has an Arbitrary instance that generates free names.
  -- Note that this doesn't guarantee /freshness/.  The name may clash with some other one.
  -- But it will never be a bound name.
  newtype FreeName a = FreeName {getFreeName :: Name a}
                       deriving (Show)
  
  instance Arbitrary (FreeName a) where
    arbitrary = do
      s <- listOf1 (elements ['a'..'z'])
      n <- arbitrary
      return $ FreeName $ makeName s n
    shrink = const []
  
  ----------------------------------------
  -- example data structure, with no bound names.
  
  data T a = Leaf !a
           | V !(Name (T a))
           | B !(T a) !(T a)
           deriving (Show, Typeable, Generic)
  
  instance (Typeable a, Alpha a) => Alpha (T a)
  
  instance Arbitrary a => Arbitrary (T a) where
    arbitrary =
      oneof
      [
        Leaf <$> arbitrary
      ,(V . getFreeName) <$> arbitrary
      , B <$> arbitrary <*> arbitrary
      ]
  
  -- generator that picks out one of the free variables of a tree
  arbVarsOf :: (Alpha a, Typeable a) => T a -> Gen (Name (T a))
  arbVarsOf t =
    let vs = toListOf fv t
    in  elements vs
  
  -- spec for free variables of a tree.
  -- fvSpec :: Traversal' (T a) (Name (T a))
  fvSpec :: Applicative f => (Name (T a) -> f (Name (T a))) -> T a -> f (T a)
  fvSpec f t =
    case t of
     Leaf {} -> pure t
     V v -> V <$> f v
     B t1 t2 -> B <$> fvSpec f t1 <*> fvSpec f t2
  
  ----------------------------------------
  -- Properties
  
  -- every tree is alpha-equivalent to itself
  prop_refl :: T Int -> Property
  prop_refl x = x =~= x
  
  -- generic fv gives the same answer as fvSpec
  prop_fv_spec :: T Int -> Property
  prop_fv_spec t = toListOf fv t === toListOf fvSpec t
    
  -- if a name is already free opening it has no effect
  prop_open_idempotent :: T Int -> Property
  prop_open_idempotent t =
    forAll (arbVarsOf t) $ \v -> open initialCtx (nthPatFind v) t =~= t
  
  -- if you close over a variable, then it is no longer free.
  prop_close_binds :: T Int -> Property
  prop_close_binds t =
    (not $ null $ toListOf fvAny t) ==>
    forAll (arbVarsOf t) $ \v -> v /~@ close initialCtx (namePatFind v) t
  
  ----------------------------------------
  -- Test group
  
  test_openClose :: TestTree
  test_openClose =
    testGroup "QuickCheck properties"
    [
      testProperty "reflexivity" prop_refl
    , testProperty "fv specification" prop_fv_spec
    , testProperty "open idempotency" prop_open_idempotent
    , testProperty "closing binds variables" prop_close_binds
    ]
  