path: root/source/Test/Unit/Semantic.hs

{-# 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