File size: 6,810 Bytes
a10b189 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 | {-|
Module : Test.Core.Assertion
Description : Tests for the explicit assertion system
Tests the assertion module which represents mathematical obligations
as first-class program entities.
-}
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
]
-- Tests for assertion construction
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
]
-- Tests for obligation store operations
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
]
-- Tests for proposition utilities
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
]
|