diff options
Diffstat (limited to 'source/Test/Unit')
| -rw-r--r-- | source/Test/Unit/Backend.hs | 259 | ||||
| -rw-r--r-- | source/Test/Unit/Core.hs | 210 | ||||
| -rw-r--r-- | source/Test/Unit/Declaration.hs | 638 | ||||
| -rw-r--r-- | source/Test/Unit/Identity.hs | 5 | ||||
| -rw-r--r-- | source/Test/Unit/Kernel.hs | 3 | ||||
| -rw-r--r-- | source/Test/Unit/Module.hs | 3477 | ||||
| -rw-r--r-- | source/Test/Unit/Provers.hs | 4 | ||||
| -rw-r--r-- | source/Test/Unit/Source.hs | 45 |
8 files changed, 4378 insertions, 263 deletions
diff --git a/source/Test/Unit/Backend.hs b/source/Test/Unit/Backend.hs index 11c36b8..ab836d8 100644 --- a/source/Test/Unit/Backend.hs +++ b/source/Test/Unit/Backend.hs @@ -52,6 +52,9 @@ unitTests = "routes implicit, explicit, and local-only problems" routesCompleteProblems , testCase + "admits only checked implicit set constructions" + admitsImplicitSetConstructions + , testCase "renders checked FOF and TH0 problems" rendersCheckedProblems ] @@ -166,8 +169,8 @@ routesCompleteProblems = do claim [higherOrderLocal, firstOrderLocal] [] - ImplicitFofPremises FirstOrderLocals + ImplicitConstructionJustification assertEqual "implicit route" RouteFof (typedProblemRoute implicit) assertEqual "implicit FOF globals" [0] @@ -186,23 +189,33 @@ routesCompleteProblems = do planned fofFacts claim - [firstOrderLocal] + [higherOrderLocal, firstOrderLocal] [] - ExplicitGlobalPremises FirstOrderLocals + ExplicitHigherOrderJustification assertEqual "explicit FOF route" RouteFof (typedProblemRoute explicitFof) + assertEqual "explicit FOF references retain only FOF locals" [0] + (localPremiseOrdinalValue + . typedLocalPremiseOrdinal + <$> toList + (typedProblemLocalPremises explicitFof)) explicitTh0 <- planned th0Facts claim - [firstOrderLocal] + [higherOrderLocal, firstOrderLocal] [] - ExplicitGlobalPremises - FirstOrderLocals + CompleteLocals + ExplicitHigherOrderJustification assertEqual "explicit TH0 route" RouteTh0 (typedProblemRoute explicitTh0) + assertEqual "explicit TH0 references retain complete locals" [0, 1] + (localPremiseOrdinalValue + . typedLocalPremiseOrdinal + <$> toList + (typedProblemLocalPremises explicitTh0)) localOnly <- planned @@ -210,8 +223,8 @@ routesCompleteProblems = do claim [higherOrderLocal, firstOrderLocal] [] - NoGlobalPremises - AllLocals + CompleteLocals + ExplicitHigherOrderJustification assertEqual "local-only TH0 route" RouteTh0 (typedProblemRoute localOnly) assertEqual "local order restored" [0, 1] @@ -235,8 +248,8 @@ routesCompleteProblems = do claim [firstOrderLocal, firstOrderLocal] [] - NoGlobalPremises - AllLocals of + CompleteLocals + ExplicitHigherOrderJustification of Left (TypedProblemDuplicateLocalPremiseOrdinal duplicateOrdinal) -> @@ -260,8 +273,8 @@ routesCompleteProblems = do higherOrderClaimProposition [] [] - ImplicitFofPremises - FirstOrderLocals of + FirstOrderLocals + ImplicitConstructionJustification of Left TypedProblemExplicitHigherOrderJustificationRequired{} -> pure () @@ -282,8 +295,8 @@ routesCompleteProblems = do [typedFoundationAuxiliaryInput checkedFoundationValue Foundation.SeparationCharacteristic] - ImplicitFofPremises - FirstOrderLocals of + FirstOrderLocals + ImplicitConstructionJustification of Left TypedProblemExplicitHigherOrderJustificationRequired{} -> pure () @@ -314,8 +327,7 @@ routesCompleteProblems = do assertFailure "unused ambient local entered exact support" where - planned selectedFacts claim locals auxiliaries - globalPolicy localPolicy = + planned selectedFacts claim locals auxiliaries localPolicy higherOrderPolicy = either (assertFailure . show) pure @@ -325,8 +337,8 @@ routesCompleteProblems = do claim locals auxiliaries - globalPolicy - localPolicy) + localPolicy + higherOrderPolicy) showProblemResult = \case Left err -> @@ -334,6 +346,205 @@ routesCompleteProblems = do Right problem -> show (typedProblemRoute problem) +admitsImplicitSetConstructions :: Assertion +admitsImplicitSetConstructions = do + checkedFoundationValue <- + either + (assertFailure . show) + pure + Foundation.checkedFoundation + let separation = + CApp + (CApp + (CIntrinsic Sep) + (CIntrinsic Empty)) + (CLam TySet + (CApp + (CGlobal HigherOrderPredicate) + (CLam TySet CFalsum))) + separationClaim = + CEq TySet separation separation + filteredDomain = + CApp + (CApp + (CIntrinsic Sep) + (CBound 0)) + (CLam TySet + (CEq TySet (CBound 0) (CBound 0))) + innerReplacement = + CApp + (CApp (CIntrinsic Repl) filteredDomain) + (CLam TySet (CBound 0)) + functionalReplacement = + CApp + (CIntrinsic FamilyUnion) + (CApp + (CApp + (CIntrinsic Repl) + (CIntrinsic Empty)) + (CLam TySet innerReplacement)) + replacementClaim = + CEq TySet functionalReplacement functionalReplacement + replacementTags = + [ Foundation.FamilyUnionCharacteristic + , Foundation.SeparationCharacteristic + , Foundation.ReplacementCharacteristic + ] + auxiliary tag = + typedFoundationAuxiliaryInput + checkedFoundationValue tag + plan selected claim locals tags = + planTypedProblem + testGlobalType + selected + claim + locals + (auxiliary <$> tags) + FirstOrderLocals + ImplicitConstructionJustification + + separationProposition <- + checkedProposition Vector.empty separationClaim + separationProblem <- + either + (assertFailure . show) + pure + (plan + Vector.empty + separationProposition + [] + [Foundation.SeparationCharacteristic]) + assertEqual "separation implicit route" RouteTh0 + (typedProblemRoute separationProblem) + assertEqual "separation characteristic only" + [Foundation.SeparationCharacteristic] + (typedProblemAuxiliaryTag + <$> toList (typedProblemAuxiliaries separationProblem)) + assertEqual "separation selects no global premise" + 0 + (Vector.length (typedProblemGlobalPremises separationProblem)) + + replacementProposition <- + checkedProposition Vector.empty replacementClaim + replacementProblem <- + either + (assertFailure . show) + pure + (plan + Vector.empty + replacementProposition + [] + replacementTags) + assertEqual "functional replacement implicit route" RouteTh0 + (typedProblemRoute replacementProblem) + assertEqual "functional replacement exact helper set" + replacementTags + (typedProblemAuxiliaryTag + <$> toList (typedProblemAuxiliaries replacementProblem)) + + firstOrderProposition <- + checkedProposition Vector.empty firstOrderClaim + firstOrderLocal <- + checkedLocalPremise 0 "first-order" firstOrderProposition + separationLocal <- + checkedLocalPremise 2 "separation" separationProposition + unrelatedLocalProposition <- + checkedProposition + (Vector.singleton + (PredicateLocal, TySet `TyArrow` TyProp)) + (CApp + (CGlobal HigherOrderPredicate) + (CBound 0)) + unrelatedLocal <- + checkedLocalPremise 1 "unrelated higher-order" unrelatedLocalProposition + separationWithLocals <- + either + (assertFailure . show) + pure + (plan + Vector.empty + separationProposition + [unrelatedLocal, firstOrderLocal] + [Foundation.SeparationCharacteristic]) + assertEqual "inline separation keeps unrelated HO local out" RouteTh0 + (typedProblemRoute separationWithLocals) + assertEqual "inline separation retains only FOF local" [0] + ( localPremiseOrdinalValue + . typedLocalPremiseOrdinal + <$> toList (typedProblemLocalPremises separationWithLocals) + ) + assertEqual "excluded HO local adds no auxiliary" + [Foundation.SeparationCharacteristic] + (typedProblemAuxiliaryTag + <$> toList (typedProblemAuxiliaries separationWithLocals)) + localProblem <- + either + (assertFailure . show) + pure + (plan + Vector.empty + firstOrderProposition + [unrelatedLocal, separationLocal, firstOrderLocal] + []) + assertEqual "implicit construction local remains excluded" RouteFof + (typedProblemRoute localProblem) + assertEqual "unrelated higher-order local remains unselected" + [0] + ( localPremiseOrdinalValue + . typedLocalPremiseOrdinal + <$> toList (typedProblemLocalPremises localProblem) + ) + + higherOrderFact <- checkedBackendFact (1 :: Int) higherOrderClaim + expectImplicitHigherOrderRejection + "implicit higher-order global remains forbidden" + (plan + (Vector.singleton higherOrderFact) + separationProposition + [] + [Foundation.SeparationCharacteristic]) + + ordinaryHigherOrder <- + checkedProposition Vector.empty + (CEq TySet + (CApp + (CIntrinsic SetChoose) + (CLam TySet CFalsum)) + (CIntrinsic Empty)) + expectImplicitHigherOrderRejection + "ordinary implicit higher-order target remains forbidden" + (plan Vector.empty ordinaryHigherOrder [] []) + mixedHigherOrder <- + checkedProposition Vector.empty + (CImp + separationClaim + (supportedPropositionTerm ordinaryHigherOrder)) + expectImplicitHigherOrderRejection + "construction does not admit another higher-order intrinsic" + (plan + Vector.empty + mixedHigherOrder + [] + [Foundation.SeparationCharacteristic]) + + expectImplicitHigherOrderRejection + "auxiliary tag alone grants no construction permission" + (plan + Vector.empty + firstOrderProposition + [] + [Foundation.SeparationCharacteristic]) + where + expectImplicitHigherOrderRejection label = \case + Left TypedProblemExplicitHigherOrderJustificationRequired{} -> + pure () + Left err -> + assertFailure (label <> ": unexpected error " <> show err) + Right problem -> + assertFailure + (label <> ": unexpectedly routed " + <> show (typedProblemRoute problem)) + rendersCheckedProblems :: Assertion rendersCheckedProblems = do fofFact <- @@ -355,14 +566,14 @@ rendersCheckedProblems = do planned (Vector.singleton fofFact) claim - ImplicitFofPremises FirstOrderLocals + ImplicitConstructionJustification th0Problem <- planned (Vector.singleton th0Fact) claim - ExplicitGlobalPremises - FirstOrderLocals + CompleteLocals + ExplicitHigherOrderJustification preparedFof <- either (assertFailure . show) @@ -430,7 +641,7 @@ rendersCheckedProblems = do then Tptp.isProperVariable target else Tptp.isProperAtomicWord target) where - planned selectedFacts claim globalPolicy localPolicy = + planned selectedFacts claim localPolicy higherOrderPolicy = either (assertFailure . show) pure @@ -440,8 +651,8 @@ rendersCheckedProblems = do claim [] [] - globalPolicy - localPolicy) + localPolicy + higherOrderPolicy) firstOrderClaim :: CanonicalTerm TestGlobal firstOrderClaim = diff --git a/source/Test/Unit/Core.hs b/source/Test/Unit/Core.hs index e1ba10d..643dc38 100644 --- a/source/Test/Unit/Core.hs +++ b/source/Test/Unit/Core.hs @@ -5,11 +5,13 @@ module Test.Unit.Core (unitTests) where import Base hiding (Empty) import Checking.Core import Checking.Foundation qualified as Foundation +import Checking.SetConstruction import Control.DeepSeq (NFData(..), force) import Hedgehog import Hedgehog.Gen qualified as Gen import Hedgehog.Range qualified as Range +import Data.Set qualified as Set import Test.Tasty import Test.Tasty.HUnit hiding (assert) import Test.Tasty.Hedgehog (testPropertyNamed) @@ -58,6 +60,9 @@ unitTests = "specializes the checked replacement characteristic" specializesCheckedReplacementCharacteristic , testCase + "derives named construction views from checked components" + derivesNamedConstructionViews + , testCase "thaws checked closed terms without changing them" thawsCheckedClosedTerms , testPropertyNamed @@ -268,6 +273,14 @@ checksScopedCanonicalOperations = do buildsSetInductionHypotheses :: Assertion buildsSetInductionHypotheses = do + let propertyTerm = + CImp + (CEq TySet + (CBound 0) + (CIntrinsic Empty)) + (CEq TySet + (CBound 0) + (CBound 0)) claimProperty <- either (assertFailure . show) @@ -275,35 +288,46 @@ buildsSetInductionHypotheses = do (checkScopedCanonicalCore testGlobalType [TySet] - (CImp - (CEq TySet - (CBound 0) - (CIntrinsic Empty)) - (CEq TySet - (CBound 0) - (CBound 0)))) - hypothesis <- + propertyTerm) + (predicate, hypothesis, step, result) <- maybe - (assertFailure "set-induction hypothesis was not constructed") + (assertFailure "set-induction instance was not constructed") pure - (scopedSetInductionHypothesis 0 claimProperty) + (scopedSetInductionInstance 0 claimProperty) + let abstractedProperty = + CImp + (CEq TySet + (CBound 0) + (CIntrinsic Empty)) + (CEq TySet + (CBound 0) + (CBound 0)) + memberHypothesis = + CForall TySet + (CImp + (CApp + (CApp + (CIntrinsic Member) + (CBound 0)) + (CBound 1)) + abstractedProperty) + assertEqual + "set induction abstracts the selected property once" + (CLam TySet abstractedProperty) + (scopedCoreTerm predicate) assertEqual "antecedent and goal are both generalized over the member" - (CForall TySet - (CImp - (CApp - (CApp - (CIntrinsic Member) - (CBound 0)) - (CBound 1)) - (CImp - (CEq TySet - (CBound 0) - (CIntrinsic Empty)) - (CEq TySet - (CBound 0) - (CBound 0))))) + memberHypothesis (scopedCoreTerm hypothesis) + assertEqual + "set-induction step owns its member-wise hypothesis" + (CForall TySet + (CImp memberHypothesis abstractedProperty)) + (scopedCoreTerm step) + assertEqual + "set-induction result closes the complete property" + (CForall TySet abstractedProperty) + (scopedCoreTerm result) specializesCheckedSeparationCharacteristic :: Assertion specializesCheckedSeparationCharacteristic = do @@ -404,6 +428,144 @@ specializesCheckedReplacementCharacteristic = do pure (checkScopedCanonicalCore testGlobalType context term) +derivesNamedConstructionViews :: Assertion +derivesNamedConstructionViews = do + foundation <- + either (assertFailure . show) pure Foundation.checkedFoundation + bound <- checked [] (CIntrinsic Empty) + predicate <- checked [TySet] (CEq TySet (CBound 0) (CBound 0)) + separation <- + maybe + (assertFailure "checked separation descriptor failed") + pure + (checkedSeparationConstruction testGlobalType bound predicate) + (separationView, separationEquation) <- + maybe + (assertFailure "checked separation views failed") + pure + (namedSetConstructionLocalViews + (checkedFoundationSetConstruction foundation) + separation) + expectedSeparationView <- + maybe + (assertFailure "checked separation characteristic failed") + pure + (scopedSetDefinition + (Foundation.foundationAxiomFrozen foundation + Foundation.SeparationCharacteristic) + (namedSetConstructionTerm separation)) + assertEqual "separation view is the checked specialization" + expectedSeparationView separationView + assertEqual "separation view is first-order" + (Set.singleton Foundation.EmptyCharacteristic) + (Foundation.foundationAxiomDependencies + (scopedCoreTerm separationView)) + assertEqual "separation equation retains exact construction" + (Set.fromList + [ Foundation.EmptyCharacteristic + , Foundation.SeparationCharacteristic + ]) + (Foundation.foundationAxiomDependencies + (scopedCoreTerm separationEquation)) + + firstDomain <- checked [] (CIntrinsic Empty) + singleValue <- checked [TySet] (CBound 0) + singleCondition <- checked [TySet] + (CEq TySet (CBound 0) (CBound 0)) + singleReplacement <- + maybe + (assertFailure "checked one-domain replacement failed") + pure + (checkedFunctionalReplacementConstruction + testGlobalType + (firstDomain :| []) + singleValue + (Just singleCondition)) + assertEqual "one-domain replacement has one canonical term" + (CApp + (CApp + (CIntrinsic Repl) + (CApp + (CApp (CIntrinsic Sep) (CIntrinsic Empty)) + (CLam TySet + (CEq TySet (CBound 0) (CBound 0))))) + (CLam TySet (CBound 0))) + (scopedCoreTerm + (namedSetConstructionTerm singleReplacement)) + + secondDomain <- checked [TySet] (CBound 0) + value <- checked [TySet, TySet] (CBound 0) + condition <- checked [TySet, TySet] + (CEq TySet (CBound 0) (CBound 0)) + replacement <- + maybe + (assertFailure "checked replacement descriptor failed") + pure + (checkedFunctionalReplacementConstruction + testGlobalType + (firstDomain :| [secondDomain]) + value + (Just condition)) + (replacementView, replacementEquation) <- + maybe + (assertFailure "checked replacement views failed") + pure + (namedSetConstructionLocalViews + (checkedFoundationSetConstruction foundation) + replacement) + let terminal = + andP + (CEq TySet (CBound 0) (CBound 0)) + (CEq TySet (CBound 2) (CBound 0)) + secondWitness = + existsP + (andP + (memberP (CBound 0) (CBound 1)) + terminal) + firstWitness = + existsP + (andP + (memberP (CBound 0) (CIntrinsic Empty)) + secondWitness) + expectedReplacementTerm = + CForall TySet + (CEq TyProp + (memberP (CBound 0) (CBound 1)) + firstWitness) + expectedReplacementView <- checked [TySet] expectedReplacementTerm + assertEqual "replacement view preserves bounds and condition" + expectedReplacementView replacementView + assertEqual "flattened replacement view is first-order" + (Set.singleton Foundation.EmptyCharacteristic) + (Foundation.foundationAxiomDependencies + (scopedCoreTerm replacementView)) + assertEqual "replacement equation retains every helper" + (Set.fromList + [ Foundation.FamilyUnionCharacteristic + , Foundation.EmptyCharacteristic + , Foundation.SeparationCharacteristic + , Foundation.ReplacementCharacteristic + ]) + (Foundation.foundationAxiomDependencies + (scopedCoreTerm replacementEquation)) + where + checked context term = + either + (assertFailure . show) + pure + (checkScopedCanonicalCore testGlobalType context term) + + memberP element set = + CApp (CApp (CIntrinsic Member) element) set + + notP proposition = CImp proposition CFalsum + + andP left right = + notP (CImp left (notP right)) + + existsP proposition = + notP (CForall TySet (notP proposition)) + specializeForall :: CanonicalTerm global -> CanonicalTerm global diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs index 26261f3..85634fe 100644 --- a/source/Test/Unit/Declaration.hs +++ b/source/Test/Unit/Declaration.hs @@ -9,28 +9,36 @@ import Checking.Core qualified as Core import Checking.Declaration qualified as Declaration import Checking.Foundation qualified as Foundation import Checking.Exact qualified as Exact +import Checking.Exact.Vocabulary qualified as Vocabulary import Checking.Identity qualified as Identity import Checking.Kernel.Derivation qualified as Kernel +import Checking.SetConstruction qualified as SetConstruction import Checking.Semantic qualified as Semantic +import Checking.Typed.Inductive qualified as Typed import Felix.Math.Codec import Felix.Module import Felix.Source import Felix.Store qualified as Store +import Meaning qualified 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 import Numeric.Natural (Natural) import Control.Exception (bracket) import Control.Exception qualified as Exception +import Control.Monad.Except (runExceptT) import Control.Monad.Logger (runNoLoggingT) +import Control.Monad.State (evalState) import System.Directory qualified as Directory import System.FilePath.Posix qualified as Posix import Test.Tasty @@ -62,6 +70,10 @@ unitTests = reconstructsImportedGlobalBindings , testCase "elaborates scoped exact propositions" elaboratesScopedExactPropositions + , testCase "lowers fixed equality aliases without global support" + lowersFixedEqualityAliases + , testCase "scopes quantified proposition terms" + scopesQuantifiedPropositionTerms , testCase "prepares exact claim envelopes" preparesExactClaimEnvelopes , testCase "lowers exact separation comprehensions" @@ -1166,8 +1178,8 @@ makePreparedObligationWithPremise fixture fingerprint = do claim [] [] - Backend.ExplicitGlobalPremises - Backend.FirstOrderLocals) + Backend.FirstOrderLocals + Backend.ExplicitHigherOrderJustification) expectRight (Provers.prepareTypedProverTask Provers.DirectTask @@ -1199,8 +1211,8 @@ makePreparedObligation fixture tag = do [Backend.typedFoundationAuxiliaryInput (fixtureFoundation fixture) tag] - Backend.NoGlobalPremises - Backend.AllLocals) + Backend.CompleteLocals + Backend.ExplicitHigherOrderJustification) expectRight (Provers.prepareTypedProverTask Provers.DirectTask @@ -1887,6 +1899,442 @@ 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) + +scopesQuantifiedPropositionTerms :: Assertion +scopesQuantifiedPropositionTerms = do + fixture <- makeNamedFixture "quantified-proposition-terms" + let x = Raw.NamedVar "x" + y = Raw.NamedVar "y" + term variable = Raw.TermExpr (Raw.ExprVar variable) + zero = Raw.TermExpr (Raw.ExprInteger Nowhere 0) + setNoun = Raw.Noun Nowhere Lexicon.builtinSetNoun [] + setPhrase named = Raw.NounPhrase [] setNoun named [] Nothing + quantified quantifier variable = + Raw.TermQuantified + quantifier Nowhere (setPhrase (Just variable)) + equalityVerb argument = + Raw.Verb Nowhere Lexicon.builtinEqualityVerb [argument] + equalityAdjective argument = + Raw.Adj + Nowhere Lexicon.builtinEqualityRightAdjective [argument] + equality left right = Core.CEq Core.TySet left right + notP proposition = Core.CImp proposition Core.CFalsum + andP left right = notP (Core.CImp left (notP right)) + existsP body = notP (Core.CForall Core.TySet (notP body)) + truth = Core.CImp Core.CFalsum Core.CFalsum + member left right = + Core.CApp + (Core.CApp (Core.CIntrinsic Core.Member) left) + right + soleSubject = + Raw.StmtNoun + (quantified Raw.Universally x :| []) + (setPhrase Nothing) + explicitSubject = + Raw.SymbolicQuantified + Nowhere Raw.Universally (x :| []) Raw.Unbounded Nothing + (Raw.StmtNoun (term x :| []) (setPhrase Nothing)) + multipleSubjects = + Raw.StmtVerbPhrase + ( quantified Raw.Universally x + :| [quantified Raw.Existentially y] + ) + (Raw.VPVerb (equalityVerb zero)) + adjectiveArgument = + Raw.StmtVerbPhrase + (zero :| []) + (Raw.VPAdj + (equalityAdjective + (quantified Raw.Universally x) :| [])) + nounArgument = + Raw.StmtNoun + (zero :| []) + (Raw.NounPhrase + [] + (Raw.Noun + Nowhere Lexicon.builtinElementNoun + [quantified Raw.Universally x]) + Nothing [] Nothing) + negatedSubject = + Raw.StmtVerbPhrase + (quantified Raw.Universally x :| []) + (Raw.VPVerbNot (equalityVerb zero)) + negatedArgument = + Raw.StmtVerbPhrase + (zero :| []) + (Raw.VPVerbNot + (equalityVerb (quantified Raw.Universally x))) + nonexistentialArgument = + Raw.StmtVerbPhrase + (zero :| []) + (Raw.VPVerb + (equalityVerb (quantified Raw.Nonexistentially x))) + negatedStatement = + Raw.StmtNeg Nowhere soleSubject + siblingConstraints = + Raw.StmtNoun + (zero :| []) + (Raw.NounPhrase + [] + (Raw.Noun + Nowhere Lexicon.builtinElementNoun + [quantified Raw.Universally x]) + Nothing + [Raw.AdjR + Nowhere Lexicon.builtinEqualityRightAdjective + [quantified Raw.Universally y]] + Nothing) + constrainedSubject = + Raw.TermQuantified Raw.Universally Nowhere + (Raw.NounPhrase + [] + (Raw.Noun + Nowhere Lexicon.builtinElementNoun [term x]) + (Just x) + [Raw.AdjR + Nowhere Lexicon.builtinEqualityRightAdjective [term x]] + (Just + (Raw.StmtVerbPhrase + (term x :| []) + (Raw.VPVerb (equalityVerb (term x)))))) + constrainedStatement = + Raw.StmtVerbPhrase + (constrainedSubject :| []) + (Raw.VPVerb (equalityVerb (term x))) + xEqualsX = equality (Core.CBound 0) (Core.CBound 0) + cases = + [ ( "sole quantified subject" + , soleSubject + , Core.CForall Core.TySet truth + ) + , ( "explicit sole quantified subject" + , explicitSubject + , Core.CForall Core.TySet truth + ) + , ( "multiple quantified subjects" + , multipleSubjects + , Core.CForall Core.TySet + (existsP + (andP + (equality + (Core.CBound 1) (Core.COpaqueInteger 0)) + (equality + (Core.CBound 0) (Core.COpaqueInteger 0)))) + ) + , ( "quantified adjective argument" + , adjectiveArgument + , Core.CForall Core.TySet + (equality (Core.COpaqueInteger 0) (Core.CBound 0)) + ) + , ( "quantified noun argument" + , nounArgument + , Core.CForall Core.TySet + (member (Core.COpaqueInteger 0) (Core.CBound 0)) + ) + , ( "quantified subject outside negation" + , negatedSubject + , Core.CForall Core.TySet + (notP + (equality + (Core.CBound 0) (Core.COpaqueInteger 0))) + ) + , ( "quantified argument inside negation" + , negatedArgument + , notP + (Core.CForall Core.TySet + (equality + (Core.COpaqueInteger 0) (Core.CBound 0))) + ) + , ( "nonexistential quantified verb argument" + , nonexistentialArgument + , notP + (existsP + (equality + (Core.COpaqueInteger 0) + (Core.CBound 0))) + ) + , ( "statement recursion bounds a quantified subject" + , negatedStatement + , notP (Core.CForall Core.TySet truth) + ) + , ( "sibling constraints own their argument quantifiers" + , siblingConstraints + , andP + (Core.CForall Core.TySet + (member + (Core.COpaqueInteger 0) + (Core.CBound 0))) + (Core.CForall Core.TySet + (equality + (Core.COpaqueInteger 0) + (Core.CBound 0))) + ) + , ( "quantified noun constraints share their binder" + , constrainedStatement + , Core.CForall Core.TySet + (Core.CImp + (andP + (member (Core.CBound 0) (Core.CBound 0)) + (andP xEqualsX xEqualsX)) + xEqualsX) + ) + ] + prepare context statement = + Exact.prepareExactProposition context statement + activeContext <- expectRight + (Exact.extendExactBinderContext + ((Exact.exactLocalId 0, x) :| []) + Exact.emptyExactBinderContext) + let action + :: Declaration.ModuleDriver Text + ( [ Either + Exact.ExactCompileError + Exact.PreparedExactProposition + ] + , Either + Exact.ExactCompileError + Exact.PreparedExactProposition + ) + action = + Declaration.runProspectiveLoweringDriver do + compiled <- traverse + (\(_label, statement, _expected) -> + prepare Exact.emptyExactBinderContext statement) + cases + collision <- prepare activeContext soleSubject + pure (compiled, collision) + runDriver fixture action >>= \case + Declaration.DriverSucceeded + (compiled, collision) _interface _prefix _closure -> do + for_ (zip cases compiled) \ + ((label, _statement, expected), result) -> + case result of + Right prepared -> + assertEqual label expected + (Core.scopedCoreTerm + (Exact.preparedExactPropositionCore prepared)) + Left failure -> + assertFailure + (label <> " failed: " + <> Text.unpack + (Exact.renderExactCompileError failure)) + case collision of + Left (Exact.ExactDuplicateLocalBinder _location variable) -> + assertEqual "quantified binder collision" x variable + Left failure -> + assertFailure + ("unexpected quantified-binder collision: " + <> Text.unpack + (Exact.renderExactCompileError failure)) + Right{} -> + assertFailure "an active quantified binder was shadowed" + case compiled of + Right sole : Right explicit : _ -> + assertEqual + "sole-subject lowering remains byte-for-byte identical" + (Exact.preparedExactPropositionCore sole) + (Exact.preparedExactPropositionCore explicit) + _ -> + assertFailure + "sole-subject equality comparison did not compile" + Declaration.DriverFailed failure _prefix -> + assertFailure + ("quantified proposition-term driver failed: " <> show failure) + Declaration.DriverSealFailed failure _prefix -> + assertFailure + ("quantified proposition-term driver did not seal: " + <> show failure) + preparesExactClaimEnvelopes :: Assertion preparesExactClaimEnvelopes = do fixture <- makeNamedFixture "exact-claim-envelope" @@ -2139,6 +2587,13 @@ lowersExactReplacementTelescopes = do (Raw.ExprInteger Nowhere 0) (equality (Raw.ExprVar x) (Raw.ExprVar y))) (Raw.ExprInteger Nowhere 0) + namedPredicateReplacement = + Raw.ExprReplacePred + predicateReplacementLocation + y + x + (Raw.ExprVar a) + (equality (Raw.ExprVar x) (Raw.ExprVar y)) app1 intrinsic argument = Core.CApp (Core.CIntrinsic intrinsic) argument app2 intrinsic first second = @@ -2170,6 +2625,9 @@ lowersExactReplacementTelescopes = do , Either Exact.ExactCompileError Exact.PreparedExactProposition + , Either + Exact.ExactCompileError + Exact.PreparedExactSetExpression ) action = Declaration.runProspectiveLoweringDriver do @@ -2182,12 +2640,24 @@ lowersExactReplacementTelescopes = do predicateReplacement <- Exact.prepareExactProposition Exact.emptyExactBinderContext predicateReplacementStatement - pure (valid, invalid, predicateReplacement) + namedContext <- + either + (impossible + . Text.unpack + . Exact.renderExactCompileError) + pure + (Exact.extendExactBinderContext + ((Exact.exactLocalId 0, a) :| []) + Exact.emptyExactBinderContext) + named <- Exact.prepareExactSetExpression + namedContext namedPredicateReplacement + pure (valid, invalid, predicateReplacement, named) runDriver fixture action >>= \case Declaration.DriverSucceeded ( Right prepared , Left failure , Left predicateReplacementFailure + , Right named ) _interface _prefix _closure -> do assertEqual "dependent replacement core" @@ -2200,27 +2670,139 @@ lowersExactReplacementTelescopes = do failure assertEqual "predicate replacement remains unsupported at its location" - (Exact.ExactUnsupportedDeclarationBody + (Exact.ExactRelationalReplacementRequiresNamedDefinition predicateReplacementLocation) predicateReplacementFailure + case Exact.preparedExactSetExpressionConstruction named of + Just (Exact.PreparedRelationalSetConstruction construction) -> do + assertEqual "relational replacement canonical term" + expectedRelationalTerm + (Core.scopedCoreTerm + (SetConstruction.relationalSetConstructionTerm + construction)) + assertEqual "relational replacement functionality" + expectedFunctionality + (Core.scopedCoreTerm + (SetConstruction.relationalSetConstructionFunctionality + construction)) + let relationalObject = + Identity.assertedObjectId + (opaqueFixtureObject fixture) + closedFunctionality = + SetConstruction.relationalSetConstructionClosedFunctionality + construction + relationalFact <- + maybe + (assertFailure + "exact functionality did not unlock relational extensionality" + >> fail "unreachable") + pure + (SetConstruction.relationalSetConstructionObjectFact + (SetConstruction.checkedFoundationSetConstruction + (fixtureFoundation fixture)) + relationalObject + construction + closedFunctionality) + assertEqual + "relational replacement flattened extensional proposition" + (expectedRelationalExtensional relationalObject) + (Core.frozenCoreTerm + (SetConstruction.relationalSetConstructionFactProposition + relationalFact)) + assertEqual + "unrelated functionality cannot unlock the relational view" + Nothing + (SetConstruction.relationalSetConstructionLocalViews + (SetConstruction.checkedFoundationSetConstruction + (fixtureFoundation fixture)) + construction + (Core.falsumScopedCore [Core.TySet])) + wrongClosed <- expectRight + (Core.checkCanonicalCore + (const Nothing) + Core.CFalsum) + assertBool + "malformed relational authority is rejected" + (isNothing + (SetConstruction.relationalSetConstructionObjectFact + (SetConstruction.checkedFoundationSetConstruction + (fixtureFoundation fixture)) + relationalObject + construction + wrongClosed)) + _ -> + assertFailure + "named predicate replacement lost its relational construction" Declaration.DriverSucceeded - (Left validFailure, _, _) _interface _prefix _closure -> + (Left validFailure, _, _, _) _interface _prefix _closure -> assertFailure ("valid replacement failed: " <> Text.unpack (Exact.renderExactCompileError validFailure)) Declaration.DriverSucceeded - (_, Right{}, _) _interface _prefix _closure -> + (_, Right{}, _, _) _interface _prefix _closure -> assertFailure "invalid replacement was accepted" Declaration.DriverSucceeded - (_, _, Right{}) _interface _prefix _closure -> + (_, _, Right{}, _) _interface _prefix _closure -> assertFailure "predicate replacement was accepted" + Declaration.DriverSucceeded + (_, _, _, Left failure) _interface _prefix _closure -> + assertFailure + ("named predicate replacement failed: " + <> Text.unpack (Exact.renderExactCompileError failure)) Declaration.DriverFailed failure _prefix -> assertFailure ("replacement driver failed: " <> show failure) Declaration.DriverSealFailed failure _prefix -> assertFailure ("replacement driver did not seal: " <> show failure) + where + relApp1 intrinsic argument = + Core.CApp (Core.CIntrinsic intrinsic) argument + relApp2 intrinsic first second = + Core.CApp (relApp1 intrinsic first) second + notP proposition = Core.CImp proposition Core.CFalsum + andP left right = notP (Core.CImp left (notP right)) + existsP body = notP (Core.CForall Core.TySet (notP body)) + relation = Core.CEq Core.TySet (Core.CBound 1) (Core.CBound 0) + restricted = + relApp2 Core.Sep (Core.CBound 0) + (Core.CLam Core.TySet (existsP relation)) + expectedRelationalTerm = + relApp2 Core.Repl restricted + (Core.CLam Core.TySet + (relApp1 Core.SetChoose (Core.CLam Core.TySet relation))) + expectedFunctionality = + Core.CForall Core.TySet + (Core.CImp + (relApp2 Core.Member (Core.CBound 0) (Core.CBound 1)) + (Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CImp + (andP + (Core.CEq Core.TySet + (Core.CBound 2) (Core.CBound 1)) + (Core.CEq Core.TySet + (Core.CBound 2) (Core.CBound 0))) + (Core.CEq Core.TySet + (Core.CBound 1) (Core.CBound 0)))))) + expectedRelationalExtensional object = + Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CEq Core.TyProp + (relApp2 Core.Member + (Core.CBound 0) + (Core.CApp + (Core.CGlobal object) + (Core.CBound 1))) + (existsP + (andP + (relApp2 Core.Member + (Core.CBound 0) + (Core.CBound 2)) + (Core.CEq Core.TySet + (Core.CBound 0) + (Core.CBound 1)))))) lowersExactFiniteSets :: Assertion lowersExactFiniteSets = do @@ -2277,6 +2859,44 @@ lowersExactFiniteSets = do (Exact.prepareExactProposition Exact.emptyExactBinderContext statement) + internal <- + expectRight + (evalState + (runExceptT (Meaning.glossStmt statement)) + Meaning.initialGlossState) + reusable <- + expectRight + (Typed.prepareTypedClosedFormula + absurd + (const Nothing) + internal + :: Either + Typed.TypedInductiveError + (Core.FrozenCheckedCore Void)) + assertEqual + "raw and reusable finite-set lowering" + expected + (Core.frozenCoreTerm reusable) + let internalSymbols = Internal.mentionedSymbols internal + assertBool + "finite-set meaning has no source-owned cons dependency" + (Internal.SymbolMixfix Raw.ConsSymbol + `Set.notMember` internalSymbols) + assertBool + "finite-set meaning retains fixed adjunction operations" + ( Set.fromList + [ Internal.SymbolMixfix Raw.UnionsSymbol + , Internal.SymbolMixfix Raw.UpairSymbol + ] + `Set.isSubsetOf` internalSymbols + ) + case Vocabulary.classifyExactSymbol + (Internal.SymbolMixfix Raw.ConsSymbol) of + Vocabulary.ExactSourceGlobal{} -> pure () + classification -> + assertFailure + ("explicit cons did not retain source ownership: " + <> show classification) runDriver fixture action >>= \case Declaration.DriverSucceeded (Right prepared) _interface _prefix _closure -> diff --git a/source/Test/Unit/Identity.hs b/source/Test/Unit/Identity.hs index b91d2b3..0cb46a5 100644 --- a/source/Test/Unit/Identity.hs +++ b/source/Test/Unit/Identity.hs @@ -547,6 +547,11 @@ validatesCompactFactAuthority = do , Authority.CheckedKernelConstruction (Authority.CheckedDefinitionEquation (fixtureIntrinsic fixture)) + , Authority.CheckedKernelConstruction + (Authority.CheckedSetConstructionExtensionality + (fixtureIntrinsic fixture) + (hashCacheFields + "test-named-construction" ["checked"])) , Authority.CheckedSourceProof requests , Authority.TrustedCompilation (Authority.DatatypeCompilation diff --git a/source/Test/Unit/Kernel.hs b/source/Test/Unit/Kernel.hs index c24debf..d01a194 100644 --- a/source/Test/Unit/Kernel.hs +++ b/source/Test/Unit/Kernel.hs @@ -430,7 +430,8 @@ replaysDirectInductiveFacts = do :| [ Inductive.DirectInductiveClause [x] [Inductive.DirectRecursiveCondition - (Internal.TermVar x)] + (Internal.TermVar x) + (Inductive.directRecursiveCarrierContext Nowhere)] (Internal.TermVar x) ] ) diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs index 267a9ad..bf4e9df 100644 --- a/source/Test/Unit/Module.hs +++ b/source/Test/Unit/Module.hs @@ -32,6 +32,7 @@ import Paths_felix qualified as Paths import Syntax.Abstract qualified as Raw import Syntax.Internal qualified as Internal import Syntax.Interface qualified as Syntax +import Syntax.Lexicon qualified as Lexicon import Syntax.Pragma qualified as Pragma import Control.Concurrent (threadDelay) @@ -51,6 +52,7 @@ import Control.Concurrent.STM , writeTVar ) import Control.Exception (bracket) +import Control.Exception qualified as Exception import Control.Monad (foldM, when) import Data.ByteString qualified as ByteString import Data.Text qualified as StrictText @@ -67,6 +69,7 @@ import Data.List (sort) import Data.Map.Strict qualified as Map import Data.Set qualified as Set import Data.Vector qualified as Vector +import Numeric.Natural (Natural) import System.Directory ( createDirectoryIfMissing , doesFileExist @@ -118,20 +121,30 @@ unitTests = compilesExactRelationExpressions , testCase "resolves source-owned set application" resolvesSourceOwnedApplication - , testCase "confines quantified terms to exact statement subjects" + , testCase "scopes quantified terms in proposition contexts" confinesExactQuantifiedTerms + , testCase "closes the exact definition declaration boundary" + closesExactDefinitionDeclarationBoundary , testCase "compiles exact ordinary proofs" compilesExactOrdinaryProofs + , testCase "restores exact binder and witness proof forms" + restoresExactBinderAndWitnessProofForms + , testCase "restores exact local reasoning and calculations" + restoresExactLocalReasoningAndCalculations + , testCase "selects calculation link failures by source order" + selectsCalculationLinkFailureBySourceOrder , testCase "compiles and reuses proof-local set definitions" compilesAndReusesProofLocalSetDefinitions , testCase "compiles and reuses proof-local function graphs" compilesAndReusesProofLocalFunctionGraphs - , testCase "confines terminal exact contradiction" + , testCase "restores exact cases and classical contradiction" confinesTerminalExactContradiction , testCase "compiles exact separation comprehensions" compilesExactSeparationComprehensions , testCase "compiles exact replacement comprehensions" compilesExactReplacementComprehensions + , testCase "compiles and reuses relational replacement" + compilesAndReusesRelationalReplacement , testCase "compiles and reuses exact finite sets" compilesAndReusesExactFiniteSets , testCase "prepares exact deterministic datatypes" @@ -142,8 +155,12 @@ unitTests = compilesAndReusesExactDatatypes , testCase "prepares exact direct inductives" preparesExactDirectInductives - , testCase "rejects nested exact inductive recursion" - rejectsNestedExactInductiveRecursion + , testCase "prepares nested exact inductive recursion" + preparesNestedExactInductiveRecursion + , testCase "compiles transparent nested inductive wrappers" + compilesTransparentNestedInductiveWrappers + , testCase "normalizes nested exact inductive contexts" + normalizesNestedExactInductiveContexts , testCase "compiles and reuses exact inductives" compilesAndReusesExactInductives , testCase "authorizes recursive exact inductives" @@ -156,8 +173,8 @@ unitTests = doesNotTreatMarkerOnlyNounAsSet , testCase "rejects proof-local generalization" rejectsProofLocalGeneralization - , testCase "rejects nested exact set induction" - rejectsNestedExactSetInduction + , testCase "restores checked set induction" + restoresCheckedSetInduction , testCase "compiles exact omitted proofs" compilesExactOmittedProofs , testCase "propagates and reuses exact escape authority" @@ -563,6 +580,7 @@ buildsConfinedFinalPrelude = do candidate "pow_iff" Foundation.PowerSetCharacteristic + assertRejectsAdditionalOmegaFact candidate FinalPrelude.FinalPreludeBuildFailed failure prefix -> assertFailure ("final prelude failed after " @@ -578,6 +596,92 @@ buildsConfinedFinalPrelude = do FinalPrelude.FinalPreludeSourceParseFailed failure -> assertFailure ("final prelude did not parse: " <> show failure) +assertRejectsAdditionalOmegaFact + :: FinalPrelude.FinalPreludeCandidate + -> Assertion +assertRejectsAdditionalOmegaFact candidate = do + omegaId <- + case FinalPrelude.finalPreludePublicRole + candidate FinalPrelude.PreludeOmegaObject of + Just (FinalPrelude.FinalPreludeObjectRole identity) -> + pure identity + role -> + assertFailure ("unexpected Omega role " <> show role) + >> fail "unreachable" + batch <- batchByAlias + (FinalPrelude.finalPreludePrefix candidate) + "prelude_omega" + let delta = Declaration.committedBatchDelta batch + facts = Semantic.declarationDeltaFacts delta + aliases = Semantic.declarationDeltaAliases delta + propositions = Declaration.committedBatchPropositions batch + certificates <- + maybe + (assertFailure "Omega declaration validation is absent" + >> fail "unreachable") + (pure . Semantic.declarationValidationRecordCertificates) + (Declaration.committedBatchDeclarationValidation batch) + (omegaBody, extensional, descriptor, extraFact, extraProposition, + extraCertificate) <- + case (facts, propositions, certificates) of + ( [_equationFact, extensionalFact] + , [equationProposition, extensionalProposition] + , [ _equationCertificate + , extensionalCertificate + ] + ) -> do + body <- case Core.frozenCoreTerm + (Identity.checkedPropositionTerm equationProposition) of + Core.CEq Core.TySet + (Core.CGlobal identity) candidateBody + | identity == omegaId -> pure candidateBody + target -> + assertFailure + ("unexpected Omega equation " <> show target) + >> fail "unreachable" + constructionDescriptor <- + case Authority.validationDirectAuthorization + extensionalCertificate of + Authority.CheckedKernelConstruction + (Authority.CheckedSetConstructionExtensionality + identity candidateDescriptor) + | identity == omegaId -> pure candidateDescriptor + authorization -> + assertFailure + ("unexpected Omega extensional authority " + <> show authorization) + >> fail "unreachable" + pure + ( body + , Identity.checkedPropositionTerm extensionalProposition + , constructionDescriptor + , extensionalFact + , extensionalProposition + , extensionalCertificate + ) + (candidateFacts, candidatePropositions, candidateCertificates) -> + assertFailure + ("unexpected Omega inventory shape " + <> show + ( length candidateFacts + , length candidatePropositions + , length candidateCertificates + )) + >> fail "unreachable" + case FinalPrelude.validateOmegaFactInventory + omegaId omegaBody extensional descriptor + (facts <> [extraFact]) + aliases + (propositions <> [extraProposition]) + (certificates <> [extraCertificate]) of + Left (FinalPrelude.FinalPreludeFactContentMismatch + "prelude_omega") -> + pure () + result -> + assertFailure + ("additional Omega construction fact was accepted: " + <> show result) + publishesFinalPreludeRoot :: Assertion publishesFinalPreludeRoot = do foundation <- expectRight Foundation.checkedFoundation @@ -720,32 +824,6 @@ checkedPropositionTermByAlias sealed name = do ] pure (Identity.checkedPropositionTerm proposition) -assertCleanFactAlias - :: Module.SealedTypedModule - -> Text - -> Assertion -assertCleanFactAlias sealed name = do - delta <- localDeltaByAlias sealed name - alias <- sole - ("semantic alias " <> StrictText.unpack name) - [ candidate - | candidate <- Semantic.declarationDeltaAliases delta - , Semantic.semanticAliasName candidate - == Semantic.semanticName name - ] - fact <- sole - ("semantic fact " <> StrictText.unpack name) - [ candidate - | candidate <- Semantic.declarationDeltaFacts delta - , Semantic.semanticFactFingerprint candidate - == Semantic.semanticAliasTarget alias - ] - assertEqual - ("clean authority for " <> StrictText.unpack name) - Authority.cleanAuthoritySafety - (Authority.factAuthoritySafety - (Semantic.semanticFactAuthority fact)) - batchByAlias :: Declaration.PendingModulePrefix -> Text @@ -974,7 +1052,7 @@ rejectsUnsupportedTypedSource = do source (Module.TypedActionFailed (Module.TypedExactCompileFailed - (Exact.ExactUnsupportedDeclarationBody location))) + (Exact.ExactGuardedOpaqueSignature location))) prefix)) , _measurements ) -> do @@ -983,7 +1061,7 @@ rejectsUnsupportedTypedSource = do (safeRelativePathFilePath (resolvedSourceRelativePath source)) assertEqual "unsupported source location line" - 1 + 2 (locLine location) assertEqual "failure retains the initial module prefix" 0 @@ -995,10 +1073,10 @@ rejectsUnsupportedTypedSource = do ("project:test/phase3/typed-unsupported.tex" `StrictText.isInfixOf` diagnostic) assertBool "diagnostic retains best location" - ("typed-unsupported.tex 1:1" + ("typed-unsupported.tex 2:14" `StrictText.isInfixOf` diagnostic) assertBool "diagnostic explains the typed failure" - ("not yet supported by exact elaboration" + ("opaque signature cannot have a header assumption" `StrictText.isInfixOf` diagnostic) Left err -> assertFailure ("unexpected verification driver error: " <> show err) @@ -1324,6 +1402,29 @@ compilesExactStructures = do (Semantic.semanticStructureOperationObject parentOperation `Set.member` operationGlobals) + let assertEquivalentClaim surface explicit = do + surfaceTerm <- + checkedPropositionTermByAlias parent surface + explicitTerm <- + checkedPropositionTermByAlias parent explicit + assertEqual + (StrictText.unpack surface + <> " uses the inherited carrier") + explicitTerm + surfaceTerm + assertEquivalentClaim + "pointed_self_member" + "pointed_self_member_explicit" + assertEquivalentClaim + "pointed_self_not_member" + "pointed_self_not_member_explicit" + assertEquivalentClaim + "pointed_self_element" + "pointed_self_element_explicit" + assertEquivalentClaim + "pointed_header_member" + "pointed_header_member_explicit" + childBatch <- sole "child structure batch" childBatches childDelta <- sole "child structure delta" childDeltas childDescriptor <- sole "child structure descriptor" @@ -1913,36 +2014,440 @@ confinesExactQuantifiedTerms = do explicit quantified + propositionWorkspace <- parseFinalExactWorkspace + prelude mounts + "test/phase5/exact-quantified-proposition-terms.tex" + observations <- newIORef [] + let observingResolver = + Declaration.vampireResolver \prepared -> do + let problem = + Provers.preparedTypedProverLogicalProblem + prepared + request = + Provers.preparedTypedProverRequest + prepared + modifyIORef' observations + (<> [ ( Provers.preparedVerificationRequestId + request + , Backend.supportedPropositionTerm + (Backend.typedProblemClaim problem) + , Backend.typedProblemRoute problem + , Backend.typedProblemAuxiliaryTag + <$> Vector.toList + (Backend.typedProblemAuxiliaries + problem) + ) + ]) + runNoLoggingT + (Provers.runPreparedTypedProver + prover prepared) + freshModules <- + compileFinalParsedWorkspaceWithResolver + foundation prelude observingResolver + propositionWorkspace + freshRoot <- case reverse freshModules of + rootModule : _ -> pure rootModule + [] -> + assertFailure + "quantified proposition-term root is absent" + >> fail "unreachable" + let member left right = + Core.CApp + (Core.CApp + (Core.CIntrinsic Core.Member) left) + right + memberAtX = + member (Core.CBound 0) (Core.CBound 1) + expectedFunctionTarget = + Core.CForall Core.TySet + (Core.CEq Core.TySet + (Core.CBound 0) + (Core.CBound 0)) + expectedVerbRequestTarget = + Core.CForall Core.TySet + (Core.CImp memberAtX memberAtX) + expectedVerbProposition = + Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CImp memberAtX memberAtX)) + expectedTargets = + [ expectedFunctionTarget + , expectedVerbRequestTarget + ] + ordinaryImplicitAuxiliaries = + [ Foundation.EmptyCharacteristic + , Foundation.PairSetCharacteristic + , Foundation.FamilyUnionCharacteristic + , Foundation.PowerSetCharacteristic + ] + freshObservations <- readIORef observations + assertEqual + "nested function and verb terms have exact FOF targets" + [ ( target + , Backend.RouteFof + , ordinaryImplicitAuxiliaries + ) + | target <- expectedTargets + ] + [ (target, route, auxiliaries) + | (_request, target, route, auxiliaries) <- + freshObservations + ] + functionTarget <- checkedPropositionTermByAlias freshRoot + "phase5_quantified_function_argument" + verbTarget <- checkedPropositionTermByAlias freshRoot + "phase5_quantified_verb_argument" + assertEqual "nested function proposition core" + expectedFunctionTarget + (Core.frozenCoreTerm functionTarget) + assertEqual "nested verb proposition core" + expectedVerbProposition + (Core.frozenCoreTerm verbTarget) + let proofRecords moduleValue = + concatMap + Declaration.committedBatchProofValidations + (Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix moduleValue)) + proofAuthorizations moduleValue = + Authority.validationDirectAuthorization + . Semantic.proofValidationRecordCertificate + <$> proofRecords moduleValue + case proofAuthorizations freshRoot of + [ Authority.CheckedSourceProof [_functionRequest] + , Authority.CheckedSourceProof [_verbRequest] + ] -> pure () + authorizations -> + assertFailure + ("unexpected quantified-term authority: " + <> show authorizations) + assertBool + "quantified terms add no escape-backed authority" + (all + ((== Authority.cleanAuthoritySafety) + . Authority.factAuthoritySafety + . Semantic.semanticFactAuthority) + (concatMap + (Semantic.declarationDeltaFacts + . Declaration.committedBatchDelta) + (Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix freshRoot)))) + + traverse_ + (expectRightIO + . Store.writePendingModulePrefix store + . Module.sealedTypedModulePrefix) + freshModules + let validation = + Declaration.WarmValidation + (Declaration.validationLookup + (expectRightIO + . Store.loadProofValidation store) + (expectRightIO + . Store.loadDeclarationValidation store)) + warmModules <- + compileParsedWorkspaceWithReadiness + foundation + (Module.finalPreludeReadiness prelude) + unusedResolver + validation + propositionWorkspace + warmRoot <- case reverse warmModules of + rootModule : _ -> pure rootModule + [] -> + assertFailure + "warm quantified proposition-term root is absent" + >> fail "unreachable" + assertEqual "fresh and warm quantified semantic interface" + (Module.sealedTypedModuleSemantic freshRoot) + (Module.sealedTypedModuleSemantic warmRoot) + assertEqual "fresh and warm quantified request authority" + (proofAuthorizations freshRoot) + (proofAuthorizations warmRoot) + assertEqual "fresh and warm quantified prefix" + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix freshRoot)) + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix warmRoot)) + negative <- - withAcceptedFixtureVampire "felix-exact-quantified-subject-nested" + withAcceptedFixtureVampire "felix-exact-quantified-term-valued" \prover -> runNoLoggingT (Api.verifyMeasured prover - "test/phase5/exact-quantified-subject-nested.tex") + "test/phase5/exact-quantified-term-valued.tex") case negative of Right ( Api.VerificationCheckingFailure _report (Api.VerificationTypedModuleError _source (Module.TypedActionFailed - (Module.TypedExactProofFailed - (ExactProof.ExactProofElaborationFailed - (Exact.ExactQuantifiedTermRequiresStatementSubject - location)))) + (Module.TypedExactCompileFailed + (Exact.ExactQuantifiedTermRequiresPropositionContext + location))) prefix) , _measurements ) -> do - assertEqual "nested quantified term line" 8 (locLine location) - assertEqual "earlier exact definition remains committed" - 1 - (length (Declaration.pendingModulePrefixBatches prefix)) + assertEqual "term-valued quantified term line" + 2 (locLine location) + assertBool "failed term-valued abbreviation publishes no prefix" + (null (Declaration.pendingModulePrefixBatches prefix)) Left failure -> assertFailure - ("unexpected nested quantified-term failure: " + ("unexpected term-valued quantified-term failure: " <> show failure) Right{} -> - assertFailure "nested quantified exact term was admitted" + assertFailure "term-valued quantified exact term was admitted" + +closesExactDefinitionDeclarationBoundary :: Assertion +closesExactDefinitionDeclarationBoundary = do + repository <- getCurrentDirectory + foundation <- expectRight Foundation.checkedFoundation + bootstrap <- + expectRight + =<< Module.buildBootstrapPreludeFixture + foundation + unusedResolver + repositoryMounts <- exactFixtureMounts repository + Temp.withSystemTempDirectory "felix-definition-boundary" \directory -> do + mounts <- exactFixtureMounts directory + annotatedText <- + readFile + (repository Posix.</> + "test/phase5/exact-definition-boundary.tex") + let relative = "entry.tex" + sourcePath = directory Posix.</> relative + unannotatedText = + StrictText.unpack + (StrictText.replace + "A set " + "" + (StrictText.pack annotatedText)) + writeFile sourcePath annotatedText + annotatedWorkspace <- + parseExactWorkspace bootstrap mounts relative + annotated <- sole "annotated definition module" + =<< compileParsedWorkspace + foundation bootstrap annotatedWorkspace + assertEqual "annotated definition declaration count" + 4 + (length + (Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix annotated))) + assertBool "annotated definitions prepare no Vampire validations" + (null (proofValidationRecords annotated)) + let annotatedBatches = + Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix annotated) + symbolicBatch <- sole "symbolic primary declaration" + (take 1 (drop 2 annotatedBatches)) + wrapperBatch <- sole "functional wrapper declaration" + (take 1 (drop 3 annotatedBatches)) + symbolicObject <- bindingObject "symbolic primary" symbolicBatch + wrapperObject <- bindingObject "functional wrapper" wrapperBatch + wrapperContent <- sole "functional wrapper transparent object" + [ Identity.assertedObjectContent object + | batch <- + Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix annotated) + , object <- Declaration.committedBatchObjects batch + , Identity.assertedObjectId object == wrapperObject + ] + case wrapperContent of + Identity.TransparentObjectContent _theory _type body -> + assertEqual + "functional wrapper applies the primary symbolic object" + (Set.singleton symbolicObject) + (Core.canonicalTermGlobals body) + content -> + assertFailure + ("functional wrapper is not transparent: " <> show content) + + writeFile sourcePath unannotatedText + unannotatedWorkspace <- + parseExactWorkspace bootstrap mounts relative + unannotated <- sole "unannotated definition module" + =<< compileParsedWorkspace + foundation bootstrap unannotatedWorkspace + assertEqual + "canonical set annotations do not change the semantic interface" + (Module.sealedTypedModuleSemantic unannotated) + (Module.sealedTypedModuleSemantic annotated) + assertEqual + "canonical set annotations do not change declaration identity" + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix unannotated)) + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix annotated)) + assertEqual + "canonical set annotations do not change direct authority" + (directDeclarationAuthorizations unannotated) + (directDeclarationAuthorizations annotated) + + let storePath = directory Posix.</> "store.sqlite" + bracket + (snd <$> (Store.openStore storePath + (Identity.theoryId foundation) >>= expectRight)) + Store.closeStore + \store -> do + expectRightIO + (Store.writePendingModulePrefix store + (Module.sealedTypedModulePrefix annotated)) + let validation = + Declaration.WarmValidation + (Declaration.validationLookup + (expectRightIO + . Store.loadProofValidation store) + (expectRightIO + . Store.loadDeclarationValidation store)) + warm <- sole "warm annotated definition module" + =<< compileParsedWorkspaceWithValidation + foundation bootstrap unusedResolver validation + annotatedWorkspace + assertEqual "warm annotated semantic interface" + (Module.sealedTypedModuleSemantic annotated) + (Module.sealedTypedModuleSemantic warm) + assertEqual "warm annotated declaration identity" + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix annotated)) + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix warm)) + assertEqual "warm annotated direct authority" + (directDeclarationAuthorizations annotated) + (directDeclarationAuthorizations warm) + assertBool "warm annotated definitions run no prover" + (null (proofValidationRecords warm)) + + annotationFailure <- exactFailure foundation bootstrap repositoryMounts + "test/phase5/exact-definition-annotation-failure.tex" + case annotationFailure of + ( Exact.ExactNonCanonicalSetDefinitionAnnotation location + , prefix + ) -> do + assertEqual "nontrivial annotation line" 2 (locLine location) + assertBool "nontrivial annotation publishes no prefix" + (null (Declaration.pendingModulePrefixBatches prefix)) + assertBool "annotation diagnostic gives the explicit migration" + ("total condition in the definiens" + `StrictText.isInfixOf` + Exact.renderExactCompileError + (fst annotationFailure)) + (failure, _prefix) -> + assertFailure + ("unexpected annotation failure: " <> show failure) + + aliasFailure <- exactFailure foundation bootstrap repositoryMounts + "test/phase5/exact-definition-alias-failure.tex" + case aliasFailure of + (Exact.ExactDefinitionCombinedSymbolicAlias location, prefix) -> do + assertEqual "combined symbolic alias line" 2 (locLine location) + assertBool "combined symbolic alias publishes no prefix" + (null (Declaration.pendingModulePrefixBatches prefix)) + assertBool "combined alias diagnostic gives the wrapper migration" + ("define the symbolic operator first" + `StrictText.isInfixOf` + Exact.renderExactCompileError (fst aliasFailure)) + (failure, _prefix) -> + assertFailure + ("unexpected combined-alias failure: " <> show failure) + + guardFailure <- exactFailure foundation bootstrap repositoryMounts + "test/phase5/exact-definition-guard-failure.tex" + case guardFailure of + (Exact.ExactGuardedTransparentDefinition location, prefix) -> do + assertEqual "guarded definition line" 2 (locLine location) + assertBool "guarded definition publishes no prefix" + (null (Declaration.pendingModulePrefixBatches prefix)) + assertBool "guard diagnostic gives the total-definition migration" + ("where a corresponding opaque signature form exists" + `StrictText.isInfixOf` + Exact.renderExactCompileError (fst guardFailure)) + (failure, _prefix) -> + assertFailure + ("unexpected guarded-definition failure: " <> show failure) + + assertRussellSetAnnotation bootstrap repository + where + proofValidationRecords moduleValue = + concatMap + Declaration.committedBatchProofValidations + (Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix moduleValue)) + + directDeclarationAuthorizations moduleValue = + [ Authority.validationDirectAuthorization certificate + | batch <- + Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix moduleValue) + , validation <- + maybeToList + (Declaration.committedBatchDeclarationValidation batch) + , certificate <- + Semantic.declarationValidationRecordCertificates validation + ] + + bindingObject label batch = do + binding <- sole (label <> " semantic binding") + (Semantic.semanticEnvironmentBindings + (Semantic.declarationDeltaEnvironment + (Declaration.committedBatchDelta batch))) + pure + (Semantic.semanticGlobalTargetObject + (Semantic.semanticGlobalBindingTarget binding)) + + exactFailure foundation bootstrap mounts relative = do + workspace <- parseExactWorkspace bootstrap mounts relative + parsed <- sole "failed exact definition module" + (toList + (Parse.parsedWorkspaceImportedBeforeImporter workspace)) + input <- expectRight + (Module.typedModuleInput + foundation + (Module.bootstrapPreludeReadiness bootstrap) + unusedResolver + Declaration.FreshValidation + parsed + []) + Module.runTypedModule input >>= \case + Module.TypedModuleFailed + (Module.TypedActionFailed + (Module.TypedExactCompileFailed failure)) + prefix -> + pure (failure, prefix) + result -> + assertFailure + (case result of + Module.TypedModuleSucceeded{} -> + "expected exact definition failure, but the module succeeded" + Module.TypedModuleOpenFailed{} -> + "expected exact definition failure, but the module did not open" + Module.TypedModuleFailed{} -> + "expected an exact compile failure, but checking failed differently") + >> fail "unreachable" + + assertRussellSetAnnotation bootstrap repository = do + mounts <- exactFixtureMounts repository + workspace <- parseExactWorkspace + bootstrap mounts "test/examples/russell.tex" + parsed <- sole "Russell parity module" + (toList + (Parse.parsedWorkspaceImportedBeforeImporter workspace)) + case Parse.identifiedParsedModuleBlocks + (Module.identifiedModuleParsed + (Module.identifiedPhysicalModule parsed)) of + Raw.BlockDefn _location _title _marker + (Raw.Defn [] + (Raw.DefnAdj + (Just (Raw.NounPhrase + [] (Raw.Noun _ noun []) Nothing [] Nothing)) + _subject _adjective) + _statement) : _ -> + assertBool "Russell uses the canonical built-in set noun" + (Lexicon.isBuiltinSetNoun noun) + _ -> + assertFailure + "Russell source does not retain its annotated adjective head" + compilesExactOrdinaryProofs :: Assertion compilesExactOrdinaryProofs = Temp.withSystemTempDirectory "felix-exact-proofs" \root -> do @@ -2084,6 +2589,925 @@ compilesExactOrdinaryProofs = element) set +restoresExactBinderAndWitnessProofForms :: Assertion +restoresExactBinderAndWitnessProofForms = + Temp.withSystemTempDirectory "felix-exact-proof-parity" \root -> do + repository <- getCurrentDirectory + foundation <- expectRight Foundation.checkedFoundation + bootstrap <- + expectRight + =<< Module.buildBootstrapPreludeFixture + foundation + unusedResolver + mounts <- exactFixtureMounts repository + workspace <- parseExactWorkspace + bootstrap mounts "test/phase5/exact-proof-parity.tex" + parsed <- sole "parsed proof-parity module" + (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) + let blocks = + Parse.identifiedParsedModuleBlocks + (Parse.parsedModuleIdentified parsed) + claims = [claim | claim@Raw.BlockClaim{} <- blocks] + proofs = + [ proof + | Raw.BlockProof _location proof _end <- blocks + ] + omittedClaim <- + case reverse claims of + claim : _ -> pure claim + [] -> assertFailure "missing omitted witness claim" + >> fail "unreachable" + omittedProof <- + case reverse proofs of + proof : _ -> pure proof + [] -> assertFailure "missing omitted witness proof" + >> fail "unreachable" + Declaration.runModuleDriver + foundation + preludeModuleName + [] + unusedResolver + Declaration.FreshValidation do + Declaration.runProspectiveLoweringDriver + (ExactProof.prepareExactProof + omittedClaim (Just omittedProof)) + >>= either Declaration.failModuleDriver pure + >>= \case + Right (Declaration.DriverSucceeded + prepared _semantic _prefix _closure) -> + case ExactProof.preparedExactProofFirstOmission prepared of + Just location -> + assertEqual "nested Take retains first omission" + 106 (locLine location) + Nothing -> + assertFailure "nested Take lost its omission" + Right Declaration.DriverFailed{} -> + assertFailure "omitted witness preparation failed" + Right Declaration.DriverSealFailed{} -> + assertFailure "omitted witness preparation did not seal" + Left failure -> + assertFailure + ("omitted witness preparation did not open: " + <> show failure) + let executable = root Posix.</> "vampire" + storePath = root Posix.</> "store.sqlite" + writeFile executable + (unlines + [ "#!/bin/sh" + , "cat >/dev/null" + , "printf '%s\\n' '% SZS status Theorem for exact-proof-parity'" + ]) + permissions <- getPermissions executable + setPermissions executable + (setOwnerExecutable True permissions) + observations <- newIORef [] + fresh <- + sole "proof-parity module" + =<< compileParsedWorkspaceWithValidation + foundation + bootstrap + (observingAcceptedResolver executable observations) + Declaration.FreshValidation + workspace + observed <- readIORef observations + assertEqual "restored proof request count" 17 (length observed) + assertEqual + "restored proof declarations preserve discharge order" + [1, 1, 1, 1, 1, 1, 3, 2, 2, 3, 1] + (proofRequestCounts fresh) + case observed of + first : second : third : fourth : _rest -> do + assertGuardRequest "single bounded fix" 2 first + assertGuardRequest "multiple bounded fix" 3 second + assertGuardRequest "negative bounded fix" 2 third + assertGuardRequest "fix such that" 2 fourth + _ -> assertFailure "missing bounded-fix requests" + case drop 4 observed of + leftFirst : rightFirst : _ -> do + assertSequentialAssumptions "left conjunct first" leftFirst + assertSequentialAssumptions "right conjunct first" rightFirst + _ -> assertFailure "missing conjunction-assumption requests" + assertTakeSequence "bounded TakeVar" (drop 6 observed) + assertTakeSequence "existential Have" (drop 13 observed) + case drop 9 observed of + namedDischarge : _namedFinal : anonymousDischarge : _ -> do + assertExactDischarge "named noun" namedDischarge + assertEqual "named noun opens two witness binders" + 2 + (leadingExistentials + (observedClaimTerm namedDischarge)) + assertExactDischarge "anonymous noun" anonymousDischarge + assertEqual "anonymous noun opens one unnameable binder" + 1 + (leadingExistentials + (observedClaimTerm anonymousDischarge)) + _ -> assertFailure "missing noun-witness requests" + lastBatch <- + case reverse + (Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix fresh)) of + batch : _ -> pure batch + [] -> assertFailure "missing restored-proof batches" + >> fail "unreachable" + lastFact <- sole "omitted witness fact" + (Semantic.declarationDeltaFacts + (Declaration.committedBatchDelta lastBatch)) + assertEqual "omitted continuation remains escape-backed" + (Authority.authoritySafety + (Authority.singletonEscapeKind Authority.Omitted)) + (Authority.factAuthoritySafety + (Semantic.semanticFactAuthority lastFact)) + assertBool "proof-local witnesses publish no objects" + (all + (null . Declaration.committedBatchObjects) + (Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix fresh))) + + bracket + (snd <$> (Store.openStore storePath + (Identity.theoryId foundation) >>= expectRight)) + Store.closeStore + \store -> do + expectRightIO + (Store.writePendingModulePrefix store + (Module.sealedTypedModulePrefix fresh)) + let validation = + Declaration.WarmValidation + (Declaration.validationLookup + (expectRightIO + . Store.loadProofValidation store) + (expectRightIO + . Store.loadDeclarationValidation store)) + warmRuns <- newIORef (0 :: Int) + warm <- + sole "warm proof-parity module" + =<< compileParsedWorkspaceWithValidation + foundation + bootstrap + (countingAcceptedResolver executable warmRuns) + validation + workspace + assertEqual "warm restored proofs skip Vampire" + 0 =<< readIORef warmRuns + assertEqual + "fresh and warm proof validation keys and authority" + (proofValidationRecords fresh) + (proofValidationRecords warm) + assertEqual + "fresh and warm checked proposition identities" + (map Identity.checkedPropositionId + (concatMap Declaration.committedBatchPropositions + (Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix fresh)))) + (map Identity.checkedPropositionId + (concatMap Declaration.committedBatchPropositions + (Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix warm)))) + + assertProofParityFailure + foundation bootstrap mounts + "test/phase5/exact-proof-parity-invalid-fix.tex" + (\case + ExactProof.ExactProofGoalStatementMismatch location -> + locLine location == 6 + _ -> False) + assertProofParityFailure + foundation bootstrap mounts + "test/phase5/exact-proof-parity-invalid-fix-shape.tex" + (\case + ExactProof.ExactProofExpectedUniversalGoal location -> + locLine location == 6 + _ -> False) + assertProofParityFailure + foundation bootstrap mounts + "test/phase5/exact-proof-parity-invalid-assume.tex" + (\case + ExactProof.ExactProofGoalStatementMismatch location -> + locLine location == 6 + _ -> False) + where + observingAcceptedResolver executable observations = + Declaration.vampireResolver \prepared -> do + let problem = Provers.preparedTypedProverLogicalProblem prepared + claim = Backend.typedProblemClaim problem + locals = Backend.typedProblemLocalPremises problem + observation = + ProofParityObservation + (snd <$> Vector.toList + (Backend.supportedPropositionSupport claim)) + (Backend.supportedPropositionTerm claim) + [ ( Backend.localPremiseOrdinalValue + (Backend.typedLocalPremiseOrdinal premise) + , snd <$> Vector.toList + (Backend.supportedPropositionSupport + (Backend.typedLocalPremiseProposition + premise)) + , Backend.supportedPropositionTerm + (Backend.typedLocalPremiseProposition premise) + ) + | premise <- Vector.toList locals + ] + modifyIORef' observations (<> [observation]) + runNoLoggingT + (Provers.runPreparedTypedProver + (Provers.vampire + executable + Provers.defaultTimeLimit + Provers.defaultMemoryLimit) + prepared) + + assertGuardRequest label supportCount observation = do + assertEqual (label <> " support") + supportCount + (length (observedClaimSupport observation)) + case observedLocals observation of + [(_ordinal, _support, local)] -> + assertEqual (label <> " exact guard") + (observedClaimTerm observation) + local + locals -> + assertFailure + (label <> ": expected one guard, found " + <> show (length locals)) + + assertTakeSequence label observations = + case observations of + discharge : continuation : _ -> do + assertExactDischarge label discharge + assertEqual (label <> " continuation premise ordinals") + [0, 1] + [ ordinal + | (ordinal, _support, _term) <- + observedLocals continuation + ] + assertEqual (label <> " continuation witness support") + 2 + (length (observedClaimSupport continuation)) + _ -> assertFailure (label <> ": missing request sequence") + + assertSequentialAssumptions label observation = do + assertEqual (label <> " premise ordinals") + [0, 1] + [ ordinal + | (ordinal, _support, _term) <- observedLocals observation + ] + case observedLocals observation of + (_ordinal, _support, first) : _ -> + assertEqual (label <> " retained source order") + (observedClaimTerm observation) + first + [] -> assertFailure (label <> ": no scoped assumptions") + + assertExactDischarge label discharge = + case observedLocals discharge of + [(_ordinal, _support, local)] -> + assertEqual (label <> " exact existential discharge") + (observedClaimTerm discharge) + local + locals -> + assertFailure + (label <> ": unexpected discharge premises " + <> show (length locals)) + + proofRequestCounts sealed = + [ case Declaration.committedBatchProofValidations batch of + [record] -> + case Authority.validationDirectAuthorization + (Semantic.proofValidationRecordCertificate record) of + Authority.CheckedSourceProof requests -> length requests + Authority.OmittedAuthorization -> 1 + authorization -> + error ("unexpected restored-proof authority: " + <> show authorization) + records -> + error ("unexpected restored-proof validation count: " + <> show (length records)) + | batch <- Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix sealed) + ] + + proofValidationRecords sealed = + concatMap Declaration.committedBatchProofValidations + (Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix sealed)) + + leadingExistentials + :: Core.CanonicalTerm Identity.ObjectId + -> Int + leadingExistentials = \case + Core.CImp + (Core.CForall Core.TySet + (Core.CImp body Core.CFalsum)) + Core.CFalsum -> + 1 + leadingExistentials body + _ -> 0 + +data ProofParityObservation = ProofParityObservation + { observedClaimSupport :: ![Core.CoreType] + , observedClaimTerm :: !(Core.CanonicalTerm Identity.ObjectId) + , observedLocals :: + ![(Natural, [Core.CoreType], Core.CanonicalTerm Identity.ObjectId)] + } + +restoresExactLocalReasoningAndCalculations :: Assertion +restoresExactLocalReasoningAndCalculations = + Temp.withSystemTempDirectory "felix-exact-local-reasoning" \root -> do + repository <- getCurrentDirectory + foundation <- expectRight Foundation.checkedFoundation + bootstrap <- + expectRight + =<< Module.buildBootstrapPreludeFixture + foundation + unusedResolver + mounts <- exactFixtureMounts repository + workspace <- parseExactWorkspace + bootstrap mounts "test/phase5/exact-proof-local-reasoning.tex" + let executable = root Posix.</> "vampire" + storePath = root Posix.</> "store.sqlite" + writeAcceptedFixtureVampire executable + observations <- newIORef [] + fresh <- + sole "exact local-reasoning module" + =<< compileParsedWorkspaceWithValidation + foundation + bootstrap + (observingResolver executable observations) + Declaration.FreshValidation + workspace + observed <- readIORef observations + assertEqual "local-reasoning request count" 16 (length observed) + assertEqual "proof forms retain source request order" + [2, 3, 3, 2, 2, 3, 1] + (requestCounts fresh) + case observed of + sufficesImplication : sufficesReduction + : equalityFirst : equalitySecond : equalityContinuation + : biconditionalFirst : biconditionalSecond + : biconditionalContinuation + : quantifiedLink : quantifiedContinuation + : sinceStructuralClaim : sinceStructuralContinuation + : sinceDischarge : sinceClaim : sinceContinuation + : _omittedSufficesImplication + : [] -> do + case localReasoningTarget sufficesImplication of + Core.CImp antecedent conclusion -> do + assertEqual + "Suffices implication starts from the reduction" + (localReasoningTarget sufficesReduction) + antecedent + assertBool + "Suffices keeps its distinct current goal as conclusion" + (conclusion /= antecedent) + implication -> + assertFailure + ("expected Suffices implication, found " + <> show implication) + assertEqual "first equality link uses its destination citation" + 1 (localReasoningGlobalCount equalityFirst) + assertEqual "second equality link uses local-only justification" + 0 (localReasoningGlobalCount equalitySecond) + assertDerivedContinuation + "equality calculation" + [0, 1] + (localReasoningTarget equalityContinuation) + equalityContinuation + assertPairwiseDistinct + "equality links and endpoint" + [ localReasoningTarget equalityFirst + , localReasoningTarget equalitySecond + , localReasoningTarget equalityContinuation + ] + assertEqual "first biconditional link remains proposition equality" + Core.TyProp + (equalityOperandType + (localReasoningTarget biconditionalFirst)) + assertDerivedContinuation + "biconditional calculation" + [0] + (localReasoningTarget biconditionalContinuation) + biconditionalContinuation + assertPairwiseDistinct + "biconditional links and endpoint" + [ localReasoningTarget biconditionalFirst + , localReasoningTarget biconditionalSecond + , localReasoningTarget biconditionalContinuation + ] + assertEqual "quantified calculation closes both binders" + 2 + (leadingForalls + (localReasoningTarget quantifiedLink)) + assertQuantifiedCalculationGuard + (localReasoningTarget quantifiedLink) + assertDerivedContinuation + "quantified calculation" + [0] + (localReasoningTarget quantifiedLink) + quantifiedContinuation + assertEqual + "quantified source goal and derived local retain the same guard shape" + (quantifiedCalculationShape + (localReasoningTarget quantifiedContinuation)) + (quantifiedCalculationShape + (localReasoningTarget quantifiedLink)) + assertQuantifiedCalculationGuard + (localReasoningTarget quantifiedContinuation) + assertEqual "structural Since submits no premise discharge" + [0] + (localReasoningLocalOrdinals sinceStructuralClaim) + assertEqual "structural Since does not duplicate its premise" + [0, 1] + (localReasoningLocalOrdinals + sinceStructuralContinuation) + assertEqual "ATP-backed Since starts from existing locals only" + [0] + (localReasoningLocalOrdinals sinceDischarge) + assertEqual "Since claim sees the admitted discourse premise" + [0, 1] + (localReasoningLocalOrdinals sinceClaim) + assertEqual "Since continuation sees premise then claim" + [0, 1, 2] + (localReasoningLocalOrdinals sinceContinuation) + assertEqual "local-only Since requests select no globals" + [0, 0, 0] + (localReasoningGlobalCount + <$> [sinceDischarge, sinceClaim, sinceContinuation]) + assertEqual "biconditional second link keeps local-only policy" + 0 (localReasoningGlobalCount biconditionalSecond) + _ -> + assertFailure + ("unexpected local-reasoning observations: " + <> show observed) + omittedBatch <- sole "omitted Suffices batch" + (take 1 + (reverse + (Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix fresh)))) + omittedFact <- sole "omitted Suffices fact" + (Semantic.declarationDeltaFacts + (Declaration.committedBatchDelta omittedBatch)) + assertEqual "Suffices continuation omission reaches final authority" + (Authority.authoritySafety + (Authority.singletonEscapeKind Authority.Omitted)) + (Authority.factAuthoritySafety + (Semantic.semanticFactAuthority omittedFact)) + + bracket + (snd <$> (Store.openStore storePath + (Identity.theoryId foundation) >>= expectRight)) + Store.closeStore + \store -> do + expectRightIO + (Store.writePendingModulePrefix store + (Module.sealedTypedModulePrefix fresh)) + let validation = + Declaration.WarmValidation + (Declaration.validationLookup + (expectRightIO + . Store.loadProofValidation store) + (expectRightIO + . Store.loadDeclarationValidation store)) + warmRuns <- newIORef (0 :: Int) + warm <- + sole "warm local-reasoning module" + =<< compileParsedWorkspaceWithValidation + foundation + bootstrap + (countingAcceptedResolver executable warmRuns) + validation + workspace + assertEqual "warm local-reasoning validation skips Vampire" + 0 =<< readIORef warmRuns + assertEqual "fresh and warm local-reasoning validations" + (validationRecords fresh) + (validationRecords warm) + + assertRejectedPrefix + "Suffices implication failure" foundation bootstrap workspace + executable 0 0 1 + assertRejectedPrefix + "Suffices reduction failure" foundation bootstrap workspace + executable 1 0 2 + assertRejectedPrefix + "middle calculation link failure" foundation bootstrap workspace + executable 3 1 4 + where + observingResolver executable observations = + Declaration.vampireResolver \prepared -> do + let problem = Provers.preparedTypedProverLogicalProblem prepared + claim = Backend.typedProblemClaim problem + locals = Backend.typedProblemLocalPremises problem + observation = + LocalReasoningObservation + { localReasoningTarget = + Backend.supportedPropositionTerm claim + , localReasoningGlobalCount = Vector.length + (Backend.typedProblemGlobalPremises problem) + , localReasoningLocalOrdinals = + [ Backend.localPremiseOrdinalValue + (Backend.typedLocalPremiseOrdinal premise) + | premise <- Vector.toList locals + ] + , localReasoningLocalTerms = + [ Backend.supportedPropositionTerm + (Backend.typedLocalPremiseProposition premise) + | premise <- Vector.toList locals + ] + , localReasoningAuxiliaries = + Backend.typedProblemAuxiliaryTag + <$> Vector.toList + (Backend.typedProblemAuxiliaries problem) + } + modifyIORef' observations (<> [observation]) + runNoLoggingT + (Provers.runPreparedTypedProver + (Provers.vampire + executable + Provers.defaultTimeLimit + Provers.defaultMemoryLimit) + prepared) + + requestCounts sealed = + [ case Declaration.committedBatchProofValidations batch of + [record] -> + case Authority.validationDirectAuthorization + (Semantic.proofValidationRecordCertificate record) of + Authority.CheckedSourceProof requests -> length requests + Authority.OmittedAuthorization -> 1 + direct -> error + ("unexpected local-reasoning authority: " <> show direct) + records -> error + ("unexpected local-reasoning validation count: " + <> show (length records)) + | batch <- Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix sealed) + ] + + validationRecords = + concatMap Declaration.committedBatchProofValidations + . Declaration.pendingModulePrefixBatches + . Module.sealedTypedModulePrefix + + assertDerivedContinuation + label expectedOrdinals expectedEndpoint continuation = do + assertEqual (label <> " local source ordinals") + expectedOrdinals + (localReasoningLocalOrdinals continuation) + case reverse (localReasoningLocalTerms continuation) of + derived : _ -> + assertEqual (label <> " derived endpoint") + expectedEndpoint derived + [] -> + assertFailure + (label <> ": continuation has no derived endpoint") + + assertPairwiseDistinct label terms = + assertEqual (label <> ": " <> show terms) + (length terms) + (Set.size (Set.fromList terms)) + + assertQuantifiedCalculationGuard proposition = + case dropForalls 2 proposition of + Core.CImp constraint endpoint -> do + assertEqual "quantified guard retains both membership bounds" + 2 (countIntrinsic Core.Member constraint) + assertEqual "quantified guard retains its such-that equality" + 1 (countSetEqualities constraint) + case endpoint of + Core.CEq Core.TySet (Core.CBound left) (Core.CBound right) -> + assertBool "quantified endpoint keeps asymmetric binders" + (left /= right) + _ -> + assertFailure + ("unexpected quantified endpoint: " <> show endpoint) + target -> + assertFailure + ("expected quantified guarded implication, found " + <> show target) + + quantifiedCalculationShape proposition = + case dropForalls 2 proposition of + Core.CImp constraint endpoint -> + Just + ( countIntrinsic Core.Member constraint + , countSetEqualities constraint + , endpoint + ) + _ -> Nothing + + dropForalls + :: Int + -> Core.CanonicalTerm Identity.ObjectId + -> Core.CanonicalTerm Identity.ObjectId + dropForalls 0 term = term + dropForalls remaining (Core.CForall _binder body) = + dropForalls (remaining - 1) body + dropForalls _remaining term = term + + countIntrinsic + :: Core.CoreIntrinsicTag + -> Core.CanonicalTerm Identity.ObjectId + -> Int + countIntrinsic intrinsic = \case + Core.CBound{} -> 0 + Core.CGlobal{} -> 0 + Core.CIntrinsic found -> fromEnum (found == intrinsic) + Core.COpaqueInteger{} -> 0 + Core.CApp function argument -> + countIntrinsic intrinsic function + + countIntrinsic intrinsic argument + Core.CLam _binder body -> countIntrinsic intrinsic body + Core.CFalsum -> 0 + Core.CImp premise conclusion -> + countIntrinsic intrinsic premise + + countIntrinsic intrinsic conclusion + Core.CEq _operand left right -> + countIntrinsic intrinsic left + + countIntrinsic intrinsic right + Core.CForall _binder body -> countIntrinsic intrinsic body + + countSetEqualities + :: Core.CanonicalTerm Identity.ObjectId + -> Int + countSetEqualities = \case + Core.CBound{} -> 0 + Core.CGlobal{} -> 0 + Core.CIntrinsic{} -> 0 + Core.COpaqueInteger{} -> 0 + Core.CApp function argument -> + countSetEqualities function + countSetEqualities argument + Core.CLam _binder body -> countSetEqualities body + Core.CFalsum -> 0 + Core.CImp premise conclusion -> + countSetEqualities premise + countSetEqualities conclusion + Core.CEq operand left right -> + fromEnum (operand == Core.TySet) + + countSetEqualities left + + countSetEqualities right + Core.CForall _binder body -> countSetEqualities body + + equalityOperandType = \case + Core.CEq operandType _left _right -> operandType + term -> error ("expected checked equality, found " <> show term) + + leadingForalls + :: Core.CanonicalTerm Identity.ObjectId + -> Int + leadingForalls = \case + Core.CForall _binder body -> 1 + leadingForalls body + _ -> 0 + + assertRejectedPrefix + label foundation bootstrap workspace executable rejectedIndex + expectedPrefix expectedRuns = do + runs <- newIORef (0 :: Int) + parsed <- sole (label <> " parsed module") + (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) + let resolver = + Declaration.vampireResolver \prepared -> do + index <- atomicModifyIORef' runs \current -> + (current + 1, current) + if index == rejectedIndex + then pure + (Right + (Provers.CounterSatisfiable + "focused deterministic rejection")) + else + runNoLoggingT + (Provers.runPreparedTypedProver + (Provers.vampire + executable + Provers.defaultTimeLimit + Provers.defaultMemoryLimit) + prepared) + input <- expectRight + (Module.typedModuleInput + foundation + (Module.bootstrapPreludeReadiness bootstrap) + resolver + Declaration.FreshValidation + parsed + []) + Module.runTypedModule input >>= \case + Module.TypedModuleFailed _failure prefix -> + assertEqual + (label <> " publishes only the prior prefix") + expectedPrefix + (length + (Declaration.pendingModulePrefixBatches prefix)) + Module.TypedModuleSucceeded{} -> + assertFailure (label <> " unexpectedly succeeded") + Module.TypedModuleOpenFailed failure -> + assertFailure + (label <> " did not open: " <> show failure) + assertEqual (label <> " selects the first rejected request") + expectedRuns =<< readIORef runs + +data LocalReasoningObservation = LocalReasoningObservation + { localReasoningTarget :: !(Core.CanonicalTerm Identity.ObjectId) + , localReasoningGlobalCount :: !Int + , localReasoningLocalOrdinals :: ![Natural] + , localReasoningLocalTerms :: + ![Core.CanonicalTerm Identity.ObjectId] + , localReasoningAuxiliaries :: ![Foundation.FoundationAxiomTag] + } + deriving (Show) + +selectsCalculationLinkFailureBySourceOrder :: Assertion +selectsCalculationLinkFailureBySourceOrder = do + foundation <- expectRight Foundation.checkedFoundation + Temp.withSystemTempDirectory "felix-calculation-link-order" \root -> do + let executable = root Posix.</> "vampire" + storePath = root Posix.</> "store.sqlite" + source = "test/phase7/calculation-link-order.tex" + laterCompleted = root Posix.</> "later-completed" + firstRun = root Posix.</> "first-run" + secondRun = root Posix.</> "second-run" + prover = + Provers.vampire + executable + Provers.defaultTimeLimit + Provers.defaultMemoryLimit + writeAcceptedFixtureVampire executable + (_startup, store) <- + Store.openStore storePath (Identity.theoryId foundation) + >>= expectRight + bracket (pure store) Store.closeStore \openStore -> do + let ignored = + Api.verificationRequestObserver + (\_position _request -> pure ()) + void + (runNoLoggingT + (Api.verifyMeasuredWithObserverAndStoreMode + openStore + Api.WarmStoreValidation + ignored + prover + "test/phase3/typed-unsupported.tex") + >>= expectRight) + writeFile executable + (unlines + [ "#!/bin/sh" + , "cat >/dev/null" + , "if mkdir \"" <> firstRun <> "\" 2>/dev/null; then" + , " printf '%s\\n' '% SZS status Theorem for calculation-link-order'" + , "elif mkdir \"" <> secondRun <> "\" 2>/dev/null; then" + , " : > \"" <> laterCompleted <> "\"" + , " printf '%s\\n' '% SZS status Theorem for calculation-link-order'" + , "else" + , " printf '%s\\n' '% SZS status CounterSatisfiable for calculation-link-order'" + , "fi" + ]) + permissions <- getPermissions executable + setPermissions executable (setOwnerExecutable True permissions) + jobs <- + Provers.selectEffectiveJobs + (Provers.effectiveJobs 2) + (fail "explicit jobs unexpectedly detected processors") + positions <- newIORef [] + middleStarted <- newEmptyTMVarIO + laterStarted <- newEmptyTMVarIO + releaseMiddle <- newEmptyTMVarIO + let observer = + Api.verificationRequestObserver \position _request -> do + let ordinal = + Provers.workPositionLocalRequestOrdinal position + modifyIORef' positions (position :) + case ordinal of + 1 -> pure () + 2 -> do + atomically (putTMVar middleStarted ()) + atomically (takeTMVar releaseMiddle) + 3 -> atomically (putTMVar laterStarted ()) + _ -> + assertFailure + ("unexpected calculation request ordinal: " + <> show ordinal) + withAsync + (runNoLoggingT + (Api.verifyMeasuredWithObserverAndStoreModeAndJobs + openStore + Api.WarmStoreValidation + jobs + observer + prover + source) + >>= expectRight) + \verification -> do + void + (awaitTmvar "middle calculation link" middleStarted) + void + (awaitTmvar "later calculation continuation" laterStarted) + waitForFileSignal + "later calculation continuation" laterCompleted + atomically (putTMVar releaseMiddle ()) + (result, measurements) <- wait verification + case result of + Api.VerificationFailure report failed -> do + assertEqual "middle link failure location" + (source, 10) + ( locFile + (Api.failedVerificationLocation failed) + , locLine + (Api.failedVerificationLocation failed) + ) + assertEqual "failed calculation admits no source fact" + [] (Api.verificationDirectEscapes report) + other -> + assertFailure + ("calculation link order did not reject: " + <> show other) + observedPositions <- + fmap + (\position -> + ( Provers.workPositionModuleOrdinal position + , Provers.workPositionLocalRequestOrdinal + position + )) + <$> readIORef positions + assertEqual "all calculation requests executed" + [(1, 1), (1, 2), (1, 3)] + (sort observedPositions) + assertEqual "later calculation request overlapped" + 2 + (Api.verificationMaximumLiveVampireProcesses + measurements) + + writeAcceptedFixtureVampire executable + retryPositions <- newIORef [] + let retryObserver = + Api.verificationRequestObserver \position _request -> + modifyIORef' retryPositions (position :) + (retry, retryMeasurements) <- + runNoLoggingT + (Api.verifyMeasuredWithObserverAndStoreModeAndJobs + openStore + Api.WarmStoreValidation + jobs + retryObserver + prover + source) + >>= expectRight + case retry of + Api.VerificationCompleted{} -> pure () + other -> + assertFailure + ("calculation rollback retry failed: " <> show other) + assertEqual "failed calculation retained no validation or root" + (1, 1, 3) + ( Api.verificationModuleRootHitCount retryMeasurements + , Api.verificationModuleRootMissCount retryMeasurements + , Api.verificationVampireRunCount retryMeasurements + ) + retryObserved <- readIORef retryPositions + assertEqual "retry executes the complete calculation proof" + 3 (length retryObserved) + where + awaitTmvar label variable = do + result <- Timeout.timeout 10000000 + (atomically (takeTMVar variable)) + maybe + (assertFailure (label <> " was not observed") + >> fail "unreachable") + pure + result + +assertProofParityFailure + :: Foundation.CheckedFoundation + -> Module.BootstrapPreludeFixture + -> SourceMounts + -> FilePath + -> (ExactProof.ExactProofError -> Bool) + -> Assertion +assertProofParityFailure foundation bootstrap mounts relative matches = do + workspace <- parseExactWorkspace bootstrap mounts relative + parsed <- sole "invalid proof-parity module" + (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) + input <- expectRight + (Module.typedModuleInput + foundation + (Module.bootstrapPreludeReadiness bootstrap) + unusedResolver + Declaration.FreshValidation + parsed + []) + Module.runTypedModule input >>= \case + Module.TypedModuleFailed + (Module.TypedActionFailed + (Module.TypedExactProofFailed failure)) + prefix -> do + assertBool ("unexpected proof failure: " <> show failure) + (matches failure) + assertBool "failing proof publishes no declaration" + (null (Declaration.pendingModulePrefixBatches prefix)) + Module.TypedModuleSucceeded{} -> + assertFailure "invalid proof-parity module succeeded" + Module.TypedModuleOpenFailed failure -> + assertFailure + ("invalid proof-parity module did not open: " <> show failure) + Module.TypedModuleFailed failure _prefix -> + assertFailure + ("unexpected proof-parity module failure: " <> show failure) + compilesExactSeparationComprehensions :: Assertion compilesExactSeparationComprehensions = Temp.withSystemTempDirectory "felix-exact-separation" \root -> do @@ -2112,11 +3536,28 @@ compilesExactSeparationComprehensions = let resolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared + request = + Provers.preparedTypedProverRequest prepared + globals = + Backend.typedProblemGlobalPremises problem modifyIORef' observations (<> [ ( Backend.typedProblemRoute problem + , Backend.typedBackendFactReference <$> globals + , all + (\fact -> + case Backend.typedBackendFactCapability fact of + Backend.FofProjectable{} -> True + Backend.RequiresTh0{} -> False) + globals + , Backend.localPremiseOrdinalValue + . Backend.typedLocalPremiseOrdinal + <$> Vector.toList + (Backend.typedProblemLocalPremises problem) , Backend.typedProblemAuxiliaryTag <$> Vector.toList (Backend.typedProblemAuxiliaries problem) + , Provers.preparedVerificationRequestId request + , Provers.preparedVerificationByteCount request ) ]) runNoLoggingT @@ -2130,12 +3571,43 @@ compilesExactSeparationComprehensions = foundation bootstrap resolver workspace sealed <- sole "exact separation module" modules assertExactSeparationModule "fresh" sealed - assertEqual - "separation proof uses its checked characteristic on TH0" - [( Backend.RouteTh0 - , [Foundation.SeparationCharacteristic] - )] - =<< readIORef observations + definition <- batchByAlias + (Module.sealedTypedModulePrefix sealed) + "phase5_separation_definition" + let definitionFacts = + Semantic.declarationDeltaFacts + (Declaration.committedBatchDelta definition) + extensional <- sole "searchable separation view" + [ Semantic.semanticFactFingerprint occurrence + | occurrence <- definitionFacts + , Semantic.semanticFactSearchEligibility occurrence + == Semantic.SearchEligible + ] + equation <- sole "explicit separation equation" + [ Semantic.semanticFactFingerprint occurrence + | occurrence <- definitionFacts + , Semantic.semanticFactSearchEligibility occurrence + == Semantic.SearchIneligible + ] + readIORef observations >>= \case + [ ( Backend.RouteFof + , selectedGlobals + , True + , [0] + , [] + , _requestId + , requestBytes + ) ] -> do + assertBool "searchable separation view is selected" + (extensional `elem` selectedGlobals) + assertBool "exact separation equation is not selected" + (equation `notElem` selectedGlobals) + assertBool "separation exact request has bytes" + (requestBytes > 0) + observed -> + assertFailure + ("unexpected implicit separation problem: " + <> show observed) createDirectoryIfMissing True (Posix.takeDirectory failedSource) original <- ByteString.readFile relative @@ -2222,7 +3694,9 @@ compilesAndReusesProofLocalSetDefinitions = premises modifyIORef' observations (<> [ ( Backend.typedProblemRoute problem - , Vector.length premises + , Backend.localPremiseOrdinalValue + . Backend.typedLocalPremiseOrdinal + <$> Vector.toList premises , fmap localDefinitionShape definition ) ]) @@ -2242,9 +3716,9 @@ compilesAndReusesProofLocalSetDefinitions = workspace assertEqual "fresh local-definition discharge count" 2 =<< readIORef freshRuns - assertEqual "local definitions remain on the FOF route" - [ (Backend.RouteFof, 2, Just expectedLocalDefinitionShape) - , (Backend.RouteFof, 2, Just expectedLocalDefinitionShape) + assertEqual "implicit and local-only definition views" + [ (Backend.RouteFof, [0, 2], Just expectedLocalDefinitionShape) + , (Backend.RouteTh0, [0, 1, 3], Just expectedLocalDefinitionShape) ] =<< readIORef observations fresh <- sole "fresh local-definition module" freshModules @@ -2581,15 +4055,18 @@ compilesAndReusesProofLocalFunctionGraphs = confinesTerminalExactContradiction :: Assertion confinesTerminalExactContradiction = Temp.withSystemTempDirectory "felix-exact-contradiction" \directory -> do - let executable = directory Posix.</> "vampire" - writeFile executable + let acceptedExecutable = directory Posix.</> "accepted-vampire" + contradictoryExecutable = directory Posix.</> "contradictory-vampire" + storePath = directory Posix.</> "store.sqlite" + writeAcceptedFixtureVampire acceptedExecutable + writeFile contradictoryExecutable (unlines [ "#!/bin/sh" , "cat >/dev/null" , "printf '%s\\n' '% SZS status ContradictoryAxioms for exact-contradiction'" ]) - permissions <- getPermissions executable - setPermissions executable + permissions <- getPermissions contradictoryExecutable + setPermissions contradictoryExecutable (setOwnerExecutable True permissions) foundation <- expectRight Foundation.checkedFoundation bootstrap <- @@ -2598,48 +4075,295 @@ confinesTerminalExactContradiction = foundation unusedResolver mounts <- exactFixtureMounts =<< getCurrentDirectory workspace <- parseExactWorkspace bootstrap mounts - "test/phase5/exact-contradiction.tex" - runs <- newIORef (0 :: Int) - modules <- - compileParsedWorkspaceWithResolver - foundation - bootstrap - (countingAcceptedResolver executable runs) - workspace - accepted <- sole "terminal contradiction module" modules - assertEqual "one indirect contradiction obligation" - 1 =<< readIORef runs - assertCleanFactAlias accepted "phase5_contradiction" - - invalidWorkspace <- parseExactWorkspace bootstrap mounts - "test/phase5/exact-contradiction-goal.tex" - invalidParsed <- - sole "invalid contradiction module" - (toList - (Parse.parsedWorkspaceImportedBeforeImporter - invalidWorkspace)) - invalidInput <- expectRight + "test/phase5/exact-cases-contradiction.tex" + assertEmptyCaseAstRejected foundation bootstrap workspace + observations <- newIORef [] + fresh <- + sole "cases and contradiction module" + =<< compileParsedWorkspaceWithValidation + foundation + bootstrap + (observingResolver + acceptedExecutable + contradictoryExecutable + observations) + Declaration.FreshValidation + workspace + observed <- readIORef observations + assertEqual "cases and contradiction request count" + 8 (length observed) + case observed of + branchOne : branchTwo : branchThree : exhaustive + : byContradiction : arbitraryContradiction + : omittedLaterBranch : omittedExhaustive : [] -> do + assertEqual "case branches have isolated local ordinals" + [[0], [1], [2]] + (localReasoningLocalOrdinals + <$> [branchOne, branchTwo, branchThree]) + assertEqual "exhaustiveness sees pre-case locals only" + [] (localReasoningLocalOrdinals exhaustive) + case + ( localReasoningLocalTerms branchOne + , localReasoningLocalTerms branchTwo + , localReasoningLocalTerms branchThree + ) of + ([caseOne], [caseTwo], [caseThree]) -> + assertEqual + "case exhaustiveness is left-associated in source order" + (orP (orP caseOne caseTwo) caseThree) + (localReasoningTarget exhaustive) + branchTerms -> + assertFailure + ("unexpected branch-local premises: " + <> show branchTerms) + assertEqual "proof by contradiction targets falsum" + Core.CFalsum + (localReasoningTarget byContradiction) + assertBool + "double-negation elimination is not an ATP auxiliary" + (Foundation.DoubleNegationElim + `notElem` localReasoningAuxiliaries byContradiction) + case localReasoningLocalTerms byContradiction of + [Core.CImp negatedGoal Core.CFalsum] -> + assertEqual + "proof by contradiction assumes the exact negated goal" + (localReasoningTarget branchOne) + negatedGoal + locals -> + assertFailure + ("unexpected contradiction locals: " + <> show locals) + assertEqual "arbitrary terminal contradiction targets falsum" + Core.CFalsum + (localReasoningTarget arbitraryContradiction) + assertEqual "omitted case does not leak into its sibling" + [1] + (localReasoningLocalOrdinals omittedLaterBranch) + assertEqual "omitted exhaustiveness sees no branch local" + [] (localReasoningLocalOrdinals omittedExhaustive) + _ -> + assertFailure + ("unexpected cases/contradiction observations: " + <> show observed) + case Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix fresh) of + [caseBatch, byContradictionBatch, terminalBatch, omittedBatch] -> do + traverse_ + (assertBatchSafety Authority.cleanAuthoritySafety) + [caseBatch, byContradictionBatch, terminalBatch] + assertBatchSafety + (Authority.authoritySafety + (Authority.singletonEscapeKind Authority.Omitted)) + omittedBatch + batches -> + assertFailure + ("unexpected cases/contradiction declaration count: " + <> show (length batches)) + + bracket + (snd <$> (Store.openStore storePath + (Identity.theoryId foundation) >>= expectRight)) + Store.closeStore + \store -> do + expectRightIO + (Store.writePendingModulePrefix store + (Module.sealedTypedModulePrefix fresh)) + let validation = + Declaration.WarmValidation + (Declaration.validationLookup + (expectRightIO + . Store.loadProofValidation store) + (expectRightIO + . Store.loadDeclarationValidation store)) + warmRuns <- newIORef (0 :: Int) + warm <- + sole "warm cases and contradiction module" + =<< compileParsedWorkspaceWithValidation + foundation + bootstrap + (countingAcceptedResolver + acceptedExecutable warmRuns) + validation + workspace + assertEqual "warm structural proofs skip Vampire" + 0 =<< readIORef warmRuns + assertEqual "fresh and warm structural proof validations" + (proofValidations fresh) + (proofValidations warm) + + failureWorkspace <- parseExactWorkspace bootstrap mounts + "test/phase5/exact-case-failure.tex" + assertCaseFailure + "middle case branch" + foundation bootstrap failureWorkspace acceptedExecutable 1 2 + assertCaseFailure + "case exhaustiveness" + foundation bootstrap failureWorkspace acceptedExecutable 3 4 + + directWorkspace <- parseExactWorkspace bootstrap mounts + "test/phase5/exact-direct-contradictory.tex" + directParsed <- sole "direct contradictory parsed module" + (toList + (Parse.parsedWorkspaceImportedBeforeImporter directWorkspace)) + directInput <- expectRight (Module.typedModuleInput foundation (Module.bootstrapPreludeReadiness bootstrap) - unusedResolver + (Declaration.vampireResolver + (runWith contradictoryExecutable)) Declaration.FreshValidation - invalidParsed + directParsed []) - Module.runTypedModule invalidInput >>= \case + Module.runTypedModule directInput >>= \case Module.TypedModuleFailed - (Module.TypedActionFailed - (Module.TypedExactProofFailed - (ExactProof.ExactProofContradictionGoalMismatch - location))) - prefix -> do - assertEqual "invalid contradiction line" - 6 (locLine location) - assertBool "invalid contradiction publishes no declaration" - (null - (Declaration.pendingModulePrefixBatches prefix)) + (Module.TypedDeclarationFailed + (Declaration.ProofObligationFailedAt + _location + Declaration.VampireObligationRejected{})) + prefix -> + assertBool + "direct contradictory input publishes no theorem" + (null (Declaration.pendingModulePrefixBatches prefix)) + _result -> + assertFailure "direct contradictory input was accepted" + where + observingResolver acceptedExecutable contradictoryExecutable observations = + Declaration.vampireResolver \prepared -> do + let problem = Provers.preparedTypedProverLogicalProblem prepared + claim = Backend.typedProblemClaim problem + locals = Backend.typedProblemLocalPremises problem + target = Backend.supportedPropositionTerm claim + modifyIORef' observations + (<> [ LocalReasoningObservation + { localReasoningTarget = target + , localReasoningGlobalCount = + Vector.length + (Backend.typedProblemGlobalPremises problem) + , localReasoningLocalOrdinals = + [ Backend.localPremiseOrdinalValue + (Backend.typedLocalPremiseOrdinal premise) + | premise <- Vector.toList locals + ] + , localReasoningLocalTerms = + Backend.supportedPropositionTerm + . Backend.typedLocalPremiseProposition + <$> Vector.toList locals + , localReasoningAuxiliaries = + Backend.typedProblemAuxiliaryTag + <$> Vector.toList + (Backend.typedProblemAuxiliaries problem) + } + ]) + runWith + (if target == Core.CFalsum + then contradictoryExecutable + else acceptedExecutable) + prepared + + runWith executable prepared = + runNoLoggingT + (Provers.runPreparedTypedProver + (Provers.vampire + executable + Provers.defaultTimeLimit + Provers.defaultMemoryLimit) + prepared) + + assertEmptyCaseAstRejected foundation bootstrap workspace = do + parsed <- sole "cases parsed module" + (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) + let blocks = + Parse.identifiedParsedModuleBlocks + (Parse.parsedModuleIdentified parsed) + claim <- sole "cases source claim" + [ candidate + | candidate@Raw.BlockClaim{} <- take 1 blocks + ] + location <- + case + [ found + | Raw.BlockProof _ (Raw.ByCase found _cases) _ <- blocks + ] of + found : _ -> pure found + [] -> + assertFailure "cases source proof is absent" + >> fail "unreachable" + let preludeModule = Module.bootstrapPreludeModule bootstrap + outcome <- Declaration.runModuleDriver + foundation + (moduleName (Parse.parsedModuleAddress parsed)) + [ Semantic.semanticInterfaceAssertedId + (Module.sealedTypedModuleSemantic preludeModule) + ] + unusedResolver + Declaration.FreshValidation do + Declaration.importSealedModuleDriver + (Module.sealedTypedModuleEvidence preludeModule) + Declaration.runProspectiveLoweringDriver + (ExactProof.prepareExactProof + claim + (Just (Raw.ByCase location []))) + case outcome of + Right (Declaration.DriverSucceeded + (Left (ExactProof.ExactProofEmptyCaseSplit found)) + _semantic prefix _closure) -> do + assertEqual "empty case AST failure location" + location found + assertBool "empty case AST publishes no declaration" + (null (Declaration.pendingModulePrefixBatches prefix)) + _ -> + assertFailure "empty programmatic case split was not rejected" + + assertBatchSafety expected batch = do + fact <- sole "structural proof fact" + (Semantic.declarationDeltaFacts + (Declaration.committedBatchDelta batch)) + assertEqual "structural proof authority safety" + expected + (Authority.factAuthoritySafety + (Semantic.semanticFactAuthority fact)) + + proofValidations = + concatMap Declaration.committedBatchProofValidations + . Declaration.pendingModulePrefixBatches + . Module.sealedTypedModulePrefix + + assertCaseFailure + label foundation bootstrap workspace executable rejectedIndex + expectedRuns = do + runs <- newIORef (0 :: Int) + parsed <- sole (label <> " parsed module") + (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) + let resolver = + Declaration.vampireResolver \prepared -> do + index <- atomicModifyIORef' runs \current -> + (current + 1, current) + if index == rejectedIndex + then pure + (Right + (Provers.CounterSatisfiable + "focused case rejection")) + else runWith executable prepared + input <- expectRight + (Module.typedModuleInput + foundation + (Module.bootstrapPreludeReadiness bootstrap) + resolver + Declaration.FreshValidation + parsed + []) + Module.runTypedModule input >>= \case + Module.TypedModuleFailed _failure prefix -> + assertBool + (label <> " publishes no declaration") + (null (Declaration.pendingModulePrefixBatches prefix)) _result -> - assertFailure "unexpected invalid contradiction result" + assertFailure (label <> " unexpectedly succeeded") + assertEqual + (label <> " selects failures in source order") + expectedRuns =<< readIORef runs + + orP left right = Core.CImp (Core.CImp left Core.CFalsum) right compilesExactReplacementComprehensions :: Assertion compilesExactReplacementComprehensions = @@ -2712,21 +4436,57 @@ assertExactReplacementModule sealed = assertEqual "replacement definition body" expectedBody body + assertEqual "replacement definition foundation helpers" + (Set.fromList + [ Foundation.FamilyUnionCharacteristic + , Foundation.SeparationCharacteristic + , Foundation.ReplacementCharacteristic + ]) + (Foundation.foundationAxiomDependencies body) content -> assertFailure ("unexpected replacement object " <> show content) + let definitionDelta = + Declaration.committedBatchDelta definitionBatch + definitionFacts = + Semantic.declarationDeltaFacts definitionDelta assertEqual "replacement definition fact count" + 2 (length definitionFacts) + assertEqual "replacement equation/search view eligibility" + [Semantic.SearchIneligible, Semantic.SearchEligible] + (Semantic.semanticFactSearchEligibility <$> definitionFacts) + assertEqual "replacement generated view is unaliased" 1 - (length - (Semantic.declarationDeltaFacts - (Declaration.committedBatchDelta definitionBatch))) + (length (Semantic.declarationDeltaAliases definitionDelta)) assertEqual "replacement definition proposition count" - 1 + 2 (length (Declaration.committedBatchPropositions definitionBatch)) assertEqual "replacement definition proof validations" [] (Declaration.committedBatchProofValidations definitionBatch) + definitionValidation <- + maybe + (assertFailure "replacement validation is absent" + >> fail "unreachable") + pure + (Declaration.committedBatchDeclarationValidation + definitionBatch) + case Authority.validationDirectAuthorization + <$> Semantic.declarationValidationRecordCertificates + definitionValidation of + [ Authority.CheckedKernelConstruction + (Authority.CheckedDefinitionEquation target) + , Authority.CheckedKernelConstruction + (Authority.CheckedSetConstructionExtensionality + generatedTarget _descriptor) + ] -> + assertEqual "replacement construction authority object" + target generatedTarget + authorizations -> + assertFailure + ("unexpected replacement definition authorities " + <> show authorizations) assertEqual "replacement theorem adds no object" [] @@ -2776,6 +4536,233 @@ assertExactReplacementModule sealed = (Core.CLam Core.TySet (Core.CBound 0)) +compilesAndReusesRelationalReplacement :: Assertion +compilesAndReusesRelationalReplacement = + Temp.withSystemTempDirectory "felix-exact-relational-replacement" \root -> do + let relative = "test/phase5/exact-relational-replacement.tex" + failureRelative = + "test/phase5/exact-relational-replacement-failure.tex" + localFailureRelative = + "test/phase5/exact-relational-replacement-local-failure.tex" + executable = root Posix.</> "vampire" + storePath = root Posix.</> "store.sqlite" + writeAcceptedFixtureVampire executable + foundation <- expectRight Foundation.checkedFoundation + bootstrap <- + expectRight + =<< Module.buildBootstrapPreludeFixture + foundation unusedResolver + mounts <- exactFixtureMounts =<< getCurrentDirectory + workspace <- parseExactWorkspace bootstrap mounts relative + observed <- newIORef [] + runs <- newIORef (0 :: Int) + let resolver = Declaration.vampireResolver \prepared -> do + modifyIORef' runs (+ 1) + let problem = + Provers.preparedTypedProverLogicalProblem prepared + modifyIORef' observed + (<> [ ( Backend.typedProblemRoute problem + , Backend.localPremiseOrdinalValue + . Backend.typedLocalPremiseOrdinal + <$> Vector.toList + (Backend.typedProblemLocalPremises problem) + , Backend.typedProblemAuxiliaryTag + <$> Vector.toList + (Backend.typedProblemAuxiliaries problem) + ) + ]) + runNoLoggingT + (Provers.runPreparedTypedProver + (Provers.vampire + executable + Provers.defaultTimeLimit + Provers.defaultMemoryLimit) + prepared) + freshModules <- + compileParsedWorkspaceWithValidation + foundation bootstrap resolver + Declaration.FreshValidation workspace + fresh <- sole "fresh relational replacement module" freshModules + assertRelationalReplacementModule fresh + problems <- readIORef observed + assertEqual "relational replacement request count" + 3 (length problems) + firstProblem <- sole "module functionality request" (take 1 problems) + assertEqual "module functionality uses FOF" + Backend.RouteFof + (case firstProblem of (route, _, _) -> route) + assertEqual "module functionality has no local premises" + [] + (case firstProblem of (_, ordinals, _) -> ordinals) + assertEqual + "relational equivalence creates no ATP obligation or auxiliary" + [ (Backend.RouteFof, [], []) + , (Backend.RouteFof, [], []) + , (Backend.RouteFof, [0], []) + ] + problems + + bracket + (snd <$> (Store.openStore storePath + (Identity.theoryId foundation) >>= expectRight)) + Store.closeStore + \store -> do + expectRightIO + (Store.writePendingModulePrefix store + (Module.sealedTypedModulePrefix fresh)) + let validation = + Declaration.WarmValidation + (Declaration.validationLookup + (expectRightIO + . Store.loadProofValidation store) + (expectRightIO + . Store.loadDeclarationValidation store)) + warmRuns <- newIORef (0 :: Int) + warmModules <- + compileParsedWorkspaceWithValidation + foundation bootstrap + (countingAcceptedResolver executable warmRuns) + validation workspace + assertEqual "warm relational replacement skips Vampire" + 0 =<< readIORef warmRuns + warm <- sole "warm relational replacement module" warmModules + assertEqual "warm relational replacement interface" + (Module.sealedTypedModuleSemantic fresh) + (Module.sealedTypedModuleSemantic warm) + assertEqual "warm relational replacement prefix" + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix fresh)) + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix warm)) + + let rejectingResolver = + Declaration.vampireResolver \_prepared -> + pure + (Right + (Provers.CounterSatisfiable + "relational functionality rejected")) + runRejected relativePath = do + failedWorkspace <- + parseExactWorkspace bootstrap mounts relativePath + input <- expectRight + (Module.typedModuleInput + foundation + (Module.bootstrapPreludeReadiness bootstrap) + rejectingResolver + Declaration.FreshValidation + (Parse.parsedWorkspaceRootModule failedWorkspace) + []) + Module.runTypedModule input + runRejected failureRelative >>= \case + Module.TypedModuleFailed _failure prefix -> do + batches <- pure + (Declaration.pendingModulePrefixBatches prefix) + assertEqual "failed relational definition keeps its prefix" + 1 (length batches) + prefixBatch <- sole "relational prefix declaration" batches + assertEqual "failed relational definition publishes no object" + 1 (length + (Declaration.committedBatchObjects prefixBatch)) + _result -> + assertFailure + "nonfunctional relational definition did not fail" + runRejected localFailureRelative >>= \case + Module.TypedModuleFailed _failure prefix -> + assertBool + "failed local functionality publishes no theorem" + (null + (Declaration.pendingModulePrefixBatches prefix)) + _result -> + assertFailure + "nonfunctional local definition did not fail" + +assertRelationalReplacementModule + :: Module.SealedTypedModule + -> Assertion +assertRelationalReplacementModule sealed = + case Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix sealed) of + [_axiomBatch, definitionBatch, proofBatch] -> do + _object <- sole "relational replacement object" + (Declaration.committedBatchObjects definitionBatch) + let definitionFacts = + Semantic.declarationDeltaFacts + (Declaration.committedBatchDelta definitionBatch) + assertEqual "relational replacement fact eligibility" + [ Semantic.SearchIneligible + , Semantic.SearchIneligible + , Semantic.SearchEligible + ] + (Semantic.semanticFactSearchEligibility <$> definitionFacts) + let sourceSafety = + Authority.authoritySafety + (Authority.singletonEscapeKind Authority.SourceAxiom) + assertEqual "relational extensionality inherits functionality safety" + [ Authority.cleanAuthoritySafety + , sourceSafety + , sourceSafety + ] + ( Authority.factAuthoritySafety + . Semantic.semanticFactAuthority + <$> definitionFacts + ) + assertEqual "relational replacement has only its equation alias" + 1 + (length + (Semantic.declarationDeltaAliases + (Declaration.committedBatchDelta definitionBatch))) + validation <- + maybe + (assertFailure "relational replacement validation absent" + >> fail "unreachable") + pure + (Declaration.committedBatchDeclarationValidation + definitionBatch) + case Authority.validationDirectAuthorization + <$> Semantic.declarationValidationRecordCertificates + validation of + [ Authority.CheckedKernelConstruction + (Authority.CheckedDefinitionEquation equationObject) + , Authority.CheckedSourceProof [_functionalityRequest] + , Authority.CheckedKernelConstruction + (Authority.CheckedSetConstructionExtensionality + extensionalObject _descriptor) + ] -> + assertEqual "relational facts target one object" + equationObject extensionalObject + authorizations -> + assertFailure + ("unexpected relational authorities " + <> show authorizations) + assertEqual "module construction generates no proof row" + [] + (Declaration.committedBatchProofValidations definitionBatch) + + proofValidation <- sole "proof-local relational validation" + (Declaration.committedBatchProofValidations proofBatch) + case Authority.validationDirectAuthorization + (Semantic.proofValidationRecordCertificate + proofValidation) of + Authority.CheckedSourceProof requests -> + assertEqual + "local functionality precedes its continuation" + 2 (length requests) + authorization -> + assertFailure + ("unexpected proof-local relational authority " + <> show authorization) + proofFact <- sole "proof-local relational theorem" + (Semantic.declarationDeltaFacts + (Declaration.committedBatchDelta proofBatch)) + assertEqual "local extensional premise retains discharge safety" + sourceSafety + (Authority.factAuthoritySafety + (Semantic.semanticFactAuthority proofFact)) + batches -> + assertFailure + ("expected relational axiom, definition, and proof, found " + <> show (length batches)) + compilesAndReusesExactFiniteSets :: Assertion compilesAndReusesExactFiniteSets = Temp.withSystemTempDirectory "felix-exact-finite-set" \root -> do @@ -2875,6 +4862,7 @@ compilesAndReusesExactFiniteSets = preparesExactDirectInductives :: Assertion preparesExactDirectInductives = do + foundation <- expectRight Foundation.checkedFoundation prepared <- expectRight =<< prepareExactInductiveFixture @@ -2918,9 +4906,52 @@ preparesExactDirectInductives = do in Core.frozenCoreType target == Core.TyProp && Set.null (Core.frozenCoreGlobals target)) facts) + + let singleton = + Internal.finiteSet + Nowhere + (Internal.EmptySet Nowhere :| []) + noGlobalType :: Void -> Core.CoreType + noGlobalType = absurd + noGlobal + :: Internal.Symbol + -> Maybe (TypedInductive.SourceGlobal Void) + noGlobal = const Nothing + finite <- + expectRight + (TypedInductive.prepareTypedInductive + noGlobalType + foundation + noGlobal + (Internal.Marker "finite_internal") + (TypedInductive.DirectInductive + [] + singleton + (TypedInductive.DirectInductiveClause + [] + [] + (Internal.EmptySet Nowhere) + :| []))) + finiteGuard <- + sole + "finite-set inductive guard" + (Vector.toList + (TypedInductive.typedInductiveGuardTargets finite)) + assertEqual + "typed inductive path uses intrinsic finite-set adjunction" + (member + (Core.CIntrinsic Core.Empty) + (Core.canonicalSetInsert + (Core.CIntrinsic Core.Empty) + (Core.CIntrinsic Core.Empty))) + (Core.frozenCoreTerm finiteGuard) where apply1 intrinsic argument = Core.CApp (Core.CIntrinsic intrinsic) argument + member element set = + Core.CApp + (Core.CApp (Core.CIntrinsic Core.Member) element) + set expectedCarrier = Core.CLam Core.TySet (Core.CApp @@ -3025,8 +5056,7 @@ preparesExactDatatypes = do (Core.CImp (member (Core.CBound 0) - (apply1 Core.FamilyUnion - (Core.CIntrinsic Core.Empty))) + singletonEmpty) (member (Core.CApp (Core.CGlobal atomId) @@ -3053,8 +5083,7 @@ preparesExactDatatypes = do (Core.CImp (member (Core.CBound 0) - (apply1 Core.FamilyUnion - (Core.CIntrinsic Core.Empty))) + singletonEmpty) (member (Core.CApp (Core.CGlobal atomId) @@ -3095,8 +5124,10 @@ preparesExactDatatypes = do (ExactDatatype.preparedExactDatatypeFactReference <$> facts)) (ExactDatatype.preparedExactDatatypeDescriptor prepared) where - apply1 intrinsic argument = - Core.CApp (Core.CIntrinsic intrinsic) argument + singletonEmpty = + Core.canonicalSetInsert + (Core.CIntrinsic Core.Empty) + (Core.CIntrinsic Core.Empty) member element set = Core.CApp @@ -3228,21 +5259,708 @@ compilesAndReusesExactDatatypes = _result -> assertFailure "unexpected nested datatype result" -rejectsNestedExactInductiveRecursion :: Assertion -rejectsNestedExactInductiveRecursion = do - result <- - prepareExactInductiveFixture - "test/phase5/exact-inductive-nested.tex" - case result of - Left (ExactInductive.ExactInductiveNestedRecursion location) -> - assertEqual "nested recursive occurrence line" - 6 - (locLine location) - Left failure -> - assertFailure - ("unexpected exact inductive failure: " <> show failure) - Right{} -> - assertFailure "nested inductive recursion was accepted" +preparesNestedExactInductiveRecursion :: Assertion +preparesNestedExactInductiveRecursion = + withAcceptedFixtureVampire "felix-nested-inductive" \vampire -> do + root <- getCurrentDirectory + foundation <- expectRight Foundation.checkedFoundation + bootstrap <- + expectRight + =<< Module.buildBootstrapPreludeFixture + foundation + unusedResolver + mounts <- exactFixtureMounts root + workspace <- + parseExactWorkspace bootstrap mounts + "test/phase5/exact-inductive-nested.tex" + parsed <- sole "nested exact inductive parsed module" + (toList + (Parse.parsedWorkspaceImportedBeforeImporter workspace)) + observed <- newIORef [] + let resolver = + Declaration.vampireResolver \prepared -> do + let problem = + Provers.preparedTypedProverLogicalProblem prepared + modifyIORef' observed + (<> [ ( Backend.typedProblemRoute problem + , Backend.supportedPropositionTerm + (Backend.typedProblemClaim problem) + ) + ]) + runNoLoggingT + (Provers.runPreparedTypedProver vampire prepared) + modules <- + compileParsedWorkspaceWithValidation + foundation bootstrap resolver + Declaration.FreshValidation workspace + sealed <- sole "nested exact inductive module" modules + observations <- readIORef observed + assertEqual "guard proof plus nested monotonicity request count" + 2 (length observations) + (route, target) <- + sole "nested monotonicity request" + [ observation + | observation@(_route, candidate) <- observations + , candidate == expectedPowerMonotonicity + ] + assertEqual "nested monotonicity target" + expectedPowerMonotonicity + target + assertEqual "nested monotonicity request is first-order" + Backend.RouteFof + route + case Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix sealed) of + [_guardBatch, _unsafeBatch, inductiveBatch] -> do + let facts = + Semantic.declarationDeltaFacts + (Declaration.committedBatchDelta inductiveBatch) + aliases = + Semantic.declarationDeltaAliases + (Declaration.committedBatchDelta inductiveBatch) + sourceSafety = + Authority.authoritySafety + (Authority.singletonEscapeKind Authority.SourceAxiom) + assertEqual "nested inductive fact eligibility" + ( Semantic.SearchEligible + : Semantic.SearchIneligible + : replicate 4 Semantic.SearchEligible + ) + (Semantic.semanticFactSearchEligibility <$> facts) + monotonicityFact <- case facts of + _definition : fact : _laws -> pure fact + _ -> assertFailure "nested inductive fact inventory" + >> fail "unreachable" + assertEqual "nested monotonicity fact is unaliased" + False + (Semantic.semanticFactFingerprint monotonicityFact + `elem` (Semantic.semanticAliasTarget <$> aliases)) + assertEqual "nested authority safety reaches generated laws" + [ Authority.cleanAuthoritySafety + , sourceSafety + , sourceSafety + , Authority.cleanAuthoritySafety + , sourceSafety + , sourceSafety + ] + ( Authority.factAuthoritySafety + . Semantic.semanticFactAuthority + <$> facts + ) + validation <- + maybe + (assertFailure "nested inductive validation is absent" + >> fail "unreachable") + pure + (Declaration.committedBatchDeclarationValidation + inductiveBatch) + assertEqual "nested inductive candidate authority shape" + [ "definition" + , "source-proof" + , "kernel" + , "kernel" + , "kernel" + , "kernel" + ] + (authorizationKind + . Authority.validationDirectAuthorization + <$> Semantic.declarationValidationRecordCertificates + validation) + requestId <- nestedRequestId inductiveBatch + Temp.withSystemTempDirectory + "felix-nested-inductive-cache" \temporary -> do + let storePath = temporary Posix.</> "store.sqlite" + bracket + (snd <$> (Store.openStore storePath + (Identity.theoryId foundation) >>= expectRight)) + Store.closeStore + \store -> do + expectRightIO + (Store.writePendingModulePrefix store + (Module.sealedTypedModulePrefix sealed)) + let warmValidation = + Declaration.WarmValidation + (Declaration.validationLookup + (expectRightIO + . Store.loadProofValidation + store) + (expectRightIO + . Store.loadDeclarationValidation + store)) + warmModules <- + compileParsedWorkspaceWithValidation + foundation bootstrap unusedResolver + warmValidation workspace + warm <- sole + "warm nested exact inductive module" + warmModules + warmBatch <- case + Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix warm) of + [_warmGuard, _warmUnsafe, batch] -> pure batch + batches -> + assertFailure + ("warm nested batch count: " + <> show (length batches)) + >> fail "unreachable" + assertEqual "warm nested exact request" + requestId + =<< nestedRequestId warmBatch + assertEqual "warm nested semantic interface" + (Module.sealedTypedModuleSemantic sealed) + (Module.sealedTypedModuleSemantic warm) + assertEqual "warm nested admitted prefix" + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix sealed)) + (Declaration.pendingModulePrefixCurrent + (Module.sealedTypedModulePrefix warm)) + freshArtifact <- + moduleArtifact + foundation bootstrap parsed sealed + warmArtifact <- + moduleArtifact + foundation bootstrap parsed warm + assertEqual "warm nested module artifact" + freshArtifact warmArtifact + batches -> + assertFailure + ("expected guard and nested inductive batches, found " + <> show (length batches)) + + failureWorkspace <- + parseExactWorkspace bootstrap mounts + "test/phase5/exact-inductive-nested-failure.tex" + successfulRequests <- newIORef [] + let successfulResolver = + Declaration.vampireResolver \prepared -> do + let problem = + Provers.preparedTypedProverLogicalProblem prepared + modifyIORef' successfulRequests + (<> [Backend.supportedPropositionTerm + (Backend.typedProblemClaim problem)]) + runNoLoggingT + (Provers.runPreparedTypedProver vampire prepared) + successfulModules <- + compileParsedWorkspaceWithValidation + foundation bootstrap successfulResolver + Declaration.FreshValidation failureWorkspace + successful <- sole + "successful repeated/distinct nested inductive module" + successfulModules + assertEqual + "repeated and distinct contexts use two monotonicity requests" + [ expectedPowerMonotonicity + , expectedDoublePowerMonotonicity + ] + =<< readIORef successfulRequests + case Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix successful) of + [_guardOne, _guardTwo, batch] -> do + validation <- maybe + (assertFailure + "successful multi-context validation absent" + >> fail "unreachable") + pure + (Declaration.committedBatchDeclarationValidation batch) + assertEqual + "deduplicated monotonicities precede all kernel laws" + ( ["definition", "source-proof", "source-proof"] + <> replicate 6 "kernel" + ) + (authorizationKind + . Authority.validationDirectAuthorization + <$> Semantic.declarationValidationRecordCertificates + validation) + batches -> + assertFailure + ("successful multi-context batch count: " + <> show (length batches)) + attempts <- newIORef (0 :: Int) + let rejectingResolver = + Declaration.vampireResolver \prepared -> do + index <- atomicModifyIORef' attempts \current -> + (current + 1, current) + if index == 0 + then pure + (Right + (Provers.CounterSatisfiable + "first monotonicity rejected")) + else runNoLoggingT + (Provers.runPreparedTypedProver vampire prepared) + failureInput <- + expectRight + (Module.typedModuleInput + foundation + (Module.bootstrapPreludeReadiness bootstrap) + rejectingResolver + Declaration.FreshValidation + (Parse.parsedWorkspaceRootModule failureWorkspace) + []) + Module.runTypedModule failureInput >>= \case + Module.TypedModuleFailed + (Module.TypedDeclarationFailed + (Declaration.ProofObligationFailedAt + location + Declaration.VampireObligationRejected{})) + prefix -> do + assertEqual "earliest monotonicity failure location" + 14 (locLine location) + assertEqual + "later monotonicity still resolves before first rejection" + 2 =<< readIORef attempts + assertEqual + "rejected monotonicity preserves only earlier declarations" + 2 + (length + (Declaration.pendingModulePrefixBatches prefix)) + _result -> + assertFailure + "nested monotonicity rejection unexpectedly succeeded" + where + authorizationKind = \case + Authority.CheckedKernelConstruction + Authority.CheckedDefinitionEquation{} -> "definition" + Authority.CheckedKernelConstruction{} -> "kernel" + Authority.CheckedSourceProof{} -> "source-proof" + authorization -> show authorization + + nestedRequestId batch = do + validation <- maybe + (assertFailure "nested declaration validation absent" + >> fail "unreachable") + pure + (Declaration.committedBatchDeclarationValidation batch) + certificate <- case + Semantic.declarationValidationRecordCertificates validation of + _definition : monotonicity : _laws -> pure monotonicity + certificates -> + assertFailure + ("nested declaration certificate count: " + <> show (length certificates)) + >> fail "unreachable" + case Authority.validationDirectAuthorization certificate of + Authority.CheckedSourceProof [request] -> pure request + authorization -> + assertFailure + ("unexpected nested proof authorization " + <> show authorization) + >> fail "unreachable" + + moduleArtifact foundation bootstrap parsed sealed = do + key <- expectRight + (Semantic.moduleArtifactKey + (moduleName (Parse.parsedModuleAddress parsed)) + (Parse.parsedModuleId parsed) + [ Semantic.semanticInterfaceAssertedId + (Module.sealedTypedModuleSemantic + (Module.bootstrapPreludeModule bootstrap)) + ] + (Identity.theoryId foundation)) + pure + (Semantic.moduleArtifactResult + key + (Syntax.moduleSyntaxAssertedId + (Module.sealedTypedModuleSyntax sealed)) + (Semantic.semanticInterfaceAssertedId + (Module.sealedTypedModuleSemantic sealed))) + + expectedPowerMonotonicity = + Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CImp + (subset (Core.CBound 1) (Core.CBound 0)) + (subset + (power (Core.CBound 1)) + (power (Core.CBound 0))))))) + + expectedDoublePowerMonotonicity = + Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CImp + (subset (Core.CBound 1) (Core.CBound 0)) + (subset + (power (power (Core.CBound 1))) + (power (power (Core.CBound 0)))))))) + + power argument = + Core.CApp (Core.CIntrinsic Core.PowerSet) argument + + subset left right = + Core.CForall Core.TySet + (Core.CImp + (member + (Core.CBound 0) + (Core.shiftCanonical 1 0 left)) + (member + (Core.CBound 0) + (Core.shiftCanonical 1 0 right))) + + member element set = + Core.CApp + (Core.CApp (Core.CIntrinsic Core.Member) element) + set + +compilesTransparentNestedInductiveWrappers :: Assertion +compilesTransparentNestedInductiveWrappers = + withAcceptedFixtureVampire "felix-nested-wrapper" \vampire -> do + repository <- getCurrentDirectory + foundation <- expectRight Foundation.checkedFoundation + bootstrap <- + expectRight + =<< Module.buildBootstrapPreludeFixture + foundation unusedResolver + mounts <- exactFixtureMounts repository + workspace <- + parseExactWorkspace bootstrap mounts + "test/phase5/exact-inductive-wrapper.tex" + observed <- newIORef [] + let resolver = + Declaration.vampireResolver \prepared -> do + let problem = + Provers.preparedTypedProverLogicalProblem prepared + modifyIORef' observed + (<> [ ( Backend.typedProblemRoute problem + , Backend.supportedPropositionTerm + (Backend.typedProblemClaim problem) + ) + ]) + runNoLoggingT + (Provers.runPreparedTypedProver vampire prepared) + modules <- + compileParsedWorkspaceWithValidation + foundation bootstrap resolver + Declaration.FreshValidation workspace + sealed <- sole "transparent-wrapper nested module" modules + observations <- readIORef observed + assertEqual "wrapper guard plus monotonicity request count" + 2 (length observations) + (route, target) <- case + [ observation + | observation@(_route, candidate) <- observations + , candidate == expectedPowerMonotonicity + ] of + [observation] -> pure observation + matches -> + assertFailure + ("normalized wrapper monotonicity matches: " + <> show matches + <> "; observed: " <> show observations) + >> fail "unreachable" + assertEqual "transparent-wrapper monotonicity is FOF" + Backend.RouteFof route + assertEqual "transparent-wrapper monotonicity target" + expectedPowerMonotonicity target + case Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix sealed) of + [_wrapperDefinition, _guardProof, inductiveBatch] -> do + let facts = + Semantic.declarationDeltaFacts + (Declaration.committedBatchDelta inductiveBatch) + assertEqual "transparent-wrapper inductive stays clean" + (replicate 6 Authority.cleanAuthoritySafety) + ( Authority.factAuthoritySafety + . Semantic.semanticFactAuthority + <$> facts + ) + validation <- maybe + (assertFailure + "transparent-wrapper declaration validation absent" + >> fail "unreachable") + pure + (Declaration.committedBatchDeclarationValidation + inductiveBatch) + assertEqual "transparent-wrapper staged authority" + [ "definition" + , "source-proof" + , "kernel" + , "kernel" + , "kernel" + , "kernel" + ] + (authorizationKind + . Authority.validationDirectAuthorization + <$> Semantic.declarationValidationRecordCertificates + validation) + batches -> + assertFailure + ("transparent-wrapper declaration count: " + <> show (length batches)) + where + authorizationKind = \case + Authority.CheckedKernelConstruction + Authority.CheckedDefinitionEquation{} -> "definition" + Authority.CheckedKernelConstruction{} -> "kernel" + Authority.CheckedSourceProof{} -> "source-proof" + authorization -> show authorization + + expectedPowerMonotonicity = + Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CImp + (subset (Core.CBound 1) (Core.CBound 0)) + (subset + (power (Core.CBound 1)) + (power (Core.CBound 0))))))) + + power argument = + Core.CApp (Core.CIntrinsic Core.PowerSet) argument + + subset left right = + Core.CForall Core.TySet + (Core.CImp + (member + (Core.CBound 0) + (Core.shiftCanonical 1 0 left)) + (member + (Core.CBound 0) + (Core.shiftCanonical 1 0 right))) + + member element set = + Core.CApp + (Core.CApp (Core.CIntrinsic Core.Member) element) + set + +normalizesNestedExactInductiveContexts :: Assertion +normalizesNestedExactInductiveContexts = do + foundation <- expectRight Foundation.checkedFoundation + powerSymbol <- fixedFunctionSymbol "pow" + carrierSymbol <- fixedFunctionSymbol "cumul" + let a = Internal.NamedVar "A" + x = Internal.NamedVar "x" + y = Internal.NamedVar "y" + z = Internal.NamedVar "z" + carrier = + Internal.TermOp Nowhere carrierSymbol [Internal.TermVar a] + powerCarrier = + Internal.TermOp Nowhere powerSymbol [carrier] + doublePowerCarrier = + Internal.TermOp Nowhere powerSymbol [powerCarrier] + parameterizedCarrier = + Internal.TermOp Nowhere powerSymbol + [ Internal.TermOp Nowhere Lexicon.UpairSymbol + [carrier, Internal.TermVar x] + ] + powerContext <- + expectRight + (TypedInductive.prepareRecursiveCarrierContext + carrierSymbol [a] powerCarrier) + doublePowerContext <- + expectRight + (TypedInductive.prepareRecursiveCarrierContext + carrierSymbol [a] doublePowerCarrier) + parameterizedContext <- + expectRight + (TypedInductive.prepareRecursiveCarrierContext + carrierSymbol [a] parameterizedCarrier) + deduplicated <- + expectRight + (TypedInductive.prepareTypedInductive + (const Core.TySet) + foundation + (const Nothing) + (Internal.Marker "nested_dedup") + (TypedInductive.DirectInductive + [a] + (Internal.EmptySet Nowhere) + (TypedInductive.DirectInductiveClause + [x, y, z] + [ TypedInductive.DirectRecursiveCondition + (Internal.TermVar x) powerContext + , TypedInductive.DirectRecursiveCondition + (Internal.TermVar y) powerContext + , TypedInductive.DirectRecursiveCondition + (Internal.TermVar z) doublePowerContext + , TypedInductive.DirectRecursiveCondition + (Internal.TermVar z) parameterizedContext + ] + (Internal.TermVar a) + :| []))) + assertEqual "equal contexts deduplicate in first-occurrence order" + [ monotonicityTarget 4 power + , monotonicityTarget 4 (power . power) + , monotonicityTarget 4 + (\hole -> power (pair hole (Core.CBound 4))) + ] + ( Core.frozenCoreTerm + . TypedInductive.typedInductiveMonotonicityTarget + <$> Vector.toList + (TypedInductive.typedInductiveMonotonicities deduplicated) + ) + + let wrapperSymbol = + Raw.mkMixfixItem + [ Just (Internal.Command "phasefivecheckedwrapper") + , Just Internal.InvisibleBraceL + , Nothing + , Just Internal.InvisibleBraceR + ] + (Internal.Marker "phasefivecheckedwrapper") + Raw.NonAssoc + wrapperCarrier = + Internal.TermOp Nowhere wrapperSymbol [carrier] + wrapperContext <- + expectRight + (TypedInductive.prepareRecursiveCarrierContext + carrierSymbol [a] wrapperCarrier) + wrapperBody <- + expectRight + (Core.checkCanonicalCore + (const Nothing) + (Core.CLam Core.TySet + (power (Core.CBound 0)))) + let wrapperId = + Identity.transparentObjectId + (Identity.theoryId foundation) + (Core.TyArrow Core.TySet Core.TySet) + (Core.frozenCoreTerm wrapperBody) + wrapped <- + expectRight + (TypedInductive.prepareTypedInductive + (const (Core.TyArrow Core.TySet Core.TySet)) + foundation + (\symbol -> + if symbol == Internal.SymbolMixfix wrapperSymbol + then Just + (TypedInductive.SourceGlobal + wrapperId (Just wrapperBody)) + else Nothing) + (Internal.Marker "nested_wrapper") + (TypedInductive.DirectInductive + [a] + (Internal.EmptySet Nowhere) + (TypedInductive.DirectInductiveClause + [x] + [TypedInductive.DirectRecursiveCondition + (Internal.TermVar x) wrapperContext] + (Internal.TermVar a) + :| []))) + assertEqual + "transparent content, not a primitive-name whitelist, owns context semantics" + [monotonicityTarget 2 power] + ( Core.frozenCoreTerm + . TypedInductive.typedInductiveMonotonicityTarget + <$> Vector.toList + (TypedInductive.typedInductiveMonotonicities wrapped) + ) + assertBool "transparent context target contains no wrapper global" + (all + (Set.null + . Core.frozenCoreGlobals + . TypedInductive.typedInductiveMonotonicityTarget) + (Vector.toList + (TypedInductive.typedInductiveMonotonicities wrapped))) + + assertExactFailure + "test/phase5/exact-inductive-wrong-arguments.tex" + 4 + (\case + ExactInductive.ExactInductiveRecursiveCarrierWrongArguments{} -> + True + _ -> False) + assertExactFailure + "test/phase5/exact-inductive-outside-membership.tex" + 4 + (\case + ExactInductive.ExactInductiveRecursiveCarrierOutsideMembership{} -> + True + _ -> False) + assertExactFailure + "test/phase5/exact-inductive-recursive-element.tex" + 4 + (\case + ExactInductive.ExactInductiveRecursiveTermMentionsCarrier{} -> + True + _ -> False) + assertExactFailure + "test/phase5/exact-inductive-recursive-domain.tex" + 2 + (\case + ExactInductive.ExactInductiveDomainMentionsCarrier{} -> True + _ -> False) + assertExactFailure + "test/phase5/exact-inductive-recursive-result.tex" + 4 + (\case + ExactInductive.ExactInductiveResultMentionsCarrier{} -> True + _ -> False) + assertExactFailure + "test/phase5/exact-inductive-unsupported-context.tex" + 4 + (\case + ExactInductive.ExactInductiveUnsupportedRecursiveCarrierContext{} -> + True + _ -> False) + where + fixedFunctionSymbol marker = + sole ("fixed function " <> StrictText.unpack marker) + [ symbol + | symbol <- Lexicon.prefixOps + , Raw.mixfixMarker symbol == Internal.Marker marker + ] + + assertExactFailure relative expectedLine expected = + prepareExactInductiveFixture relative >>= \case + Left failure + | expected failure -> + assertEqual + ("nested-context failure line for " <> relative) + expectedLine + (locLine + (ExactInductive.exactInductiveErrorLocation + failure)) + | otherwise -> + assertFailure + ("unexpected nested-context failure for " + <> relative <> ": " <> show failure) + Right{} -> + assertFailure + ("unsupported nested context was accepted: " <> relative) + + monotonicityTarget + :: Int + -> (Core.CanonicalTerm Identity.ObjectId + -> Core.CanonicalTerm Identity.ObjectId) + -> Core.CanonicalTerm Identity.ObjectId + monotonicityTarget sourceBinders context = + foldr + (const (Core.CForall Core.TySet)) + (Core.CForall Core.TySet + (Core.CForall Core.TySet + (Core.CImp + (subset (Core.CBound 1) (Core.CBound 0)) + (subset + (context (Core.CBound 1)) + (context (Core.CBound 0)))))) + [1 .. sourceBinders] + + power argument = + Core.CApp (Core.CIntrinsic Core.PowerSet) argument + + pair left right = + Core.CApp + (Core.CApp (Core.CIntrinsic Core.PairSet) left) + right + + subset left right = + Core.CForall Core.TySet + (Core.CImp + (member + (Core.CBound 0) + (Core.shiftCanonical 1 0 left)) + (member + (Core.CBound 0) + (Core.shiftCanonical 1 0 right))) + + member element set = + Core.CApp + (Core.CApp (Core.CIntrinsic Core.Member) element) + set compilesAndReusesExactInductives :: Assertion compilesAndReusesExactInductives = @@ -3311,37 +6029,6 @@ compilesAndReusesExactInductives = freshArtifact =<< artifact warm - mounts <- exactFixtureMounts =<< getCurrentDirectory - nestedWorkspace <- - parseExactWorkspace bootstrap mounts - "test/phase5/exact-inductive-nested.tex" - nestedParsed <- - sole "nested exact inductive module" - (toList - (Parse.parsedWorkspaceImportedBeforeImporter - nestedWorkspace)) - nestedInput <- - expectRight - (Module.typedModuleInput - foundation - (Module.bootstrapPreludeReadiness bootstrap) - unusedResolver - Declaration.FreshValidation - nestedParsed - []) - Module.runTypedModule nestedInput >>= \case - Module.TypedModuleFailed - (Module.TypedActionFailed - (Module.TypedExactInductiveFailed - (ExactInductive.ExactInductiveNestedRecursion - location))) - prefix -> do - assertEqual "nested failure line" 6 (locLine location) - assertBool "nested declaration publishes no prefix" - (null (Declaration.pendingModulePrefixBatches prefix)) - _result -> - assertFailure "unexpected nested inductive result" - authorizesRecursiveExactInductives :: Assertion authorizesRecursiveExactInductives = Temp.withSystemTempDirectory "felix-recursive-inductive" \directory -> do @@ -3733,13 +6420,20 @@ assertExactSeparationModule label sealed = do assertFailure (label <> ": unexpected separation object " <> show content) + let definitionDelta = + Declaration.committedBatchDelta definitionBatch + definitionFacts = + Semantic.declarationDeltaFacts definitionDelta assertEqual (label <> " definition fact count") + 2 (length definitionFacts) + assertEqual (label <> " defining equation is explicit-only") + [Semantic.SearchIneligible, Semantic.SearchEligible] + (Semantic.semanticFactSearchEligibility <$> definitionFacts) + assertEqual (label <> " generated view is unaliased") 1 - (length - (Semantic.declarationDeltaFacts - (Declaration.committedBatchDelta definitionBatch))) + (length (Semantic.declarationDeltaAliases definitionDelta)) assertEqual (label <> " definition proposition count") - 1 + 2 (length (Declaration.committedBatchPropositions definitionBatch)) assertEqual (label <> " definition proof validations") @@ -3753,19 +6447,22 @@ assertExactSeparationModule label sealed = do pure (Declaration.committedBatchDeclarationValidation definitionBatch) - definitionCertificate <- sole - (label <> " definition certificate") - (Semantic.declarationValidationRecordCertificates - definitionValidation) case Authority.validationDirectAuthorization - definitionCertificate of - Authority.CheckedKernelConstruction - (Authority.CheckedDefinitionEquation _target) -> - pure () - authorization -> + <$> Semantic.declarationValidationRecordCertificates + definitionValidation of + [ Authority.CheckedKernelConstruction + (Authority.CheckedDefinitionEquation target) + , Authority.CheckedKernelConstruction + (Authority.CheckedSetConstructionExtensionality + generatedTarget _descriptor) + ] -> + assertEqual + (label <> " construction authority object") + target generatedTarget + authorizations -> assertFailure - (label <> ": unexpected definition authority " - <> show authorization) + (label <> ": unexpected definition authorities " + <> show authorizations) assertEqual (label <> " theorem adds no object") [] @@ -3821,19 +6518,76 @@ reusesExactSeparationValidation = unusedResolver mounts <- exactFixtureMounts root workspace <- parseExactWorkspace bootstrap mounts relative - freshRuns <- newIORef (0 :: Int) + freshRequests <- newIORef [] + let freshResolver = Declaration.vampireResolver \prepared -> do + modifyIORef' freshRequests + (<> [Provers.preparedTypedProverRequest prepared]) + runNoLoggingT + (Provers.runPreparedTypedProver + (Provers.vampire + executable + Provers.defaultTimeLimit + Provers.defaultMemoryLimit) + prepared) freshModules <- compileParsedWorkspaceWithValidation foundation bootstrap - (countingAcceptedResolver executable freshRuns) + freshResolver Declaration.FreshValidation workspace assertEqual "fresh separation proof runs Vampire once" 1 - =<< readIORef freshRuns + . length + =<< readIORef freshRequests fresh <- sole "fresh exact separation module" freshModules assertExactSeparationModule "fresh cached" fresh + freshDefinitionBatch <- + case Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix fresh) of + batch : _theorem : [] -> pure batch + batches -> + assertFailure + ("fresh separation declaration count: " + <> show (length batches)) + >> fail "unreachable" + freshDefinitionValidation <- + maybe + (assertFailure "fresh separation definition validation absent" + >> fail "unreachable") + pure + (Declaration.committedBatchDeclarationValidation + freshDefinitionBatch) + corruptedDefinitionValidation <- + case Semantic.declarationValidationRecordCertificates + freshDefinitionValidation of + [equation, extensional] -> do + corruptedExtensional <- + expectRight + (Authority.validationCertificate + (Authority.validationTarget extensional) + (Authority.validationDirectAuthorization + equation)) + pure + (Semantic.declarationValidationRecord + (Semantic.declarationValidationRecordKey + freshDefinitionValidation) + [equation, corruptedExtensional]) + certificates -> + assertFailure + ("fresh separation certificate count: " + <> show (length certificates)) + >> fail "unreachable" + freshRequest <- + sole "fresh separation request" + =<< readIORef freshRequests + freshAcceptedRequest <- + acceptedRequestId "fresh separation" fresh + assertEqual "fresh authority binds the exact request bytes" + freshAcceptedRequest + (Provers.preparedVerificationRequestId freshRequest) + assertBool "fresh separation request bytes are retained by the caller" + (Provers.preparedVerificationByteCount freshRequest > 0) bracket (snd <$> (Store.openStore storePath (Identity.theoryId foundation) >>= expectRight)) @@ -3862,6 +6616,12 @@ reusesExactSeparationValidation = =<< readIORef warmRuns warm <- sole "warm exact separation module" warmModules assertExactSeparationModule "warm cached" warm + warmAcceptedRequest <- + acceptedRequestId "warm separation" warm + assertEqual + "warm validation retains the fresh request-byte identity" + freshAcceptedRequest + warmAcceptedRequest assertEqual "warm separation semantic interface" (Module.sealedTypedModuleSemantic fresh) (Module.sealedTypedModuleSemantic warm) @@ -3890,6 +6650,64 @@ reusesExactSeparationValidation = assertEqual "warm separation checked artifacts" (components fresh) (components warm) + corruptRuns <- newIORef (0 :: Int) + let corruptedValidation = + Declaration.WarmValidation + (Declaration.validationLookup + (expectRightIO + . Store.loadProofValidation store) + (\key -> + if key + == Semantic.declarationValidationRecordKey + corruptedDefinitionValidation + then pure + (Just corruptedDefinitionValidation) + else expectRightIO + (Store.loadDeclarationValidation + store key))) + corrupted <- Exception.try + (compileParsedWorkspaceWithValidation + foundation + bootstrap + (countingAcceptedResolver executable corruptRuns) + corruptedValidation + workspace) + :: IO + (Either + Declaration.ValidationIntegrityError + [Module.SealedTypedModule]) + case corrupted of + Left Declaration.CachedValidationIntegrityError{} -> + pure () + Right _ -> + assertFailure + "mismatched generated authority replay succeeded" + assertEqual + "mismatched generated authority does not invoke Vampire" + 0 + =<< readIORef corruptRuns + where + acceptedRequestId label sealed = do + theoremBatch <- + case Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix sealed) of + [_definitionBatch, batch] -> pure batch + batches -> + assertFailure + (label <> ": unexpected declaration count " + <> show (length batches)) + >> fail "unreachable" + validation <- sole + (label <> " proof validation") + (Declaration.committedBatchProofValidations theoremBatch) + case Authority.validationDirectAuthorization + (Semantic.proofValidationRecordCertificate validation) of + Authority.CheckedSourceProof [request] -> pure request + authorization -> + assertFailure + (label <> ": unexpected direct authorization " + <> show authorization) + >> fail "unreachable" compilesExactSourceAxioms :: Assertion compilesExactSourceAxioms = @@ -5862,7 +8680,7 @@ retainsExactPrefixBeforeFailure = do source (Module.TypedActionFailed (Module.TypedExactCompileFailed - (Exact.ExactUnsupportedDeclarationBody location))) + (Exact.ExactGuardedOpaqueSignature location))) prefix) , _measurements ) -> do @@ -5870,7 +8688,7 @@ retainsExactPrefixBeforeFailure = do "test/phase5/exact-failure.tex" (safeRelativePathFilePath (resolvedSourceRelativePath source)) - assertEqual "unsupported declaration line" 5 (locLine location) + assertEqual "unsupported declaration line" 6 (locLine location) assertEqual "earlier exact declaration remains committed" 1 (length (Declaration.pendingModulePrefixBatches prefix)) @@ -6002,34 +8820,283 @@ retainsExactPrefixBeforeFailure = do _result -> assertFailure "unexpected runtime proof failure" -rejectsNestedExactSetInduction :: Assertion -rejectsNestedExactSetInduction = do - result <- - withAcceptedFixtureVampire "felix-nested-set-induction" \prover -> +restoresCheckedSetInduction :: Assertion +restoresCheckedSetInduction = + Temp.withSystemTempDirectory "felix-checked-set-induction" \root -> do + let executable = root Posix.</> "vampire" + storePath = root Posix.</> "store.sqlite" + writeAcceptedFixtureVampire executable + foundation <- expectRight Foundation.checkedFoundation + bootstrap <- + expectRight + =<< Module.buildBootstrapPreludeFixture + foundation unusedResolver + mounts <- exactFixtureMounts =<< getCurrentDirectory + + initialWorkspace <- parseExactWorkspace bootstrap mounts + "test/phase5/exact-induction-initial.tex" + initialObservations <- newIORef [] + initial <- + sole "initial set-induction module" + =<< compileParsedWorkspaceWithValidation + foundation bootstrap + (observingResolver executable initialObservations) + Declaration.FreshValidation + initialWorkspace + [initialRequest] <- + expectCount "initial set-induction request" 1 + =<< readIORef initialObservations + assertEqual "initial induction retains header then hypothesis ordinals" + [0, 1] + (localReasoningLocalOrdinals initialRequest) + let initialTarget = + Core.CEq Core.TySet (Core.CBound 0) (Core.CBound 0) + initialAntecedent = + member (Core.CBound 1) (Core.CBound 0) + initialHypothesis = + Core.CForall Core.TySet + (Core.CImp + (member (Core.CBound 0) (Core.CBound 2)) + (Core.CImp + (member (Core.CBound 0) (Core.CBound 1)) + (Core.CEq Core.TySet + (Core.CBound 0) + (Core.CBound 0)))) + assertEqual "initial induction child target" + initialTarget + (localReasoningTarget initialRequest) + assertEqual "initial induction uses the complete guarded property" + [initialAntecedent, initialHypothesis] + (localReasoningLocalTerms initialRequest) + + nestedWorkspace <- parseExactWorkspace bootstrap mounts + "test/phase5/exact-induction-nested.tex" + nestedObservations <- newIORef [] + nested <- + sole "nested set-induction module" + =<< compileParsedWorkspaceWithValidation + foundation bootstrap + (observingResolver executable nestedObservations) + Declaration.FreshValidation + nestedWorkspace + [nestedChild, nestedContinuation] <- + expectCount "nested set-induction requests" 2 + =<< readIORef nestedObservations + let x = Core.CBound 0 + a = Core.CBound 1 + y = Core.CBound 0 + xUnderY = Core.CBound 1 + aUnderY = Core.CBound 2 + guardAtX = + andP + (member x a) + (notP (Core.CEq Core.TySet x a)) + guardAtY = + andP + (member y aUnderY) + (notP (Core.CEq Core.TySet y aUnderY)) + nestedHypothesis = + Core.CForall Core.TySet + (Core.CImp + (member y xUnderY) + (Core.CImp + guardAtY + (Core.CEq Core.TySet y y))) + nestedTarget = Core.CEq Core.TySet x x + assertEqual + "omitted leading induction retains its source binder and guard" + ([0, 1], [nestedHypothesis, guardAtX], nestedTarget) + ( localReasoningLocalOrdinals nestedChild + , localReasoningLocalTerms nestedChild + , localReasoningTarget nestedChild + ) + case localReasoningLocalTerms nestedContinuation of + [derived] -> do + assertEqual "subproof continuation uses one derived local" + [2] (localReasoningLocalOrdinals nestedContinuation) + assertEqual "subproof closes the exact binder-level result" + derived (localReasoningTarget nestedContinuation) + locals -> + assertFailure + ("unexpected induction continuation locals: " + <> show locals) + + formulaWorkspace <- parseExactWorkspace bootstrap mounts + "test/phase5/exact-induction-formula-quantified.tex" + formulaObservations <- newIORef [] + _formula <- + sole "formula-quantified set-induction module" + =<< compileParsedWorkspaceWithValidation + foundation bootstrap + (observingResolver executable formulaObservations) + Declaration.FreshValidation + formulaWorkspace + [formulaChild, formulaContinuation] <- + expectCount "formula-quantified set-induction requests" 2 + =<< readIORef formulaObservations + assertEqual + "formula-quantified omitted induction retains its written binder" + (Core.CEq Core.TySet (Core.CBound 0) (Core.CBound 0)) + (localReasoningTarget formulaChild) + assertEqual + "formula-quantified continuation retains hypothesis and derived local" + [0, 1] + (localReasoningLocalOrdinals formulaContinuation) + + anchorWorkspace <- parseExactWorkspace bootstrap mounts + "test/examples/no-reflexive-set.tex" + anchorObservations <- newIORef [] + _anchor <- + sole "omitted-focus set-induction module" + =<< compileParsedWorkspaceWithValidation + foundation bootstrap + (observingResolver executable anchorObservations) + Declaration.FreshValidation + anchorWorkspace + [anchorRequest] <- + expectCount "omitted-focus set-induction request" 1 + =<< readIORef anchorObservations + anchorLocal <- + case localReasoningLocalTerms anchorRequest of + [term] -> pure term + terms -> + assertFailure + ("unexpected omitted-focus locals: " <> show terms) + >> fail "unreachable" + assertEqual "omitted focus retains its source binder in the child" + ([0], Core.CForall Core.TySet + (Core.CImp + (member (Core.CBound 0) (Core.CBound 1)) + (notP (member (Core.CBound 0) (Core.CBound 0))))) + ( localReasoningLocalOrdinals anchorRequest + , anchorLocal + ) + + assertProofParityFailure + foundation bootstrap mounts + "test/phase5/exact-induction-ambiguous.tex" + (\case + ExactProof.ExactProofSetInductionFocusAmbiguous location -> + locLine location == 5 + _failure -> False) + assertProofParityFailure + foundation bootstrap mounts + "test/phase5/exact-induction-fixed.tex" + (\case + ExactProof.ExactProofSetInductionActiveBinderIneligible + location (Raw.NamedVar "x") -> + locLine location == 7 + _failure -> False) + + failedInput <- + moduleInput + foundation bootstrap initialWorkspace + (Declaration.vampireResolver \_prepared -> + pure + (Right + (Provers.CounterSatisfiable + "focused induction child rejection"))) + Declaration.FreshValidation + Module.runTypedModule failedInput >>= \case + Module.TypedModuleFailed _failure prefix -> + assertBool "failed induction child publishes no theorem" + (null (Declaration.pendingModulePrefixBatches prefix)) + _result -> + assertFailure "rejected induction child unexpectedly succeeded" + + bracket + (snd <$> (Store.openStore storePath + (Identity.theoryId foundation) >>= expectRight)) + Store.closeStore + \store -> do + expectRightIO + (Store.writePendingModulePrefix store + (Module.sealedTypedModulePrefix nested)) + let validation = + Declaration.WarmValidation + (Declaration.validationLookup + (expectRightIO + . Store.loadProofValidation store) + (expectRightIO + . Store.loadDeclarationValidation store)) + warmRuns <- newIORef (0 :: Int) + warm <- + sole "warm nested set-induction module" + =<< compileParsedWorkspaceWithValidation + foundation bootstrap + (countingAcceptedResolver executable warmRuns) + validation nestedWorkspace + assertEqual "warm set induction skips Vampire" + 0 =<< readIORef warmRuns + assertEqual "fresh and warm induction proof validations" + (proofValidations nested) + (proofValidations warm) + assertBool "initial induction publishes one theorem" + (not + (null + (Declaration.pendingModulePrefixBatches + (Module.sealedTypedModulePrefix initial)))) + where + observingResolver executable observations = + Declaration.vampireResolver \prepared -> do + let problem = Provers.preparedTypedProverLogicalProblem prepared + locals = Backend.typedProblemLocalPremises problem + modifyIORef' observations + (<> [ LocalReasoningObservation + { localReasoningTarget = + Backend.supportedPropositionTerm + (Backend.typedProblemClaim problem) + , localReasoningGlobalCount = + Vector.length + (Backend.typedProblemGlobalPremises problem) + , localReasoningLocalOrdinals = + Backend.localPremiseOrdinalValue + . Backend.typedLocalPremiseOrdinal + <$> Vector.toList locals + , localReasoningLocalTerms = + Backend.supportedPropositionTerm + . Backend.typedLocalPremiseProposition + <$> Vector.toList locals + , localReasoningAuxiliaries = + Backend.typedProblemAuxiliaryTag + <$> Vector.toList + (Backend.typedProblemAuxiliaries problem) + } + ]) runNoLoggingT - (Api.verifyMeasured - prover - "test/phase5/exact-induction-nested.tex") - case result of - Right - ( Api.VerificationCheckingFailure _report - (Api.VerificationTypedModuleError - _source - (Module.TypedActionFailed - (Module.TypedExactProofFailed - (ExactProof.ExactProofSetInductionNotOutermost - location))) - prefix) - , _measurements - ) -> do - assertEqual "nested induction line" 7 (locLine location) - assertBool "failed proof publishes no theorem" - (null (Declaration.pendingModulePrefixBatches prefix)) - Left err -> - assertFailure - ("unexpected nested-induction failure: " <> show err) - Right{} -> - assertFailure "nested exact set induction was admitted" + (Provers.runPreparedTypedProver + (Provers.vampire + executable + Provers.defaultTimeLimit + Provers.defaultMemoryLimit) + prepared) + + expectCount label expected values = do + assertEqual label expected (length values) + pure values + + member element set = + Core.CApp + (Core.CApp (Core.CIntrinsic Core.Member) element) + set + + notP proposition = Core.CImp proposition Core.CFalsum + + andP left right = notP (Core.CImp left (notP right)) + + moduleInput foundation bootstrap workspace resolver validation = do + parsed <- sole "set-induction parsed module" + (toList (Parse.parsedWorkspaceImportedBeforeImporter workspace)) + expectRight + (Module.typedModuleInput + foundation + (Module.bootstrapPreludeReadiness bootstrap) + resolver validation parsed []) + + proofValidations = + concatMap Declaration.committedBatchProofValidations + . Declaration.pendingModulePrefixBatches + . Module.sealedTypedModulePrefix routesProductionVerification :: Assertion routesProductionVerification = @@ -6320,14 +9387,18 @@ prepareExactInductiveFixture relative = do let identified = Module.identifiedPhysicalModule parsed owner = Module.identifiedModuleOwner identified parsedModule = Module.identifiedModuleParsed identified - block <- + (blockIndex, block) <- sole "exact inductive block" - (Parse.identifiedParsedModuleBlocks parsedModule) + [ (index, candidate) + | (index, candidate@Raw.BlockInductive{}) <- + zip [0..] + (Parse.identifiedParsedModuleBlocks parsedModule) + ] let entries = [ Parse.parsedSyntaxOccurrenceEntry occurrence | occurrence <- Parse.identifiedParsedModuleSyntaxOccurrences parsedModule - , Parse.parsedSyntaxOccurrenceBlockIndex occurrence == 0 + , Parse.parsedSyntaxOccurrenceBlockIndex occurrence == blockIndex ] action :: Declaration.ModuleDriver Void diff --git a/source/Test/Unit/Provers.hs b/source/Test/Unit/Provers.hs index d5173e1..d351652 100644 --- a/source/Test/Unit/Provers.hs +++ b/source/Test/Unit/Provers.hs @@ -1053,8 +1053,8 @@ preparedTypedTask factCount = do proposition [] [] - ExplicitGlobalPremises - FirstOrderLocals) + FirstOrderLocals + ExplicitHigherOrderJustification) expectRight (prepareTypedProverTask DirectTask problem) where propositionTerm = diff --git a/source/Test/Unit/Source.hs b/source/Test/Unit/Source.hs index 73eaef5..fabe943 100644 --- a/source/Test/Unit/Source.hs +++ b/source/Test/Unit/Source.hs @@ -139,6 +139,8 @@ unitTests = testGroup "Source resolution" , testCase "parses loaded sources without rereading files" parsesWithoutRereading , testCase "returns source-local failures after prior chunk callbacks" returnsSourceParseFailures + , testCase "rejects guarded symbolic declarations before publication" + rejectsGuardedSymbolicDeclarations ] validatesRelativePaths :: Assertion @@ -2298,6 +2300,49 @@ returnsSourceParseFailures = Right workspace -> assertFailure ("expected parse failure, got " <> show workspace) +rejectsGuardedSymbolicDeclarations :: Assertion +rejectsGuardedSymbolicDeclarations = + for_ [("definition", 3 :: Int), ("abbreviation", 2)] + \(kind, failureLine) -> + withTemporaryDirectory + ("felix-guarded-symbolic-" <> kind) + \temp -> do + let relative = "entry.tex" + source = unlines + [ "\\begin{" <> kind <> "}\\label{guarded_symbolic}" + , " Suppose $\\top$." + , " $\\guardedsymbolic{X} = X$." + , "\\end{" <> kind <> "}" + ] + writeFile (temp Posix.</> relative) source + graph <- buildSearchedGraph temp relative + emittedRef <- newIORef ([] :: [Raw.Block]) + result <- + Parse.parseResolvedSourceGraphWith graph + (\_source block -> modifyIORef' emittedRef (block :)) + case result of + Left (Parse.SourceParseError failed parseFailure) -> do + assertEqual (kind <> " source") relative + (safeRelativePathFilePath + (resolvedSourceRelativePath failed)) + assertBool + (kind <> " parse failure retains a located source position: " + <> show parseFailure) + (("entry.tex " <> show failureLine <> ":") + `List.isInfixOf` show parseFailure) + assertEqual + (kind <> " publishes no completed source block") + [] + =<< readIORef emittedRef + Left failure -> + assertFailure + ("expected guarded-symbolic parse failure, got " + <> show failure) + Right workspace -> + assertFailure + ("guarded symbolic " <> kind + <> " was silently accepted: " <> show workspace) + buildSearchedGraph :: FilePath -> FilePath -> IO ResolvedSourceGraph buildSearchedGraph root path = do mounts <- oneMount "project" root |