Migrate to `Felix` namespaceHEADhotg

1 files changed, 1119 insertions, 0 deletions

diff --git a/source/Felix/Test/Unit/Meaning.hs b/source/Felix/Test/Unit/Meaning.hs
new file mode 100644
index 0000000..3093a84
--- /dev/null
+++ b/source/Felix/Test/Unit/Meaning.hs
@@ -0,0 +1,1119 @@
+{-# 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