summaryrefslogtreecommitdiff
path: root/source/Felix/Test/Unit/Meaning.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Felix/Test/Unit/Meaning.hs')
-rw-r--r--source/Felix/Test/Unit/Meaning.hs1119
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
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 19:47:37 +0000