diff options
Diffstat (limited to 'source/Checking/Exact/Proof.hs')
| -rw-r--r-- | source/Checking/Exact/Proof.hs | 1359 |
1 files changed, 0 insertions, 1359 deletions
diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs deleted file mode 100644 index 40911b0..0000000 --- a/source/Checking/Exact/Proof.hs +++ /dev/null @@ -1,1359 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Exact lowering for the first ordinary theorem/proof fragment. --- --- This module is the trusted owner of structural local-proof composition. Its --- private prepared tree controls when assumptions and proved local claims --- become available and executes discharges depth-first. The declaration --- boundary validates typed tasks and authority; it does not reconstruct this --- derivation. -module Checking.Exact.Proof - ( PreparedExactProof - , preparedExactProofSyntaxId - , preparedExactProofFirstOmission - , prepareExactProof - , CheckedExactProofAuthorization - , lowerPreparedExactProof - , authorizeCheckedExactProof - , PreparedFinalPreludeFoundationClaim - , prepareFinalPreludeFoundationClaim - , CheckedFinalPreludeFoundationAuthorization - , lowerPreparedFinalPreludeFoundationClaim - , authorizeCheckedFinalPreludeFoundationClaim - , ExactProofError(..) - , exactProofErrorLocation - , renderExactProofError - ) where - -import Base -import Checking.Authority qualified as Authority -import Checking.Backend.Problem qualified as Backend -import Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Exact qualified as Exact -import Checking.Foundation -import Checking.Identity -import Checking.Kernel.Derivation (foundationFactDerivation) -import Checking.Semantic -import Felix.Cache.Codec -import Report.Location -import Syntax.Abstract qualified as Raw - -import Control.Monad.Except (ExceptT) -import Control.Monad.Except qualified as Except -import Control.Monad (foldM, unless, when) -import Control.Monad.State.Strict (StateT) -import Control.Monad.State.Strict qualified as State -import Data.ByteString (ByteString) -import Data.List.NonEmpty qualified as NonEmpty -import Data.Set qualified as Set -import Data.Text qualified as Text -import Data.Vector (Vector) -import Numeric.Natural (Natural) - - -data ExactProofError - = ExactProofUnsupportedClaim !Location - | ExactProofUnsupportedStep !Location - | ExactProofBoundedFixNotSupported !Location - | ExactProofBoundedTakeNotSupported !Location - | ExactProofSetInductionVariableRequired !Location - | ExactProofSetInductionVariableNotActive - !Location !Raw.VarSymbol - | ExactProofSetInductionNotOutermost !Location - | ExactProofSetInductionGoalMismatch !Location - | ExactProofSetExtensionalityGoalMismatch !Location - | ExactProofSetExtensionalityDirectionsUnavailable !Location - | ExactProofExpectedUniversalGoal !Location - | ExactProofExpectedImplicationGoal !Location - | ExactProofGoalStatementMismatch !Location - | ExactProofContradictionGoalMismatch !Location - | ExactProofLocalFunctionBinderMismatch !Location - | ExactProofLocalFunctionNameConflict !Location - | ExactProofUnknownReference !Location !Raw.Marker - | ExactProofElaborationFailed !Exact.ExactCompileError - | ExactProofObligationPreparationFailed - !Location - !(Declaration.VampireObligationPreparationError - Exact.ExactLocalId) - | ExactProofFoundationLeafRequiresImplicitAuto !Location - | ExactProofFoundationLeafTargetMismatch !Location - | ExactProofFoundationLeafTargetAmbiguous !Location - deriving stock (Show, Eq) - -exactProofErrorLocation :: ExactProofError -> Location -exactProofErrorLocation = \case - ExactProofUnsupportedClaim location -> location - ExactProofUnsupportedStep location -> location - ExactProofBoundedFixNotSupported location -> location - ExactProofBoundedTakeNotSupported location -> location - ExactProofSetInductionVariableRequired location -> location - ExactProofSetInductionVariableNotActive location _variable -> - location - ExactProofSetInductionNotOutermost location -> location - ExactProofSetInductionGoalMismatch location -> location - ExactProofSetExtensionalityGoalMismatch location -> location - ExactProofSetExtensionalityDirectionsUnavailable location -> location - ExactProofExpectedUniversalGoal location -> location - ExactProofExpectedImplicationGoal location -> location - ExactProofGoalStatementMismatch location -> location - ExactProofContradictionGoalMismatch location -> location - ExactProofLocalFunctionBinderMismatch location -> location - ExactProofLocalFunctionNameConflict location -> location - ExactProofUnknownReference location _marker -> location - ExactProofElaborationFailed failure -> - Exact.exactCompileErrorLocation failure - ExactProofObligationPreparationFailed location _failure -> location - ExactProofFoundationLeafRequiresImplicitAuto location -> location - ExactProofFoundationLeafTargetMismatch location -> location - ExactProofFoundationLeafTargetAmbiguous location -> location - -renderExactProofError :: ExactProofError -> Text -renderExactProofError = \case - ExactProofUnsupportedClaim location -> - 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 -> - at location <> "the set-induction variable " <> shown variable - <> " is not an active exact binder" - ExactProofSetInductionNotOutermost location -> - at location <> "set induction must currently be outermost" - ExactProofSetInductionGoalMismatch location -> - at location <> "the set-induction variable does not belong to this goal" - ExactProofSetExtensionalityGoalMismatch location -> - at location <> "set extensionality requires a set-equality goal" - ExactProofSetExtensionalityDirectionsUnavailable location -> - at location - <> "set extensionality requires both directions as proved local claims" - ExactProofExpectedUniversalGoal location -> - at location <> "this fix step requires a universal goal" - ExactProofExpectedImplicationGoal location -> - at location <> "this assume step requires an implication goal" - ExactProofGoalStatementMismatch location -> - at location <> "the proof step does not match the current goal" - ExactProofContradictionGoalMismatch location -> - at location <> "contradiction requires falsum as the current goal" - ExactProofLocalFunctionBinderMismatch location -> - at location <> "the function argument must match its domain binder" - ExactProofLocalFunctionNameConflict location -> - at location <> "the function and argument names must be distinct" - ExactProofUnknownReference location marker -> - at location <> "the cited fact " <> shown marker <> " is not visible" - ExactProofElaborationFailed failure -> - Exact.renderExactCompileError failure - ExactProofObligationPreparationFailed location failure -> - at location <> "the exact proof obligation is invalid: " <> shown failure - ExactProofFoundationLeafRequiresImplicitAuto location -> - at location - <> "a confined foundation claim requires an implicit Auto proof" - ExactProofFoundationLeafTargetMismatch location -> - at location <> "the claim does not exactly match a foundation axiom" - ExactProofFoundationLeafTargetAmbiguous location -> - at location <> "the claim matches more than one foundation axiom" - where - at location = locationToText location <> ": " - shown :: Show value => value -> Text - shown = Text.pack . show - -data ExactLocalOrigin - = ExactAssumption - | ExactDerivedClaim - | ExactLocalDefinition - deriving stock (Show, Eq, Ord) - -data PreparedLocal = PreparedLocal - !Backend.LocalPremiseOrdinal - !ExactLocalOrigin - !(Vector (Exact.ExactLocalId, CoreType)) - !(ScopedCheckedCore ObjectId) - -data PreparedJustification - = PreparedAuto - | PreparedReferences - !(NonEmpty SemanticFactOccurrenceFingerprint) - | PreparedLocalOnly - -data PreparedDischarge - = PreparedVampireDischarge - !Location - !PreparedJustification - !(ScopedCheckedCore ObjectId) - !(Declaration.PreparedVampireObligation - Exact.ExactLocalId - ExactLocalOrigin) - | PreparedSetExtensionality - !Location - !(ScopedCheckedCore ObjectId) - -data PreparedProof - = PreparedImplicitAuto !PreparedDischarge - | PreparedQed !PreparedDischarge - | PreparedOmitted - !Location - !(ScopedCheckedCore ObjectId) - | PreparedFix ![Exact.ExactLocalId] !PreparedProof - | PreparedAssume - !(ScopedCheckedCore ObjectId) - !PreparedProof - | PreparedTake - ![Exact.ExactLocalId] - !(ScopedCheckedCore ObjectId) - !PreparedDischarge - !PreparedProof - | PreparedSetInduction - !(ScopedCheckedCore ObjectId) - !PreparedDischarge - | PreparedHave - !(ScopedCheckedCore ObjectId) - !PreparedDischarge - !PreparedProof - | PreparedSubclaim - !(ScopedCheckedCore ObjectId) - !PreparedProof - !PreparedProof - | PreparedDefine - !Exact.ExactLocalId - !(ScopedCheckedCore ObjectId) - !(ScopedCheckedCore ObjectId) - !PreparedProof - | PreparedDefineFunction - !Exact.ExactLocalId - !(ScopedCheckedCore ObjectId) - !(ScopedCheckedCore ObjectId) - !PreparedProof - | PreparedContradiction !PreparedDischarge - -data PreparedExactProof = PreparedExactProof - !Location - !SemanticName - !(ScopedCheckedCore ObjectId) - !PreparedProof - !ProofSyntaxId - -data PreparedFinalPreludeFoundationClaim = - PreparedFinalPreludeFoundationClaim - !Location - !SemanticName - !(ScopedCheckedCore ObjectId) - !FoundationAxiomTag - !ProofSyntaxId - -preparedExactProofSyntaxId :: PreparedExactProof -> ProofSyntaxId -preparedExactProofSyntaxId - (PreparedExactProof _location _alias _target _proof syntax) = - syntax - -preparedExactProofFirstOmission :: PreparedExactProof -> Maybe Location -preparedExactProofFirstOmission - (PreparedExactProof _location _alias _target proof _syntax) = - preparedProofFirstOmission proof - -data PrepareState = PrepareState - { prepareNextLocal :: !Natural - , prepareNextPremise :: !Natural - } - -type Prepare = - StateT - PrepareState - (ExceptT ExactProofError (Declaration.LoweringDriver)) - -prepareExactProof - :: Raw.Block - -> Maybe Raw.Proof - -> Declaration.LoweringDriver - (Either ExactProofError PreparedExactProof) -prepareExactProof block explicitProof = - Except.runExceptT - (State.evalStateT prepare initialState) - where - initialState = PrepareState 0 0 - - prepare = - case block of - Raw.BlockClaim - _kind location _title (Raw.Marker marker) - (Raw.Claim assumptions statement) -> do - envelope <- - liftDriver - (Exact.prepareExactClaimEnvelope assumptions statement) - >>= either - (throwProof . ExactProofElaborationFailed) - pure - let targetCore = Exact.preparedExactClaimTarget envelope - unless (null (scopedCoreContext targetCore)) - (throwProof - (ExactProofUnsupportedClaim location)) - (context, openedGoal, identities) <- - openEnvelopeVariables - targetCore - (Exact.preparedExactClaimVariables envelope) - (Exact.preparedExactClaimContext envelope) - (locals, bodyGoal, antecedents) <- - openEnvelopeAntecedents - context - openedGoal - (Exact.preparedExactClaimAntecedentCount envelope) - bodyProof <- - case explicitProof of - Nothing -> - PreparedImplicitAuto - <$> prepareDischargeWith - DirectDischarge - [] - Nothing - location - context - locals - bodyGoal - Raw.JustificationEmpty - Just sourceProof -> - prepareProof - location - context - locals - (Just antecedents) - bodyGoal - sourceProof - let withAssumptions = - foldr PreparedAssume bodyProof antecedents - proof = - case identities of - [] -> withAssumptions - _ -> PreparedFix identities withAssumptions - pure - (PreparedExactProof - location - (semanticName marker) - targetCore - proof - (proofSyntaxId - (encodePreparedProof proof))) - _ -> - throwProof - (ExactProofUnsupportedClaim (locate block)) - -prepareFinalPreludeFoundationClaim - :: CheckedFoundation - -> Raw.Block - -> Maybe Raw.Proof - -> Declaration.LoweringDriver - (Either ExactProofError PreparedFinalPreludeFoundationClaim) -prepareFinalPreludeFoundationClaim foundation block explicitProof = - Except.runExceptT do - case (block, explicitProof) of - ( Raw.BlockClaim - _kind location _title (Raw.Marker marker) - (Raw.Claim assumptions statement) - , Nothing - ) -> do - envelope <- - Except.lift - (Exact.prepareExactClaimEnvelope - assumptions - statement) - >>= either - (Except.throwError - . ExactProofElaborationFailed) - pure - unless - ( null (Exact.preparedExactClaimVariables envelope) - && Exact.preparedExactClaimAntecedentCount envelope - == 0 - ) - (Except.throwError - (ExactProofFoundationLeafRequiresImplicitAuto - location)) - let target = Exact.preparedExactClaimTarget envelope - matches = - [ tag - | tag <- [minBound .. maxBound] - , target == foundationTarget tag - ] - tag <- case matches of - [] -> - Except.throwError - (ExactProofFoundationLeafTargetMismatch location) - [only] -> - pure only - _ -> - Except.throwError - (ExactProofFoundationLeafTargetAmbiguous location) - pure - (PreparedFinalPreludeFoundationClaim - location - (semanticName marker) - target - tag - (implicitAutoProofSyntaxId target)) - (Raw.BlockClaim _kind location _title _marker _claim, Just{}) -> - Except.throwError - (ExactProofFoundationLeafRequiresImplicitAuto location) - _ -> - Except.throwError - (ExactProofUnsupportedClaim (locate block)) - where - foundationTarget tag = - embedClosedCore [] - (mapFrozenGlobals - absurd - (foundationAxiomFrozen foundation tag)) - -openEnvelopeVariables - :: ScopedCheckedCore ObjectId - -> [Raw.VarSymbol] - -> Exact.ExactBinderContext - -> Prepare - ( Exact.ExactBinderContext - , ScopedCheckedCore ObjectId - , [Exact.ExactLocalId] - ) -openEnvelopeVariables target variables preparedContext = - case NonEmpty.nonEmpty variables of - Nothing -> - pure (preparedContext, target, []) - Just nonempty -> do - (_unannotated, opened, identities) <- - openFixedVariables - Exact.emptyExactBinderContext - target - nonempty - let expected = - reverse - (fst <$> toList - (Exact.exactBinderContextSupport preparedContext)) - unless - (identities == expected) - (impossible - "prepared claim annotations do not match opened binders") - pure (preparedContext, opened, identities) - -openEnvelopeAntecedents - :: Exact.ExactBinderContext - -> ScopedCheckedCore ObjectId - -> Natural - -> Prepare - ( [PreparedLocal] - , ScopedCheckedCore ObjectId - , [ScopedCheckedCore ObjectId] - ) -openEnvelopeAntecedents context initialGoal initialCount = - go [] [] initialGoal initialCount - where - go locals antecedents goal 0 = - pure (locals, goal, antecedents) - go locals antecedents goal remaining = do - (antecedent, conclusion) <- - maybe - (impossible - "a prepared claim envelope has too few implications") - pure - (openScopedImplication goal) - local <- allocateLocal ExactAssumption context antecedent - go - (locals <> [local]) - (antecedents <> [antecedent]) - conclusion - (remaining - 1) - -prepareProof - :: Location - -> Exact.ExactBinderContext - -> [PreparedLocal] - -- Only the initial proof carries set-induction antecedents. - -> Maybe [ScopedCheckedCore ObjectId] - -> ScopedCheckedCore ObjectId - -> Raw.Proof - -> Prepare PreparedProof -prepareProof fallback context locals inductionAntecedents goal = \case - Raw.Omitted location -> - pure (PreparedOmitted location goal) - Raw.Qed maybeLocation justification -> - PreparedQed - <$> prepareDischarge - (fromMaybe fallback maybeLocation) - context - locals - 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 - Raw.Assume location statement continuation -> do - (antecedent, conclusion) <- - maybe - (throwProof - (ExactProofExpectedImplicationGoal location)) - pure - (openScopedImplication goal) - supplied <- prepareStatement context statement - unless - (Exact.preparedExactPropositionCore supplied - == antecedent) - (throwProof - (ExactProofGoalStatementMismatch location)) - local <- allocateLocal ExactAssumption context antecedent - PreparedAssume antecedent - <$> prepareProof - fallback - context - (locals <> [local]) - Nothing - 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 - Raw.BySetInduction location variable continuation -> - case (inductionAntecedents, continuation) of - (Nothing, _proof) -> - throwProof - (ExactProofSetInductionNotOutermost location) - (Just antecedents, Raw.Qed maybeLocation justification) -> do - sourceVariable <- - case variable of - Just (Raw.TermExpr (Raw.ExprVar candidate)) -> - pure candidate - _ -> - throwProof - (ExactProofSetInductionVariableRequired - location) - selected <- - maybe - (throwProof - (ExactProofSetInductionVariableNotActive - location - sourceVariable)) - pure - (Exact.exactBinderContextIndex - sourceVariable context) - let property = - foldr implyChecked goal antecedents - hypothesis <- - maybe - (throwProof - (ExactProofSetInductionGoalMismatch - location)) - pure - (scopedSetInductionHypothesis selected property) - local <- allocateLocal ExactAssumption context hypothesis - PreparedSetInduction hypothesis - <$> prepareDischarge - (fromMaybe location maybeLocation) - context - (locals <> [local]) - goal - justification - (Just _antecedents, _proof) -> - throwProof (ExactProofUnsupportedStep location) - Raw.Have location since statement justification continuation -> do - when (isJust since) - (throwProof (ExactProofUnsupportedStep location)) - claim <- - Exact.preparedExactPropositionCore - <$> prepareStatement context statement - discharge <- - prepareDischarge - location context locals claim justification - local <- allocateLocal ExactDerivedClaim context claim - PreparedHave claim discharge - <$> prepareProof - fallback - context - (locals <> [local]) - Nothing - goal - continuation - Raw.Subclaim location statement subproof continuation -> do - claim <- - Exact.preparedExactPropositionCore - <$> prepareStatement context statement - preparedSubproof <- - prepareProof - location - context - locals - Nothing - claim - subproof - local <- allocateLocal ExactDerivedClaim context claim - PreparedSubclaim claim preparedSubproof - <$> prepareProof - fallback - context - (locals <> [local]) - Nothing - goal - continuation - Raw.Define _location variable expression continuation -> do - body <- - Exact.preparedExactSetExpressionCore - <$> ( liftDriver - (Exact.prepareExactSetExpression - context expression) - >>= either - (throwProof . ExactProofElaborationFailed) - pure - ) - identity <- allocateLocalIdentity - context' <- - either - (throwProof . ExactProofElaborationFailed) - pure - (Exact.extendExactBinderContext - ((identity, variable) :| []) - context) - separationCharacteristic <- - liftDriver - (Declaration.currentFoundationAxiomLowering - SeparationCharacteristic) - definition <- - maybe - (impossible - "an exact set expression did not form a local definition") - pure - (scopedSetDefinition separationCharacteristic body) - local <- - allocateLocal ExactLocalDefinition context' definition - PreparedDefine identity body definition - <$> prepareProof - fallback - context' - (locals <> [local]) - Nothing - (weakenCheckedScopedCore TySet goal) - continuation - Raw.DefineFunction - location function argument value bound domain continuation -> do - unless (argument == bound) - (throwProof - (ExactProofLocalFunctionBinderMismatch (locate bound))) - when (function == argument) - (throwProof - (ExactProofLocalFunctionNameConflict (locate function))) - argumentIdentity <- allocateLocalIdentity - argumentContext <- - either - (throwProof . ExactProofElaborationFailed) - pure - (Exact.extendExactBinderContext - ((argumentIdentity, argument) :| []) - context) - graph <- - liftDriver - (Exact.prepareExactLocalFunctionGraph - location context argumentContext domain value) - >>= either - (throwProof . ExactProofElaborationFailed) - pure - functionIdentity <- allocateLocalIdentity - functionContext <- - either - (throwProof . ExactProofElaborationFailed) - pure - (Exact.extendExactBinderContext - ((functionIdentity, function) :| []) - context) - replacementCharacteristic <- - liftDriver - (Declaration.currentFoundationAxiomLowering - ReplacementCharacteristic) - definition <- - maybe - (impossible - "a checked replacement graph did not form a local definition") - pure - (scopedCharacteristicDefinition - replacementCharacteristic - (Exact.preparedExactLocalFunctionGraphCore graph) - ( Exact.preparedExactLocalFunctionGraphDomain graph - :| [Exact.preparedExactLocalFunctionGraphMap graph] - )) - local <- - allocateLocal ExactLocalDefinition functionContext definition - PreparedDefineFunction - functionIdentity - (Exact.preparedExactLocalFunctionGraphCore graph) - definition - <$> prepareProof - fallback - functionContext - (locals <> [local]) - Nothing - (weakenCheckedScopedCore TySet goal) - continuation - Raw.Contradiction location justification -> do - unless - ( scopedCoreType goal == TyProp - && scopedCoreTerm goal == CFalsum - ) - (throwProof - (ExactProofContradictionGoalMismatch location)) - PreparedContradiction - <$> prepareDischargeWith - IndirectContradictionDischarge - [] - Nothing - location - context - locals - goal - justification - proof -> - throwProof - (ExactProofUnsupportedStep - (proofLocation fallback proof)) - where - implyChecked antecedent conclusion = - fromMaybe - (impossible "an exact claim antecedent changed context") - (implyScopedCore antecedent conclusion) - --- The discharged existential and the opened witness premise are the same --- checked proposition viewed on opposite sides of existential elimination. -closeTakenWitnesses - :: Int - -> ScopedCheckedCore ObjectId - -> ScopedCheckedCore ObjectId -closeTakenWitnesses binderCount = go binderCount - where - go 0 proposition = proposition - go remaining proposition = - go (remaining - 1) - (fromMaybe - (impossible "a taken witness has no checked binder") - (closeScopedExists proposition)) - -weakenForTakenWitnesses - :: Int - -> ScopedCheckedCore ObjectId - -> ScopedCheckedCore ObjectId -weakenForTakenWitnesses binderCount = go binderCount - where - go 0 proposition = proposition - go remaining proposition = - go (remaining - 1) - (weakenCheckedScopedCore TySet proposition) - -openFixedVariables - :: Exact.ExactBinderContext - -> ScopedCheckedCore ObjectId - -> NonEmpty Raw.VarSymbol - -> Prepare - ( Exact.ExactBinderContext - , ScopedCheckedCore ObjectId - , [Exact.ExactLocalId] - ) -openFixedVariables initialContext initialGoal variables = - foldM openOne - (initialContext, initialGoal, []) - (toList variables) - where - openOne (context, goal, identities) variable = do - (binderType, body) <- - maybe - (throwProof - (ExactProofExpectedUniversalGoal - (locate variable))) - pure - (openScopedForall goal) - unless (binderType == TySet) - (throwProof - (ExactProofExpectedUniversalGoal - (locate variable))) - identity <- allocateLocalIdentity - context' <- - either - (throwProof . ExactProofElaborationFailed) - pure - (Exact.extendExactBinderContext - ((identity, variable) :| []) - context) - pure (context', body, identities <> [identity]) - -allocateLocalIdentity :: Prepare Exact.ExactLocalId -allocateLocalIdentity = do - state <- State.get - State.put - state - { prepareNextLocal = prepareNextLocal state + 1 - } - pure (Exact.exactLocalId (prepareNextLocal state)) - -allocateLocal - :: ExactLocalOrigin - -> Exact.ExactBinderContext - -> ScopedCheckedCore ObjectId - -> Prepare PreparedLocal -allocateLocal origin context proposition = do - state <- State.get - State.put - state - { prepareNextPremise = prepareNextPremise state + 1 - } - pure - (PreparedLocal - (Backend.localPremiseOrdinal - (prepareNextPremise state)) - origin - (Exact.exactBinderContextSupport context) - proposition) - -prepareDischarge - :: Location - -> Exact.ExactBinderContext - -> [PreparedLocal] - -> ScopedCheckedCore ObjectId - -> Raw.Justification - -> Prepare PreparedDischarge -prepareDischarge location context locals goal justification = - prepareDischargeWith - DirectDischarge - [] Nothing location context locals goal justification - -data DischargeMode - = DirectDischarge - | IndirectContradictionDischarge - -prepareDischargeWith - :: DischargeMode - -> [FoundationAxiomTag] - -> Maybe Declaration.VampirePremiseSelection - -> Location - -> Exact.ExactBinderContext - -> [PreparedLocal] - -> ScopedCheckedCore ObjectId - -> Raw.Justification - -> Prepare PreparedDischarge -prepareDischargeWith - dischargeMode auxiliaries selectionOverride - location context locals goal justification = - case justification of - Raw.JustificationSetExt -> do - (leftToRight, rightToLeft) <- - maybe - (throwProof - (ExactProofSetExtensionalityGoalMismatch location)) - pure - (splitScopedSetEquality goal) - unless - ( hasDerivedLocal leftToRight - && hasDerivedLocal rightToLeft - ) - (throwProof - (ExactProofSetExtensionalityDirectionsUnavailable - location)) - pure (PreparedSetExtensionality location goal) - _ -> do - preparedJustification <- - prepareJustification location justification - prepared <- - liftDriver - (prepareObligation - (Exact.exactBinderContextSupport context) - goal - (toScopedPremise <$> locals) - auxiliaries - (fromMaybe - (vampirePremiseSelection preparedJustification) - selectionOverride)) - >>= either - (throwProof - . ExactProofObligationPreparationFailed location) - pure - pure - (PreparedVampireDischarge - location - preparedJustification - goal - prepared) - where - prepareObligation = - case dischargeMode of - DirectDischarge -> - Declaration.prepareScopedVampireObligationLowering - IndirectContradictionDischarge -> - Declaration.prepareScopedContradictionObligationLowering - - hasDerivedLocal proposition = - any - (\case - PreparedLocal - _ordinal ExactDerivedClaim _support local -> - local == proposition - PreparedLocal{} -> - False) - locals - - toScopedPremise - (PreparedLocal ordinal origin support proposition) = - Declaration.scopedVampirePremise - ordinal origin support proposition - -prepareJustification - :: Location - -> Raw.Justification - -> Prepare PreparedJustification -prepareJustification _location Raw.JustificationEmpty = - pure PreparedAuto -prepareJustification location (Raw.JustificationRef markers) = do - resolved <- traverse (resolveReference location) (toList markers) - let unique = stableUnique resolved - case unique of - [] -> - impossible "a nonempty citation list resolved to no facts" - first : rest -> - pure (PreparedReferences (first :| rest)) -prepareJustification _location Raw.JustificationLocal = - pure PreparedLocalOnly -prepareJustification location Raw.JustificationSetExt = - throwProof (ExactProofUnsupportedStep location) - -vampirePremiseSelection - :: PreparedJustification - -> Declaration.VampirePremiseSelection -vampirePremiseSelection = \case - PreparedAuto -> - Declaration.VampireImplicitPremises - PreparedReferences fingerprints -> - Declaration.VampireExplicitPremises fingerprints - PreparedLocalOnly -> - Declaration.VampireLocalPremises - -resolveReference - :: Location - -> Raw.Marker - -> Prepare SemanticFactOccurrenceFingerprint -resolveReference location marker@(Raw.Marker name) = do - resolved <- - liftDriver - (Declaration.resolveVisibleFactAliasLowering - (semanticName name)) - maybe - (throwProof - (ExactProofUnknownReference location marker)) - pure - resolved - -prepareStatement - :: Exact.ExactBinderContext - -> Raw.Stmt - -> Prepare Exact.PreparedExactProposition -prepareStatement context statement = - liftDriver - (Exact.prepareExactProposition context statement) - >>= either - (throwProof . ExactProofElaborationFailed) - pure - -data CheckedExactProofAuthorization = CheckedExactProofAuthorization - !PreparedProof - !Bool - -lowerPreparedExactProof - :: PreparedExactProof - -> Declaration.LoweringDriver - (Either - Declaration.DeclarationError - (Declaration.CheckedDeclaration CheckedExactProofAuthorization)) -lowerPreparedExactProof - (PreparedExactProof _location alias target proof syntax) = - fmap checked - <$> Declaration.prepareCandidateSpecLowering - [] target SearchEligible [alias] - where - checked spec = - Declaration.checkedProofDeclaration - syntax [] [] [] [] - [Declaration.checkedCandidate spec planning :| []] - (CheckedExactProofAuthorization - proof - (isJust (preparedProofFirstOmission proof))) - where - requests = plannedProofRequests proof - planning - | isJust (preparedProofFirstOmission proof) = - Declaration.checkedOmittedPlanning requests [] - | otherwise = - Declaration.checkedSourceProofPlanning requests [] - -authorizeCheckedExactProof - :: CheckedExactProofAuthorization - -> [NonEmpty Declaration.ReservedCandidate] - -> Declaration.Declaration () -authorizeCheckedExactProof - (CheckedExactProofAuthorization proof hasOmission) = \case - [candidate :| []] - | hasOmission -> - Declaration.authorizeOmittedCandidate - candidate - (executePreparedProof proof) - | otherwise -> - Declaration.authorizeVampireCandidate - candidate - (executePreparedProof proof) - stages -> - Declaration.failDeclaration - (Declaration.CheckedAuthorizationCandidateShapeMismatch - 1 (length stages)) - -data CheckedFinalPreludeFoundationAuthorization = - CheckedFinalPreludeFoundationAuthorization !FoundationAxiomTag - -lowerPreparedFinalPreludeFoundationClaim - :: PreparedFinalPreludeFoundationClaim - -> Declaration.LoweringDriver - (Either - Declaration.DeclarationError - (Declaration.CheckedDeclaration - CheckedFinalPreludeFoundationAuthorization)) -lowerPreparedFinalPreludeFoundationClaim - (PreparedFinalPreludeFoundationClaim - _location alias target tag syntax) = - fmap checked - <$> Declaration.prepareCandidateSpecLowering - [] target SearchEligible [alias] - where - checked spec = - Declaration.checkedProofDeclaration - syntax [] [] [] [] - [ Declaration.checkedCandidate spec - (Declaration.checkedKernelPlanning - (Authority.FoundationLeaf tag) []) - :| [] - ] - (CheckedFinalPreludeFoundationAuthorization tag) - -authorizeCheckedFinalPreludeFoundationClaim - :: CheckedFinalPreludeFoundationAuthorization - -> [NonEmpty Declaration.ReservedCandidate] - -> Declaration.Declaration () -authorizeCheckedFinalPreludeFoundationClaim - (CheckedFinalPreludeFoundationAuthorization tag) = \case - [candidate :| []] -> - Declaration.authorizeKernelConstructionCandidate - (Authority.FoundationLeaf tag) - candidate - (pure (foundationFactDerivation tag)) - stages -> - Declaration.failDeclaration - (Declaration.CheckedAuthorizationCandidateShapeMismatch - 1 (length stages)) - -preparedProofFirstOmission :: PreparedProof -> Maybe Location -preparedProofFirstOmission = \case - PreparedImplicitAuto{} -> Nothing - PreparedQed{} -> Nothing - PreparedOmitted location _goal -> Just location - PreparedFix _identities continuation -> - preparedProofFirstOmission continuation - PreparedAssume _antecedent continuation -> - preparedProofFirstOmission continuation - PreparedTake _identities _witness _discharge continuation -> - preparedProofFirstOmission continuation - PreparedSetInduction _hypothesis _discharge -> Nothing - PreparedHave _claim _discharge continuation -> - preparedProofFirstOmission continuation - PreparedSubclaim _claim subproof continuation -> - preparedProofFirstOmission subproof - <|> preparedProofFirstOmission continuation - PreparedDefine _identity _body _definition continuation -> - preparedProofFirstOmission continuation - PreparedDefineFunction _identity _graph _definition continuation -> - preparedProofFirstOmission continuation - PreparedContradiction{} -> Nothing - -plannedProofRequests - :: PreparedProof - -> [Declaration.CheckedPlannedVampireRequest] -plannedProofRequests = \case - PreparedImplicitAuto discharge -> plannedDischargeRequests discharge - PreparedQed discharge -> plannedDischargeRequests discharge - PreparedOmitted{} -> [] - PreparedFix _identities continuation -> - plannedProofRequests continuation - PreparedAssume _antecedent continuation -> - plannedProofRequests continuation - PreparedTake _identities _witness discharge continuation -> - plannedDischargeRequests discharge <> plannedProofRequests continuation - PreparedSetInduction _hypothesis discharge -> - plannedDischargeRequests discharge - PreparedHave _claim discharge continuation -> - plannedDischargeRequests discharge <> plannedProofRequests continuation - PreparedSubclaim _claim subproof continuation -> - plannedProofRequests subproof <> plannedProofRequests continuation - PreparedDefine _identity _body _definition continuation -> - plannedProofRequests continuation - PreparedDefineFunction _identity _graph _definition continuation -> - plannedProofRequests continuation - PreparedContradiction discharge -> - plannedDischargeRequests discharge - -plannedDischargeRequests - :: PreparedDischarge - -> [Declaration.CheckedPlannedVampireRequest] -plannedDischargeRequests = \case - PreparedVampireDischarge location _justification _goal obligation -> - [Declaration.checkedPlannedVampireRequest location obligation] - PreparedSetExtensionality{} -> [] - -executePreparedProof - :: PreparedProof - -> Declaration.CandidateProof () -executePreparedProof = \case - PreparedImplicitAuto discharge -> - executeDischarge discharge - PreparedQed discharge -> - executeDischarge discharge - PreparedOmitted _location _goal -> - Declaration.recordOmittedUse - PreparedFix _identities continuation -> - executePreparedProof continuation - PreparedAssume _antecedent continuation -> - executePreparedProof continuation - PreparedTake _identities _witness discharge continuation -> do - executeDischarge discharge - executePreparedProof continuation - PreparedSetInduction _hypothesis discharge -> - executeDischarge discharge - PreparedHave _claim discharge continuation -> do - executeDischarge discharge - executePreparedProof continuation - PreparedSubclaim _claim subproof continuation -> do - executePreparedProof subproof - executePreparedProof continuation - PreparedDefine _identity _body _definition continuation -> - executePreparedProof continuation - PreparedDefineFunction _identity _graph _definition continuation -> - executePreparedProof continuation - PreparedContradiction discharge -> - executeDischarge discharge - -executeDischarge - :: PreparedDischarge - -> Declaration.CandidateProof () -executeDischarge - (PreparedVampireDischarge - location _justification _goal obligation) = - Declaration.locateProofObligation location - (Declaration.acceptPreparedVampireObligation obligation) -executeDischarge PreparedSetExtensionality{} = - pure () - -encodePreparedProof :: PreparedProof -> ByteString -encodePreparedProof = - encodeCache . putPreparedProof - -putPreparedProof :: PreparedProof -> CachePut -putPreparedProof = \case - PreparedImplicitAuto discharge -> do - putCacheTag 0x00 - putPreparedDischarge discharge - PreparedQed discharge -> do - putCacheTag 0x01 - putPreparedDischarge discharge - PreparedOmitted _location goal -> do - putCacheTag 0x06 - putScopedProposition goal - PreparedFix identities continuation -> do - putCacheTag 0x02 - putCacheList - (putCacheNatural . Exact.exactLocalIdValue) - identities - putPreparedProof continuation - PreparedAssume antecedent continuation -> do - putCacheTag 0x03 - putScopedProposition antecedent - putPreparedProof continuation - PreparedTake identities witness discharge continuation -> do - putCacheTag 0x08 - putCacheList - (putCacheNatural . Exact.exactLocalIdValue) - identities - putScopedProposition witness - putPreparedDischarge discharge - putPreparedProof continuation - PreparedSetInduction hypothesis discharge -> do - putCacheTag 0x07 - putScopedProposition hypothesis - putPreparedDischarge discharge - PreparedHave claim discharge continuation -> do - putCacheTag 0x04 - putScopedProposition claim - putPreparedDischarge discharge - putPreparedProof continuation - PreparedSubclaim claim subproof continuation -> do - putCacheTag 0x05 - putScopedProposition claim - putPreparedProof subproof - putPreparedProof continuation - PreparedDefine identity body definition continuation -> do - putCacheTag 0x09 - putCacheNatural (Exact.exactLocalIdValue identity) - putScopedTerm body - putScopedProposition definition - putPreparedProof continuation - PreparedContradiction discharge -> do - putCacheTag 0x0a - putPreparedDischarge discharge - PreparedDefineFunction identity graph definition continuation -> do - putCacheTag 0x0b - putCacheNatural (Exact.exactLocalIdValue identity) - putScopedTerm graph - putScopedProposition definition - putPreparedProof continuation - -putPreparedDischarge :: PreparedDischarge -> CachePut -putPreparedDischarge - (PreparedVampireDischarge - _location justification goal _obligation) = do - putPreparedDischargeSyntax justification goal -putPreparedDischarge - (PreparedSetExtensionality _location goal) = do - putCacheTag 0x03 - putScopedProposition goal - -putPreparedDischargeSyntax - :: PreparedJustification - -> ScopedCheckedCore ObjectId - -> CachePut -putPreparedDischargeSyntax justification goal = do - putPreparedJustification justification - putScopedProposition goal - -implicitAutoProofSyntaxId - :: ScopedCheckedCore ObjectId - -> ProofSyntaxId -implicitAutoProofSyntaxId goal = - proofSyntaxId - (encodeCache do - putCacheTag 0x00 - putPreparedDischargeSyntax PreparedAuto goal) - -putPreparedJustification :: PreparedJustification -> CachePut -putPreparedJustification = \case - PreparedAuto -> - putCacheTag 0x00 - PreparedReferences fingerprints -> do - putCacheTag 0x01 - putCacheList - putSemanticFactOccurrenceFingerprintCache - (toList fingerprints) - PreparedLocalOnly -> - putCacheTag 0x02 - -putScopedProposition - :: ScopedCheckedCore ObjectId - -> CachePut -putScopedProposition proposition = do - putCacheList putCoreTypeCache - (scopedCoreContext proposition) - putCanonicalTermCache putObjectIdCache - (scopedCoreTerm proposition) - -putScopedTerm - :: ScopedCheckedCore ObjectId - -> CachePut -putScopedTerm term = do - putCacheList putCoreTypeCache - (scopedCoreContext term) - putCoreTypeCache (scopedCoreType term) - putCanonicalTermCache putObjectIdCache - (scopedCoreTerm term) - -proofLocation :: Location -> Raw.Proof -> Location -proofLocation fallback = \case - Raw.Omitted location -> location - Raw.Qed maybeLocation _justification -> - fromMaybe fallback maybeLocation - Raw.Contradiction location _justification -> location - Raw.ByCase location _cases -> location - Raw.ByContradiction location _proof -> location - Raw.BySetInduction location _term _proof -> location - Raw.ByOrdInduction location _proof -> location - Raw.Assume location _statement _proof -> location - Raw.FixSymbolic location _variables _bound _proof -> location - Raw.FixSuchThat location _variables _statement _proof -> location - Raw.Calc location _quantifier _calculation _proof -> location - Raw.TakeVar location _variables _bound _statement _justification _proof -> - location - Raw.TakeNoun location _noun _justification _proof -> location - Raw.Have location _since _statement _justification _proof -> location - Raw.Suffices location _statement _justification _proof -> location - Raw.Subclaim location _statement _subproof _proof -> location - Raw.Define location _variable _expression _proof -> location - Raw.DefineFunction location _function _argument _value _bound _domain _proof -> - location - Raw.DefineFunctionLocal - location _function _argument _value _bound _target _rules _proof -> - location - -throwProof :: ExactProofError -> Prepare value -throwProof = - State.lift . Except.throwError - -liftDriver - :: Declaration.LoweringDriver value - -> Prepare value -liftDriver = - State.lift . Except.lift - -stableUnique :: Ord value => [value] -> [value] -stableUnique = - reverse . snd - . foldl' - (\(seen, reversed) value -> - if value `Set.member` seen - then (seen, reversed) - else - ( Set.insert value seen - , value : reversed - )) - (Set.empty, []) |