    module Agda.TypeChecking.Tests where

    import qualified Data.Set as Set
    import Agda.Utils.QuickCheck

    import Agda.Syntax.Internal
    import Agda.TypeChecking.Test.Generators
    import Agda.TypeChecking.Telescope
    import Agda.TypeChecking.Substitute
    import Agda.Utils.Size
    import Agda.Utils.Permutation
    import Agda.Utils.TestHelpers

    ---------------------------------------------------------------------------
    -- * Tests for "Agda.Utils.Permutation"
    ---------------------------------------------------------------------------

    ---------------------------------------------------------------------------
    -- * Tests for "Agda.TypeChecking.Telescope"
    ---------------------------------------------------------------------------

    -- | @telFromList . telToList == id@
    prop_telToListInv :: TermConfiguration -> Property
    prop_telToListInv conf =
      forAll (genC conf) $ \tel ->
      telFromList (telToList tel) == tel

    -- | All elements of 'flattenTel' are well-scoped under the original telescope.
    prop_flattenTelScope :: TermConfiguration -> Property
    prop_flattenTelScope conf =
      forAll (genC conf) $ \tel ->
      all (isWellScoped $ extendWithTelConf tel conf) (flattenTel tel)

    -- | @unflattenTel . flattenTel == id@
    prop_flattenTelInv :: TermConfiguration -> Property
    prop_flattenTelInv conf =
      forAll (genC conf) $ \tel ->
      unflattenTel (teleNames tel) (flattenTel tel) == tel

    -- | 'reorderTel' is stable.
    prop_reorderTelStable :: TermConfiguration -> Property
    prop_reorderTelStable conf =
      forAll (genC conf) $ \tel ->
      reorderTel (flattenTel tel) == idP (size tel)

    -- | The result of splitting a telescope is well-scoped.
    prop_splitTelescopeScope :: TermConfiguration -> Property
    prop_splitTelescopeScope conf =
      forAll (genC conf)			    $ \tel ->
      forAll (listOfElements [0..size tel - 1]) $ \vs ->
      let SplitTel tel1 tel2 perm = splitTelescope (Set.fromList vs) tel
          tel' = telFromList (telToList tel1 ++ telToList tel2)
      in  isWellScoped conf tel'

    -- | The permutation generated when splitting a telescope preserves scoping.
    prop_splitTelescopePermScope :: TermConfiguration -> Property
    prop_splitTelescopePermScope conf =
          forAllShrink (genC conf) (shrinkC conf)		     $ \tel ->
          forAllShrink (listOfElements [0..size tel - 1]) shrink $ \vs ->
      let SplitTel tel1 tel2 perm = splitTelescope (Set.fromList vs) tel
          conf1 = extendWithTelConf tel1 conf
          conf2 = conf1 { tcFreeVariables = map (size tel2 +) (tcFreeVariables conf1) }
          conf' = conf  { tcFreeVariables = map (size tel +) (tcFreeVariables conf) ++ vs }
      in  forAllShrink (genC conf') (shrinkC conf') $ \t ->
          isWellScoped conf2 (substs (renamingR $ invertP perm) (t :: Term))

    {-
    -- | The permutation generated when splitting a telescope correctly translates
    --   between the old and the new telescope.
    prop_splitTelescopePermInv :: TermConfiguration -> Property
    prop_splitTelescopePermInv conf =
          forAll (wellScopedTel conf)		$ \tel ->
          forAll (listOfElements [0..size tel - 1]) $ \vs ->
      let SplitTel tel1 tel2 perm = splitTelescope (Set.fromList vs) tel
          tel' = telFromList (telToList tel1 ++ telToList tel2)
          conf1 = extendWithTelConf tel  conf
          conf2 = extendWithTelConf tel' conf
      in  forAll (wellScopedTerm conf1) $ \t1 ->
          forAll (wellScopedTerm conf2) $ \t2 ->
      let t1' = rename (invertP perm) $ rename perm t1
          t2' = rename perm $ rename (invertP perm) t2
      in  t1 == t1' && t2 == t2'
    -}

    tests :: IO Bool
    tests = runTests "Agda.TypeChecking.Tests"
      [ quickCheck' prop_telToListInv
      , quickCheck' prop_flattenTelScope
      , quickCheck' prop_flattenTelInv
      , quickCheck' prop_reorderTelStable
      , quickCheck' prop_splitTelescopeScope
      , quickCheck' prop_splitTelescopePermScope
      ]