module Agda.TypeChecking.SizedTypes.Tests where
import Control.Applicative
import Test.QuickCheck
import Test.QuickCheck.All
import Agda.TypeChecking.SizedTypes.Syntax
import Agda.TypeChecking.SizedTypes.WarshallSolver
import Agda.TypeChecking.SizedTypes.Utils
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
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
propDioid_Gen :: Dioid a => a -> a -> a -> Bool
propDioid_Gen = propDioid meet top compose unitCompose
prop_Dioid_Weight :: Weight -> Weight -> Weight -> Bool
prop_Dioid_Weight x y z = propDioid_Gen x y z
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
return []
tests :: IO Bool
tests = do
putStrLn "Agda.TypeChecking.SizedTypes.Tests"
$quickCheckAll