summaryrefslogtreecommitdiff
path: root/src/full/Agda/TypeChecking/SizedTypes/Tests.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/TypeChecking/SizedTypes/Tests.hs')
-rw-r--r--src/full/Agda/TypeChecking/SizedTypes/Tests.hs145
1 files changed, 0 insertions, 145 deletions
diff --git a/src/full/Agda/TypeChecking/SizedTypes/Tests.hs b/src/full/Agda/TypeChecking/SizedTypes/Tests.hs
deleted file mode 100644
index 2a0acad..0000000
--- a/src/full/Agda/TypeChecking/SizedTypes/Tests.hs
+++ /dev/null
@@ -1,145 +0,0 @@
-{-# LANGUAGE TemplateHaskell #-}
-
-module Agda.TypeChecking.SizedTypes.Tests where
-
-import Test.QuickCheck
-
-import Agda.TypeChecking.SizedTypes.Syntax
-import Agda.TypeChecking.SizedTypes.WarshallSolver
-import Agda.TypeChecking.SizedTypes.Utils
-
--- * Label interpretation
-
-type Relation a = a -> a -> Bool
-
-class AsWeightRelation b where
- eval :: b -> Relation Weight
-
-instance AsWeightRelation Cmp where
- eval Le = (<=)
- eval Lt = (<)
-
-instance AsWeightRelation Label where
- eval (Label cmp w) x y = eval cmp x (y `plus` w)
- eval LInf _ _ = True
-
-prop_MeetSound :: Label -> Label -> Weight -> Weight -> Property
-prop_MeetSound l l' x y =
- eval l x y && eval l' x y ==> eval (meet l l') x y
-
-prop_MeetComplete :: Label -> Label -> Weight -> Weight -> Property
-prop_MeetComplete l l' x y =
- eval (meet l l') x y ==> eval l x y && eval l' x y
-
-prop_ComposeSound :: Label -> Label -> Weight -> Weight -> Weight -> Property
-prop_ComposeSound l1 l2 x y z =
- eval l1 x y && eval l2 y z ==> eval (compose l1 l2) x z
-
-prop_ComposeComplete :: Label -> Label -> Offset -> Weight -> Property
-prop_ComposeComplete l1 l2 k z = let x = Offset k in
- eval (compose l1 l2) x z ==>
- let y = z + toWeight l2
- in eval l1 x y -- && eval l2 y z -- does not hold for l2 = \infty
- -- Andreas, 2014-05-20, Issue 1134
- -- If we replace the \infty with its unicode, issue 1134 is triggered:
- -- "... GHC 7.6.3 and quickcheck 2.6.
- -- It turns out that for some reason Gentoo eclass unsets locale
- -- to POSIX when building haskell packages. So the issue is easy
- -- to reproduce with `LANG=POSIX ./setup build`."
- --
- -- Funnily, the offending unicode symbol is in a comment.
- -- Some issue for TemplateHaskell / QuickCheck.
-
--- * Generic properties
-
-propCommutative :: Eq b => (a -> a -> b) -> a -> a -> Bool
-propCommutative o x y = x `o` y == y `o` x
-
-propAssociative :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool
-propAssociative o x y z = x `o` (y `o` z) == (x `o` y) `o` z
-
-propIdempotent :: Eq a => (a -> a -> a) -> a -> Bool
-propIdempotent o x = (x `o` x) == x
-
-propUnit :: Eq a => (a -> a -> a) -> a -> a -> Bool
-propUnit o u x = u `o` x == x && x `o` u == x
-
-propZero :: Eq a => (a -> a -> a) -> a -> a -> Bool
-propZero o z x = z `o` x == z && x `o` z == z
-
-propDistL :: Eq b => (a -> b -> b) -> (b -> b -> b) -> a -> b -> b -> Bool
-propDistL o p x y z = x `o` (y `p` z) == (x `o` y) `p` (x `o` z)
-
-propDistR :: Eq a => (a -> b -> a) -> (a -> a -> a) -> a -> a -> b -> Bool
-propDistR o p x y z = (x `p` y) `o` z == (x `o` z) `p` (y `o` z)
-
-propDistributive :: Eq a =>
- (a -> a -> a) -> (a -> a -> a) -> a -> a -> a -> Bool
-propDistributive o p x y z = propDistL o p x y z && propDistR o p x y z
-
-propSemiLattice :: Eq a => (a -> a -> a) -> a -> a -> a -> Bool
-propSemiLattice o x y z =
- propCommutative o x y && propAssociative o x y z && propIdempotent o x
-
-propBoundedSemiLattice :: Eq a => (a -> a -> a) -> a -> a -> a -> a -> Bool
-propBoundedSemiLattice o u x y z = propSemiLattice o x y z && propUnit o u x
-
-propMonoid :: Eq a => (a -> a -> a) -> a -> a -> a -> a -> Bool
-propMonoid o u x y z = propAssociative o x y z && propUnit o u x
-
-propDioid :: Eq a =>
- (a -> a -> a) -> a -> (a -> a -> a) -> a -> a -> a -> a -> Bool
-propDioid p n o u x y z = propBoundedSemiLattice p n x y z
- && propMonoid o u x y z
- && propDistributive o p x y z
- && propZero o n x
-
--- | Properties of 'Dioid' class.
-propDioid_Gen :: Dioid a => a -> a -> a -> Bool
-propDioid_Gen = propDioid meet top compose unitCompose
-
--- | @Weight@ instance.
-prop_Dioid_Weight :: Weight -> Weight -> Weight -> Bool
-prop_Dioid_Weight x y z = propDioid_Gen x y z
-
--- | @Label@ instance.
-prop_SemiLattice_Label :: Label -> Label -> Label -> Bool
-prop_SemiLattice_Label x y z = propSemiLattice meet x y z
-
-prop_Unit_Label :: Label -> Bool
-prop_Unit_Label x = propUnit meet top x
-
-prop_BoundedSemiLattice_Label :: Label -> Label -> Label -> Bool
-prop_BoundedSemiLattice_Label x y z = propBoundedSemiLattice meet top x y z
-
-prop_Monoid_Label :: Label -> Label -> Label -> Bool
-prop_Monoid_Label x y z = propMonoid compose unitCompose x y z
-
-prop_DistL_Label :: Label -> Label -> Label -> Bool
-prop_DistL_Label x y z = propDistL compose meet x y z
-
-prop_DistR_Label :: Label -> Label -> Label -> Bool
-prop_DistR_Label x y z = propDistR compose meet x y z
-
-prop_Dist_Label :: Label -> Label -> Label -> Bool
-prop_Dist_Label x y z = propDistributive compose meet x y z
-
-prop_Zero_Label :: Label -> Bool
-prop_Zero_Label x = propZero compose top x
-
-prop_Dioid_Label :: Label -> Label -> Label -> Bool
-prop_Dioid_Label x y z = propDioid_Gen x y z
-
-------------------------------------------------------------------------
--- * All tests
-------------------------------------------------------------------------
-
--- Template Haskell hack to make the following $quickCheckAll work
--- under ghc-7.8.
-return [] -- KEEP!
-
--- | Runs all tests starting with "prop_" in this file.
-tests :: IO Bool
-tests = do
- putStrLn "Agda.TypeChecking.SizedTypes.Tests"
- $quickCheckAll