diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-07-28 02:41:42 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-07-28 02:41:42 +0200 |
| commit | 7c0d42f7c5d64eba3aeb917c8095ac89adb44ae5 (patch) | |
| tree | 861e4a988b349ac1226ae2f299db747ce2b42192 /source/Test/Unit/Meaning.hs | |
| parent | 23e56079250e2fec1f7d9d24856a9d50e3528400 (diff) | |
Reject unsupported definite source forms
Diffstat (limited to 'source/Test/Unit/Meaning.hs')
| -rw-r--r-- | source/Test/Unit/Meaning.hs | 45 |
1 files changed, 45 insertions, 0 deletions
diff --git a/source/Test/Unit/Meaning.hs b/source/Test/Unit/Meaning.hs index 6cef182..8954aa7 100644 --- a/source/Test/Unit/Meaning.hs +++ b/source/Test/Unit/Meaning.hs @@ -67,6 +67,9 @@ unitTests = "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 @@ -240,6 +243,42 @@ glossTestStmt statement = (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 @@ -754,6 +793,12 @@ 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) -> |