| {-# LANGUAGE OverloadedStrings #-} |
|
|
| |
| |
| |
| |
| |
|
|
| module Test.StdLib.Setoid |
| ( tests |
| ) where |
|
|
| import Test.Tasty |
| import Test.Tasty.HUnit |
| import Test.Tasty.QuickCheck as QC |
| import qualified Data.Set as Set |
|
|
| import Assertica.Core.AST |
| import Assertica.Core.ProofTerm |
| import Assertica.StdLib.Setoid |
|
|
| |
| |
| |
|
|
| tests :: TestTree |
| tests = testGroup "Assertica.StdLib.Setoid" |
| [ testGroup "Trivial Setoid" |
| [ testCase "Trivial setoid carrier is Unit" testTrivialCarrier |
| , testCase "Trivial setoid reflexivity" testTrivialRefl |
| , testCase "Trivial setoid symmetry" testTrivialSymm |
| , testCase "Trivial setoid transitivity" testTrivialTrans |
| , testCase "Trivial setoid all elements equivalent" testTrivialAllEq |
| ] |
| , testGroup "Discrete Setoid" |
| [ testCase "Discrete setoid reflexivity" testDiscreteRefl |
| , testCase "Discrete setoid symmetry" testDiscreteSymm |
| , testCase "Discrete setoid transitivity" testDiscreteTrans |
| ] |
| , testGroup "Product Setoid" |
| [ testCase "Product setoid carrier" testProductCarrier |
| , testCase "Product setoid reflexivity" testProductRefl |
| , testCase "Product setoid pair equality" testProductPairEq |
| , testCase "Product setoid commutativity" testProductComm |
| ] |
| , testGroup "Setoid Morphisms" |
| [ testCase "Identity morphism preserves equivalence" testIdMorphismPreserves |
| , testCase "Identity morphism is left identity" testIdMorphismLeftId |
| , testCase "Identity morphism is right identity" testIdMorphismRightId |
| , testCase "Morphism composition" testMorphismComposition |
| , testCase "Composed morphism preserves equivalence" testComposedMorphismPreserves |
| ] |
| , testGroup "Proof Terms" |
| [ testCase "Reflexivity proof checks" testReflProofChecks |
| , testCase "Symmetry proof checks" testSymmProofChecks |
| , testCase "Transitivity proof checks" testTransProofChecks |
| ] |
| , testGroup "Equivalence Laws" |
| [ testCase "Reflexivity law holds" testReflLaw |
| , testCase "Symmetry law holds" testSymmLaw |
| , testCase "Transitivity law holds" testTransLaw |
| , testCase "Equivalence is reflexive everywhere" testReflEvery |
| , testCase "Equivalence is symmetric everywhere" testSymmEvery |
| , testCase "Equivalence is transitive everywhere" testTransEvery |
| ] |
| , testGroup "Setoid Morphism Laws" |
| [ testCase "Morphism preserves reflexivity" testMorphismReflPreserved |
| , testCase "Morphism preserves symmetry" testMorphismSymmPreserved |
| , testCase "Morphism preserves transitivity" testMorphismTransPreserved |
| ] |
| , testGroup "Determinism Tests" |
| [ testCase "Equivalence check is deterministic" testDeterminism |
| , testCase "Morphism application is deterministic" testMorphismDeterminism |
| ] |
| , testGroup "Negative Tests" |
| [ testCase "Reflexivity fails for unequal terms" testReflFails |
| , testCase "Symmetry proof is not involutive" testSymmNotInvolutive |
| ] |
| ] |
|
|
| |
| |
| |
|
|
| testTrivialCarrier :: Assertion |
| testTrivialCarrier = |
| let s = trivialSetoid |
| in setoidCarrier s @?= TConst (QName [] "Unit") |
|
|
| testTrivialRefl :: Assertion |
| testTrivialRefl = |
| let s = trivialSetoid |
| proof = setoidRefl s (Const UnitConst) |
| in proof @?= Refl |
|
|
| testTrivialSymm :: Assertion |
| testTrivialSymm = |
| let s = trivialSetoid |
| innerProof = setoidRefl s (Const UnitConst) |
| proof = setoidSymm s (Const UnitConst) (Const UnitConst) innerProof |
| in proof @?= Refl |
|
|
| testTrivialTrans :: Assertion |
| testTrivialTrans = |
| let s = trivialSetoid |
| proof1 = setoidRefl s (Const UnitConst) |
| proof2 = setoidRefl s (Const UnitConst) |
| proof = setoidTrans s (Const UnitConst) (Const UnitConst) (Const UnitConst) proof1 proof2 |
| in proof @?= Trans Refl Refl |
|
|
| testTrivialAllEq :: Assertion |
| testTrivialAllEq = |
| let s = trivialSetoid |
| prop1 = setoidEq s (Const UnitConst) (Const UnitConst) |
| prop2 = setoidEq s (Const UnitConst) (Const UnitConst) |
| in prop1 @?= prop2 |
|
|
| |
| |
| |
|
|
| testDiscreteRefl :: Assertion |
| testDiscreteRefl = |
| let s = discreteSetoid |
| a = Const (IntLit 42) |
| proof = setoidRefl s a |
| in proof @?= Refl |
|
|
| testDiscreteSymm :: Assertion |
| testDiscreteSymm = |
| let s = discreteSetoid |
| a = Const (IntLit 42) |
| innerProof = Refl |
| proof = setoidSymm s a a innerProof |
| in proof @?= Symm Refl |
|
|
| testDiscreteTrans :: Assertion |
| testDiscreteTrans = |
| let s = discreteSetoid |
| a = Const (IntLit 42) |
| proof1 = Refl |
| proof2 = Refl |
| proof = setoidTrans s a a a proof1 proof2 |
| in proof @?= Trans Refl Refl |
|
|
| |
| |
| |
|
|
| testProductCarrier :: Assertion |
| testProductCarrier = |
| let s1 = trivialSetoid |
| s2 = discreteSetoid |
| prod = productSetoid s1 s2 |
| carrier = setoidCarrier prod |
| in case carrier of |
| TPair {} -> assertBool "Product carrier is a pair" True |
| _ -> assertFailure "Product carrier should be a pair" |
|
|
| testProductRefl :: Assertion |
| testProductRefl = |
| let s1 = trivialSetoid |
| s2 = discreteSetoid |
| prod = productSetoid s1 s2 |
| pair = TPair (Const UnitConst) (Const (IntLit 1)) |
| proof = setoidRefl prod pair |
| in proof @?= Refl |
|
|
| testProductPairEq :: Assertion |
| testProductPairEq = |
| let s1 = trivialSetoid |
| s2 = discreteSetoid |
| prod = productSetoid s1 s2 |
| a1 = Const UnitConst |
| b1 = Const (IntLit 1) |
| a2 = Const UnitConst |
| b2 = Const (IntLit 1) |
| p1 = TPair a1 b1 |
| p2 = TPair a2 b2 |
| prop = setoidEq prod p1 p2 |
| in case prop of |
| ConjunctionProp {} -> assertBool "Product equality is a conjunction" True |
| _ -> assertFailure "Product equality should be a conjunction" |
|
|
| testProductComm :: Assertion |
| testProductComm = |
| let s1 = trivialSetoid |
| s2 = discreteSetoid |
| prod = productSetoid s1 s2 |
| p1 = TPair (Const UnitConst) (Const (IntLit 1)) |
| p2 = TPair (Const UnitConst) (Const (IntLit 1)) |
| proof1 = setoidSymm prod p1 p2 Refl |
| proof2 = setoidSymm prod p1 p2 Refl |
| in proof1 @?= proof2 |
|
|
| |
| |
| |
|
|
| testIdMorphismPreserves :: Assertion |
| testIdMorphismPreserves = |
| let s = trivialSetoid |
| morph = idMorphism s |
| a = Const UnitConst |
| b = Const UnitConst |
| eqProof = Refl |
| result = morphismPreservesEq morph a b eqProof |
| in result @?= Refl |
|
|
| testIdMorphismLeftId :: Assertion |
| testIdMorphismLeftId = |
| let s = discreteSetoid |
| id_s = idMorphism s |
| a = Const (IntLit 42) |
| fa = morphismMap id_s a |
| in fa @?= a |
|
|
| testIdMorphismRightId :: Assertion |
| testIdMorphismRightId = |
| let s = discreteSetoid |
| id_s = idMorphism s |
| b = Const (IntLit 42) |
| gb = morphismMap id_s b |
| in gb @?= b |
|
|
| testMorphismComposition :: Assertion |
| testMorphismComposition = |
| let s1 = trivialSetoid |
| s2 = discreteSetoid |
| s3 = trivialSetoid |
| f = SetoidMorphism |
| { morphismSource = s1 |
| , morphismTarget = s2 |
| , morphismMap = \a -> Const (IntLit 1) |
| , morphismProof = \_ _ _ -> Refl |
| } |
| g = SetoidMorphism |
| { morphismSource = s2 |
| , morphismTarget = s3 |
| , morphismMap = \_ -> Const UnitConst |
| , morphismProof = \_ _ _ -> Refl |
| } |
| composed = composeMorphisms f g |
| in morphismSource composed @?= s1 && morphismTarget composed @?= s3 |
|
|
| testComposedMorphismPreserves :: Assertion |
| testComposedMorphismPreserves = |
| let s1 = trivialSetoid |
| s2 = discreteSetoid |
| s3 = trivialSetoid |
| f = idMorphism s2 |
| g = idMorphism s3 |
| composed = composeMorphisms f g |
| a = Const (IntLit 42) |
| b = Const (IntLit 42) |
| eqProof = Refl |
| result = morphismPreservesEq composed a b eqProof |
| in result @?= Refl |
|
|
| |
| |
| |
|
|
| testReflProofChecks :: Assertion |
| testReflProofChecks = |
| let s = discreteSetoid |
| a = Const (IntLit 42) |
| proof = setoidRefl s a |
| prop = EqualityProp a a |
| result = proofChecks proof prop |
| in case result of |
| Right () -> assertBool "Reflexivity proof checks" True |
| Left err -> assertFailure $ "Proof should check: " ++ show err |
|
|
| testSymmProofChecks :: Assertion |
| testSymmProofChecks = |
| let s = discreteSetoid |
| a = Const (IntLit 42) |
| innerProof = Refl |
| proof = setoidSymm s a a innerProof |
| prop = EqualityProp a a |
| result = proofChecks proof prop |
| in case result of |
| Right () -> assertBool "Symmetry proof checks" True |
| Left err -> assertFailure $ "Proof should check: " ++ show err |
|
|
| testTransProofChecks :: Assertion |
| testTransProofChecks = |
| let s = discreteSetoid |
| a = Const (IntLit 42) |
| proof1 = Refl |
| proof2 = Refl |
| proof = setoidTrans s a a a proof1 proof2 |
| prop = EqualityProp a a |
| result = proofChecks proof prop |
| in case result of |
| Right () -> assertBool "Transitivity proof checks" True |
| Left err -> assertFailure $ "Proof should check: " ++ show err |
|
|
| |
| |
| |
|
|
| testReflLaw :: Assertion |
| testReflLaw = |
| let s = discreteSetoid |
| a = Const (IntLit 42) |
| proof = setoidRefl s a |
| prop = EqualityProp a a |
| in proofChecks proof prop `shouldSucceed` () |
|
|
| testSymmLaw :: Assertion |
| testSymmLaw = |
| let s = discreteSetoid |
| a = Const (IntLit 42) |
| proof1 = setoidRefl s a |
| proof2 = setoidSymm s a a proof1 |
| prop = EqualityProp a a |
| in proofChecks proof2 prop `shouldSucceed` () |
|
|
| testTransLaw :: Assertion |
| testTransLaw = |
| let s = discreteSetoid |
| a = Const (IntLit 42) |
| proof1 = setoidRefl s a |
| proof2 = setoidRefl s a |
| proof3 = setoidTrans s a a a proof1 proof2 |
| prop = EqualityProp a a |
| in proofChecks proof3 prop `shouldSucceed` () |
|
|
| testReflEvery :: Assertion |
| testReflEvery = |
| let s = discreteSetoid |
| elements = [Const (IntLit 1), Const (IntLit 2), Const UnitConst] |
| results = map (\a -> (a, setoidRefl s a)) elements |
| in all (\(_, proof) -> proofChecks proof (EqualityProp (Const (IntLit 1)) (Const (IntLit 1))) == Right ()) |
| results |
| @? "All elements satisfy reflexivity" |
|
|
| testSymmEvery :: Assertion |
| testSymmEvery = |
| let s = discreteSetoid |
| a = Const (IntLit 42) |
| proof1 = Refl |
| proof2 = setoidSymm s a a proof1 |
| in proofChecks proof2 (EqualityProp a a) `shouldSucceed` () |
|
|
| testTransEvery :: Assertion |
| testTransEvery = |
| let s = discreteSetoid |
| a = Const (IntLit 42) |
| proof1 = Refl |
| proof2 = Refl |
| proof3 = setoidTrans s a a a proof1 proof2 |
| in proofChecks proof3 (EqualityProp a a) `shouldSucceed` () |
|
|
| |
| |
| |
|
|
| testMorphismReflPreserved :: Assertion |
| testMorphismReflPreserved = |
| let s1 = discreteSetoid |
| s2 = discreteSetoid |
| morph = idMorphism s1 |
| a = Const (IntLit 42) |
| reflProof = setoidRefl s1 a |
| result = morphismPreservesEq morph a a reflProof |
| in result @?= Refl |
|
|
| testMorphismSymmPreserved :: Assertion |
| testMorphismSymmPreserved = |
| let s1 = discreteSetoid |
| morph = idMorphism s1 |
| a = Const (IntLit 42) |
| symmProof = Symm Refl |
| result = morphismPreservesEq morph a a symmProof |
| in result @?= Symm Refl |
|
|
| testMorphismTransPreserved :: Assertion |
| testMorphismTransPreserved = |
| let s1 = discreteSetoid |
| morph = idMorphism s1 |
| a = Const (IntLit 42) |
| transProof = Trans Refl Refl |
| result = morphismPreservesEq morph a a transProof |
| in result @?= Trans Refl Refl |
|
|
| |
| |
| |
|
|
| testDeterminism :: Assertion |
| testDeterminism = |
| let s = discreteSetoid |
| a = Const (IntLit 42) |
| proof1 = setoidRefl s a |
| proof2 = setoidRefl s a |
| in proof1 @?= proof2 |
|
|
| testMorphismDeterminism :: Assertion |
| testMorphismDeterminism = |
| let s = discreteSetoid |
| morph = idMorphism s |
| a = Const (IntLit 42) |
| result1 = morphismMap morph a |
| result2 = morphismMap morph a |
| in result1 @?= result2 |
|
|
| |
| |
| |
|
|
| testReflFails :: Assertion |
| testReflFails = |
| let a = Const (IntLit 42) |
| b = Const (IntLit 43) |
| proof = Refl |
| prop = EqualityProp a b |
| result = proofChecks proof prop |
| in case result of |
| Left _ -> assertBool "Reflexivity correctly fails" True |
| Right () -> assertFailure "Reflexivity should fail for unequal terms" |
|
|
| testSymmNotInvolutive :: Assertion |
| testSymmNotInvolutive = |
| let proof1 = Refl |
| proof2 = Symm proof1 |
| proof3 = Symm proof2 |
| in proof3 @?= Refl |
|
|
| |
| |
| |
|
|
| shouldSucceed :: Either e a -> a -> Assertion |
| shouldSucceed (Right x) expected = x @?= expected |
| shouldSucceed (Left err) _ = assertFailure $ "Expected success, got error: " ++ show err |
|
|
| |
| _propTest :: String -> Bool -> TestTree |
| _propTest name prop = testCase name $ assertBool name prop |
|
|
