diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | source/Checking/Backend/Problem.hs | 224 | ||||
| -rw-r--r-- | source/Checking/Core.hs | 47 | ||||
| -rw-r--r-- | source/Checking/Declaration.hs | 19 | ||||
| -rw-r--r-- | source/Checking/Exact.hs | 299 | ||||
| -rw-r--r-- | source/Checking/Exact/Proof.hs | 272 | ||||
| -rw-r--r-- | source/Checking/Exact/Vocabulary.hs | 28 | ||||
| -rw-r--r-- | source/Checking/Typed/Inductive.hs | 36 | ||||
| -rw-r--r-- | source/Felix/Cache/Codec.hs | 2 | ||||
| -rw-r--r-- | source/Syntax/Lexicon.hs | 12 | ||||
| -rw-r--r-- | source/Test/Unit/Backend.hs | 219 | ||||
| -rw-r--r-- | source/Test/Unit/Declaration.hs | 202 | ||||
| -rw-r--r-- | source/Test/Unit/Module.hs | 481 | ||||
| -rw-r--r-- | source/Test/Unit/Provers.hs | 3 | ||||
| -rw-r--r-- | test/phase5/exact-proof-parity-invalid-assume.tex | 8 | ||||
| -rw-r--r-- | test/phase5/exact-proof-parity-invalid-fix-shape.tex | 8 | ||||
| -rw-r--r-- | test/phase5/exact-proof-parity-invalid-fix.tex | 8 | ||||
| -rw-r--r-- | test/phase5/exact-proof-parity.tex | 107 | ||||
| -rw-r--r-- | test/phase5/exact-replacement.tex | 1 | ||||
| -rw-r--r-- | test/phase5/exact-separation.tex | 1 | ||||
| -rw-r--r-- | test/phase5/exact-structure.tex | 66 |
21 files changed, 1772 insertions, 273 deletions
@@ -46,3 +46,5 @@ check/ html/ /notes library/naprochelibrary*.tex +profiling/ +experimental/ diff --git a/source/Checking/Backend/Problem.hs b/source/Checking/Backend/Problem.hs index 61a31d2..1f51eb2 100644 --- a/source/Checking/Backend/Problem.hs +++ b/source/Checking/Backend/Problem.hs @@ -38,8 +38,7 @@ module Checking.Backend.Problem , typedProblemAuxiliaryTag , typedProblemAuxiliaryProposition , typedProblemAuxiliaryCapability - , GlobalPremiseMode(..) - , LocalPremisePolicy(..) + , PremiseSelectionMode(..) , selectTypedLocalPremises , TypedProblemRoute(..) , TypedProblem @@ -806,33 +805,44 @@ typedProblemAuxiliaryCapability capability -data GlobalPremiseMode - = ImplicitFofPremises - | ExplicitGlobalPremises - | NoGlobalPremises - deriving stock (Show, Eq) - -data LocalPremisePolicy - = FirstOrderLocals - | AllLocals +-- | Source justification policy for premise selection. Higher-order routing +-- is validated separately after the complete selected problem is known. +data PremiseSelectionMode + = ImplicitPremiseSelection + | ExplicitGlobalPremiseSelection + | LocalOnlyPremiseSelection deriving stock (Show, Eq) selectTypedLocalPremises - :: LocalPremisePolicy + :: PremiseSelectionMode -> [TypedLocalPremise local origin global] -> Vector (TypedLocalPremise local origin global) -selectTypedLocalPremises localPolicy availableLocals = +selectTypedLocalPremises selection availableLocals = Vector.fromList (List.sortOn typedLocalPremiseOrdinal - (case localPolicy of - FirstOrderLocals -> + (case selection of + ImplicitPremiseSelection -> + List.filter implicitLocalPremise availableLocals + ExplicitGlobalPremiseSelection -> List.filter (isFofCapability . typedLocalPremiseCapability) availableLocals - AllLocals -> + LocalOnlyPremiseSelection -> availableLocals)) + where + implicitLocalPremise premise = + isFofCapability (typedLocalPremiseCapability premise) + || isJust + (implicitConstructionAdmission + (typedLocalPremiseProposition premise) + (typedLocalPremiseCapability premise)) + +data ImplicitHigherOrderConstruction + = ImplicitSeparation + | ImplicitFunctionalReplacement + deriving stock (Show, Eq, Ord) data TypedProblemRoute = RouteFof @@ -855,9 +865,6 @@ data TypedProblemError local global !(BackendClassificationError global) | TypedProblemExplicitHigherOrderJustificationRequired !(NonEmpty BackendFofExclusion) - | TypedProblemInvalidPolicyCombination - !GlobalPremiseMode - !LocalPremisePolicy | TypedProblemDuplicateLocalPremiseOrdinal !LocalPremiseOrdinal | TypedProblemLocalTypeMismatch @@ -873,8 +880,7 @@ planTypedProblem -> SupportedProposition local global -> [TypedLocalPremise local origin global] -> [TypedFoundationAuxiliaryInput global] - -> GlobalPremiseMode - -> LocalPremisePolicy + -> PremiseSelectionMode -> Either (TypedProblemError local global) (TypedProblem ref local origin global) @@ -884,11 +890,7 @@ planTypedProblem claim availableLocals auxiliaries - globalPolicy - localPolicy = do - validatePolicyCombination - globalPolicy - localPolicy + selection = do validateLocalPremiseOrdinals availableLocals claimCapability <- @@ -899,25 +901,21 @@ planTypedProblem claim) let selectedLocals = selectTypedLocalPremises - localPolicy + selection availableLocals let preparedAuxiliaries = zipWith prepareAuxiliary [0..] auxiliaries - case globalPolicy of - ImplicitFofPremises -> - case implicitTh0Requirement - claimCapability - (typedProblemAuxiliaryCapability - <$> preparedAuxiliaries) of - Nothing -> - pure () - Just exclusions -> - Left - (TypedProblemExplicitHigherOrderJustificationRequired - exclusions) + case selection of + ImplicitPremiseSelection -> + validateImplicitHigherOrderAdmission + claim + claimCapability + selectedFacts + selectedLocals + preparedAuxiliaries _ -> pure () let selectedFofCapabilities = @@ -956,23 +954,6 @@ planTypedProblem globalTypes localTypes) where - implicitTh0Requirement claimCapability - auxiliaryCapabilities = - case claimCapability of - RequiresTh0 exclusions -> - Just exclusions - FofProjectable{} -> - firstAuxiliaryRequirement - auxiliaryCapabilities - - firstAuxiliaryRequirement = \case - [] -> - Nothing - FofProjectable{} : remaining -> - firstAuxiliaryRequirement remaining - RequiresTh0 exclusions : _remaining -> - Just exclusions - prepareAuxiliary ordinal (TypedFoundationAuxiliaryInput @@ -985,25 +966,120 @@ planTypedProblem proposition capability -validatePolicyCombination - :: GlobalPremiseMode - -> LocalPremisePolicy - -> Either - (TypedProblemError local global) - () -validatePolicyCombination globalPolicy localPolicy = - case (globalPolicy, localPolicy) of - (ImplicitFofPremises, FirstOrderLocals) -> - Right () - (ExplicitGlobalPremises, FirstOrderLocals) -> - Right () - (NoGlobalPremises, AllLocals) -> - Right () +-- | Implicit automation admits higher-order routing only for a checked +-- proposition that itself contains one of the two approved set constructions. +-- This classification selects no premise and grants no authority. +implicitConstructionAdmission + :: SupportedProposition local global + -> FofCapability projection + -> Maybe (Set ImplicitHigherOrderConstruction) +implicitConstructionAdmission proposition capability = + case capability of + FofProjectable{} -> + Nothing + RequiresTh0 exclusions + | Set.null constructions -> + Nothing + | all (admittedExclusion constructions) exclusions -> + Just constructions + | otherwise -> + Nothing + where + dependencies = + foundationAxiomDependencies + (supportedPropositionTerm proposition) + constructions = + Set.fromList + ( [ ImplicitSeparation + | SeparationCharacteristic `Set.member` dependencies + ] + <> [ ImplicitFunctionalReplacement + | ReplacementCharacteristic `Set.member` dependencies + ] + ) + + admittedExclusion allowed = \case + StructuralFofExclusion HigherOrderLambda -> + True + StructuralFofExclusion (HigherOrderIntrinsic Sep) -> + ImplicitSeparation `Set.member` allowed + StructuralFofExclusion (HigherOrderIntrinsic Repl) -> + ImplicitFunctionalReplacement `Set.member` allowed + -- The checked proposition is the deliberate granularity: its typed + -- global occurrences neither select another fact nor grant authority. + HigherOrderGlobalType{} -> + True + StructuralFofExclusion{} -> + False + HigherOrderAmbientLocal{} -> + False + +validateImplicitHigherOrderAdmission + :: SupportedProposition local global + -> FofCapability claimProjection + -> Vector (TypedBackendFact ref global) + -> Vector (TypedLocalPremise local origin global) + -> [TypedProblemAuxiliary global] + -> Either (TypedProblemError local global) () +validateImplicitHigherOrderAdmission + claim claimCapability selectedFacts selectedLocals auxiliaries = do + claimConstructions <- + admittedPropositionConstructions claim claimCapability + traverse_ requireFirstOrderGlobal selectedFacts + localConstructions <- + foldM + (\admitted premise -> + (admitted <>) + <$> admittedPropositionConstructions + (typedLocalPremiseProposition premise) + (typedLocalPremiseCapability premise)) + Set.empty + (Vector.toList selectedLocals) + let admitted = claimConstructions <> localConstructions + traverse_ (requireAdmittedAuxiliary admitted) auxiliaries + where + admittedPropositionConstructions proposition = \case + FofProjectable{} -> + Right Set.empty + RequiresTh0 exclusions -> + maybe + (Left + (TypedProblemExplicitHigherOrderJustificationRequired + exclusions)) + Right + (implicitConstructionAdmission + proposition + (RequiresTh0 exclusions)) + + requireFirstOrderGlobal fact = + case typedBackendFactCapability fact of + FofProjectable{} -> + Right () + RequiresTh0 exclusions -> + Left + (TypedProblemExplicitHigherOrderJustificationRequired + exclusions) + + requireAdmittedAuxiliary admitted auxiliary = + case typedProblemAuxiliaryCapability auxiliary of + FofProjectable{} -> + Right () + RequiresTh0 exclusions + | auxiliaryAdmitted admitted + (typedProblemAuxiliaryTag auxiliary) -> + Right () + | otherwise -> + Left + (TypedProblemExplicitHigherOrderJustificationRequired + exclusions) + + auxiliaryAdmitted admitted = \case + SeparationCharacteristic -> + ImplicitSeparation `Set.member` admitted + ReplacementCharacteristic -> + ImplicitFunctionalReplacement `Set.member` admitted _ -> - Left - (TypedProblemInvalidPolicyCombination - globalPolicy - localPolicy) + False validateLocalPremiseOrdinals :: [TypedLocalPremise local origin global] diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs index 4b7478f..f8466af 100644 --- a/source/Checking/Core.hs +++ b/source/Checking/Core.hs @@ -58,6 +58,7 @@ module Checking.Core , closeScopedExists , openScopedForall , openScopedImplication + , openScopedAssumption , closeScopedCore , instantiateCanonical , mapCanonicalGlobals @@ -1058,6 +1059,52 @@ openScopedImplication openScopedImplication _scoped = Nothing +-- | Open a checked proof assumption against the current goal. Besides a +-- direct implication antecedent, the source language historically permits +-- either immediate side of one binary conjunction antecedent to be assumed +-- first. The other side remains the next implication antecedent. This is a +-- deliberately shallow structural rule: it neither flattens conjunctions nor +-- treats disjunction as an eliminable assumption. +openScopedAssumption + :: Eq global + => ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + ) +openScopedAssumption supplied goal = do + (antecedent, conclusion) <- openScopedImplication goal + if supplied == antecedent + then pure (antecedent, conclusion) + else do + (left, right) <- splitScopedConjunction antecedent + if supplied == left + then do + remaining <- implyScopedCore right conclusion + pure (left, remaining) + else if supplied == right + then do + remaining <- implyScopedCore left conclusion + pure (right, remaining) + else Nothing + +splitScopedConjunction + :: ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + ) +splitScopedConjunction + (ScopedCheckedCore context TyProp + (CImp (CImp left (CImp right CFalsum)) CFalsum)) = + Just + ( ScopedCheckedCore context TyProp left + , ScopedCheckedCore context TyProp right + ) +splitScopedConjunction _scoped = + Nothing + closeScopedCore :: ScopedCheckedCore global -> Maybe (FrozenCheckedCore global) diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs index 65b7675..f95286c 100644 --- a/source/Checking/Declaration.hs +++ b/source/Checking/Declaration.hs @@ -2817,20 +2817,14 @@ prepareVampireObligationWith globalType builder selection - let (globalMode, localPolicy) = + let premiseSelection = case selection of VampireImplicitPremises -> - ( Backend.ImplicitFofPremises - , Backend.FirstOrderLocals - ) + Backend.ImplicitPremiseSelection VampireExplicitPremises{} -> - ( Backend.ExplicitGlobalPremises - , Backend.FirstOrderLocals - ) + Backend.ExplicitGlobalPremiseSelection VampireLocalPremises -> - ( Backend.NoGlobalPremises - , Backend.AllLocals - ) + Backend.LocalOnlyPremiseSelection propositionDependencies = foundationAxiomDependencies . Backend.supportedPropositionTerm @@ -2846,7 +2840,7 @@ prepareVampireObligationWith (propositionDependencies . Backend.typedLocalPremiseProposition) (Backend.selectTypedLocalPremises - localPolicy + premiseSelection locals) ) auxiliaries = @@ -2861,8 +2855,7 @@ prepareVampireObligationWith claim locals auxiliaries - globalMode - localPolicy) + premiseSelection) task <- first VampireObligationEncodingFailed (Provers.prepareTypedProverTask diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs index d0278f5..1788224 100644 --- a/source/Checking/Exact.hs +++ b/source/Checking/Exact.hs @@ -9,11 +9,15 @@ module Checking.Exact , ExactBinderContext , emptyExactBinderContext , extendExactBinderContext + , extendExactAnonymousBinderContext , exactBinderContextSupport , exactBinderContextIndex , PreparedExactProposition , preparedExactPropositionCore , prepareExactProposition + , prepareExactSymbolicBoundConstraints + , prepareExactSymbolicWitnessConstraints + , prepareExactNounWitnessConstraints , PreparedExactSetExpression , preparedExactSetExpressionCore , prepareExactSetExpression @@ -95,7 +99,7 @@ exactLocalIdValue (ExactLocalId value) = value data ExactBinder = ExactBinder !ExactLocalId - !Raw.VarSymbol + !(Maybe Raw.VarSymbol) !CoreType !(Maybe ExactStructureAnnotation) @@ -123,14 +127,33 @@ extendExactBinderContext additions (ExactBinderContext initial) = | any (sameIdentity identity) binders = Left (ExactDuplicateLocalIdentity (locate variable) identity) | otherwise = - Right (ExactBinder identity variable TySet Nothing : binders) + Right (ExactBinder identity (Just variable) TySet Nothing : binders) sameVariable variable (ExactBinder _identity existing _coreType _structure) = - existing == variable + existing == Just variable sameIdentity identity (ExactBinder existing _variable _coreType _structure) = existing == identity +-- | Add one proof-owned binder which deliberately has no source-resolvable +-- spelling. This is used for a nameless singular witness; it participates in +-- checked support and de Bruijn weakening but cannot shadow or be looked up by +-- a later source variable. +extendExactAnonymousBinderContext + :: ExactLocalId + -> ExactBinderContext + -> Either ExactCompileError ExactBinderContext +extendExactAnonymousBinderContext identity (ExactBinderContext binders) + | any sameIdentity binders = + Left (ExactDuplicateLocalIdentity Nowhere identity) + | otherwise = + Right + (ExactBinderContext + (ExactBinder identity Nothing TySet Nothing : binders)) + where + sameIdentity (ExactBinder existing _variable _coreType _structure) = + existing == identity + exactBinderContextSupport :: ExactBinderContext -> Vector (ExactLocalId, CoreType) @@ -150,7 +173,7 @@ exactBinderContextIndex variable (ExactBinderContext binders) = go _index [] = Nothing go index (ExactBinder _identity candidate _coreType _structure : rest) - | candidate == variable = Just index + | candidate == Just variable = Just index | otherwise = go (index + 1) rest newtype PreparedExactProposition = PreparedExactProposition @@ -547,16 +570,88 @@ prepareExactProposition -> Declaration.LoweringDriver (Either ExactCompileError PreparedExactProposition) prepareExactProposition context statement = + prepareExactPropositionTerm + context + (locate statement) + (compileStatement statement) + +-- | Compile the source bound of already-opened symbolic binders. This is the +-- shared checked constraint seam used by quantified statements and proof +-- binders, so relation signs, carrier casts, and global occurrences are +-- elaborated exactly once by the ordinary expression compiler. +prepareExactSymbolicBoundConstraints + :: ExactBinderContext + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactSymbolicBoundConstraints context variables bound = + prepareExactPropositionTerm + context + (case bound of + Raw.Unbounded -> locate (NonEmpty.head variables) + _ -> locate bound) + (logicalConjunction + <$> compileSymbolicBoundConstraintList variables bound) + +-- | Compile the opened body used by a symbolic existential witness. Its +-- grouping is deliberately identical to 'SymbolicExists': all bound +-- constraints form the existential restriction and the stated proposition is +-- its body. +prepareExactSymbolicWitnessConstraints + :: ExactBinderContext + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Raw.Stmt + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactSymbolicWitnessConstraints context variables bound statement = + prepareExactPropositionTerm context (locate statement) do + constraints <- + logicalConjunction + <$> compileSymbolicBoundConstraintList variables bound + body <- compileStatement statement + pure + (if constraints == logicalTruth + then body + else logicalAnd constraints body) + +-- | Compile the checked constraint of an already-opened noun witness. Named +-- binders are resolved normally; a nameless singular noun uses the nearest +-- anonymous binder and therefore introduces no lookup spelling. +prepareExactNounWitnessConstraints + :: ExactBinderContext + -> Raw.NounPhrase [] + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactNounWitnessConstraints context nounPhrase = + case nounPhrase of + Raw.NounPhrase left noun variables right suchThat -> + prepareExactPropositionTerm context (locate noun) do + subjects <- + case NonEmpty.nonEmpty variables of + Just binders -> + toList + <$> traverse compileIntroducedVariable binders + Nothing -> + pure [CBound 0] + compileNounPhraseConstraints + subjects left noun right suchThat + +prepareExactPropositionTerm + :: ExactBinderContext + -> Location + -> Elaborate (CanonicalTerm ObjectId) + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactPropositionTerm context location compile = Except.runExceptT do let initialElaboration = initialElaborationState context (term, finalElaboration) <- - State.runStateT - (compileStatement statement) - initialElaboration + State.runStateT compile initialElaboration checked <- either - (Except.throwError - . ExactCoreCheckFailed (locate statement)) + (Except.throwError . ExactCoreCheckFailed location) pure (checkScopedCanonicalCore (`Map.lookup` elaborationGlobals finalElaboration) @@ -565,7 +660,7 @@ prepareExactProposition context statement = unless (scopedCoreType checked == TyProp) (Except.throwError (ExactFormulaExpectedProposition - (locate statement) + location (scopedCoreType checked))) pure (PreparedExactProposition checked) @@ -786,7 +881,7 @@ binderIndices :: ExactBinderContext -> Map.Map Raw.VarSymbol Natural binderIndices (ExactBinderContext binders) = Map.fromList [ (variable, fromIntegral index) - | (index, ExactBinder _identity variable _coreType _structure) <- + | (index, ExactBinder _identity (Just variable) _coreType _structure) <- zip [0 :: Int ..] binders ] @@ -849,18 +944,17 @@ compileHeaderAssumption = \case ] Raw.AsmLetIn variables domain -> do variableTerms <- traverse compileIntroducedVariable variables - domainTerm <- - compileExpressionAsSet domain - >>= structureCarrierCast (locate domain) - pure - [ ( locate variable - , CApp - (CApp (CIntrinsic Member) variableTerm) - domainTerm - ) - | (variable, variableTerm) <- - zip (toList variables) (toList variableTerms) - ] + domainTerm <- compileExpressionAsSet domain + traverse + (\(variable, variableTerm) -> do + proposition <- + compileMembership + (locate domain) + Raw.Positive + variableTerm + domainTerm + pure (locate variable, proposition)) + (zip (toList variables) (toList variableTerms)) Raw.AsmLetEq variable expression -> do variableTerm <- compileIntroducedVariable variable expressionTerm <- compileExpressionAsSet expression @@ -2130,6 +2224,22 @@ structureCarrierCast location term = pure (CApp (CGlobal carrier) term) _ -> pure term +compileMembership + :: Location + -> Raw.Sign + -> CanonicalTerm ObjectId + -> CanonicalTerm ObjectId + -> Elaborate (CanonicalTerm ObjectId) +compileMembership location sign element set = do + checkedSet <- structureCarrierCast location set + let proposition = + CApp + (CApp (CIntrinsic Member) element) + checkedSet + pure case sign of + Raw.Positive -> proposition + Raw.Negative -> logicalNot proposition + compileReplacement :: Raw.Expr -> NonEmpty (Raw.VarSymbol, Raw.Expr) @@ -2260,21 +2370,8 @@ compileSymbolicQuantified -> Elaborate (CanonicalTerm ObjectId) compileSymbolicQuantified quantifier variables bound suchThat compileBody = withSetBinders variables do - subjects <- traverse compileIntroducedVariable variables - boundConstraints <- case bound of - Raw.Unbounded -> - pure [] - Raw.Bounded _location sign relation domain -> do - domain' <- compileExpressionAsSet domain - traverse - (\subject -> do - proposition <- - compileAtomicRelationTerms - subject relation domain' - pure case sign of - Raw.Positive -> proposition - Raw.Negative -> logicalNot proposition) - (toList subjects) + boundConstraints <- + compileSymbolicBoundConstraintList variables bound suchThatConstraints <- maybeToList <$> traverse compileStatement suchThat body <- compileBody @@ -2286,6 +2383,25 @@ compileSymbolicQuantified quantifier variables bound suchThat compileBody = (boundConstraints <> suchThatConstraints)) body) +compileSymbolicBoundConstraintList + :: NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Elaborate [CanonicalTerm ObjectId] +compileSymbolicBoundConstraintList variables = \case + Raw.Unbounded -> + pure [] + Raw.Bounded _location sign relation domain -> do + subjects <- traverse compileIntroducedVariable variables + domain' <- compileExpressionAsSet domain + traverse + (\subject -> do + proposition <- + compileAtomicRelationTerms subject relation domain' + pure case sign of + Raw.Positive -> proposition + Raw.Negative -> logicalNot proposition) + (toList subjects) + compileAtomicRelationTerms :: CanonicalTerm ObjectId -> Raw.Relation @@ -2299,16 +2415,18 @@ compileAtomicRelationTerms left relation right = (Raw.relationSymbolToken symbol) (Raw.relationSymbolParameterArity symbol) compiledParameters <- traverse compileExpressionAsSet parameters - checkedRight <- - if symbol == Raw.ElementSymbol && null parameters - then structureCarrierCast location right - else pure right case fixedSemanticMeaning key of Just FixedEquality | null parameters -> pure (CEq TySet left right) Just FixedDisequality | null parameters -> pure (logicalNot (CEq TySet left right)) + Just (FixedIntrinsic Member) + | null parameters -> + compileMembership location Raw.Positive left right + Just (FixedNegatedIntrinsic Member) + | null parameters -> + compileMembership location Raw.Negative left right Just (FixedIntrinsic intrinsic) -> do (term, actual) <- applyTyped @@ -2316,7 +2434,7 @@ compileAtomicRelationTerms left relation right = (CIntrinsic intrinsic) (coreIntrinsicType intrinsic) ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, checkedRight])) + <$> (compiledParameters <> [left, right])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -2328,7 +2446,7 @@ compileAtomicRelationTerms left relation right = (CIntrinsic intrinsic) (coreIntrinsicType intrinsic) ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, checkedRight])) + <$> (compiledParameters <> [left, right])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -2338,7 +2456,7 @@ compileAtomicRelationTerms left relation right = applyResolvedTyped location key ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, checkedRight])) + <$> (compiledParameters <> [left, right])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -2424,6 +2542,13 @@ compileNoun subject (Raw.Noun location item arguments) key = SemanticNoun (Raw.sg patterns) (Raw.pl patterns) compiled <- traverse compileTermAsSet arguments case fixedSemanticMeaning key of + Just (FixedIntrinsic Member) -> + case compiled of + [set] -> + compileMembership location Raw.Positive subject set + _ -> + impossible + "the fixed element noun does not have one argument" Just (FixedIntrinsic intrinsic) -> do (term, actual) <- applyTyped @@ -2770,6 +2895,18 @@ compileAtomicRelation left relation right = | otherwise -> Except.throwError (ExactUnsupportedDeclarationBody location) + Just (FixedIntrinsic Member) + | null parameters -> do + left' <- compileExpressionAsSet leftExpression + right' <- compileExpressionAsSet rightExpression + compileMembership + location Raw.Positive left' right' + Just (FixedNegatedIntrinsic Member) + | null parameters -> do + left' <- compileExpressionAsSet leftExpression + right' <- compileExpressionAsSet rightExpression + compileMembership + location Raw.Negative left' right' Just (FixedIntrinsic intrinsic) -> do compiled <- traverse compileExpression (parameters <> [leftExpression, rightExpression]) @@ -2827,10 +2964,7 @@ compileRelationExpression location expression left right = do (SemanticExpressionFunction (Raw.mixfixPattern Raw.PairSymbol)) [left, right] - pure - (CApp - (CApp (CIntrinsic Member) pair) - relation) + compileMembership location Raw.Positive pair relation compileRelationChain :: Raw.Chain @@ -2884,14 +3018,8 @@ applyResolvedPredicate -> SemanticGlobalKey -> [CanonicalTerm ObjectId] -> Elaborate (CanonicalTerm ObjectId) -applyResolvedPredicate location key arguments = do - (term, actual) <- - applyResolvedTyped - location key ((\argument -> (argument, TySet)) <$> arguments) - unless (actual == TyProp) - (Except.throwError - (ExactFormulaExpectedProposition location actual)) - pure term +applyResolvedPredicate location key = + applyResolvedPredicateChoice location (key :| []) applyResolvedPredicateChoice :: Location @@ -2899,28 +3027,41 @@ applyResolvedPredicateChoice -> [CanonicalTerm ObjectId] -> Elaborate (CanonicalTerm ObjectId) applyResolvedPredicateChoice location keys arguments = do - visible <- for (toList keys) \key -> do - found <- - State.lift - (Except.lift - (Declaration.resolveVisibleGlobalLowering key)) - pure ((\target -> (key, target)) <$> found) - case catMaybes visible of - [(key, _target)] -> do - (term, actual) <- - applyResolvedTyped - location key - ((\argument -> (argument, TySet)) <$> arguments) - unless (actual == TyProp) - (Except.throwError - (ExactFormulaExpectedProposition location actual)) - pure term - [] -> - Except.throwError - (ExactGlobalNotVisible location (NonEmpty.head keys)) - _ -> - impossible - "one adjective surface resolves to several exact globals" + case firstFixedMeaning (toList keys) of + Just meaning -> + maybe + (impossible + "a fixed equality predicate has an invalid source arity") + pure + (lowerFixedEqualityPredicate meaning arguments) + Nothing -> do + visible <- for (toList keys) \key -> do + found <- + State.lift + (Except.lift + (Declaration.resolveVisibleGlobalLowering key)) + pure ((\target -> (key, target)) <$> found) + case catMaybes visible of + [(key, _target)] -> do + (term, actual) <- + applyResolvedTyped + location key + ((\argument -> (argument, TySet)) <$> arguments) + unless (actual == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition location actual)) + pure term + [] -> + Except.throwError + (ExactGlobalNotVisible location (NonEmpty.head keys)) + _ -> + impossible + "one adjective surface resolves to several exact globals" + where + firstFixedMeaning = + foldr + (\key found -> fixedSemanticMeaning key <|> found) + Nothing applyResolvedTyped :: Location diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs index 40911b0..f3f3b9d 100644 --- a/source/Checking/Exact/Proof.hs +++ b/source/Checking/Exact/Proof.hs @@ -56,8 +56,6 @@ import Numeric.Natural (Natural) data ExactProofError = ExactProofUnsupportedClaim !Location | ExactProofUnsupportedStep !Location - | ExactProofBoundedFixNotSupported !Location - | ExactProofBoundedTakeNotSupported !Location | ExactProofSetInductionVariableRequired !Location | ExactProofSetInductionVariableNotActive !Location !Raw.VarSymbol @@ -86,8 +84,6 @@ exactProofErrorLocation :: ExactProofError -> Location exactProofErrorLocation = \case ExactProofUnsupportedClaim location -> location ExactProofUnsupportedStep location -> location - ExactProofBoundedFixNotSupported location -> location - ExactProofBoundedTakeNotSupported location -> location ExactProofSetInductionVariableRequired location -> location ExactProofSetInductionVariableNotActive location _variable -> location @@ -115,10 +111,6 @@ renderExactProofError = \case at location <> "this claim is not yet supported by the typed checker" ExactProofUnsupportedStep location -> at location <> "this proof step is not yet supported by the typed checker" - ExactProofBoundedFixNotSupported location -> - at location <> "bounded proof binders are not yet supported" - ExactProofBoundedTakeNotSupported location -> - at location <> "bounded proof witnesses are not yet supported" ExactProofSetInductionVariableRequired location -> at location <> "exact set induction requires a named set variable" ExactProofSetInductionVariableNotActive location variable -> @@ -485,34 +477,47 @@ prepareProof fallback context locals inductionAntecedents goal = \case goal justification Raw.FixSymbolic location variables bound continuation -> do - unless (bound == Raw.Unbounded) - (throwProof - (ExactProofBoundedFixNotSupported location)) (context', goal', identities) <- openFixedVariables context goal variables - PreparedFix identities - <$> prepareProof - fallback - context' - locals - Nothing - goal' - continuation + case bound of + Raw.Unbounded -> + PreparedFix identities + <$> prepareProof + fallback + context' + locals + Nothing + goal' + continuation + _ -> do + constraint <- + prepareSymbolicBoundConstraints + context' variables bound + prepareGuardedFix + fallback location context' locals goal' + identities constraint continuation + Raw.FixSuchThat location variables statement continuation -> do + (context', goal', identities) <- + openFixedVariables context goal variables + constraint <- + Exact.preparedExactPropositionCore + <$> prepareStatement context' statement + prepareGuardedFix + fallback location context' locals goal' + identities constraint continuation Raw.Assume location statement continuation -> do - (antecedent, conclusion) <- + supplied <- prepareStatement context statement + when (isNothing (openScopedImplication goal)) + (throwProof (ExactProofExpectedImplicationGoal location)) + (assumption, conclusion) <- maybe - (throwProof - (ExactProofExpectedImplicationGoal location)) + (throwProof (ExactProofGoalStatementMismatch location)) pure - (openScopedImplication goal) - supplied <- prepareStatement context statement - unless - (Exact.preparedExactPropositionCore supplied - == antecedent) - (throwProof - (ExactProofGoalStatementMismatch location)) - local <- allocateLocal ExactAssumption context antecedent - PreparedAssume antecedent + (openScopedAssumption + (Exact.preparedExactPropositionCore supplied) + goal) + local <- allocateLocal ExactAssumption context assumption + PreparedAssume assumption <$> prepareProof fallback context @@ -521,36 +526,13 @@ prepareProof fallback context locals inductionAntecedents goal = \case conclusion continuation Raw.TakeVar location variables bound statement justification continuation -> do - unless (bound == Raw.Unbounded) - (throwProof - (ExactProofBoundedTakeNotSupported location)) - identities <- - traverse (const allocateLocalIdentity) variables - context' <- - either - (throwProof . ExactProofElaborationFailed) - pure - (Exact.extendExactBinderContext - (NonEmpty.zip identities variables) - context) - witness <- - Exact.preparedExactPropositionCore - <$> prepareStatement context' statement - let witnessCount = length (toList variables) - existence = closeTakenWitnesses witnessCount witness - goal' = weakenForTakenWitnesses witnessCount goal - discharge <- - prepareDischarge - location context locals existence justification - local <- allocateLocal ExactAssumption context' witness - PreparedTake (toList identities) witness discharge - <$> prepareProof - fallback - context' - (locals <> [local]) - Nothing - goal' - continuation + prepareSymbolicTake + fallback location context locals goal variables bound statement + justification continuation + Raw.TakeNoun location nounPhrase justification continuation -> + prepareNounTake + fallback location context locals goal nounPhrase + justification continuation Raw.BySetInduction location variable continuation -> case (inductionAntecedents, continuation) of (Nothing, _proof) -> @@ -593,6 +575,12 @@ prepareProof fallback context locals inductionAntecedents goal = \case justification (Just _antecedents, _proof) -> throwProof (ExactProofUnsupportedStep location) + Raw.Have location Nothing + (Raw.SymbolicExists _existential variables bound statement) + justification continuation -> + prepareSymbolicTake + fallback location context locals goal variables bound statement + justification continuation Raw.Have location since statement justification continuation -> do when (isJust since) (throwProof (ExactProofUnsupportedStep location)) @@ -756,6 +744,168 @@ prepareProof fallback context locals inductionAntecedents goal = \case (impossible "an exact claim antecedent changed context") (implyScopedCore antecedent conclusion) +prepareGuardedFix + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> [Exact.ExactLocalId] + -> ScopedCheckedCore ObjectId + -> Raw.Proof + -> Prepare PreparedProof +prepareGuardedFix + fallback location context locals goal identities constraint continuation = do + (antecedent, conclusion) <- + maybe + (throwProof (ExactProofExpectedImplicationGoal location)) + pure + (openScopedImplication goal) + unless (constraint == antecedent) + (throwProof (ExactProofGoalStatementMismatch location)) + local <- allocateLocal ExactAssumption context constraint + prepared <- + prepareProof + fallback + context + (locals <> [local]) + Nothing + conclusion + continuation + pure (PreparedFix identities (PreparedAssume constraint prepared)) + +prepareSymbolicBoundConstraints + :: Exact.ExactBinderContext + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Prepare (ScopedCheckedCore ObjectId) +prepareSymbolicBoundConstraints context variables bound = + Exact.preparedExactPropositionCore + <$> ( liftDriver + (Exact.prepareExactSymbolicBoundConstraints + context variables bound) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + +prepareSymbolicTake + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Raw.Stmt + -> Raw.Justification + -> Raw.Proof + -> Prepare PreparedProof +prepareSymbolicTake + fallback location context locals goal variables bound statement + justification continuation = do + identities <- traverse (const allocateLocalIdentity) variables + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + (NonEmpty.zip identities variables) + context) + witness <- + Exact.preparedExactPropositionCore + <$> ( liftDriver + (Exact.prepareExactSymbolicWitnessConstraints + context' variables bound statement) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + prepareTake + fallback location context locals goal context' + (toList identities) witness justification continuation + +prepareNounTake + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> Raw.NounPhrase [] + -> Raw.Justification + -> Raw.Proof + -> Prepare PreparedProof +prepareNounTake + fallback location context locals goal nounPhrase + justification continuation = do + (identities, context') <- + case nounPhrase of + Raw.NounPhrase _left _noun variables _right _suchThat -> + case NonEmpty.nonEmpty variables of + Just binders -> do + identities <- + traverse (const allocateLocalIdentity) binders + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + (NonEmpty.zip identities binders) + context) + pure (toList identities, context') + Nothing -> do + identity <- allocateLocalIdentity + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactAnonymousBinderContext + identity context) + pure ([identity], context') + witness <- + Exact.preparedExactPropositionCore + <$> ( liftDriver + (Exact.prepareExactNounWitnessConstraints + context' nounPhrase) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + prepareTake + fallback location context locals goal context' + identities witness justification continuation + +prepareTake + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> Exact.ExactBinderContext + -> [Exact.ExactLocalId] + -> ScopedCheckedCore ObjectId + -> Raw.Justification + -> Raw.Proof + -> Prepare PreparedProof +prepareTake + fallback location context locals goal witnessContext + identities witness justification continuation = do + let witnessCount = length identities + existence = closeTakenWitnesses witnessCount witness + goal' = weakenForTakenWitnesses witnessCount goal + discharge <- + prepareDischarge + location context locals existence justification + local <- allocateLocal ExactAssumption witnessContext witness + PreparedTake identities witness discharge + <$> prepareProof + fallback + witnessContext + (locals <> [local]) + Nothing + goal' + continuation + -- The discharged existential and the opened witness premise are the same -- checked proposition viewed on opposite sides of existential elimination. closeTakenWitnesses diff --git a/source/Checking/Exact/Vocabulary.hs b/source/Checking/Exact/Vocabulary.hs index 5701f64..b1310f2 100644 --- a/source/Checking/Exact/Vocabulary.hs +++ b/source/Checking/Exact/Vocabulary.hs @@ -5,6 +5,7 @@ module Checking.Exact.Vocabulary ( FixedSemanticMeaning(..) , fixedSemanticMeaning + , lowerFixedEqualityPredicate , ExactSymbolClass(..) , classifyExactSymbol , FixedSetTermDispatch(..) @@ -43,6 +44,14 @@ fixedSemanticVocabulary = [ ( relationKey Raw.EqSymbol , FixedEquality ) + , ( SemanticRightAdjective + (Raw.lexicalItemPattern + Lexicon.builtinEqualityRightAdjective) + , FixedEquality + ) + , ( verbKey Lexicon.builtinEqualityVerb + , FixedEquality + ) , ( relationKey Raw.ElementSymbol , FixedIntrinsic Member ) @@ -80,8 +89,27 @@ fixedSemanticVocabulary = nounKey item = let patterns = Raw.lexicalItemSgPlPattern item in SemanticNoun (Raw.sg patterns) (Raw.pl patterns) + verbKey item = + let patterns = Raw.lexicalItemSgPlPattern item + in SemanticVerb (Raw.sg patterns) (Raw.pl patterns) expressionKey = SemanticExpressionFunction +-- | Lower the fixed proposition meanings shared by raw exact elaboration and +-- the reusable internal-formula path. Membership deliberately retains its +-- carrier-aware source lowering and is not handled here. +lowerFixedEqualityPredicate + :: FixedSemanticMeaning + -> [CanonicalTerm global] + -> Maybe (CanonicalTerm global) +lowerFixedEqualityPredicate meaning arguments = + case (meaning, arguments) of + (FixedEquality, [left, right]) -> + Just (CEq TySet left right) + (FixedDisequality, [left, right]) -> + Just (CImp (CEq TySet left right) CFalsum) + _ -> + Nothing + unaryCommandPattern :: Text -> Raw.Pattern unaryCommandPattern command = Raw.TokenCons (Raw.Command command) diff --git a/source/Checking/Typed/Inductive.hs b/source/Checking/Typed/Inductive.hs index 7a895c6..02e68ea 100644 --- a/source/Checking/Typed/Inductive.hs +++ b/source/Checking/Typed/Inductive.hs @@ -3708,7 +3708,7 @@ lowerFormulaWith allowQuantified resolveGlobal environment = \case <*> lowerFormulaWith allowQuantified resolveGlobal environment right Atomic _location predicate arguments -> - lowerApplication + lowerPredicateApplication resolveGlobal environment (SymbolPredicate predicate) @@ -3783,6 +3783,40 @@ lowerApplication resolveGlobal environment symbol arguments = do resolveGlobal environment) arguments + lowerApplicationTerms resolveGlobal symbol arguments' + +lowerPredicateApplication + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> InductiveEnvironment + -> Symbol + -> [Expr] + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +lowerPredicateApplication resolveGlobal environment symbol arguments = do + arguments' <- + traverse + (lowerTerm + resolveGlobal + environment) + arguments + case classifyExactSymbol symbol of + ExactFixedPrimitive meaning -> + maybe + (lowerApplicationTerms resolveGlobal symbol arguments') + Right + (lowerFixedEqualityPredicate meaning arguments') + _ -> + lowerApplicationTerms resolveGlobal symbol arguments' + +lowerApplicationTerms + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> Symbol + -> [CanonicalTerm (InductiveGlobal global)] + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +lowerApplicationTerms resolveGlobal symbol arguments' = case dispatchFixedSetTerm symbol arguments' of LoweredFixedSetTerm term -> pure term diff --git a/source/Felix/Cache/Codec.hs b/source/Felix/Cache/Codec.hs index 2d81e57..d684b11 100644 --- a/source/Felix/Cache/Codec.hs +++ b/source/Felix/Cache/Codec.hs @@ -75,7 +75,7 @@ newtype CacheEpoch = CacheEpoch Word32 currentCacheEpoch :: CacheEpoch currentCacheEpoch = - CacheEpoch 23 + CacheEpoch 27 cacheEpochValue :: CacheEpoch -> Word32 cacheEpochValue (CacheEpoch value) = diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs index 7ee44ae..61fdac4 100644 --- a/source/Syntax/Lexicon.hs +++ b/source/Syntax/Lexicon.hs @@ -179,14 +179,22 @@ binOp' tok assoc = ([Nothing, Just tok, Nothing], assoc) builtinAdjRs :: [LexicalItem] builtinAdjRs = - [ mkLexicalItem (unsafeReadPhrase "equal to ?") "eq" + [ builtinEqualityRightAdjective ] +builtinEqualityRightAdjective :: LexicalItem +builtinEqualityRightAdjective = + mkLexicalItem (unsafeReadPhrase "equal to ?") "eq" + builtinVerbs :: [LexicalItemSgPl] builtinVerbs = - [ mkLexicalItemSgPl (unsafeReadPhraseSgPl "equal[s/] ?") "eq" + [ builtinEqualityVerb ] +builtinEqualityVerb :: LexicalItemSgPl +builtinEqualityVerb = + mkLexicalItemSgPl (unsafeReadPhraseSgPl "equal[s/] ?") "eq" + -- Some of these do/should correspond to mathlib structures, -- e.g.: lattice, complete lattice, ring, etc. diff --git a/source/Test/Unit/Backend.hs b/source/Test/Unit/Backend.hs index 11c36b8..81a911a 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,7 @@ routesCompleteProblems = do claim [higherOrderLocal, firstOrderLocal] [] - ImplicitFofPremises - FirstOrderLocals + ImplicitPremiseSelection assertEqual "implicit route" RouteFof (typedProblemRoute implicit) assertEqual "implicit FOF globals" [0] @@ -188,8 +190,7 @@ routesCompleteProblems = do claim [firstOrderLocal] [] - ExplicitGlobalPremises - FirstOrderLocals + ExplicitGlobalPremiseSelection assertEqual "explicit FOF route" RouteFof (typedProblemRoute explicitFof) @@ -199,8 +200,7 @@ routesCompleteProblems = do claim [firstOrderLocal] [] - ExplicitGlobalPremises - FirstOrderLocals + ExplicitGlobalPremiseSelection assertEqual "explicit TH0 route" RouteTh0 (typedProblemRoute explicitTh0) @@ -210,8 +210,7 @@ routesCompleteProblems = do claim [higherOrderLocal, firstOrderLocal] [] - NoGlobalPremises - AllLocals + LocalOnlyPremiseSelection assertEqual "local-only TH0 route" RouteTh0 (typedProblemRoute localOnly) assertEqual "local order restored" [0, 1] @@ -235,8 +234,7 @@ routesCompleteProblems = do claim [firstOrderLocal, firstOrderLocal] [] - NoGlobalPremises - AllLocals of + LocalOnlyPremiseSelection of Left (TypedProblemDuplicateLocalPremiseOrdinal duplicateOrdinal) -> @@ -260,8 +258,7 @@ routesCompleteProblems = do higherOrderClaimProposition [] [] - ImplicitFofPremises - FirstOrderLocals of + ImplicitPremiseSelection of Left TypedProblemExplicitHigherOrderJustificationRequired{} -> pure () @@ -282,8 +279,7 @@ routesCompleteProblems = do [typedFoundationAuxiliaryInput checkedFoundationValue Foundation.SeparationCharacteristic] - ImplicitFofPremises - FirstOrderLocals of + ImplicitPremiseSelection of Left TypedProblemExplicitHigherOrderJustificationRequired{} -> pure () @@ -314,8 +310,7 @@ routesCompleteProblems = do assertFailure "unused ambient local entered exact support" where - planned selectedFacts claim locals auxiliaries - globalPolicy localPolicy = + planned selectedFacts claim locals auxiliaries selection = either (assertFailure . show) pure @@ -325,8 +320,7 @@ routesCompleteProblems = do claim locals auxiliaries - globalPolicy - localPolicy) + selection) showProblemResult = \case Left err -> @@ -334,6 +328,184 @@ 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) + ImplicitPremiseSelection + + 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 + localProblem <- + either + (assertFailure . show) + pure + (plan + Vector.empty + firstOrderProposition + [unrelatedLocal, separationLocal, firstOrderLocal] + [Foundation.SeparationCharacteristic]) + assertEqual "construction local promotes the complete problem" RouteTh0 + (typedProblemRoute localProblem) + assertEqual "unrelated higher-order local remains unselected" + [0, 2] + ( 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 +527,12 @@ rendersCheckedProblems = do planned (Vector.singleton fofFact) claim - ImplicitFofPremises - FirstOrderLocals + ImplicitPremiseSelection th0Problem <- planned (Vector.singleton th0Fact) claim - ExplicitGlobalPremises - FirstOrderLocals + ExplicitGlobalPremiseSelection preparedFof <- either (assertFailure . show) @@ -430,7 +600,7 @@ rendersCheckedProblems = do then Tptp.isProperVariable target else Tptp.isProperAtomicWord target) where - planned selectedFacts claim globalPolicy localPolicy = + planned selectedFacts claim selection = either (assertFailure . show) pure @@ -440,8 +610,7 @@ rendersCheckedProblems = do claim [] [] - globalPolicy - localPolicy) + selection) firstOrderClaim :: CanonicalTerm TestGlobal firstOrderClaim = diff --git a/source/Test/Unit/Declaration.hs b/source/Test/Unit/Declaration.hs index 26261f3..0823606 100644 --- a/source/Test/Unit/Declaration.hs +++ b/source/Test/Unit/Declaration.hs @@ -12,6 +12,7 @@ import Checking.Exact qualified as Exact import Checking.Identity qualified as Identity import Checking.Kernel.Derivation qualified as Kernel import Checking.Semantic qualified as Semantic +import Checking.Typed.Inductive qualified as Typed import Felix.Math.Codec import Felix.Module import Felix.Source @@ -20,10 +21,12 @@ import Provers qualified import Report.Location import Syntax.Abstract qualified as Raw import Syntax.Interface qualified as Syntax +import Syntax.Internal qualified as Internal import Syntax.Lexicon qualified as Lexicon import Data.List.NonEmpty qualified as NonEmpty import Data.IORef qualified as IORef +import Data.Set qualified as Set import Data.Text qualified as Text import Data.Text.Encoding qualified as TextEncoding import Data.Vector qualified as Vector @@ -62,6 +65,8 @@ unitTests = reconstructsImportedGlobalBindings , testCase "elaborates scoped exact propositions" elaboratesScopedExactPropositions + , testCase "lowers fixed equality aliases without global support" + lowersFixedEqualityAliases , testCase "prepares exact claim envelopes" preparesExactClaimEnvelopes , testCase "lowers exact separation comprehensions" @@ -1166,8 +1171,7 @@ makePreparedObligationWithPremise fixture fingerprint = do claim [] [] - Backend.ExplicitGlobalPremises - Backend.FirstOrderLocals) + Backend.ExplicitGlobalPremiseSelection) expectRight (Provers.prepareTypedProverTask Provers.DirectTask @@ -1199,8 +1203,7 @@ makePreparedObligation fixture tag = do [Backend.typedFoundationAuxiliaryInput (fixtureFoundation fixture) tag] - Backend.NoGlobalPremises - Backend.AllLocals) + Backend.LocalOnlyPremiseSelection) expectRight (Provers.prepareTypedProverTask Provers.DirectTask @@ -1887,6 +1890,197 @@ elaboratesScopedExactPropositions = do Declaration.DriverSealFailed failure _prefix -> assertFailure ("scoped exact driver did not seal: " <> show failure) +lowersFixedEqualityAliases :: Assertion +lowersFixedEqualityAliases = do + fixture <- makeNamedFixture "fixed-equality-aliases" + let x = Raw.NamedVar "x" + y = Raw.NamedVar "y" + z = Raw.NamedVar "z" + term variable = Raw.TermExpr (Raw.ExprVar variable) + equality left right = + Raw.StmtFormula + (Raw.FormulaChain + (Raw.ChainBase + (Raw.ExprVar left :| []) + Raw.Positive + (Raw.Relation Nowhere Raw.EqSymbol []) + (Raw.ExprVar right :| []))) + quantified variables statement = + Raw.SymbolicQuantified + Nowhere + Raw.Universally + variables + Raw.Unbounded + Nothing + statement + adjective = + Raw.Adj + Nowhere + Lexicon.builtinEqualityRightAdjective + [term y] + copular = + Raw.StmtVerbPhrase + (term x :| []) + (Raw.VPAdj (adjective :| [])) + rightAttribute = + Raw.StmtNoun + (term x :| []) + (Raw.NounPhrase + [] + (Raw.Noun Nowhere Lexicon.builtinSetNoun []) + Nothing + [ Raw.AdjR + Nowhere + Lexicon.builtinEqualityRightAdjective + [term y] + ] + Nothing) + rightAttributeExpected = + Raw.StmtNoun + (term x :| []) + (Raw.NounPhrase + [] + (Raw.Noun Nowhere Lexicon.builtinSetNoun []) + Nothing + [] + (Just (equality x y))) + verb argument = + Raw.Verb + Nowhere + Lexicon.builtinEqualityVerb + [term argument] + singular = + Raw.StmtVerbPhrase + (term x :| []) + (Raw.VPVerb (verb y)) + negated = + Raw.StmtVerbPhrase + (term x :| []) + (Raw.VPVerbNot (verb y)) + coordinated = + Raw.StmtVerbPhrase + (term x :| [term y]) + (Raw.VPVerb (verb z)) + coordinatedExpected = + Raw.StmtConnected + Raw.Conjunction + Nothing + (equality x z) + (equality y z) + comparisons = + [ ( "copular adjective" + , quantified (x :| [y]) copular + , quantified (x :| [y]) (equality x y) + ) + , ( "right adjective" + , quantified (x :| [y]) rightAttribute + , quantified (x :| [y]) rightAttributeExpected + ) + , ( "singular verb" + , quantified (x :| [y]) singular + , quantified (x :| [y]) (equality x y) + ) + , ( "negated verb" + , quantified (x :| [y]) negated + , quantified + (x :| [y]) + (Raw.StmtNeg Nowhere (equality x y)) + ) + , ( "quantified coordinated verb" + , quantified (x :| [y, z]) coordinated + , quantified (x :| [y, z]) coordinatedExpected + ) + ] + action + :: Declaration.ModuleDriver Text + [ ( Either + Exact.ExactCompileError + Exact.PreparedExactProposition + , Either + Exact.ExactCompileError + Exact.PreparedExactProposition + ) + ] + action = + Declaration.runProspectiveLoweringDriver + (traverse + (\(_label, alias, symbolic) -> + (,) + <$> Exact.prepareExactProposition + Exact.emptyExactBinderContext alias + <*> Exact.prepareExactProposition + Exact.emptyExactBinderContext symbolic) + comparisons) + runDriver fixture action >>= \case + Declaration.DriverSucceeded results _interface _prefix _closure -> + for_ (zip comparisons results) \((label, _alias, _symbolic), result) -> + case result of + (Right alias, Right symbolic) -> do + let aliasTerm = + Core.scopedCoreTerm + (Exact.preparedExactPropositionCore alias) + symbolicTerm = + Core.scopedCoreTerm + (Exact.preparedExactPropositionCore symbolic) + assertEqual + (label <> " checked core") + symbolicTerm + aliasTerm + assertEqual + (label <> " global support") + Set.empty + (Core.canonicalTermGlobals aliasTerm) + assertEqual + (label <> " foundation support") + Set.empty + (Foundation.foundationAxiomDependencies aliasTerm) + (Left failure, _) -> + assertFailure + (label <> " alias failed: " + <> Text.unpack + (Exact.renderExactCompileError failure)) + (_, Left failure) -> + assertFailure + (label <> " symbolic comparison failed: " + <> Text.unpack + (Exact.renderExactCompileError failure)) + Declaration.DriverFailed failure _prefix -> + assertFailure ("fixed equality driver failed: " <> show failure) + Declaration.DriverSealFailed failure _prefix -> + assertFailure ("fixed equality driver did not seal: " <> show failure) + + let internalEquality = + Internal.FormulaVerb + Nowhere + (Internal.EmptySet Nowhere) + Lexicon.builtinEqualityVerb + [Internal.EmptySet Nowhere] + internalResult + :: Either + Typed.TypedInductiveError + (Core.FrozenCheckedCore Void) + internalResult = + Typed.prepareTypedClosedFormula + absurd + (const Nothing) + internalEquality + case internalResult of + Right checked -> do + assertEqual + "internal fixed verb core" + (Core.CEq + Core.TySet + (Core.CIntrinsic Core.Empty) + (Core.CIntrinsic Core.Empty)) + (Core.frozenCoreTerm checked) + assertEqual + "internal fixed verb global support" + Set.empty + (Core.frozenCoreGlobals checked) + Left failure -> + assertFailure + ("internal fixed verb failed: " <> show failure) + preparesExactClaimEnvelopes :: Assertion preparesExactClaimEnvelopes = do fixture <- makeNamedFixture "exact-claim-envelope" diff --git a/source/Test/Unit/Module.hs b/source/Test/Unit/Module.hs index 267a9ad..7748dac 100644 --- a/source/Test/Unit/Module.hs +++ b/source/Test/Unit/Module.hs @@ -67,6 +67,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 @@ -122,6 +123,8 @@ unitTests = confinesExactQuantifiedTerms , testCase "compiles exact ordinary proofs" compilesExactOrdinaryProofs + , testCase "restores exact binder and witness proof forms" + restoresExactBinderAndWitnessProofForms , testCase "compiles and reuses proof-local set definitions" compilesAndReusesProofLocalSetDefinitions , testCase "compiles and reuses proof-local function graphs" @@ -1324,6 +1327,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" @@ -2084,6 +2110,363 @@ 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)] + } + +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 +2495,27 @@ compilesExactSeparationComprehensions = let resolver = Declaration.vampireResolver \prepared -> do let problem = Provers.preparedTypedProverLogicalProblem prepared + request = + Provers.preparedTypedProverRequest prepared + globalsAreFof = + all + (\fact -> + case Backend.typedBackendFactCapability fact of + Backend.FofProjectable{} -> True + Backend.RequiresTh0{} -> False) + (Backend.typedProblemGlobalPremises problem) modifyIORef' observations (<> [ ( Backend.typedProblemRoute problem + , globalsAreFof + , 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 +2529,20 @@ 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 + readIORef observations >>= \case + [ ( Backend.RouteTh0 + , True + , [0] + , [Foundation.SeparationCharacteristic] + , _requestId + , requestBytes + ) ] -> + 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 @@ -2712,6 +3119,13 @@ 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) @@ -3821,19 +4235,40 @@ 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 + 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 +4297,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 +4331,28 @@ reusesExactSeparationValidation = assertEqual "warm separation checked artifacts" (components fresh) (components warm) + 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 = diff --git a/source/Test/Unit/Provers.hs b/source/Test/Unit/Provers.hs index d5173e1..ad6bf4f 100644 --- a/source/Test/Unit/Provers.hs +++ b/source/Test/Unit/Provers.hs @@ -1053,8 +1053,7 @@ preparedTypedTask factCount = do proposition [] [] - ExplicitGlobalPremises - FirstOrderLocals) + ExplicitGlobalPremiseSelection) expectRight (prepareTypedProverTask DirectTask problem) where propositionTerm = diff --git a/test/phase5/exact-proof-parity-invalid-assume.tex b/test/phase5/exact-proof-parity-invalid-assume.tex new file mode 100644 index 0000000..3bb04bc --- /dev/null +++ b/test/phase5/exact-proof-parity-invalid-assume.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{invalid_disjunct_assume} + Let $A,B$ be sets. + $A=A$ or $B=B$. +\end{proposition} +\begin{proof} + Assume $A=A$. + Follows. +\end{proof} diff --git a/test/phase5/exact-proof-parity-invalid-fix-shape.tex b/test/phase5/exact-proof-parity-invalid-fix-shape.tex new file mode 100644 index 0000000..16a58a2 --- /dev/null +++ b/test/phase5/exact-proof-parity-invalid-fix-shape.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{invalid_fix_shape} + Let $A$ be a set. + $A=A$. +\end{proposition} +\begin{proof} + Fix $x\in A$. + Follows. +\end{proof} diff --git a/test/phase5/exact-proof-parity-invalid-fix.tex b/test/phase5/exact-proof-parity-invalid-fix.tex new file mode 100644 index 0000000..0a2b24c --- /dev/null +++ b/test/phase5/exact-proof-parity-invalid-fix.tex @@ -0,0 +1,8 @@ +\begin{proposition}\label{invalid_bounded_fix} + Let $A$ be a set. + For all $x\in A$ we have $x\in A$. +\end{proposition} +\begin{proof} + Fix $x\notin A$. + Follows. +\end{proof} diff --git a/test/phase5/exact-proof-parity.tex b/test/phase5/exact-proof-parity.tex new file mode 100644 index 0000000..73d849f --- /dev/null +++ b/test/phase5/exact-proof-parity.tex @@ -0,0 +1,107 @@ +\begin{proposition}\label{bounded_fix_single} + Let $A$ be a set. + For all $x\in A$ we have $x\in A$. +\end{proposition} +\begin{proof} + Fix $x\in A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{bounded_fix_multiple} + Let $A$ be a set. + For all $x,y\in A$ we have $x\in A$ and $y\in A$. +\end{proposition} +\begin{proof} + Fix $x,y\in A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{bounded_fix_negative} + Let $A$ be a set. + For all $x\notin A$ we have $x\notin A$. +\end{proposition} +\begin{proof} + Fix $x\notin A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{fix_such_that} + Let $A$ be a set. + For all $x$ such that $x\in A$ we have $x\in A$. +\end{proposition} +\begin{proof} + Fix $x$ such that $x\in A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{assume_left_conjunct} + Let $A,B$ be sets. + If $A=A$ and $B=B$, then $A=A$. +\end{proposition} +\begin{proof} + Assume $A=A$. + Assume $B=B$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{assume_right_conjunct} + Let $A,B$ be sets. + If $A=A$ and $B=B$, then $B=B$. +\end{proposition} +\begin{proof} + Assume $B=B$. + Assume $A=A$. + Follows by assumption. +\end{proof} + +\begin{proposition}\label{take_bounded} + Let $A$ be a set. + Suppose there exists $x\in A$ such that $x=x$. + Then $A=A$. +\end{proposition} +\begin{proof} + Take $x\in A$ such that $x=x$ by assumption. + We have $x\in A$ by assumption. + Follows. +\end{proof} + +\begin{proposition}\label{take_named_noun} + Let $A$ be a set. + Suppose there exist sets $x,y$ such that $x=x$ and $y=y$. + Then $A=A$. +\end{proposition} +\begin{proof} + Take a set $x,y$ such that $x=x$ and $y=y$ by assumption. + Follows. +\end{proof} + +\begin{proposition}\label{take_anonymous_noun} + Let $A$ be a set. + Suppose there exists a set. + Then $A=A$. +\end{proposition} +\begin{proof} + Take a set by assumption. + Follows. +\end{proof} + +\begin{proposition}\label{existential_have_witness} + Let $A$ be a set. + Suppose there exists $x\in A$ such that $x=x$. + Then $A=A$. +\end{proposition} +\begin{proof} + We have there exists $x\in A$ such that $x=x$ by assumption. + We have $x\in A$ by assumption. + Follows. +\end{proof} + +\begin{proposition}\label{take_omitted_continuation} + Let $A$ be a set. + Suppose there exists $x\in A$ such that $x=x$. + Then $A=A$. +\end{proposition} +\begin{proof} + Take $x\in A$ such that $x=x$ by assumption. + Omitted. +\end{proof} diff --git a/test/phase5/exact-replacement.tex b/test/phase5/exact-replacement.tex index 901fabe..d23ba42 100644 --- a/test/phase5/exact-replacement.tex +++ b/test/phase5/exact-replacement.tex @@ -8,5 +8,4 @@ \begin{proof} Fix $A, x$. Assume $x \in A$. - Follows by assumption. \end{proof} diff --git a/test/phase5/exact-separation.tex b/test/phase5/exact-separation.tex index e5b23a6..82f4263 100644 --- a/test/phase5/exact-separation.tex +++ b/test/phase5/exact-separation.tex @@ -8,5 +8,4 @@ \begin{proof} Fix $A, x$. Assume $x \in \{ y \in A \mid y = y \}$. - Follows by assumption. \end{proof} diff --git a/test/phase5/exact-structure.tex b/test/phase5/exact-structure.tex index b1a0d86..fb34abe 100644 --- a/test/phase5/exact-structure.tex +++ b/test/phase5/exact-structure.tex @@ -25,3 +25,69 @@ \begin{proof} Follows by assumption. \end{proof} + +\begin{proposition}\label{pointed_self_member} + Let $X$ be a pointed set. + Then $X \in X$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_self_member_explicit} + Let $X$ be a pointed set. + Then $X \in \carrier[X]$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_self_not_member} + Let $X$ be a pointed set. + Then $X \notin X$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_self_not_member_explicit} + Let $X$ be a pointed set. + Then $X \notin \carrier[X]$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_self_element} + Let $X$ be a pointed set. + Then $X$ is an element of $X$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_self_element_explicit} + Let $X$ be a pointed set. + Then $X$ is an element of $\carrier[X]$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_header_member} + Let $X$ be a pointed set. + Let $x \in X$. + Then $x = x$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} + +\begin{proposition}\label{pointed_header_member_explicit} + Let $X$ be a pointed set. + Let $x \in \carrier[X]$. + Then $x = x$. +\end{proposition} +\begin{proof} + Follows. +\end{proof} |