1
module Agda.TypeChecking.Tests where
3
import qualified Data.Set as Set
4
import Agda.Utils.QuickCheck
6
import Agda.Syntax.Internal
7
import Agda.TypeChecking.Test.Generators
8
import Agda.TypeChecking.Telescope
9
import Agda.TypeChecking.Substitute
10
import Agda.Utils.Size
11
import Agda.Utils.Permutation
12
import Agda.Utils.TestHelpers
14
---------------------------------------------------------------------------
15
-- * Tests for "Agda.Utils.Permutation"
16
---------------------------------------------------------------------------
18
---------------------------------------------------------------------------
19
-- * Tests for "Agda.TypeChecking.Telescope"
20
---------------------------------------------------------------------------
22
-- | @telFromList . telToList == id@
23
prop_telToListInv :: TermConfiguration -> Property
24
prop_telToListInv conf =
25
forAll (genC conf) $ \tel ->
26
telFromList (telToList tel) == tel
28
-- | All elements of 'flattenTel' are well-scoped under the original telescope.
29
prop_flattenTelScope :: TermConfiguration -> Property
30
prop_flattenTelScope conf =
31
forAll (genC conf) $ \tel ->
32
all (isWellScoped $ extendWithTelConf tel conf) (flattenTel tel)
34
-- | @unflattenTel . flattenTel == id@
35
prop_flattenTelInv :: TermConfiguration -> Property
36
prop_flattenTelInv conf =
37
forAll (genC conf) $ \tel ->
38
unflattenTel (teleNames tel) (flattenTel tel) == tel
40
-- | 'reorderTel' is stable.
41
prop_reorderTelStable :: TermConfiguration -> Property
42
prop_reorderTelStable conf =
43
forAll (genC conf) $ \tel ->
44
reorderTel (flattenTel tel) == idP (size tel)
46
-- | The result of splitting a telescope is well-scoped.
47
prop_splitTelescopeScope :: TermConfiguration -> Property
48
prop_splitTelescopeScope conf =
49
forAll (genC conf) $ \tel ->
50
forAll (listOfElements [0..size tel - 1]) $ \vs ->
51
let SplitTel tel1 tel2 perm = splitTelescope (Set.fromList vs) tel
52
tel' = telFromList (telToList tel1 ++ telToList tel2)
53
in isWellScoped conf tel'
55
-- | The permutation generated when splitting a telescope preserves scoping.
56
prop_splitTelescopePermScope :: TermConfiguration -> Property
57
prop_splitTelescopePermScope conf =
58
forAllShrink (genC conf) (shrinkC conf) $ \tel ->
59
forAllShrink (listOfElements [0..size tel - 1]) shrink $ \vs ->
60
let SplitTel tel1 tel2 perm = splitTelescope (Set.fromList vs) tel
61
conf1 = extendWithTelConf tel1 conf
62
conf2 = conf1 { tcFreeVariables = map (size tel2 +) (tcFreeVariables conf1) }
63
conf' = conf { tcFreeVariables = map (size tel +) (tcFreeVariables conf) ++ vs }
64
in forAllShrink (genC conf') (shrinkC conf') $ \t ->
65
isWellScoped conf2 (substs (renamingR $ invertP perm) (t :: Term))
68
-- | The permutation generated when splitting a telescope correctly translates
69
-- between the old and the new telescope.
70
prop_splitTelescopePermInv :: TermConfiguration -> Property
71
prop_splitTelescopePermInv conf =
72
forAll (wellScopedTel conf) $ \tel ->
73
forAll (listOfElements [0..size tel - 1]) $ \vs ->
74
let SplitTel tel1 tel2 perm = splitTelescope (Set.fromList vs) tel
75
tel' = telFromList (telToList tel1 ++ telToList tel2)
76
conf1 = extendWithTelConf tel conf
77
conf2 = extendWithTelConf tel' conf
78
in forAll (wellScopedTerm conf1) $ \t1 ->
79
forAll (wellScopedTerm conf2) $ \t2 ->
80
let t1' = rename (invertP perm) $ rename perm t1
81
t2' = rename perm $ rename (invertP perm) t2
82
in t1 == t1' && t2 == t2'
86
tests = runTests "Agda.TypeChecking.Tests"
87
[ quickCheck' prop_telToListInv
88
, quickCheck' prop_flattenTelScope
89
, quickCheck' prop_flattenTelInv
90
, quickCheck' prop_reorderTelStable
91
, quickCheck' prop_splitTelescopeScope
92
, quickCheck' prop_splitTelescopePermScope
added
removed
src/full/Agda/TypeChecking/Tests.hs
