diff options
Diffstat (limited to 'source/Test/Unit/Encoding.hs')
| -rw-r--r-- | source/Test/Unit/Encoding.hs | 363 |
1 files changed, 0 insertions, 363 deletions
diff --git a/source/Test/Unit/Encoding.hs b/source/Test/Unit/Encoding.hs deleted file mode 100644 index cba359f..0000000 --- a/source/Test/Unit/Encoding.hs +++ /dev/null @@ -1,363 +0,0 @@ -{-# LANGUAGE OverloadedStrings #-} - -module Test.Unit.Encoding (unitTests, propertyTests) where - -import Base -import Checking.Backend.Problem qualified as Backend -import Checking.Core qualified as Core -import Encoding -import Provers -import Report.Location -import Syntax.Internal -import Tptp.UnsortedFirstOrder qualified as Tptp - -import Control.Monad.Logger (runNoLoggingT) -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set -import Data.Text qualified as Text -import Data.Vector qualified as Vector -import Hedgehog hiding (Command) -import Hedgehog.Gen qualified as Gen -import Hedgehog.Range qualified as Range -import Test.Tasty -import Test.Tasty.HUnit hiding (assert) -import Test.Tasty.Hedgehog (testPropertyNamed) -import UnliftIO.Environment (lookupEnv) - -unitTests :: TestTree -unitTests = - testGroup "Encoding" - [ propertyTests - , testCase - "real Vampire distinguishes Unicode free constants from symbols" - realVampireDistinguishesNames - , testCase - "real Vampire proves a typed higher-order problem" - realVampireProvesTypedHigherOrderProblem - ] - -propertyTests :: TestTree -propertyTests = - testGroup "properties" - [ testPropertyNamed - "allocates legal dense names deterministically" - "prop_taskLocalNames" - prop_taskLocalNames - ] - -prop_taskLocalNames :: Property -prop_taskLocalNames = property do - generatedSpellings <- - forAll - (Gen.list - (Range.linear 0 20) - sourceSpelling) - let spellings = - zipWith - (\ordinal spelling -> - spelling <> "#" <> Text.pack (show ordinal)) - [0 :: Int ..] - (adversarialSpellings <> generatedSpellings) - originalBinders = - zipWith - (\ordinal spelling -> - NamedVar - ( spelling - <> "_bound_" - <> Text.pack (show ordinal) - )) - [0 :: Int ..] - spellings - renamedBinders = - [ NamedVar ("renamed_" <> Text.pack (show ordinal)) - | ordinal <- [0 .. length spellings - 1] - ] - baseHypotheses = - zipWith makeHypothesis spellings originalBinders - firstHypothesis = - listToMaybe baseHypotheses - ?? impossible "allocator property has no seeded hypothesis" - duplicateHypotheses = - baseHypotheses <> [firstHypothesis] - alphaHypotheses = - let renamed = - zipWith makeHypothesis spellings renamedBinders - firstRenamed = - listToMaybe renamed - ?? impossible - "allocator property has no renamed hypothesis" - in renamed <> [firstRenamed] - shuffledHypotheses <- forAll (Gen.shuffle duplicateHypotheses) - let prepared = - prepareTptpTask (namingTask duplicateHypotheses) - shuffled = - prepareTptpTask (namingTask shuffledHypotheses) - alphaRenamed = - prepareTptpTask (namingTask alphaHypotheses) - nameOrigins = preparedTptpNameOrigins prepared - targetNames = Map.keysSet nameOrigins - renderedIdentifiers = - tptpIdentifiers (preparedTptpText prepared) - semanticCount = length spellings - hypothesisCount = length duplicateHypotheses - binderCount = 2 * hypothesisCount - - preparedTptpText shuffled === preparedTptpText prepared - preparedTptpText alphaRenamed === preparedTptpText prepared - preparedTptpNameOrigins shuffled === nameOrigins - preparedTptpNameOrigins alphaRenamed === nameOrigins - - categoryNames "zf_u" targetNames - === ordinalNames "zf_u" semanticCount - categoryNames "zf_f" targetNames - === ordinalNames "zf_f" semanticCount - categoryNames "zf_s" targetNames - === ordinalNames "zf_s" semanticCount - categoryNames "zf_h" targetNames - === ordinalNames "zf_h" hypothesisCount - categoryNames "zf_q" targetNames - === Set.singleton "zf_q0" - categoryNames "V" targetNames - === ordinalNames "V" binderCount - assert (targetNames `Set.isSubsetOf` renderedIdentifiers) - - Set.size targetNames - === 3 * semanticCount + hypothesisCount + binderCount + 1 - for_ targetNames \target -> - if "V" `Text.isPrefixOf` target - then assert (Tptp.isProperVariable target) - else assert (Tptp.isProperAtomicWord target) - -sourceSpelling :: Gen Text -sourceSpelling = - Gen.text - (Range.linear 0 16) - (Gen.element - ( ['a'..'z'] - <> ['A'..'Z'] - <> ['0'..'9'] - <> "_'-.:/\\" - <> ['λ', 'Ω', '\x0301', '💥'] - )) - -adversarialSpellings :: [Text] -adversarialSpellings = - [ "" - , "λ" - , "e\x0301" - , "name'" - , "under_score" - , "zf_u0" - , "zf_f0" - , "zf_s0" - , "V0" - , "Case" - , "case" - , "a-b" - , "💥" - ] - -makeHypothesis :: Text -> VarSymbol -> Hypothesis -makeHypothesis spelling binder = - let freeConstant = TermVar (NamedVar spelling) - structureTerm = - TermSymbolStruct - (StructSymbol spelling) - (Just freeConstant) - body = - Atomic - Nowhere - (PredicateSymbol spelling) - [ freeConstant - , structureTerm - , TermVar binder - ] - shadowedBody = - makeExists - [binder] - (Atomic - Nowhere - (PredicateSymbol spelling) - [TermVar binder]) - nativeRelations = - Equals Nowhere freeConstant freeConstant - `And` NotEquals Nowhere freeConstant structureTerm - in - Hypothesis - (Marker ("label_" <> spelling)) - (makeForall - [binder] - (body `And` shadowedBody `And` nativeRelations)) - -namingTask :: [Hypothesis] -> Task -namingTask hypotheses = - Task - { taskDirectness = Direct - , taskHypotheses = hypotheses - , taskConjectureLabel = "ignored_conjecture_label" - , taskLocation = Nowhere - , taskConjecture = Top - } - -categoryNames :: Text -> Set Text -> Set Text -categoryNames prefix = - Set.filter (prefix `Text.isPrefixOf`) - -ordinalNames :: Text -> Int -> Set Text -ordinalNames prefix size = - Set.fromList - [ prefix <> Text.pack (show ordinal) - | ordinal <- [0 .. size - 1] - ] - -tptpIdentifiers :: Text -> Set Text -tptpIdentifiers = - Set.delete "" - . Set.fromList - . Text.split (not . Tptp.isAsciiAlphaNumOrUnderscore) - -realVampireDistinguishesNames :: Assertion -realVampireDistinguishesNames = do - executable <- fromMaybe "vampire" <$> lookupEnv "NAPROCHE_ZF_VAMPIRE" - let collisionSymbol = - mkMixfixItem - [Just (Command "collision")] - "fx" - NonAssoc - freeConstant = TermVar (NamedVar "x") - userConstant = - TermSymbol - Nowhere - (SymbolMixfix collisionSymbol) - [] - unicodeVariable = NamedVar "λ" - unicodeReflexivity = - makeForall - [unicodeVariable] - (Equals - Nowhere - (TermVar unicodeVariable) - (TermVar unicodeVariable)) - task = - Task - { taskDirectness = Direct - , taskHypotheses = [] - , taskConjectureLabel = "unicode_collision" - , taskLocation = Nowhere - , taskConjecture = - Equals Nowhere freeConstant userConstant - `And` unicodeReflexivity - } - (_location, _formula, answer) <- - runNoLoggingT - (runProver - (vampire - executable - defaultTimeLimit - defaultMemoryLimit) - task) - case answer of - Right CounterSatisfiable{} -> - pure () - result -> - assertFailure - ("expected a countermodel, got " <> show result) - -data Th0Global - = Th0Predicate - | Th0PredicateConsumer - deriving (Show, Eq, Ord) - -th0GlobalType :: Th0Global -> Maybe Core.CoreType -th0GlobalType = \case - Th0Predicate -> - Just - (Core.TySet - `Core.TyArrow` Core.TyProp) - Th0PredicateConsumer -> - Just - ((Core.TySet - `Core.TyArrow` Core.TyProp) - `Core.TyArrow` Core.TyProp) - -realVampireProvesTypedHigherOrderProblem :: Assertion -realVampireProvesTypedHigherOrderProblem = do - executable <- - fromMaybe "vampire" - <$> lookupEnv "NAPROCHE_ZF_VAMPIRE" - let claimTerm = - Core.CApp - (Core.CGlobal Th0PredicateConsumer) - (Core.CLam Core.TySet - (Core.CApp - (Core.CGlobal Th0Predicate) - (Core.CBound 0))) - checked <- - either - (assertFailure . show) - pure - (Core.checkScopedCanonicalCore - th0GlobalType - [] - claimTerm) - claim <- - either - (assertFailure . show) - pure - (Backend.supportedProposition - (Vector.empty - :: Vector.Vector - (Void, Core.CoreType)) - checked) - capability <- - either - (assertFailure . show) - pure - (Backend.classifySupportedProposition - th0GlobalType - claim) - problem <- - either - (assertFailure . show) - pure - (Backend.planTypedProblem - th0GlobalType - (Vector.singleton - (Backend.typedBackendFact - (0 :: Int) - claim - capability)) - claim - [] - [] - Backend.ExplicitGlobalPremises - Backend.FirstOrderLocals) - prepared <- - either - (assertFailure . show) - pure - (prepareTypedProverTask - DirectTask - problem) - assertEqual - "higher-order request dialect" - VerificationTh0 - (preparedVerificationDialect - (preparedTypedProverRequest - prepared)) - answer <- - runNoLoggingT - (runPreparedTypedProver - (vampire - executable - defaultTimeLimit - defaultMemoryLimit) - prepared) - case answer of - Right result - | isJust (provedVampireRun result) -> - pure () - result -> - assertFailure - ("expected a higher-order theorem, got " - <> show result) |