content: {-# LANGUAGE TemplateHaskell #-}
  
  module Internal.Syntax.Internal ( tests ) where
  
  import Agda.Syntax.Internal
  import Agda.TypeChecking.Substitute ()
  
  import Internal.Helpers
  import Internal.Syntax.Common ()
  import Internal.Syntax.Abstract.Name ()
  
  ------------------------------------------------------------------------
  -- Instances
  
  instance Arbitrary NotBlocked where
    arbitrary = oneof
      [ pure Underapplied
      , pure AbsurdMatch
      , MissingClauses <$> arbitrary
      , pure ReallyNotBlocked
      -- , StuckOn Elim  -- TODO
      ]
  
  instance Arbitrary (Blocked ()) where
    arbitrary = do
      m  <- arbitrary
      bs <- arbitrary
      elements [ blocked_ m, NotBlocked bs () ]
  
  ------------------------------------------------------------------------------
  -- Properties
  
  -- | 'NotBlocked' is a monoid.
  prop_monoid_NotBlocked :: Property3 NotBlocked
  prop_monoid_NotBlocked = isMonoid
  
  -- | 'Blocked_' is a monoid.
  prop_monoid_Blocked_ :: Property3 Blocked_
  prop_monoid_Blocked_ = isMonoid
  
  ------------------------------------------------------------------------
  -- * All tests
  ------------------------------------------------------------------------
  
  -- Template Haskell hack to make the following $allProperties work
  -- under ghc-7.8.
  return [] -- KEEP!
  
  -- | All tests as collected by 'allProperties'.
  --
  -- Using 'allProperties' is convenient and superior to the manual
  -- enumeration of tests, since the name of the property is added
  -- automatically.
  
  tests :: TestTree
  tests = testProperties "Internal.Syntax.Internal" $allProperties
  