#if __GLASGOW_HASKELL__ >= 710
#endif
module Agda.TypeChecking.Free.Tests (tests) where
import qualified Data.IntMap as Map
import Test.QuickCheck
import Agda.Syntax.Common
import Agda.Syntax.Internal
import Agda.TypeChecking.Free.Lazy hiding (FlexRig(..))
import qualified Agda.TypeChecking.Free.Lazy as Free
import qualified Agda.TypeChecking.Free.Old as Old
import Agda.TypeChecking.Free (freeIn)
import qualified Agda.TypeChecking.Free as New
import Agda.TypeChecking.Test.Generators
import Agda.Utils.TestHelpers
prop_FlexRig_order = strictlyAscending
[ Free.Flexible [], Free.WeaklyRigid, Free.Unguarded, Free.StronglyRigid ]
strictlyAscending l = and $ zipWith (<) l $ tail l
prop_composeFlexRig_associative = associative composeFlexRig
prop_composeFlexRig_commutative = commutative composeFlexRig
prop_composeFlexRig_idempotent = idempotent composeFlexRig
prop_composeFlexRig_zero = isZero (Free.Flexible []) composeFlexRig
prop_composeFlexRig_unit = identity Free.Unguarded composeFlexRig
prop_FlexRig_distributive = distributive composeFlexRig max
prop_maxVarOcc_top = isZero topVarOcc maxVarOcc
prop_maxVarOcc_bot = identity botVarOcc maxVarOcc
prop_freeIn = all (0 `freeIn`)
[ var 0
, Lam defaultArgInfo $ Abs "x" $ var 1
, Sort $ varSort 0
]
prop_old_freeVars_Pi = same_freeVars ty
same_freeVars t = new_to_old_FV (New.freeVars t) == Old.freeVars t
old_to_new_FV (Old.FV a b c d e f) = New.FV a b c (Map.fromSet (const []) d) e f
new_to_old_FV (New.FV a b c d e f) = Old.FV a b c (Map.keysSet d) e f
ty = Pi (defaultDom ab) $ Abs "x" $ El (Type $ Max []) $ var 5
where
a = El Prop $
var 4
b = El (Type $ Max []) $
Sort $ Type $ Max []
ab = El (Type $ Max [ClosedLevel 1]) $
Pi (defaultDom a) (Abs "x" b)
new_fv_ty :: New.FreeVars
new_fv_ty = New.freeVars ty
old_fv_ty :: Old.FreeVars
old_fv_ty = Old.freeVars ty
prop_old_freeVars_Term conf x = forAll (genC conf) $ \ (t :: Term) ->
same_freeVars t
prop_old_freeIn_Term conf x = forAll (genC conf) $ \ (t :: Term) ->
New.freeIn x t == Old.freeIn x t
prop_old_freeIn_Type conf x = forAll (genC conf) $ \ (t :: Type) ->
New.freeIn x t == Old.freeIn x t
return []
tests :: IO Bool
tests = do
putStrLn "Agda.TypeChecking.Free.Tests"
$quickCheckAll