module Agda.TypeChecking.Positivity.Occurrence where
import Control.DeepSeq
import Data.Typeable (Typeable)
import Test.QuickCheck
import Agda.Syntax.Position
import Agda.Utils.Null
import Agda.Utils.SemiRing
data Occurrence
= Mixed
| JustNeg
| JustPos
| StrictPos
| GuardPos
| Unused
deriving (Typeable, Show, Eq, Ord, Enum, Bounded)
instance NFData Occurrence where rnf x = seq x ()
instance KillRange Occurrence where
killRange = id
instance Arbitrary Occurrence where
arbitrary = elements [minBound .. maxBound]
shrink Unused = []
shrink _ = [Unused]
instance CoArbitrary Occurrence where
coarbitrary = coarbitrary . fromEnum
instance SemiRing Occurrence where
ozero = Unused
oone = StrictPos
oplus Mixed _ = Mixed
oplus _ Mixed = Mixed
oplus Unused o = o
oplus o Unused = o
oplus JustNeg JustNeg = JustNeg
oplus JustNeg o = Mixed
oplus o JustNeg = Mixed
oplus GuardPos o = o
oplus o GuardPos = o
oplus StrictPos o = o
oplus o StrictPos = o
oplus JustPos JustPos = JustPos
otimes Unused _ = Unused
otimes _ Unused = Unused
otimes Mixed _ = Mixed
otimes _ Mixed = Mixed
otimes JustNeg JustNeg = JustPos
otimes JustNeg _ = JustNeg
otimes _ JustNeg = JustNeg
otimes JustPos _ = JustPos
otimes _ JustPos = JustPos
otimes GuardPos _ = GuardPos
otimes _ GuardPos = GuardPos
otimes StrictPos StrictPos = StrictPos
instance StarSemiRing Occurrence where
ostar Mixed = Mixed
ostar JustNeg = Mixed
ostar JustPos = JustPos
ostar StrictPos = StrictPos
ostar GuardPos = StrictPos
ostar Unused = StrictPos
instance Null Occurrence where
empty = Unused
prop_Occurrence_oplus_associative ::
Occurrence -> Occurrence -> Occurrence -> Bool
prop_Occurrence_oplus_associative x y z =
oplus x (oplus y z) == oplus (oplus x y) z
prop_Occurrence_oplus_ozero :: Occurrence -> Bool
prop_Occurrence_oplus_ozero x =
oplus ozero x == x
prop_Occurrence_oplus_commutative :: Occurrence -> Occurrence -> Bool
prop_Occurrence_oplus_commutative x y =
oplus x y == oplus y x
prop_Occurrence_otimes_associative ::
Occurrence -> Occurrence -> Occurrence -> Bool
prop_Occurrence_otimes_associative x y z =
otimes x (otimes y z) == otimes (otimes x y) z
prop_Occurrence_otimes_oone :: Occurrence -> Bool
prop_Occurrence_otimes_oone x =
otimes oone x == x
&&
otimes x oone == x
prop_Occurrence_distributive ::
Occurrence -> Occurrence -> Occurrence -> Bool
prop_Occurrence_distributive x y z =
otimes x (oplus y z) == oplus (otimes x y) (otimes x z)
&&
otimes (oplus x y) z == oplus (otimes x z) (otimes y z)
prop_Occurrence_otimes_ozero :: Occurrence -> Bool
prop_Occurrence_otimes_ozero x =
otimes ozero x == ozero
&&
otimes x ozero == ozero
prop_Occurrence_ostar :: Occurrence -> Bool
prop_Occurrence_ostar x =
ostar x == oplus oone (otimes x (ostar x))
&&
ostar x == oplus oone (otimes (ostar x) x)
return []
tests :: IO Bool
tests = do
putStrLn "Agda.TypeChecking.Positivity.Occurrence"
$quickCheckAll