diff options
Diffstat (limited to 'source/Test/Unit/Core.hs')
| -rw-r--r-- | source/Test/Unit/Core.hs | 210 |
1 files changed, 186 insertions, 24 deletions
diff --git a/source/Test/Unit/Core.hs b/source/Test/Unit/Core.hs index e1ba10d..643dc38 100644 --- a/source/Test/Unit/Core.hs +++ b/source/Test/Unit/Core.hs @@ -5,11 +5,13 @@ module Test.Unit.Core (unitTests) where import Base hiding (Empty) import Checking.Core import Checking.Foundation qualified as Foundation +import Checking.SetConstruction import Control.DeepSeq (NFData(..), force) import Hedgehog import Hedgehog.Gen qualified as Gen import Hedgehog.Range qualified as Range +import Data.Set qualified as Set import Test.Tasty import Test.Tasty.HUnit hiding (assert) import Test.Tasty.Hedgehog (testPropertyNamed) @@ -58,6 +60,9 @@ unitTests = "specializes the checked replacement characteristic" specializesCheckedReplacementCharacteristic , testCase + "derives named construction views from checked components" + derivesNamedConstructionViews + , testCase "thaws checked closed terms without changing them" thawsCheckedClosedTerms , testPropertyNamed @@ -268,6 +273,14 @@ checksScopedCanonicalOperations = do buildsSetInductionHypotheses :: Assertion buildsSetInductionHypotheses = do + let propertyTerm = + CImp + (CEq TySet + (CBound 0) + (CIntrinsic Empty)) + (CEq TySet + (CBound 0) + (CBound 0)) claimProperty <- either (assertFailure . show) @@ -275,35 +288,46 @@ buildsSetInductionHypotheses = do (checkScopedCanonicalCore testGlobalType [TySet] - (CImp - (CEq TySet - (CBound 0) - (CIntrinsic Empty)) - (CEq TySet - (CBound 0) - (CBound 0)))) - hypothesis <- + propertyTerm) + (predicate, hypothesis, step, result) <- maybe - (assertFailure "set-induction hypothesis was not constructed") + (assertFailure "set-induction instance was not constructed") pure - (scopedSetInductionHypothesis 0 claimProperty) + (scopedSetInductionInstance 0 claimProperty) + let abstractedProperty = + CImp + (CEq TySet + (CBound 0) + (CIntrinsic Empty)) + (CEq TySet + (CBound 0) + (CBound 0)) + memberHypothesis = + CForall TySet + (CImp + (CApp + (CApp + (CIntrinsic Member) + (CBound 0)) + (CBound 1)) + abstractedProperty) + assertEqual + "set induction abstracts the selected property once" + (CLam TySet abstractedProperty) + (scopedCoreTerm predicate) assertEqual "antecedent and goal are both generalized over the member" - (CForall TySet - (CImp - (CApp - (CApp - (CIntrinsic Member) - (CBound 0)) - (CBound 1)) - (CImp - (CEq TySet - (CBound 0) - (CIntrinsic Empty)) - (CEq TySet - (CBound 0) - (CBound 0))))) + memberHypothesis (scopedCoreTerm hypothesis) + assertEqual + "set-induction step owns its member-wise hypothesis" + (CForall TySet + (CImp memberHypothesis abstractedProperty)) + (scopedCoreTerm step) + assertEqual + "set-induction result closes the complete property" + (CForall TySet abstractedProperty) + (scopedCoreTerm result) specializesCheckedSeparationCharacteristic :: Assertion specializesCheckedSeparationCharacteristic = do @@ -404,6 +428,144 @@ specializesCheckedReplacementCharacteristic = do pure (checkScopedCanonicalCore testGlobalType context term) +derivesNamedConstructionViews :: Assertion +derivesNamedConstructionViews = do + foundation <- + either (assertFailure . show) pure Foundation.checkedFoundation + bound <- checked [] (CIntrinsic Empty) + predicate <- checked [TySet] (CEq TySet (CBound 0) (CBound 0)) + separation <- + maybe + (assertFailure "checked separation descriptor failed") + pure + (checkedSeparationConstruction testGlobalType bound predicate) + (separationView, separationEquation) <- + maybe + (assertFailure "checked separation views failed") + pure + (namedSetConstructionLocalViews + (checkedFoundationSetConstruction foundation) + separation) + expectedSeparationView <- + maybe + (assertFailure "checked separation characteristic failed") + pure + (scopedSetDefinition + (Foundation.foundationAxiomFrozen foundation + Foundation.SeparationCharacteristic) + (namedSetConstructionTerm separation)) + assertEqual "separation view is the checked specialization" + expectedSeparationView separationView + assertEqual "separation view is first-order" + (Set.singleton Foundation.EmptyCharacteristic) + (Foundation.foundationAxiomDependencies + (scopedCoreTerm separationView)) + assertEqual "separation equation retains exact construction" + (Set.fromList + [ Foundation.EmptyCharacteristic + , Foundation.SeparationCharacteristic + ]) + (Foundation.foundationAxiomDependencies + (scopedCoreTerm separationEquation)) + + firstDomain <- checked [] (CIntrinsic Empty) + singleValue <- checked [TySet] (CBound 0) + singleCondition <- checked [TySet] + (CEq TySet (CBound 0) (CBound 0)) + singleReplacement <- + maybe + (assertFailure "checked one-domain replacement failed") + pure + (checkedFunctionalReplacementConstruction + testGlobalType + (firstDomain :| []) + singleValue + (Just singleCondition)) + assertEqual "one-domain replacement has one canonical term" + (CApp + (CApp + (CIntrinsic Repl) + (CApp + (CApp (CIntrinsic Sep) (CIntrinsic Empty)) + (CLam TySet + (CEq TySet (CBound 0) (CBound 0))))) + (CLam TySet (CBound 0))) + (scopedCoreTerm + (namedSetConstructionTerm singleReplacement)) + + secondDomain <- checked [TySet] (CBound 0) + value <- checked [TySet, TySet] (CBound 0) + condition <- checked [TySet, TySet] + (CEq TySet (CBound 0) (CBound 0)) + replacement <- + maybe + (assertFailure "checked replacement descriptor failed") + pure + (checkedFunctionalReplacementConstruction + testGlobalType + (firstDomain :| [secondDomain]) + value + (Just condition)) + (replacementView, replacementEquation) <- + maybe + (assertFailure "checked replacement views failed") + pure + (namedSetConstructionLocalViews + (checkedFoundationSetConstruction foundation) + replacement) + let terminal = + andP + (CEq TySet (CBound 0) (CBound 0)) + (CEq TySet (CBound 2) (CBound 0)) + secondWitness = + existsP + (andP + (memberP (CBound 0) (CBound 1)) + terminal) + firstWitness = + existsP + (andP + (memberP (CBound 0) (CIntrinsic Empty)) + secondWitness) + expectedReplacementTerm = + CForall TySet + (CEq TyProp + (memberP (CBound 0) (CBound 1)) + firstWitness) + expectedReplacementView <- checked [TySet] expectedReplacementTerm + assertEqual "replacement view preserves bounds and condition" + expectedReplacementView replacementView + assertEqual "flattened replacement view is first-order" + (Set.singleton Foundation.EmptyCharacteristic) + (Foundation.foundationAxiomDependencies + (scopedCoreTerm replacementView)) + assertEqual "replacement equation retains every helper" + (Set.fromList + [ Foundation.FamilyUnionCharacteristic + , Foundation.EmptyCharacteristic + , Foundation.SeparationCharacteristic + , Foundation.ReplacementCharacteristic + ]) + (Foundation.foundationAxiomDependencies + (scopedCoreTerm replacementEquation)) + where + checked context term = + either + (assertFailure . show) + pure + (checkScopedCanonicalCore testGlobalType context term) + + memberP element set = + CApp (CApp (CIntrinsic Member) element) set + + notP proposition = CImp proposition CFalsum + + andP left right = + notP (CImp left (notP right)) + + existsP proposition = + notP (CForall TySet (notP proposition)) + specializeForall :: CanonicalTerm global -> CanonicalTerm global |