| |
| |
| |
| |
| |
| |
| |
|
|
| module Test.Core.Assertion (tests) where |
|
|
| import Test.Tasty |
| import Test.Tasty.HUnit |
| import Test.Tasty.QuickCheck |
|
|
| import Assertica.Core.AST |
| import Assertica.Core.Assertion |
|
|
| tests :: TestTree |
| tests = testGroup "Assertica.Core.Assertion" |
| [ assertionConstructionTests |
| , obligationStoreTests |
| , propositionUtilityTests |
| ] |
|
|
| |
| assertionConstructionTests :: TestTree |
| assertionConstructionTests = testGroup "Assertion Construction" |
| [ testCase "Create a simple assertion" $ |
| let x = Var "x" |
| y = Var "y" |
| prop = EqualityProp (TVar x) (TVar y) |
| loc = SourceLoc "test.assertica" 1 1 |
| assertion = mkAssertion "eq_test" prop loc |
| in assertionName assertion @?= "eq_test" |
|
|
| , testCase "Assertion maintains proposition" $ |
| let x = Var "x" |
| prop = EqualityProp (TVar x) (TConst "5") |
| loc = SourceLoc "test.assertica" 1 1 |
| assertion = mkAssertion "const_eq" prop loc |
| in assertionProp assertion @?= prop |
|
|
| , testCase "Assertion maintains source location" $ |
| let x = Var "x" |
| prop = EqualityProp (TVar x) (TConst "5") |
| loc = SourceLoc "test.assertica" 42 7 |
| assertion = mkAssertion "test" prop loc |
| in assertionLoc assertion @?= loc |
| ] |
|
|
| |
| obligationStoreTests :: TestTree |
| obligationStoreTests = testGroup "Obligation Store" |
| [ testCase "Empty store is empty" $ |
| length (getObligations emptyStore) @?= 0 |
|
|
| , testCase "Insert obligation into store" $ |
| let x = Var "x" |
| prop = EqualityProp (TVar x) (TConst "5") |
| loc = SourceLoc "test.assertica" 1 1 |
| assertion = mkAssertion "test1" prop loc |
| store = insertObligation assertion emptyStore |
| in length (getObligations store) @?= 1 |
|
|
| , testCase "Look up obligation by name" $ |
| let x = Var "x" |
| prop = EqualityProp (TVar x) (TConst "5") |
| loc = SourceLoc "test.assertica" 1 1 |
| assertion = mkAssertion "test_lookup" prop loc |
| store = insertObligation assertion emptyStore |
| in case lookupObligation "test_lookup" store of |
| Just ob -> obligationState ob @?= Asserted |
| Nothing -> False @?= True |
|
|
| , testCase "Obligation starts in Asserted state" $ |
| let x = Var "x" |
| prop = EqualityProp (TVar x) (TConst "5") |
| loc = SourceLoc "test.assertica" 1 1 |
| assertion = mkAssertion "test_asserted" prop loc |
| store = insertObligation assertion emptyStore |
| in case lookupObligation "test_asserted" store of |
| Just ob -> obligationState ob @?= Asserted |
| Nothing -> False @?= True |
|
|
| , testCase "Mark obligation as proven" $ |
| let x = Var "x" |
| prop = EqualityProp (TVar x) (TConst "5") |
| loc = SourceLoc "test.assertica" 1 1 |
| assertion = mkAssertion "test_proven" prop loc |
| store = insertObligation assertion emptyStore |
| in case markProven "test_proven" (Just "proof_term_1") store of |
| Right store' -> |
| case lookupObligation "test_proven" store' of |
| Just ob -> obligationState ob @?= Proven |
| Nothing -> False @?= True |
| Left _ -> False @?= True |
|
|
| , testCase "Mark obligation as unproven" $ |
| let x = Var "x" |
| prop = EqualityProp (TVar x) (TConst "5") |
| loc = SourceLoc "test.assertica" 1 1 |
| assertion = mkAssertion "test_unproven" prop loc |
| store = insertObligation assertion emptyStore |
| in case markUnproven "test_unproven" store of |
| Right store' -> |
| case lookupObligation "test_unproven" store' of |
| Just ob -> obligationState ob @?= Unproven |
| Nothing -> False @?= True |
| Left _ -> False @?= True |
|
|
| , testCase "Check allProven when all proven" $ |
| let x = Var "x" |
| prop = EqualityProp (TVar x) (TConst "5") |
| loc = SourceLoc "test.assertica" 1 1 |
| assertion = mkAssertion "test_all_proven" prop loc |
| store = insertObligation assertion emptyStore |
| in case markProven "test_all_proven" Nothing store of |
| Right store' -> allProven store' @?= True |
| Left _ -> False @?= True |
|
|
| , testCase "Check allProven when some unproven" $ |
| let x = Var "x" |
| prop1 = EqualityProp (TVar x) (TConst "5") |
| prop2 = EqualityProp (TConst "1") (TConst "1") |
| loc = SourceLoc "test.assertica" 1 1 |
| assertion1 = mkAssertion "test_1" prop1 loc |
| assertion2 = mkAssertion "test_2" prop2 loc |
| store = insertObligation assertion1 $ insertObligation assertion2 emptyStore |
| in allProven store @?= False |
|
|
| , testCase "Count obligations by state" $ |
| let x = Var "x" |
| prop = EqualityProp (TVar x) (TConst "5") |
| loc = SourceLoc "test.assertica" 1 1 |
| assertion = mkAssertion "test_count" prop loc |
| store = insertObligation assertion emptyStore |
| in countByState Asserted store @?= 1 |
| ] |
|
|
| |
| propositionUtilityTests :: TestTree |
| propositionUtilityTests = testGroup "Proposition Utilities" |
| [ testCase "Pretty print equality proposition" $ |
| let x = Var "x" |
| prop = EqualityProp (TVar x) (TConst "5") |
| in length (prettyPrintProposition prop) > 0 @?= True |
|
|
| , testCase "Pretty print universal quantification" $ |
| let x = Var "x" |
| innerProp = EqualityProp (TVar x) (TConst "5") |
| prop = UniversalQuantProp x innerProp |
| in length (prettyPrintProposition prop) > 0 @?= True |
|
|
| , testCase "Pretty print implication" $ |
| let x = Var "x" |
| prop1 = EqualityProp (TVar x) (TConst "5") |
| prop2 = EqualityProp (TConst "1") (TConst "1") |
| prop = ImplicationProp prop1 prop2 |
| in length (prettyPrintProposition prop) > 0 @?= True |
|
|
| , testCase "Pretty print conjunction" $ |
| let x = Var "x" |
| prop1 = EqualityProp (TVar x) (TConst "5") |
| prop2 = EqualityProp (TConst "1") (TConst "1") |
| prop = ConjunctionProp prop1 prop2 |
| in length (prettyPrintProposition prop) > 0 @?= True |
|
|
| , testCase "Pretty print disjunction" $ |
| let x = Var "x" |
| prop1 = EqualityProp (TVar x) (TConst "5") |
| prop2 = EqualityProp (TConst "1") (TConst "1") |
| prop = DisjunctionProp prop1 prop2 |
| in length (prettyPrintProposition prop) > 0 @?= True |
|
|
| , testCase "Pretty print negation" $ |
| let x = Var "x" |
| prop = NegationProp (EqualityProp (TVar x) (TConst "5")) |
| in length (prettyPrintProposition prop) > 0 @?= True |
| ] |
|
|
