| {-# LANGUAGE OverloadedStrings #-} |
|
|
| |
| |
| |
| |
| |
|
|
| module Test.StdLib.Lattice |
| ( tests |
| ) where |
|
|
| import Test.Tasty |
| import Test.Tasty.HUnit |
| import Test.Tasty.QuickCheck as QC |
|
|
| import Assertica.Core.AST |
| import Assertica.Core.ProofTerm |
| import Assertica.StdLib.Setoid |
| import Assertica.StdLib.Lattice |
|
|
| |
| |
| |
|
|
| tests :: TestTree |
| tests = testGroup "Assertica.StdLib.Lattice" |
| [ testGroup "Boolean Lattice" |
| [ testCase "Boolean lattice carrier" testBooleanCarrier |
| , testCase "Boolean join operation" testBooleanJoin |
| , testCase "Boolean meet operation" testBooleanMeet |
| , testCase "Boolean join reflexivity" testBooleanJoinRefl |
| , testCase "Boolean meet reflexivity" testBooleanMeetRefl |
| ] |
| , testGroup "Trivial Lattice" |
| [ testCase "Trivial lattice carrier" testTrivialLatticeCarrier |
| , testCase "Trivial lattice join" testTrivialLatticeJoin |
| , testCase "Trivial lattice meet" testTrivialLatticeMeet |
| ] |
| , testGroup "Join Operation Properties" |
| [ testCase "Join associativity" testJoinAssociativity |
| , testCase "Join commutativity" testJoinCommutativity |
| , testCase "Join idempotence" testJoinIdempotence |
| , testCase "Join preserves equivalence (left)" testJoinPreservesEqLeft |
| , testCase "Join preserves equivalence (right)" testJoinPreservesEqRight |
| ] |
| , testGroup "Meet Operation Properties" |
| [ testCase "Meet associativity" testMeetAssociativity |
| , testCase "Meet commutativity" testMeetCommutativity |
| , testCase "Meet idempotence" testMeetIdempotence |
| , testCase "Meet preserves equivalence (left)" testMeetPreservesEqLeft |
| , testCase "Meet preserves equivalence (right)" testMeetPreservesEqRight |
| ] |
| , testGroup "Lattice Homomorphisms" |
| [ testCase "Identity homomorphism" testIdentityHomomorphism |
| , testCase "Identity preserves join" testIdPreservesJoin |
| , testCase "Identity preserves meet" testIdPreservesMeet |
| , testCase "Homomorphism composition" testHomomorphismComposition |
| ] |
| , testGroup "Proof Term Checking" |
| [ testCase "Join associativity proof checks" testJoinAssocProofChecks |
| , testCase "Join commutativity proof checks" testJoinCommProofChecks |
| , testCase "Join idempotence proof checks" testJoinIdempProofChecks |
| , testCase "Meet associativity proof checks" testMeetAssocProofChecks |
| , testCase "Meet commutativity proof checks" testMeetCommProofChecks |
| , testCase "Meet idempotence proof checks" testMeetIdempProofChecks |
| ] |
| , testGroup "Lattice Laws Interplay" |
| [ testCase "Join and meet compatibility" testJoinMeetCompat |
| , testCase "Join properties hold simultaneously" testJoinPropsSimultaneous |
| , testCase "Meet properties hold simultaneously" testMeetPropsSimultaneous |
| ] |
| , testGroup "Determinism Tests" |
| [ testCase "Join operation is deterministic" testJoinDeterminism |
| , testCase "Meet operation is deterministic" testMeetDeterminism |
| , testCase "Proof generation is deterministic" testProofDeterminism |
| ] |
| , testGroup "Negative Tests" |
| [ testCase "Different elements don't unify wrongly" testElementsDifferent |
| ] |
| ] |
|
|
| |
| |
| |
|
|
| testBooleanCarrier :: Assertion |
| testBooleanCarrier = |
| let carrier = latticeCarrier booleanLattice |
| setoidCarrier' = setoidCarrier carrier |
| in case setoidCarrier' of |
| TConst (QName [] "Bool") -> assertBool "Boolean lattice carrier is Bool" True |
| _ -> assertFailure "Boolean lattice carrier should be Bool" |
|
|
| testBooleanJoin :: Assertion |
| testBooleanJoin = |
| let result = join booleanLattice (Const (BoolLit True)) (Const (BoolLit False)) |
| in case result of |
| Constr (QName [] "or") [_, _] -> assertBool "Join creates OR constructor" True |
| _ -> assertFailure "Join should create 'or' constructor" |
|
|
| testBooleanMeet :: Assertion |
| testBooleanMeet = |
| let result = meet booleanLattice (Const (BoolLit True)) (Const (BoolLit False)) |
| in case result of |
| Constr (QName [] "and") [_, _] -> assertBool "Meet creates AND constructor" True |
| _ -> assertFailure "Meet should create 'and' constructor" |
|
|
| testBooleanJoinRefl :: Assertion |
| testBooleanJoinRefl = |
| let proof = joinAssociativity booleanLattice |
| (Const (BoolLit True)) |
| (Const (BoolLit False)) |
| (Const (BoolLit True)) |
| in proof @?= Refl |
|
|
| testBooleanMeetRefl :: Assertion |
| testBooleanMeetRefl = |
| let proof = meetAssociativity booleanLattice |
| (Const (BoolLit True)) |
| (Const (BoolLit False)) |
| (Const (BoolLit True)) |
| in proof @?= Refl |
|
|
| |
| |
| |
|
|
| testTrivialLatticeCarrier :: Assertion |
| testTrivialLatticeCarrier = |
| let carrier = latticeCarrier trivialLattice |
| setoidCarrier' = setoidCarrier carrier |
| in case setoidCarrier' of |
| TConst (QName [] "Unit") -> assertBool "Trivial lattice carrier is Unit" True |
| _ -> assertFailure "Trivial lattice carrier should be Unit" |
|
|
| testTrivialLatticeJoin :: Assertion |
| testTrivialLatticeJoin = |
| let result = join trivialLattice (Const UnitConst) (Const UnitConst) |
| in result @?= Const UnitConst |
|
|
| testTrivialLatticeMeet :: Assertion |
| testTrivialLatticeMeet = |
| let result = meet trivialLattice (Const UnitConst) (Const UnitConst) |
| in result @?= Const UnitConst |
|
|
| |
| |
| |
|
|
| testJoinAssociativity :: Assertion |
| testJoinAssociativity = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| c = Const (BoolLit True) |
| proof = joinAssociativity booleanLattice a b c |
| in proof @?= Refl |
|
|
| testJoinCommutativity :: Assertion |
| testJoinCommutativity = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = joinCommutativity booleanLattice a b |
| in proof @?= Refl |
|
|
| testJoinIdempotence :: Assertion |
| testJoinIdempotence = |
| let a = Const (BoolLit True) |
| proof = joinIdempotence booleanLattice a |
| in proof @?= Refl |
|
|
| testJoinPreservesEqLeft :: Assertion |
| testJoinPreservesEqLeft = |
| let a = Const (BoolLit True) |
| a' = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = preserveJoin booleanLattice a a' b b Refl Refl |
| in proof @?= Refl |
|
|
| testJoinPreservesEqRight :: Assertion |
| testJoinPreservesEqRight = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| b' = Const (BoolLit False) |
| proof = preserveJoin booleanLattice a a b b' Refl Refl |
| in proof @?= Refl |
|
|
| |
| |
| |
|
|
| testMeetAssociativity :: Assertion |
| testMeetAssociativity = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| c = Const (BoolLit True) |
| proof = meetAssociativity booleanLattice a b c |
| in proof @?= Refl |
|
|
| testMeetCommutativity :: Assertion |
| testMeetCommutativity = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = meetCommutativity booleanLattice a b |
| in proof @?= Refl |
|
|
| testMeetIdempotence :: Assertion |
| testMeetIdempotence = |
| let a = Const (BoolLit True) |
| proof = meetIdempotence booleanLattice a |
| in proof @?= Refl |
|
|
| testMeetPreservesEqLeft :: Assertion |
| testMeetPreservesEqLeft = |
| let a = Const (BoolLit True) |
| a' = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = preserveMeet booleanLattice a a' b b Refl Refl |
| in proof @?= Refl |
|
|
| testMeetPreservesEqRight :: Assertion |
| testMeetPreservesEqRight = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| b' = Const (BoolLit False) |
| proof = preserveMeet booleanLattice a a b b' Refl Refl |
| in proof @?= Refl |
|
|
| |
| |
| |
|
|
| testIdentityHomomorphism :: Assertion |
| testIdentityHomomorphism = |
| let hom = LatticeHomomorphism |
| { homSource = booleanLattice |
| , homTarget = booleanLattice |
| , homMap = id |
| , homPreservesJoin = \_ _ -> Refl |
| , homPreservesMeet = \_ _ -> Refl |
| } |
| a = Const (BoolLit True) |
| in homMap hom a @?= a |
|
|
| testIdPreservesJoin :: Assertion |
| testIdPreservesJoin = |
| let hom = LatticeHomomorphism |
| { homSource = booleanLattice |
| , homTarget = booleanLattice |
| , homMap = id |
| , homPreservesJoin = \_ _ -> Refl |
| , homPreservesMeet = \_ _ -> Refl |
| } |
| a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = homPreservesJoin hom a b |
| in proof @?= Refl |
|
|
| testIdPreservesMeet :: Assertion |
| testIdPreservesMeet = |
| let hom = LatticeHomomorphism |
| { homSource = booleanLattice |
| , homTarget = booleanLattice |
| , homMap = id |
| , homPreservesJoin = \_ _ -> Refl |
| , homPreservesMeet = \_ _ -> Refl |
| } |
| a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = homPreservesMeet hom a b |
| in proof @?= Refl |
|
|
| testHomomorphismComposition :: Assertion |
| testHomomorphismComposition = |
| let hom1 = LatticeHomomorphism |
| { homSource = booleanLattice |
| , homTarget = booleanLattice |
| , homMap = id |
| , homPreservesJoin = \_ _ -> Refl |
| , homPreservesMeet = \_ _ -> Refl |
| } |
| hom2 = LatticeHomomorphism |
| { homSource = booleanLattice |
| , homTarget = booleanLattice |
| , homMap = id |
| , homPreservesJoin = \_ _ -> Refl |
| , homPreservesMeet = \_ _ -> Refl |
| } |
| a = Const (BoolLit True) |
| composed = homMap hom1 (homMap hom2 a) |
| in composed @?= a |
|
|
| |
| |
| |
|
|
| testJoinAssocProofChecks :: Assertion |
| testJoinAssocProofChecks = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| c = Const (BoolLit True) |
| proof = joinAssociativity booleanLattice a b c |
| |
| lhs = join booleanLattice (join booleanLattice a b) c |
| rhs = join booleanLattice a (join booleanLattice b c) |
| prop = EqualityProp lhs rhs |
| result = proofChecks proof prop |
| in case result of |
| Right () -> assertBool "Join associativity proof checks" True |
| Left err -> assertFailure $ "Proof should check: " ++ show err |
|
|
| testJoinCommProofChecks :: Assertion |
| testJoinCommProofChecks = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = joinCommutativity booleanLattice a b |
| |
| lhs = join booleanLattice a b |
| rhs = join booleanLattice b a |
| prop = EqualityProp lhs rhs |
| result = proofChecks proof prop |
| in case result of |
| Right () -> assertBool "Join commutativity proof checks" True |
| Left err -> assertFailure $ "Proof should check: " ++ show err |
|
|
| testJoinIdempProofChecks :: Assertion |
| testJoinIdempProofChecks = |
| let a = Const (BoolLit True) |
| proof = joinIdempotence booleanLattice a |
| |
| lhs = join booleanLattice a a |
| rhs = a |
| prop = EqualityProp lhs rhs |
| result = proofChecks proof prop |
| in case result of |
| Right () -> assertBool "Join idempotence proof checks" True |
| Left err -> assertFailure $ "Proof should check: " ++ show err |
|
|
| testMeetAssocProofChecks :: Assertion |
| testMeetAssocProofChecks = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| c = Const (BoolLit True) |
| proof = meetAssociativity booleanLattice a b c |
| |
| lhs = meet booleanLattice (meet booleanLattice a b) c |
| rhs = meet booleanLattice a (meet booleanLattice b c) |
| prop = EqualityProp lhs rhs |
| result = proofChecks proof prop |
| in case result of |
| Right () -> assertBool "Meet associativity proof checks" True |
| Left err -> assertFailure $ "Proof should check: " ++ show err |
|
|
| testMeetCommProofChecks :: Assertion |
| testMeetCommProofChecks = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof = meetCommutativity booleanLattice a b |
| |
| lhs = meet booleanLattice a b |
| rhs = meet booleanLattice b a |
| prop = EqualityProp lhs rhs |
| result = proofChecks proof prop |
| in case result of |
| Right () -> assertBool "Meet commutativity proof checks" True |
| Left err -> assertFailure $ "Proof should check: " ++ show err |
|
|
| testMeetIdempProofChecks :: Assertion |
| testMeetIdempProofChecks = |
| let a = Const (BoolLit True) |
| proof = meetIdempotence booleanLattice a |
| |
| lhs = meet booleanLattice a a |
| rhs = a |
| prop = EqualityProp lhs rhs |
| result = proofChecks proof prop |
| in case result of |
| Right () -> assertBool "Meet idempotence proof checks" True |
| Left err -> assertFailure $ "Proof should check: " ++ show err |
|
|
| |
| |
| |
|
|
| testJoinMeetCompat :: Assertion |
| testJoinMeetCompat = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| join_result = join booleanLattice a b |
| meet_result = meet booleanLattice a b |
| in (join_result /= meet_result) @? "Join and meet produce different results" |
|
|
| testJoinPropsSimultaneous :: Assertion |
| testJoinPropsSimultaneous = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| c = Const (BoolLit True) |
| assoc = joinAssociativity booleanLattice a b c |
| comm = joinCommutativity booleanLattice a b |
| idemp = joinIdempotence booleanLattice a |
| in (assoc @?= Refl) >> (comm @?= Refl) >> (idemp @?= Refl) |
|
|
| testMeetPropsSimultaneous :: Assertion |
| testMeetPropsSimultaneous = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| c = Const (BoolLit True) |
| assoc = meetAssociativity booleanLattice a b c |
| comm = meetCommutativity booleanLattice a b |
| idemp = meetIdempotence booleanLattice a |
| in (assoc @?= Refl) >> (comm @?= Refl) >> (idemp @?= Refl) |
|
|
| |
| |
| |
|
|
| testJoinDeterminism :: Assertion |
| testJoinDeterminism = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| result1 = join booleanLattice a b |
| result2 = join booleanLattice a b |
| in result1 @?= result2 |
|
|
| testMeetDeterminism :: Assertion |
| testMeetDeterminism = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| result1 = meet booleanLattice a b |
| result2 = meet booleanLattice a b |
| in result1 @?= result2 |
|
|
| testProofDeterminism :: Assertion |
| testProofDeterminism = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| proof1 = joinCommutativity booleanLattice a b |
| proof2 = joinCommutativity booleanLattice a b |
| in proof1 @?= proof2 |
|
|
| |
| |
| |
|
|
| testElementsDifferent :: Assertion |
| testElementsDifferent = |
| let a = Const (BoolLit True) |
| b = Const (BoolLit False) |
| in a /= b @? "Different boolean values should not be equal" |
|
|
