Migrate to `Felix` namespaceHEADhotg

1 files changed, 0 insertions, 1119 deletions

diff --git a/source/Test/Unit/Meaning.hs b/source/Test/Unit/Meaning.hs
deleted file mode 100644
index acb33d0..0000000
--- a/source/Test/Unit/Meaning.hs
+++ /dev/null
@@ -1,1119 +0,0 @@
-{-# LANGUAGE OverloadedStrings #-}
-
-module Test.Unit.Meaning (unitTests) where
-
-import Base
-import Felix.Meaning
-import Report.Location
-import Syntax.Abstract qualified as Raw
-import Syntax.Internal qualified as Sem
-import 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