diff options
Diffstat (limited to 'source/Felix/Test/Unit/Semantic.hs')
| -rw-r--r-- | source/Felix/Test/Unit/Semantic.hs | 437 |
1 files changed, 437 insertions, 0 deletions
diff --git a/source/Felix/Test/Unit/Semantic.hs b/source/Felix/Test/Unit/Semantic.hs new file mode 100644 index 0000000..f62a003 --- /dev/null +++ b/source/Felix/Test/Unit/Semantic.hs @@ -0,0 +1,437 @@ +{-# LANGUAGE NoImplicitPrelude #-} + +module Felix.Test.Unit.Semantic (unitTests) where + +import Base +import Felix.Checking.Authority qualified as Authority +import Felix.Checking.Core qualified as Core +import Felix.Checking.Foundation qualified as Foundation +import Felix.Checking.Identity qualified as Identity +import Felix.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 Felix.Syntax.Interface qualified as Syntax +import Felix.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 |