path: root/source/Felix/Test/Unit/Meaning.hs

{-# LANGUAGE OverloadedStrings #-}

module Felix.Test.Unit.Meaning (unitTests) where

import Base
import Felix.Meaning
import Felix.Report.Location
import Felix.Syntax.Abstract qualified as Raw
import Felix.Syntax.Internal qualified as Sem
import Felix.Syntax.LexicalPhrase
    ( unsafeReadPhrase
    , unsafeReadPhraseSgPl
    )

import Bound (instantiate)
import Control.Monad.Except (runExceptT)
import Control.Monad.State (evalState, gets)
import Data.Map qualified as Map
import Data.Set qualified as Set
import Test.Tasty
import Test.Tasty.HUnit

unitTests :: TestTree
unitTests =
    testGroup "Meaning"
        [ testCase "relation applications reject missing and extra parameters" do
            for_ [(0, Raw.ParameterArity 0), (2, Raw.ParameterArity 2)]
                \(actualCount, actualArity) ->
                    case meaning [relationClaim actualCount] of
                        Left
                            (GlossRelationApplicationError
                                (Sem.RelationParameterArityMismatch
                                    actualLocation
                                    actualSymbol
                                    expectedArity
                                    reportedActualArity)) -> do
                                assertEqual
                                    "relation location"
                                    relationLocation
                                    actualLocation
                                assertEqual
                                    "relation symbol"
                                    relationSymbol
                                    actualSymbol
                                assertEqual
                                    "expected parameter arity"
                                    (Raw.ParameterArity 1)
                                    expectedArity
                                assertEqual
                                    "actual parameter arity"
                                    actualArity
                                    reportedActualArity
                        Left err ->
                            assertFailure
                                ("expected a relation arity error, got "
                                    <> show err)
                        Right _ ->
                            assertFailure
                                "expected relation arity validation to fail"
        , testCase
            "dependent replacement domains report their occurrences"
            dependentReplacementDomains
        , testCase
            "replacement domains remain outside own and future binders"
            independentReplacementDomains
        , testCase
            "functional definitions reject quantified terms with source context"
            quantifiedFunctionalDefinition
        , testCase
            "unsupported source constructs return located errors"
            unsupportedSourceConstructs
        , testCase
            "proof-local function definitions reject mismatched heads"
            proofLocalFunctionDefinitionMismatches
        , testCase
            "abbreviations reject duplicate parameters with source context"
            duplicateAbbreviationParameters
        , testCase
            "abbreviations reject named free body variables"
            freeAbbreviationBodyVariable
        , testCase
            "abbreviation parameters retain positional slots"
            orderedAbbreviationParameters
        , testCase
            "quantified noun binders resolve their whole scope"
            quantifiedNounBinderScope
        , testCase
            "quantified noun binders obey lexical scope"
            quantifiedNounLexicalScope
        , testCase
            "resolved binder adaptation is injective and ignores trivia"
            resolvedBinderAdapter
        ]

dependentReplacementDomains :: Assertion
dependentReplacementDomains =
    for_ cases \(label, replacement, expectedLocation) ->
        assertEqual
            label
            (Left
                (DependentReplacementDomainNotSupported
                    expectedLocation))
            (glossTestExpr replacement)
  where
    cases =
        [ ( "two-domain replacement"
          , replacementExpr
                (Raw.ExprVar y)
                ( (x, rawInteger 1)
                    :| [(y, rawVarAt twoXLocation "x")]
                )
          , twoXLocation
          )
        , ( "three-domain replacement reports its first dependent occurrence"
          , replacementExpr
                (Raw.ExprVar z)
                ( (x, rawInteger 1)
                    :| [ (y, rawInteger 2)
                       , (z, Raw.ExprOp
                            Nowhere
                            (testFunctionSymbol "dependent_domain" 2)
                            [ rawVarAt threeYLocation "y"
                            , rawVarAt threeXLocation "x"
                            ])
                       ]
                )
          , threeYLocation
          )
        ]
    x = Raw.NamedVar "x"
    y = Raw.NamedVar "y"
    z = Raw.NamedVar "z"
    twoXLocation = mkLocation replacementFile 3 17
    threeYLocation = mkLocation replacementFile 4 29
    threeXLocation = mkLocation replacementFile 4 32

independentReplacementDomains :: Assertion
independentReplacementDomains =
    case glossTestExpr replacement of
        Right
            (Sem.ReplaceFun
                ( (actualX, Sem.TermVar actualOwnX)
                    :| [ (actualY, Sem.TermVar actualFutureZ)
                       , ( actualZ
                         , Sem.TermSymbol
                            _thirdDomainLocation
                            (Sem.SymbolInteger 3)
                            []
                         )
                       ]
                )
                valueScope
                conditionScope) -> do
                    assertEqual
                        "replacement binder order"
                        [x, y, z]
                        [actualX, actualY, actualZ]
                    assertEqual
                        "own-domain occurrence remains free"
                        ownXLocation
                        (locate actualOwnX)
                    assertEqual
                        "future-binder occurrence remains free"
                        futureZLocation
                        (locate actualFutureZ)
                    assertEqual
                        "replacement value lowering"
                        expectedValue
                        (instantiate instantiateBinder valueScope)
                    assertEqual
                        "default replacement condition"
                        Sem.Top
                        (instantiate instantiateBinder conditionScope)
        Right expr ->
            assertFailure
                ("expected an independent functional replacement, got "
                    <> show expr)
        Left err ->
            assertFailure
                ("expected independent replacement domains to succeed, got "
                    <> show err)
  where
    replacement =
        replacementExpr
            ( Raw.ExprOp
                replacementValueLocation
                replacementValueSymbol
                [ rawVarAt replacementValueLocation "x"
                , rawVarAt replacementValueLocation "y"
                , rawVarAt replacementValueLocation "z"
                ]
            )
            ( (x, rawVarAt ownXLocation "x")
                :| [ (y, rawVarAt futureZLocation "z")
                   , (z, rawInteger 3)
                   ]
            )
    x = Raw.NamedVar "x"
    y = Raw.NamedVar "y"
    z = Raw.NamedVar "z"
    ownXLocation = mkLocation replacementFile 6 7
    futureZLocation = mkLocation replacementFile 6 16
    replacementValueLocation = mkLocation replacementFile 6 29
    replacementValueSymbol = testFunctionSymbol "replacement_value" 3
    expectedValue =
        Sem.TermSymbol
            replacementValueLocation
            (Sem.SymbolMixfix replacementValueSymbol)
            [ closedInteger 11
            , closedInteger 22
            , closedInteger 33
            ]
    instantiateBinder binder
        | binder == x = closedInteger 11
        | binder == y = closedInteger 22
        | binder == z = closedInteger 33
        | otherwise = closedInteger (-1)

replacementExpr
    :: Raw.Expr
    -> NonEmpty (Raw.VarSymbol, Raw.Expr)
    -> Raw.Expr
replacementExpr value bounds =
    Raw.ExprReplace replacementLocation value bounds Nothing

rawVarAt :: Location -> Text -> Raw.Expr
rawVarAt location name =
    Raw.ExprVar (Raw.NamedVarAt location name)

rawInteger :: Int -> Raw.Expr
rawInteger =
    Raw.ExprInteger Nowhere

glossTestExpr :: Raw.Expr -> Either GlossError Sem.Expr
glossTestExpr expr =
    evalState
        (runExceptT (glossExpr expr))
        initialGlossState

glossTestStmt :: Raw.Stmt -> Either GlossError Sem.Formula
glossTestStmt statement =
    evalState
        (runExceptT (glossStmt statement))
        initialGlossState

unsupportedSourceConstructs :: Assertion
unsupportedSourceConstructs = do
    assertEqual
        "definite-description term"
        (Left (IotaTermNotSupported iotaLocation))
        (runGlossUnit (glossH0Term [] iotaTerm))
    assertEqual
        "definite-function assumption"
        (Left
            (DefiniteFunctionAssumptionNotSupported
                definiteFunctionLocation))
        (runGlossUnit (glossAsm definiteFunctionAssumption))
  where
    iotaTerm =
        Raw.TermIota
            iotaLocation
            (Raw.NamedVarAt iotaLocation "x")
            (Raw.StmtFormula
                (Raw.PropositionalConstant iotaLocation Raw.IsTop))
    definiteFunctionAssumption =
        Raw.AsmLetThe
            (Raw.NamedVarAt definiteFunctionLocation "f")
            (Raw.Fun
                definiteFunctionLocation
                (Raw.mkLexicalItemSgPl
                    (unsafeReadPhraseSgPl "function[/s]")
                    "function")
                [])

runGlossUnit :: Gloss a -> Either GlossError ()
runGlossUnit action =
    void
        (evalState
            (runExceptT action)
            initialGlossState)

quantifiedNounBinderScope :: Assertion
quantifiedNounBinderScope = do
    case glossTestStmt (namedSetEquality "x") of
        Right formula@(Sem.Quantified Sem.Universally scope) -> do
            assertEqual
                "the written binder does not remain free"
                Set.empty
                (Sem.freeVars formula)
            assertEqual
                "the continuation uses the quantified witness"
                (Sem.Top
                    `Sem.Implies`
                        Sem.Equals
                            equalityLocation
                            witness
                            witness)
                (instantiate (const witness) scope)
        Right formula ->
            assertFailure
                ("expected a universal named binder, got " <> show formula)
        Left err ->
            assertFailure
                ("expected the named binder to gloss, got " <> show err)

    case glossTestStmt constrainedNamedBinder of
        Right formula@(Sem.Quantified Sem.Universally scope) -> do
            assertEqual
                "only the ambient noun argument remains free"
                (Set.singleton ambientVariable)
                (Sem.freeVars formula)
            assertEqual
                "noun, modifier, such-that, and continuation share the binder"
                expectedConstrainedBody
                (instantiate (const witness) scope)
        Right formula ->
            assertFailure
                ("expected a constrained universal binder, got "
                    <> show formula)
        Left err ->
            assertFailure
                ("expected the constrained binder to gloss, got "
                    <> show err)
  where
    witness = closedInteger 17
    ambientVariable =
        Raw.NamedVarAt ambientLocation "T"
    nounConstraint =
        Sem.FormulaNoun
            nounLocation
            witness
            subsetNounPattern
            [Sem.TermVar ambientVariable]
    modifierConstraint =
        Sem.FormulaAdj
            modifierLocation
            witness
            modifierPattern
            [witness]
    suchThatConstraint =
        Sem.Equals suchThatLocation witness witness
    continuation =
        Sem.Equals equalityLocation witness witness
    expectedConstrainedBody =
        Sem.makeConjunction
            [ suchThatConstraint
            , Sem.makeConjunction
                [nounConstraint, modifierConstraint]
            ]
            `Sem.Implies` continuation

quantifiedNounLexicalScope :: Assertion
quantifiedNounLexicalScope = do
    assertEqual
        "alpha-renaming a referenced binder"
        (glossTestStmt (namedSetEquality "x"))
        (glossTestStmt (namedSetEquality "renamed"))
    assertEqual
        "a vacuous written name is semantic trivia"
        (glossTestStmt (vacuousSetStatement Nothing))
        (glossTestStmt
            (vacuousSetStatement
                (Just
                    (Raw.NamedVarAt binderLocation "unused"))))

    assertEqual
        "overlapping sibling names are rejected"
        (Left
            (DuplicateQuantifiedNounBinder
                firstSiblingLocation
                secondSiblingLocation
                "same"))
        (glossTestStmt duplicateSiblingStatement)

    case glossTestStmt nestedShadowingStatement of
        Right (Sem.Quantified Sem.Universally outerScope) ->
            case instantiate (const outerWitness) outerScope of
                Sem.Top
                    `Sem.Implies`
                        Sem.Quantified Sem.Existentially innerScope ->
                            assertEqual
                                "the nearest binder owns the nested occurrences"
                                expectedInnerBody
                                (instantiate
                                    (const innerWitness)
                                    innerScope)
                body ->
                    assertFailure
                        ("expected a nested existential binder, got "
                            <> show body)
        Right formula ->
            assertFailure
                ("expected an outer universal binder, got " <> show formula)
        Left err ->
            assertFailure
                ("expected nested shadowing to gloss, got " <> show err)
  where
    outerWitness = closedInteger 23
    innerWitness = closedInteger 29
    expectedInnerBody =
        Sem.makeConjunction
            [ Sem.Equals
                nestedSuchThatLocation
                innerWitness
                innerWitness
            , Sem.Top
            ]
            `Sem.And`
                Sem.Equals
                    nestedEqualityLocation
                    outerWitness
                    innerWitness

resolvedBinderAdapter :: Assertion
resolvedBinderAdapter = do
    case ( binderAdapterObservation
            ("first", firstAdapterLocation)
            ("second", secondAdapterLocation)
         , binderAdapterObservation
            ("alpha", alternateFirstLocation)
            ("beta", alternateSecondLocation)
         ) of
        ( Right (firstId :| [secondId], firstTokens, firstResult)
          , Right (alternateIds, alternateTokens, alternateResult)
          ) -> do
                assertBool
                    "pre-adapter local identities are distinct"
                    (firstId /= secondId)
                case
                    ( Map.lookup firstId firstTokens
                    , Map.lookup secondId firstTokens
                    ) of
                    (Just firstToken, Just secondToken) -> do
                        assertBool
                            "legacy tokens are injective"
                            (firstToken /= secondToken)
                        assertBool
                            "legacy tokens avoid ambient variables"
                            ( firstToken /= adapterAmbientVariable
                                && secondToken
                                    /= adapterAmbientVariable
                            )
                    tokens ->
                        assertFailure
                            ("expected two adapter assignments, got "
                                <> show tokens)
                assertEqual
                    "trivia does not affect local identities"
                    (firstId :| [secondId])
                    alternateIds
                assertEqual
                    "trivia does not affect adapter assignments"
                    firstTokens
                    alternateTokens
                assertEqual
                    "trivia does not affect the alpha-normal result"
                    firstResult
                    alternateResult
                assertEqual
                    "ambient references pass through unchanged"
                    (Set.singleton adapterAmbientVariable)
                    (Sem.freeVars firstResult)
        (firstResult, secondResult) ->
            assertFailure
                ("expected successful adapter observations, got "
                    <> show (firstResult, secondResult))

    assertEqual
        "an unadapted local reference is a located typed error"
        (Left
            (GlossResolvedBinderAdapterError
                firstAdapterLocation
                (UnknownResolvedLocal (LocalId 0))))
        ( evalState
            (runExceptT
                do
                    binder <-
                        freshH0Binder
                            firstAdapterLocation
                            (Just
                                (Raw.NamedVarAt
                                    firstAdapterLocation
                                    "unadapted"))
                    lowerH0Expr
                        (Sem.TermVar
                            (LocalRef (h0BinderId binder))))
            initialGlossState
        )

binderAdapterObservation
    :: (Text, Location)
    -> (Text, Location)
    -> Either
        GlossError
        ( NonEmpty LocalId
        , Map LocalId Sem.VarSymbol
        , Sem.Expr
        )
binderAdapterObservation
        (firstName, firstLocation)
        (secondName, secondLocation) =
    evalState
        (runExceptT do
            firstBinder <-
                freshH0Binder
                    firstLocation
                    (Just
                        (Raw.NamedVarAt firstLocation firstName))
            secondBinder <-
                freshH0Binder
                    secondLocation
                    (Just
                        (Raw.NamedVarAt secondLocation secondName))
            let firstId = h0BinderId firstBinder
                secondId = h0BinderId secondBinder
                resolvedBody =
                    Sem.TermSymbol
                        Nowhere
                        (Sem.SymbolMixfix adapterBodySymbol)
                        [ Sem.TermVar (LocalRef firstId)
                        , Sem.TermVar (LocalRef secondId)
                        , Sem.TermVar
                            (AmbientRef adapterAmbientVariable)
                        ]
                quantifiedTerms =
                    [ H0QuantifiedTerm
                        Raw.Universally
                        firstBinder
                        []
                    , H0QuantifiedTerm
                        Raw.Existentially
                        secondBinder
                        []
                    ]
            adapted <-
                applyH0Quantifiers quantifiedTerms resolvedBody
                    >>= lowerH0Expr
            assignments <- gets legacyLocalTokens
            pure
                ( firstId :| [secondId]
                , assignments
                , adapted
                ))
        initialGlossState

namedSetEquality :: Text -> Raw.Stmt
namedSetEquality name =
    Raw.StmtVerbPhrase
        ( quantifiedSetTerm
            Raw.Universally
            binderLocation
            (Just
                (Raw.NamedVarAt binderLocation name))
            []
            Nothing
            :| []
        )
        (equalityVerbPhrase
            equalityLocation
            (rawTermVar equalityLocation name))

constrainedNamedBinder :: Raw.Stmt
constrainedNamedBinder =
    Raw.StmtVerbPhrase
        ( Raw.TermQuantified
            Raw.Universally
            binderLocation
            ( Raw.NounPhrase
                [ Raw.AdjL
                    modifierLocation
                    modifierPattern
                    [rawTermVar modifierLocation "x"]
                ]
                ( Raw.Noun
                    nounLocation
                    subsetNounPattern
                    [rawTermVar ambientLocation "T"]
                )
                (Just
                    (Raw.NamedVarAt binderLocation "x"))
                []
                (Just
                    (equalityStatement
                        suchThatLocation
                        "x"
                        "x"))
            )
            :| []
        )
        (equalityVerbPhrase
            equalityLocation
            (rawTermVar equalityLocation "x"))

vacuousSetStatement :: Maybe Raw.VarSymbol -> Raw.Stmt
vacuousSetStatement mayName =
    Raw.StmtVerbPhrase
        ( quantifiedSetTerm
            Raw.Universally
            binderLocation
            mayName
            []
            Nothing
            :| []
        )
        ( Raw.VPAdj
            ( Raw.Adj
                reflexiveLocation
                reflexivePattern
                []
                :| []
            )
        )

duplicateSiblingStatement :: Raw.Stmt
duplicateSiblingStatement =
    Raw.StmtVerbPhrase
        ( quantifiedSetTerm
            Raw.Universally
            firstSiblingLocation
            (Just
                (Raw.NamedVarAt firstSiblingLocation "same"))
            []
            Nothing
            :| [ quantifiedSetTerm
                    Raw.Existentially
                    secondSiblingLocation
                    (Just
                        (Raw.NamedVarAt secondSiblingLocation "same"))
                    []
                    Nothing
               ]
        )
        ( Raw.VPAdj
            ( Raw.Adj
                reflexiveLocation
                reflexivePattern
                []
                :| []
            )
        )

nestedShadowingStatement :: Raw.Stmt
nestedShadowingStatement =
    Raw.StmtVerbPhrase
        ( quantifiedSetTerm
            Raw.Universally
            outerBinderLocation
            (Just
                (Raw.NamedVarAt outerBinderLocation "shadow"))
            []
            Nothing
            :| []
        )
        ( equalityVerbPhrase
            nestedEqualityLocation
            ( Raw.TermQuantified
                Raw.Existentially
                innerBinderLocation
                ( Raw.NounPhrase
                    []
                    (setNoun innerBinderLocation)
                    (Just
                        (Raw.NamedVarAt
                            innerBinderLocation
                            "shadow"))
                    []
                    (Just
                        (equalityStatement
                            nestedSuchThatLocation
                            "shadow"
                            "shadow"))
                )
            )
        )

quantifiedSetTerm
    :: Raw.Quantifier
    -> Location
    -> Maybe Raw.VarSymbol
    -> [Raw.AdjL]
    -> Maybe Raw.Stmt
    -> Raw.Term
quantifiedSetTerm quantifier location mayName leftAdjectives maySuchThat =
    Raw.TermQuantified
        quantifier
        location
        ( Raw.NounPhrase
            leftAdjectives
            (setNoun location)
            mayName
            []
            maySuchThat
        )

setNoun :: Location -> Raw.Noun
setNoun location =
    Raw.Noun location setNounPattern []

rawTermVar :: Location -> Text -> Raw.Term
rawTermVar location name =
    Raw.TermExpr (rawVarAt location name)

equalityStatement :: Location -> Text -> Text -> Raw.Stmt
equalityStatement location leftName rightName =
    Raw.StmtVerbPhrase
        (rawTermVar location leftName :| [])
        (equalityVerbPhrase
            location
            (rawTermVar location rightName))

equalityVerbPhrase :: Location -> Raw.Term -> Raw.VerbPhrase
equalityVerbPhrase location argument =
    Raw.VPAdj
        ( Raw.Adj
            location
            equalityPattern
            [argument]
            :| []
        )

setNounPattern :: Raw.LexicalItemSgPl
setNounPattern =
    Raw.mkLexicalItemSgPl
        (unsafeReadPhraseSgPl "set[/s]")
        "set"

subsetNounPattern :: Raw.LexicalItemSgPl
subsetNounPattern =
    Raw.mkLexicalItemSgPl
        (unsafeReadPhraseSgPl "subset[/s] of ?")
        "test_subset"

modifierPattern :: Raw.LexicalItem
modifierPattern =
    Raw.mkLexicalItem
        (unsafeReadPhrase "related to ?")
        "test_modifier"

equalityPattern :: Raw.LexicalItem
equalityPattern =
    Raw.mkLexicalItem
        (unsafeReadPhrase "equal to ?")
        "eq"

reflexivePattern :: Raw.LexicalItem
reflexivePattern =
    Raw.mkLexicalItem
        (unsafeReadPhrase "reflexive")
        "test_reflexive"

adapterBodySymbol :: Raw.FunctionSymbol
adapterBodySymbol =
    testFunctionSymbol "adapter_body" 3

adapterAmbientVariable :: Sem.VarSymbol
adapterAmbientVariable =
    Sem.FreshVar 0

binderLocation, equalityLocation, nounLocation, ambientLocation :: Location
binderLocation = mkLocation (FileId 48) 2 7
equalityLocation = mkLocation (FileId 48) 2 24
nounLocation = mkLocation (FileId 48) 3 7
ambientLocation = mkLocation (FileId 48) 3 20

modifierLocation, suchThatLocation, reflexiveLocation :: Location
modifierLocation = mkLocation (FileId 48) 3 27
suchThatLocation = mkLocation (FileId 48) 3 42
reflexiveLocation = mkLocation (FileId 48) 4 17

firstSiblingLocation, secondSiblingLocation :: Location
firstSiblingLocation = mkLocation (FileId 48) 5 7
secondSiblingLocation = mkLocation (FileId 48) 5 24

outerBinderLocation, innerBinderLocation :: Location
outerBinderLocation = mkLocation (FileId 48) 6 7
innerBinderLocation = mkLocation (FileId 48) 6 31

nestedSuchThatLocation, nestedEqualityLocation :: Location
nestedSuchThatLocation = mkLocation (FileId 48) 6 45
nestedEqualityLocation = mkLocation (FileId 48) 6 20

firstAdapterLocation, secondAdapterLocation :: Location
firstAdapterLocation = mkLocation (FileId 48) 7 7
secondAdapterLocation = mkLocation (FileId 48) 7 19

alternateFirstLocation, alternateSecondLocation :: Location
alternateFirstLocation = mkLocation (FileId 48) 8 7
alternateSecondLocation = mkLocation (FileId 48) 8 19

replacementFile :: FileId
replacementFile = FileId 47

replacementLocation :: Location
replacementLocation = mkLocation replacementFile 2 1

iotaLocation :: Location
iotaLocation = mkLocation (FileId 49) 3 5

definiteFunctionLocation :: Location
definiteFunctionLocation = mkLocation (FileId 49) 4 9

proofLocalFunctionDefinitionMismatches :: Assertion
proofLocalFunctionDefinitionMismatches =
    for_ mismatchCases \(label, proof, expectedError) ->
        assertEqual
            label
            (Left expectedError)
            (meaning
                [ Raw.BlockProof
                    proofLocation
                    proof
                    proofLocation
                ])
  where
    mismatchCases =
        [ ( "argument and domain binder"
          , Raw.DefineFunction
                proofLocation
                "f"
                "x"
                (Raw.ExprVar "x")
                "y"
                (Raw.ExprVar "domain")
                (Raw.Omitted proofLocation)
          , GlossProofFunctionArgumentMismatch
                proofLocation
                "x"
                "y"
          )
        , ( "declared and defined function name"
          , Raw.DefineFunctionLocal
                proofLocation
                "f"
                "domain"
                (Raw.ExprVar "range")
                "g"
                "x"
                ( ( Raw.ExprVar "x"
                  , Raw.PropositionalConstant
                        proofLocation
                        Raw.IsTop
                  )
                    :| []
                )
                (Raw.Omitted proofLocation)
          , GlossProofFunctionNameMismatch
                proofLocation
                "f"
                "g"
          )
        ]
    proofLocation = mkLocation (FileId 46) 5 9

quantifiedFunctionalDefinition :: Assertion
quantifiedFunctionalDefinition =
    case meaning [definitionBlock] of
        Left
            (GlossDefnError
                actualLocation
                DefnErrorQuantifiedRhsTerm
                actualMarker) -> do
                    assertEqual
                        "quantified term location"
                        termLocation
                        actualLocation
                    assertEqual
                        "definition marker"
                        definitionMarker
                        actualMarker
        Left err ->
            assertFailure
                ("expected a quantified definition term error, got "
                    <> show err)
        Right _ ->
            assertFailure
                "expected quantified definition term validation to fail"
  where
    definitionBlock =
        Raw.BlockDefn
            blockLocation
            Nothing
            definitionMarker
            ( Raw.DefnFun
                []
                ( Raw.Fun
                    blockLocation
                    ( Raw.mkLexicalItemSgPl
                        (unsafeReadPhraseSgPl "value[/s] of ?")
                        "quantified_function"
                    )
                    ["argument"]
                )
                Nothing
                ( Raw.TermQuantified
                    Raw.Existentially
                    termLocation
                    ( Raw.NounPhrase
                        []
                        ( Raw.Noun
                            termLocation
                            ( Raw.mkLexicalItemSgPl
                                (unsafeReadPhraseSgPl "set[/s]")
                                "set"
                            )
                            []
                        )
                        Nothing
                        []
                        Nothing
                    )
                )
            )
    definitionMarker = "quantified_definition"
    blockLocation = mkLocation (FileId 44) 8 1
    termLocation = mkLocation (FileId 44) 8 29

duplicateAbbreviationParameters :: Assertion
duplicateAbbreviationParameters = do
    let marker = "duplicate_abbreviation"
        duplicate = Raw.NamedVar "duplicate"
    expectAbbreviationError
        marker
        [duplicate, duplicate]
        (Raw.ExprVar duplicate)
        \case
            DuplicateAbbreviationParameters actualVariables ->
                assertEqual
                    "duplicate parameter names"
                    (duplicate :| [])
                    actualVariables
            err ->
                assertFailure
                    ("expected duplicate abbreviation parameters, got "
                        <> show err)

freeAbbreviationBodyVariable :: Assertion
freeAbbreviationBodyVariable = do
    let marker = "free_abbreviation_body"
        freeVariable = Raw.NamedVar "free"
    expectAbbreviationError
        marker
        ["parameter"]
        (Raw.ExprVar freeVariable)
        \case
            FreeAbbreviationBodyVariables actualVariables ->
                assertEqual
                    "free body variable names"
                    (freeVariable :| [])
                    actualVariables
            err ->
                assertFailure
                    ("expected free abbreviation variables, got "
                        <> show err)

orderedAbbreviationParameters :: Assertion
orderedAbbreviationParameters = do
    let first = Raw.NamedVar "first"
        second = Raw.NamedVar "second"
        third = Raw.NamedVar "third"
        firstArgument = closedInteger 11
        secondArgument = closedInteger 22
        thirdArgument = closedInteger 33
        arguments =
            [ firstArgument
            , secondArgument
            , thirdArgument
            ]
        expectedBody =
            Sem.TermSymbol
                abbreviationLocation
                (Sem.SymbolMixfix abbreviationBodySymbol)
                [thirdArgument, firstArgument, secondArgument]
        unexpectedArgument = closedInteger (-1)
    case meaning
        [ abbreviationBlock
            abbreviationLocation
            "ordered_abbreviation"
            [first, second, third]
            ( Raw.ExprOp
                abbreviationLocation
                abbreviationBodySymbol
                [ Raw.ExprVar third
                , Raw.ExprVar first
                , Raw.ExprVar second
                ]
            )
        ] of
        Right
            [Sem.BlockAbbr
                _actualLocation
                _actualMarker
                (Sem.Abbreviation _actualSymbol scope)] ->
                    assertEqual
                        "instantiated abbreviation body"
                        expectedBody
                        ( instantiate
                            (\parameterIndex ->
                                nth parameterIndex arguments
                                    ?? unexpectedArgument)
                            scope
                        )
        Right blocks ->
            assertFailure
                ("expected one glossed abbreviation, got "
                    <> show blocks)
        Left err ->
            assertFailure
                ("expected a valid abbreviation, got "
                    <> show err)

expectAbbreviationError
    :: Raw.Marker
    -> [Raw.VarSymbol]
    -> Raw.Expr
    -> (AbbreviationParameterError -> Assertion)
    -> Assertion
expectAbbreviationError marker parameters body checkError =
    case meaning
        [ abbreviationBlock
            abbreviationLocation
            marker
            parameters
            body
        ] of
        Left
            (GlossAbbreviationError
                actualLocation
                actualMarker
                abbreviationError) -> do
                    assertEqual
                        "abbreviation location"
                        abbreviationLocation
                        actualLocation
                    assertEqual
                        "abbreviation marker"
                        marker
                        actualMarker
                    checkError abbreviationError
        Left err ->
            assertFailure
                ("expected an abbreviation parameter error, got "
                    <> show err)
        Right _ ->
            assertFailure
                "expected abbreviation parameter validation to fail"

abbreviationBlock
    :: Location
    -> Raw.Marker
    -> [Raw.VarSymbol]
    -> Raw.Expr
    -> Raw.Block
abbreviationBlock location marker parameters body =
    Raw.BlockAbbr
        location
        Nothing
        marker
        ( Raw.AbbreviationEq
            ( Raw.SymbolPattern
                (testFunctionSymbol
                    "abbreviation_head"
                    (length parameters))
                parameters
            )
            body
        )

abbreviationBodySymbol :: Raw.FunctionSymbol
abbreviationBodySymbol =
    testFunctionSymbol "abbreviation_body" 3

testFunctionSymbol :: Text -> Int -> Raw.FunctionSymbol
testFunctionSymbol name arity =
    Raw.mkMixfixItem
        (Just (Raw.Command name) : replicate arity Nothing)
        (Raw.Marker name)
        Raw.NonAssoc

closedInteger :: Int -> Sem.ExprOf a
closedInteger value =
    Sem.TermSymbol
        Nowhere
        (Sem.SymbolInteger value)
        []

abbreviationLocation :: Location
abbreviationLocation =
    mkLocation (FileId 43) 8 12

relationClaim :: Int -> Raw.Block
relationClaim actualParameterCount =
    Raw.BlockClaim
        Raw.Proposition
        relationLocation
        Nothing
        "relation_arity"
        (Raw.Claim []
            (Raw.StmtFormula
                (Raw.FormulaChain
                    (Raw.ChainBase
                        (Raw.ExprVar "x" :| [])
                        Raw.Positive
                        (Raw.Relation
                            relationLocation
                            relationSymbol
                            (replicate
                                actualParameterCount
                                (Raw.ExprVar "p")))
                        (Raw.ExprVar "y" :| [])))))

relationSymbol :: Raw.RelationSymbol
relationSymbol =
    Raw.RelationSymbol
        (Raw.Command "parametric")
        (Raw.ParameterArity 1)
        "parametric"

relationLocation :: Location
relationLocation = mkLocation (FileId 42) 7 11