diff options
Diffstat (limited to 'source/Test/Unit/Declaration.hs')
| -rw-r--r-- | source/Test/Unit/Declaration.hs | 202 |
1 files changed, 198 insertions, 4 deletions
diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs index 26261f3..0823606 100644 --- a/source/Test/Unit/Declaration.hs +++ b/source/Test/Unit/Declaration.hs @@ -12,6 +12,7 @@ import Checking.Exact qualified as Exact import Checking.Identity qualified as Identity import Checking.Kernel.Derivation qualified as Kernel import Checking.Semantic qualified as Semantic +import Checking.Typed.Inductive qualified as Typed import Felix.Math.Codec import Felix.Module import Felix.Source @@ -20,10 +21,12 @@ import Provers qualified import Report.Location import Syntax.Abstract qualified as Raw import Syntax.Interface qualified as Syntax +import Syntax.Internal qualified as Internal import Syntax.Lexicon qualified as Lexicon import Data.List.NonEmpty qualified as NonEmpty import Data.IORef qualified as IORef +import Data.Set qualified as Set import Data.Text qualified as Text import Data.Text.Encoding qualified as TextEncoding import Data.Vector qualified as Vector @@ -62,6 +65,8 @@ unitTests = reconstructsImportedGlobalBindings , testCase "elaborates scoped exact propositions" elaboratesScopedExactPropositions + , testCase "lowers fixed equality aliases without global support" + lowersFixedEqualityAliases , testCase "prepares exact claim envelopes" preparesExactClaimEnvelopes , testCase "lowers exact separation comprehensions" @@ -1166,8 +1171,7 @@ makePreparedObligationWithPremise fixture fingerprint = do claim [] [] - Backend.ExplicitGlobalPremises - Backend.FirstOrderLocals) + Backend.ExplicitGlobalPremiseSelection) expectRight (Provers.prepareTypedProverTask Provers.DirectTask @@ -1199,8 +1203,7 @@ makePreparedObligation fixture tag = do [Backend.typedFoundationAuxiliaryInput (fixtureFoundation fixture) tag] - Backend.NoGlobalPremises - Backend.AllLocals) + Backend.LocalOnlyPremiseSelection) expectRight (Provers.prepareTypedProverTask Provers.DirectTask @@ -1887,6 +1890,197 @@ elaboratesScopedExactPropositions = do Declaration.DriverSealFailed failure _prefix -> assertFailure ("scoped exact driver did not seal: " <> show failure) +lowersFixedEqualityAliases :: Assertion +lowersFixedEqualityAliases = do + fixture <- makeNamedFixture "fixed-equality-aliases" + let x = Raw.NamedVar "x" + y = Raw.NamedVar "y" + z = Raw.NamedVar "z" + term variable = Raw.TermExpr (Raw.ExprVar variable) + equality left right = + Raw.StmtFormula + (Raw.FormulaChain + (Raw.ChainBase + (Raw.ExprVar left :| []) + Raw.Positive + (Raw.Relation Nowhere Raw.EqSymbol []) + (Raw.ExprVar right :| []))) + quantified variables statement = + Raw.SymbolicQuantified + Nowhere + Raw.Universally + variables + Raw.Unbounded + Nothing + statement + adjective = + Raw.Adj + Nowhere + Lexicon.builtinEqualityRightAdjective + [term y] + copular = + Raw.StmtVerbPhrase + (term x :| []) + (Raw.VPAdj (adjective :| [])) + rightAttribute = + Raw.StmtNoun + (term x :| []) + (Raw.NounPhrase + [] + (Raw.Noun Nowhere Lexicon.builtinSetNoun []) + Nothing + [ Raw.AdjR + Nowhere + Lexicon.builtinEqualityRightAdjective + [term y] + ] + Nothing) + rightAttributeExpected = + Raw.StmtNoun + (term x :| []) + (Raw.NounPhrase + [] + (Raw.Noun Nowhere Lexicon.builtinSetNoun []) + Nothing + [] + (Just (equality x y))) + verb argument = + Raw.Verb + Nowhere + Lexicon.builtinEqualityVerb + [term argument] + singular = + Raw.StmtVerbPhrase + (term x :| []) + (Raw.VPVerb (verb y)) + negated = + Raw.StmtVerbPhrase + (term x :| []) + (Raw.VPVerbNot (verb y)) + coordinated = + Raw.StmtVerbPhrase + (term x :| [term y]) + (Raw.VPVerb (verb z)) + coordinatedExpected = + Raw.StmtConnected + Raw.Conjunction + Nothing + (equality x z) + (equality y z) + comparisons = + [ ( "copular adjective" + , quantified (x :| [y]) copular + , quantified (x :| [y]) (equality x y) + ) + , ( "right adjective" + , quantified (x :| [y]) rightAttribute + , quantified (x :| [y]) rightAttributeExpected + ) + , ( "singular verb" + , quantified (x :| [y]) singular + , quantified (x :| [y]) (equality x y) + ) + , ( "negated verb" + , quantified (x :| [y]) negated + , quantified + (x :| [y]) + (Raw.StmtNeg Nowhere (equality x y)) + ) + , ( "quantified coordinated verb" + , quantified (x :| [y, z]) coordinated + , quantified (x :| [y, z]) coordinatedExpected + ) + ] + action + :: Declaration.ModuleDriver Text + [ ( Either + Exact.ExactCompileError + Exact.PreparedExactProposition + , Either + Exact.ExactCompileError + Exact.PreparedExactProposition + ) + ] + action = + Declaration.runProspectiveLoweringDriver + (traverse + (\(_label, alias, symbolic) -> + (,) + <$> Exact.prepareExactProposition + Exact.emptyExactBinderContext alias + <*> Exact.prepareExactProposition + Exact.emptyExactBinderContext symbolic) + comparisons) + runDriver fixture action >>= \case + Declaration.DriverSucceeded results _interface _prefix _closure -> + for_ (zip comparisons results) \((label, _alias, _symbolic), result) -> + case result of + (Right alias, Right symbolic) -> do + let aliasTerm = + Core.scopedCoreTerm + (Exact.preparedExactPropositionCore alias) + symbolicTerm = + Core.scopedCoreTerm + (Exact.preparedExactPropositionCore symbolic) + assertEqual + (label <> " checked core") + symbolicTerm + aliasTerm + assertEqual + (label <> " global support") + Set.empty + (Core.canonicalTermGlobals aliasTerm) + assertEqual + (label <> " foundation support") + Set.empty + (Foundation.foundationAxiomDependencies aliasTerm) + (Left failure, _) -> + assertFailure + (label <> " alias failed: " + <> Text.unpack + (Exact.renderExactCompileError failure)) + (_, Left failure) -> + assertFailure + (label <> " symbolic comparison failed: " + <> Text.unpack + (Exact.renderExactCompileError failure)) + Declaration.DriverFailed failure _prefix -> + assertFailure ("fixed equality driver failed: " <> show failure) + Declaration.DriverSealFailed failure _prefix -> + assertFailure ("fixed equality driver did not seal: " <> show failure) + + let internalEquality = + Internal.FormulaVerb + Nowhere + (Internal.EmptySet Nowhere) + Lexicon.builtinEqualityVerb + [Internal.EmptySet Nowhere] + internalResult + :: Either + Typed.TypedInductiveError + (Core.FrozenCheckedCore Void) + internalResult = + Typed.prepareTypedClosedFormula + absurd + (const Nothing) + internalEquality + case internalResult of + Right checked -> do + assertEqual + "internal fixed verb core" + (Core.CEq + Core.TySet + (Core.CIntrinsic Core.Empty) + (Core.CIntrinsic Core.Empty)) + (Core.frozenCoreTerm checked) + assertEqual + "internal fixed verb global support" + Set.empty + (Core.frozenCoreGlobals checked) + Left failure -> + assertFailure + ("internal fixed verb failed: " <> show failure) + preparesExactClaimEnvelopes :: Assertion preparesExactClaimEnvelopes = do fixture <- makeNamedFixture "exact-claim-envelope" |