diff options
Diffstat (limited to 'source/Test/Unit/Semantic.hs')
| -rw-r--r-- | source/Test/Unit/Semantic.hs | 437 |
1 files changed, 0 insertions, 437 deletions
diff --git a/source/Test/Unit/Semantic.hs b/source/Test/Unit/Semantic.hs deleted file mode 100644 index 160735c..0000000 --- a/source/Test/Unit/Semantic.hs +++ /dev/null @@ -1,437 +0,0 @@ -{-# LANGUAGE NoImplicitPrelude #-} - -module Test.Unit.Semantic (unitTests) where - -import Base -import Checking.Authority qualified as Authority -import Checking.Core qualified as Core -import Checking.Foundation qualified as Foundation -import Checking.Identity qualified as Identity -import Checking.Semantic qualified as Semantic -import Felix.Cache.Codec -import Felix.Math.Codec -import Felix.Module -import Felix.Parsed.Identity -import Felix.Source -import Felix.Source.Content -import Syntax.Interface qualified as Syntax -import Syntax.Abstract qualified as Raw - -import Data.ByteString (ByteString) -import Data.List qualified as List -import Data.Map.Strict qualified as Map -import Test.Tasty -import Test.Tasty.HUnit - - -unitTests :: TestTree -unitTests = - testGroup "Semantic interfaces" - [ testCase "separates syntax and semantic Merkle identities" - separatesSyntaxAndSemantics - , testCase "round-trips closed semantic declaration state" - roundTripsSemanticState - , testCase "round-trips exact semantic global keys" - roundTripsSemanticGlobalKeys - , testCase "round-trips canonical structure descriptors" - roundTripsStructureDescriptors - , testCase "keys exact proof and module inputs" - keysExactInputs - ] - -separatesSyntaxAndSemantics :: Assertion -separatesSyntaxAndSemantics = do - fixture <- makeFixture - firstSyntax <- makeSyntax "first" - secondSyntax <- makeSyntax "second" - assertBool - "notation changes syntax identity" - ( Syntax.moduleSyntaxAssertedId firstSyntax - /= Syntax.moduleSyntaxAssertedId secondSyntax - ) - assertEqual - "notation does not enter semantic prefix identity" - (fixtureNextPrefix fixture) - (Semantic.nextPrefixContextId - (fixtureInitialPrefix fixture) - (fixtureDelta fixture)) - -roundTripsSemanticState :: Assertion -roundTripsSemanticState = do - fixture <- makeFixture - assertEqual - "semantic interface cache round trip" - (Right (fixtureInterface fixture)) - (decodeCache - Semantic.getSemanticInterfaceCache - (encodeCache - (Semantic.putSemanticInterfaceCache - (fixtureInterface fixture)))) - assertEqual - "walking-subset environment delta round trip" - (Right Semantic.emptySemanticEnvironmentDelta) - (decodeCache - Semantic.getSemanticEnvironmentDeltaCache - (encodeCache - (Semantic.putSemanticEnvironmentDeltaCache - Semantic.emptySemanticEnvironmentDelta))) - -roundTripsSemanticGlobalKeys :: Assertion -roundTripsSemanticGlobalKeys = do - fixture <- makeFixture - let unary = Raw.HoleCons (Raw.TokenCons (Raw.Command "f") Raw.End) - plural = Raw.HoleCons (Raw.TokenCons (Raw.Word "things") Raw.End) - keys = - [ Semantic.SemanticLeftAdjective unary - , Semantic.SemanticRightAdjective unary - , Semantic.SemanticFunctionPhrase unary plural - , Semantic.SemanticNoun unary plural - , Semantic.SemanticVerb unary plural - , Semantic.SemanticRelation - (Raw.Command "rel") - (Raw.ParameterArity 2) - , Semantic.SemanticExpressionFunction unary - , Semantic.SemanticPrefixPredicate "Pred" 3 - ] - target = - Identity.intrinsicObjectId - (fixtureTheory fixture) - Core.Empty - Core.TySet - bindings = - List.sortOn Semantic.semanticGlobalBindingKey - ( case keys of - [] -> [] - first : rest -> - Semantic.semanticGlobalBinding - first - (Semantic.ContextualTransparentExpansion - target - (Map.singleton - (Raw.StructSymbol "operation") - target)) - : [ Semantic.semanticGlobalBinding - key - (Semantic.GlobalReference target) - | key <- rest - ] - ) - delta <- expectRight (Semantic.semanticEnvironmentDelta bindings) - assertEqual "binding cache round trip" - (Right delta) - (decodeCache - Semantic.getSemanticEnvironmentDeltaCache - (encodeCache - (Semantic.putSemanticEnvironmentDeltaCache delta))) - case bindings of - first : second : _ -> do - assertEqual "rejects noncanonical order" - (Left Semantic.NonCanonicalSemanticGlobalBindingOrder) - (Semantic.semanticEnvironmentDelta - (second : first : drop 2 bindings)) - assertEqual "rejects duplicate key" - (Left - (Semantic.DuplicateSemanticGlobalKey - (Semantic.semanticGlobalBindingKey first))) - (Semantic.semanticEnvironmentDelta [first, first]) - _ -> assertFailure "semantic key fixture is unexpectedly empty" - -roundTripsStructureDescriptors :: Assertion -roundTripsStructureDescriptors = do - fixture <- makeFixture - let structurePhrase marker word = - Semantic.semanticStructurePhrase - (Raw.LexicalItemSgPl - (Raw.SgPl - (Raw.TokenCons (Raw.Word word) Raw.End) - (Raw.TokenCons (Raw.Word (word <> "s")) Raw.End)) - marker) - base = structurePhrase "onesorted_structure" "base" - child = structurePhrase "ordered_structure" "ordered" - object = - Identity.intrinsicObjectId - (fixtureTheory fixture) - Core.Empty - Core.TySet - operation = - Semantic.semanticStructureOperation - (Raw.StructSymbol "carrier") - object - descriptor <- expectRight - (Semantic.semanticStructureDescriptor - child - (Just object) - [base] - [operation]) - delta <- expectRight - (Semantic.semanticEnvironmentWithStructures [] [descriptor]) - assertEqual - "structure environment cache round trip" - (Right delta) - (decodeCache - Semantic.getSemanticEnvironmentDeltaCache - (encodeCache - (Semantic.putSemanticEnvironmentDeltaCache delta))) - assertEqual - "duplicate local operation is rejected" - (Left - (Semantic.DuplicateSemanticStructureOperation - (Raw.StructSymbol "carrier"))) - (Semantic.semanticStructureDescriptor - child - (Just object) - [base] - [operation, operation]) - -keysExactInputs :: Assertion -keysExactInputs = do - fixture <- makeFixture - let authority = - Authority.factAuthority - (fixtureTheorem fixture) - Authority.cleanAuthoritySafety - certificate <- expectRight - (Authority.validationCertificate - authority - (Authority.CheckedSourceProof [])) - let theorem = - Identity.theoremId - (fixtureTheorem fixture) - firstProof = - Semantic.proofValidationKey - theorem - (Semantic.proofSyntaxId "proof-a") - (fixtureInitialPrefix fixture) - secondProof = - Semantic.proofValidationKey - theorem - (Semantic.proofSyntaxId "proof-b") - (fixtureInitialPrefix fixture) - laterContext = - Semantic.proofValidationKey - theorem - (Semantic.proofSyntaxId "proof-a") - (fixtureNextPrefix fixture) - assertBool - "proof syntax is an exact validation input" - (firstProof /= secondProof) - assertBool - "semantic predecessor is an exact validation input" - (firstProof /= laterContext) - let proofRecord = - Semantic.proofValidationRecord - firstProof certificate - declarationKey = - Semantic.declarationValidationKey - (Semantic.declarationSyntaxId "declaration") - (fixtureInitialPrefix fixture) - [] - [theorem, theorem] - declarationRecord = - Semantic.declarationValidationRecord - declarationKey - [certificate, certificate] - assertEqual - "proof validation record cache round trip" - (Right proofRecord) - (decodeCache - Semantic.getProofValidationRecordCache - (encodeCache - (Semantic.putProofValidationRecordCache - proofRecord))) - assertEqual - "ordered declaration certificates retain repetitions" - (Right declarationRecord) - (decodeCache - Semantic.getDeclarationValidationRecordCache - (encodeCache - (Semantic.putDeclarationValidationRecordCache - declarationRecord))) - firstParsedKey <- expectRight - (parsedModuleKey - (fixtureSourceContentId "source-a") - Syntax.baseSyntaxInterfaceId - []) - secondParsedKey <- expectRight - (parsedModuleKey - (fixtureSourceContentId "source-b") - Syntax.baseSyntaxInterfaceId - []) - directSyntax <- makeSyntax "direct" - let directSyntaxId = - Syntax.moduleSyntaxAssertedId directSyntax - assertEqual - "parsed identity rejects duplicate direct syntax" - (Left - (DuplicateParsedDirectSyntaxInput - directSyntaxId)) - (parsedModuleKey - (fixtureSourceContentId "source-a") - Syntax.baseSyntaxInterfaceId - [directSyntaxId, directSyntaxId]) - let - firstParsed = - parsedModuleId firstParsedKey "parsed" - secondParsed = - parsedModuleId secondParsedKey "parsed" - firstArtifactKey <- expectRight - (Semantic.moduleArtifactKey - (fixtureOwner fixture) - firstParsed - [] - (fixtureTheory fixture)) - secondArtifactKey <- expectRight - (Semantic.moduleArtifactKey - (fixtureOwner fixture) - secondParsed - [] - (fixtureTheory fixture)) - let firstArtifact = - Semantic.moduleArtifactId firstArtifactKey - secondArtifact = - Semantic.moduleArtifactId secondArtifactKey - assertBool - "module artifact binds parsed source identity" - (firstArtifact /= secondArtifact) - let semanticId = - Semantic.semanticInterfaceAssertedId - (fixtureInterface fixture) - assertEqual - "prefix identity rejects duplicate direct semantics" - (Left - (Semantic.DuplicateInitialPrefixSemanticInput - semanticId)) - (Semantic.initialPrefixContextId - (fixtureTheory fixture) - (fixtureOwner fixture) - [semanticId, semanticId]) - assertEqual - "module artifact key cache round trip" - (Right firstArtifactKey) - (decodeCache - Semantic.getModuleArtifactKeyCache - (encodeCache - (Semantic.putModuleArtifactKeyCache - firstArtifactKey))) - syntax <- makeSyntax "artifact" - let artifactResult = - Semantic.moduleArtifactResult - firstArtifactKey - (Syntax.moduleSyntaxAssertedId syntax) - (Semantic.semanticInterfaceAssertedId - (fixtureInterface fixture)) - assertEqual - "module artifact root round trip" - (Right artifactResult) - (decodeCache - (Semantic.getModuleArtifactResultCache - firstArtifact) - (encodeCache - (Semantic.putModuleArtifactResultCache - artifactResult))) - - -data Fixture = Fixture - { fixtureTheory :: !Identity.TheoryId - , fixtureOwner :: !ModuleName - , fixtureTheorem :: !Identity.TheoremRef - , fixtureDelta :: !Semantic.DeclarationInterfaceDelta - , fixtureInterface :: !Semantic.SemanticInterface - , fixtureInitialPrefix :: !Semantic.PrefixContextId - , fixtureNextPrefix :: !Semantic.PrefixContextId - } - -makeFixture :: IO Fixture -makeFixture = do - foundation <- expectRight Foundation.checkedFoundation - namespaceDigest <- expectRight - (hashCanonicalFields - "semantic-test-namespace" - ["root"]) - relative <- expectRight (safeRelativePath "module.tex") - closure <- expectRight - (Identity.validateObjectClosure - (Identity.theoryId foundation) - []) - proposition <- expectRight - (Identity.validatePropositionContent - closure - Core.CFalsum) - let theory = - Identity.theoryId foundation - owner = - moduleNameFromParts - (sourceNamespaceIdFromDigest namespaceDigest) - relative - reference = - Identity.theoremRef - theory - (Identity.checkedPropositionId proposition) - authority = - Authority.factAuthority - reference - Authority.cleanAuthoritySafety - occurrence = - Semantic.semanticFactOccurrence - (Semantic.factSlot owner (localFactOrdinal 0)) - authority - Semantic.SearchEligible - slot = - Semantic.declarationSlot - owner - (localDeclarationOrdinal 0) - delta <- expectRight - (Semantic.declarationInterfaceDelta - slot - [occurrence] - [ Semantic.semanticAlias - (Semantic.semanticName "theorem") - (Semantic.semanticFactOccurrenceFingerprint - (Semantic.factSlot owner (localFactOrdinal 0)) - authority) - ] - [] - [Identity.checkedPropositionId proposition] - Semantic.emptySemanticEnvironmentDelta) - interface <- expectRight - (Semantic.semanticInterface owner [] [delta]) - initial <- expectRight - (Semantic.initialPrefixContextId theory owner []) - pure - Fixture - { fixtureTheory = theory - , fixtureOwner = owner - , fixtureTheorem = reference - , fixtureDelta = delta - , fixtureInterface = interface - , fixtureInitialPrefix = initial - , fixtureNextPrefix = - Semantic.nextPrefixContextId initial delta - } - -makeSyntax :: Text -> IO Syntax.ModuleSyntaxInterface -makeSyntax command = do - delta <- expectRight - (Syntax.canonicalSyntaxDelta - [Syntax.CanonicalStructureOperation command]) - expectRight (Syntax.moduleSyntaxInterface [] delta) - -fixtureSourceContentId :: ByteString -> SourceContentId -fixtureSourceContentId bytes = - either - (impossible . show) - id - (decodeCache - getSourceContentIdCache - (encodeCache - (putCacheDigest - (hashCacheFields - "semantic-test-source" - [bytes])))) - -expectRight :: Show error => Either error value -> IO value -expectRight = \case - Left err -> - assertFailure (show err) >> fail "unreachable" - Right value -> - pure value |