diff options
Diffstat (limited to 'source/Checking/Exact')
| -rw-r--r-- | source/Checking/Exact/Inductive.hs | 214 | ||||
| -rw-r--r-- | source/Checking/Exact/Proof.hs | 1652 | ||||
| -rw-r--r-- | source/Checking/Exact/Vocabulary.hs | 30 |
3 files changed, 1675 insertions, 221 deletions
diff --git a/source/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs index 6764ec8..74208fc 100644 --- a/source/Checking/Exact/Inductive.hs +++ b/source/Checking/Exact/Inductive.hs @@ -63,6 +63,7 @@ data CheckedExactInductiveAuthorization = !ObjectId !(Typed.PreparedTypedInductive ObjectId) ![SemanticFactOccurrenceFingerprint] + ![(Location, Declaration.PreparedVampireObligation Void ())] preparedExactInductiveCarrierId :: PreparedExactInductive @@ -116,7 +117,9 @@ data ExactInductiveError | ExactInductiveResultShape !Location | ExactInductiveResultMentionsCarrier !Location | ExactInductiveRecursiveTermMentionsCarrier !Location - | ExactInductiveNestedRecursion !Location + | ExactInductiveRecursiveCarrierWrongArguments !Location + | ExactInductiveRecursiveCarrierOutsideMembership !Location + | ExactInductiveUnsupportedRecursiveCarrierContext !Location | ExactInductiveFixedSemanticCollision !Location !SemanticGlobalKey | ExactInductiveGlobalAlreadyVisible !Location !SemanticGlobalKey | ExactInductiveGlobalNotVisible !Location !Internal.Symbol @@ -143,7 +146,9 @@ exactInductiveErrorLocation = \case ExactInductiveResultShape location -> location ExactInductiveResultMentionsCarrier location -> location ExactInductiveRecursiveTermMentionsCarrier location -> location - ExactInductiveNestedRecursion location -> location + ExactInductiveRecursiveCarrierWrongArguments location -> location + ExactInductiveRecursiveCarrierOutsideMembership location -> location + ExactInductiveUnsupportedRecursiveCarrierContext location -> location ExactInductiveFixedSemanticCollision location _key -> location ExactInductiveGlobalAlreadyVisible location _key -> location ExactInductiveGlobalNotVisible location _symbol -> location @@ -182,8 +187,12 @@ renderExactInductiveError failure = "an inductive result term must not mention its carrier" ExactInductiveRecursiveTermMentionsCarrier{} -> "a recursive occurrence must be in the carrier of a membership premise" - ExactInductiveNestedRecursion{} -> - "nested inductive recursion is not supported by the typed checker" + ExactInductiveRecursiveCarrierWrongArguments{} -> + "the inductive carrier occurs with arguments other than its declared parameters" + ExactInductiveRecursiveCarrierOutsideMembership{} -> + "an inductive carrier occurrence must be in the set operand of a membership premise" + ExactInductiveUnsupportedRecursiveCarrierContext{} -> + "this recursive carrier context is outside the supported first-order set-term fragment" ExactInductiveFixedSemanticCollision _location key -> "the inductive carrier collides with fixed semantics for " <> shown key @@ -448,18 +457,28 @@ normalizeCondition carrier parameters formula Left (ExactInductiveRecursiveTermMentionsCarrier (termLocation recursiveTerm)) - | matchesCarrier carrier parameters recursiveCarrier -> + | otherwise -> do + context <- + first recursiveCarrierContextError + (Typed.prepareRecursiveCarrierContext + carrier parameters recursiveCarrier) Right - (Typed.DirectRecursiveCondition recursiveTerm) - | otherwise -> - Left - (ExactInductiveNestedRecursion - (termLocation recursiveCarrier)) + (Typed.DirectRecursiveCondition + recursiveTerm context) _ -> Left - (ExactInductiveNestedRecursion + (ExactInductiveRecursiveCarrierOutsideMembership (termLocation formula)) +recursiveCarrierContextError + :: Typed.RecursiveCarrierContextError + -> ExactInductiveError +recursiveCarrierContextError = \case + Typed.RecursiveCarrierWrongArguments location -> + ExactInductiveRecursiveCarrierWrongArguments location + Typed.RecursiveCarrierUnsupportedContext location -> + ExactInductiveUnsupportedRecursiveCarrierContext location + matchesCarrier :: Internal.FunctionSymbol -> [Internal.VarSymbol] @@ -543,8 +562,9 @@ directSymbols direct = conditionSymbols = \case Typed.DirectSideCondition formula -> Internal.mentionedSymbols formula - Typed.DirectRecursiveCondition term -> + Typed.DirectRecursiveCondition term context -> Internal.mentionedSymbols term + <> Typed.recursiveCarrierContextSymbols context lowerPreparedExactInductive :: PreparedExactInductive @@ -558,34 +578,107 @@ lowerPreparedExactInductive _location key identity asserted alias syntax typed guards) = do let facts = Typed.typedInductiveFacts typed + monotonicities = + Vector.toList + (Typed.typedInductiveMonotonicities typed) objects = maybeToList asserted definition <- Declaration.prepareDefinitionEquationSpecLowering objects identity alias + preparedMonotonicities <- + traverse + (\monotonicity -> Except.runExceptT do + let factLocation = + Typed.typedInductiveMonotonicityLocation + monotonicity + target = + Typed.typedInductiveMonotonicityTarget + monotonicity + spec <- + Except.lift + (Declaration.prepareFrozenCandidateSpecLowering + objects target SearchIneligible []) + >>= Except.liftEither + obligation <- + Except.lift + (Declaration.prepareScopedVampireObligationLowering + Vector.empty + (embedClosedCore [] target) + [] + [] + Declaration.VampireImplicitPremises) + >>= either + (Except.throwError + . Declaration.ProofObligationFailedAt + factLocation + . Declaration.CurrentCandidateVampirePreparationFailed) + pure + pure + ( Declaration.checkedCandidate + spec + (Declaration.checkedSourceProofPlanning + [ Declaration.checkedPlannedVampireRequest + factLocation obligation + ] + []) + , (factLocation, obligation) + )) + monotonicities preparedCandidates <- traverse - (\fact -> - fmap - (fmap - (\spec -> - Declaration.checkedCandidate spec - (Declaration.checkedKernelPlanning - (GuardedFoundationRules - (guardedRuleSet - (Typed.typedInductiveFactRules - fact))) - guards))) - (Declaration.prepareCandidateSpecLowering + (\fact -> do + prepared <- + Declaration.prepareCandidateSpecLowering objects (embedClosedCore [] (Typed.typedInductiveFactTarget fact)) SearchEligible [markerAlias - (Typed.typedInductiveFactMarker fact)])) + (Typed.typedInductiveFactMarker fact)] + let descriptor = + GuardedFoundationRules + (guardedRuleSet + (Typed.typedInductiveFactRules fact)) + planning + | null monotonicities = + Declaration.checkedKernelPlanning + descriptor guards + | otherwise = + Declaration.checkedKernelPlanningWithStaged + descriptor + guards + (if Typed.typedInductiveFactRequiresMonotonicities + fact + then + [ Declaration.plannedEarlierCandidate + 1 index + | (index, _target) <- + zip [0 ..] monotonicities + ] + else []) + pure + (fmap + (\spec -> + Declaration.checkedCandidate spec planning) + prepared)) facts pure do definitionSpec <- definition + monotonicityCandidates <- sequence preparedMonotonicities factCandidates <- sequence preparedCandidates + let stages + | null monotonicityCandidates = + [ Declaration.checkedCandidate definitionSpec + (Declaration.checkedDefinitionEquationPlanning identity) + :| toList factCandidates + ] + | otherwise = + [ Declaration.checkedCandidate definitionSpec + (Declaration.checkedDefinitionEquationPlanning identity) + :| [] + , NonEmpty.fromList (fst <$> monotonicityCandidates) + , factCandidates + ] pure (Declaration.checkedCompiledDeclaration syntax @@ -593,12 +686,10 @@ lowerPreparedExactInductive [] [semanticGlobalBinding key (GlobalReference identity)] [] - [ Declaration.checkedCandidate definitionSpec - (Declaration.checkedDefinitionEquationPlanning identity) - :| toList factCandidates - ] + stages (CheckedExactInductiveAuthorization - identity typed guards)) + identity typed guards + (snd <$> monotonicityCandidates))) where markerAlias (Raw.Marker name) = semanticName name @@ -608,8 +699,12 @@ authorizeCheckedExactInductive -> [NonEmpty Declaration.ReservedCandidate] -> Declaration.Declaration () authorizeCheckedExactInductive - (CheckedExactInductiveAuthorization identity typed guards) = \case + (CheckedExactInductiveAuthorization + identity typed guards monotonicityObligations) = \case [definitionCandidate :| candidates] -> do + unless (null monotonicityObligations) + (Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch 3 1)) Declaration.authorizeDefinitionEquationCandidate identity definitionCandidate let facts = Typed.typedInductiveFacts typed @@ -618,7 +713,7 @@ authorizeCheckedExactInductive | NonEmpty.length factCandidates == NonEmpty.length facts -> sequence_ (NonEmpty.zipWith - authorizeFact + (authorizeFact []) factCandidates facts) _ -> @@ -626,20 +721,60 @@ authorizeCheckedExactInductive (Declaration.CheckedAuthorizationCandidateShapeMismatch (1 + NonEmpty.length facts) (1 + length candidates)) + [ definitionCandidate :| [] + , monotonicityCandidates + , factCandidates + ] + | NonEmpty.length monotonicityCandidates + == length monotonicityObligations + , NonEmpty.length factCandidates + == NonEmpty.length (Typed.typedInductiveFacts typed) -> do + obligations <- + maybe + (Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch + 1 0)) + pure + (NonEmpty.nonEmpty monotonicityObligations) + Declaration.authorizeDefinitionEquationCandidate + identity definitionCandidate + Declaration.authorizeVampireCandidateBatch + (NonEmpty.zipWith + (\candidate (factLocation, obligation) -> + (factLocation, candidate, pure obligation)) + monotonicityCandidates + obligations) + sequence_ + (NonEmpty.zipWith + (\candidate fact -> + authorizeFact + (if Typed.typedInductiveFactRequiresMonotonicities + fact + then NonEmpty.toList monotonicityCandidates + else []) + candidate + fact) + factCandidates + (Typed.typedInductiveFacts typed)) stages -> Declaration.failDeclaration (Declaration.CheckedAuthorizationCandidateShapeMismatch - 1 (length stages)) + (if null monotonicityObligations then 1 else 3) + (length stages)) where - authorizeFact candidate fact = + authorizeFact monotonicityCandidates candidate fact = Declaration.authorizeKernelConstructionCandidate (GuardedFoundationRules (guardedRuleSet (Typed.typedInductiveFactRules fact))) candidate do traverse_ Declaration.useAuthorizedFact guards + traverse_ + Declaration.useStagedCandidate + monotonicityCandidates pure (Typed.typedInductiveFactDerivation fact) + encodePreparedInductive :: SemanticGlobalKey -> SemanticName @@ -654,10 +789,21 @@ encodePreparedInductive key alias typed = putCanonicalTermCache putObjectIdCache (frozenCoreTerm (Typed.typedInductiveCarrierBody typed)) + putCacheList putFrozenTerm + (Vector.toList + (Typed.typedInductiveContextInventory typed)) + putCacheList + (putFrozenTerm + . Typed.typedInductiveMonotonicityTarget) + (Vector.toList + (Typed.typedInductiveMonotonicities typed)) putCacheText (semanticNameText alias) putCacheList putFact (toList (Typed.typedInductiveFacts typed)) where + putFrozenTerm = + putCanonicalTermCache putObjectIdCache . frozenCoreTerm + putFact fact = do let Raw.Marker marker = Typed.typedInductiveFactMarker fact diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs index 40911b0..92ff500 100644 --- a/source/Checking/Exact/Proof.hs +++ b/source/Checking/Exact/Proof.hs @@ -35,6 +35,8 @@ import Checking.Exact qualified as Exact import Checking.Foundation import Checking.Identity import Checking.Kernel.Derivation (foundationFactDerivation) +import Checking.Kernel.Proof qualified as KernelProof +import Checking.SetConstruction import Checking.Semantic import Felix.Cache.Codec import Report.Location @@ -47,28 +49,34 @@ 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.Map.Strict qualified as Map import Data.Set qualified as Set import Data.Text qualified as Text import Data.Vector (Vector) +import Data.Vector qualified as Vector import Numeric.Natural (Natural) data ExactProofError = ExactProofUnsupportedClaim !Location | ExactProofUnsupportedStep !Location - | ExactProofBoundedFixNotSupported !Location - | ExactProofBoundedTakeNotSupported !Location | ExactProofSetInductionVariableRequired !Location | ExactProofSetInductionVariableNotActive !Location !Raw.VarSymbol - | ExactProofSetInductionNotOutermost !Location + | ExactProofSetInductionFocusAmbiguous !Location + | ExactProofSetInductionActiveBinderIneligible + !Location !Raw.VarSymbol + | ExactProofSetInductionBinderConflict + !Location !Raw.VarSymbol | ExactProofSetInductionGoalMismatch !Location | ExactProofSetExtensionalityGoalMismatch !Location | ExactProofSetExtensionalityDirectionsUnavailable !Location | ExactProofExpectedUniversalGoal !Location | ExactProofExpectedImplicationGoal !Location | ExactProofGoalStatementMismatch !Location - | ExactProofContradictionGoalMismatch !Location + | ExactProofEmptyCaseSplit !Location + | ExactProofStructuralCompositionFailed + !Location !KernelProof.KernelProofBuildError | ExactProofLocalFunctionBinderMismatch !Location | ExactProofLocalFunctionNameConflict !Location | ExactProofUnknownReference !Location !Raw.Marker @@ -86,19 +94,22 @@ 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 + ExactProofSetInductionFocusAmbiguous location -> location + ExactProofSetInductionActiveBinderIneligible location _variable -> + location + ExactProofSetInductionBinderConflict location _variable -> + location ExactProofSetInductionGoalMismatch location -> location ExactProofSetExtensionalityGoalMismatch location -> location ExactProofSetExtensionalityDirectionsUnavailable location -> location ExactProofExpectedUniversalGoal location -> location ExactProofExpectedImplicationGoal location -> location ExactProofGoalStatementMismatch location -> location - ExactProofContradictionGoalMismatch location -> location + ExactProofEmptyCaseSplit location -> location + ExactProofStructuralCompositionFailed location _failure -> location ExactProofLocalFunctionBinderMismatch location -> location ExactProofLocalFunctionNameConflict location -> location ExactProofUnknownReference location _marker -> location @@ -115,17 +126,20 @@ 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 -> at location <> "the set-induction variable " <> shown variable - <> " is not an active exact binder" - ExactProofSetInductionNotOutermost location -> - at location <> "set induction must currently be outermost" + <> " is not an eligible exact focus" + ExactProofSetInductionFocusAmbiguous location -> + at location + <> "set induction without an explicit variable has no unique focus" + ExactProofSetInductionActiveBinderIneligible location variable -> + at location <> "the active binder " <> shown variable + <> " is not an eligible set-induction focus" + ExactProofSetInductionBinderConflict location variable -> + at location <> "the leading set-induction binder " <> shown variable + <> " conflicts with an active exact binder" ExactProofSetInductionGoalMismatch location -> at location <> "the set-induction variable does not belong to this goal" ExactProofSetExtensionalityGoalMismatch location -> @@ -139,8 +153,10 @@ renderExactProofError = \case 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" + ExactProofEmptyCaseSplit location -> + at location <> "case analysis requires at least one case" + ExactProofStructuralCompositionFailed location failure -> + at location <> "invalid structural proof composition: " <> shown failure ExactProofLocalFunctionBinderMismatch location -> at location <> "the function argument must match its domain binder" ExactProofLocalFunctionNameConflict location -> @@ -167,6 +183,8 @@ data ExactLocalOrigin = ExactAssumption | ExactDerivedClaim | ExactLocalDefinition + | ExactLocalConstructionExtensional + | ExactLocalConstructionEquation deriving stock (Show, Eq, Ord) data PreparedLocal = PreparedLocal @@ -193,6 +211,75 @@ data PreparedDischarge !Location !(ScopedCheckedCore ObjectId) +data PreparedCalculationLink = PreparedCalculationLink + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + +-- The private constructor stores every destination with the discharge derived +-- from its immediately preceding endpoint. Planning and admission can +-- therefore traverse one immutable sequence without re-associating shapes. +data PreparedCalculation = PreparedCheckedCalculation + !CoreType + ![Exact.ExactLocalId] + !(Maybe (ScopedCheckedCore ObjectId)) + !(ScopedCheckedCore ObjectId) + !(NonEmpty PreparedCalculationLink) + !(ScopedCheckedCore ObjectId) + +data PreparedSinceEvidence + = PreparedSinceExisting !PreparedLocal + | PreparedSinceDischarged !PreparedDischarge !PreparedLocal + +data PreparedCase = PreparedCase + !(ScopedCheckedCore ObjectId) + !PreparedProof + +data PreparedCaseAnalysis = PreparedCaseAnalysis + !(ScopedCheckedCore ObjectId) + !(NonEmpty PreparedCase) + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + +data InitialSetInductionFocus = InitialSetInductionFocus + !Raw.VarSymbol + !Exact.ExactLocalId + !Natural + +data InitialSetInductionView = InitialSetInductionView + ![InitialSetInductionFocus] + !(Vector (Exact.ExactLocalId, CoreType)) + !(ScopedCheckedCore ObjectId) + ![ScopedCheckedCore ObjectId] + !(ScopedCheckedCore ObjectId) + !(Maybe Raw.VarSymbol) + +data SetInductionBoundary + = InitialClaimInduction !InitialSetInductionView + -- A direct source-statement goal may retain only its leading binder name. + -- Recursive proof transformations deliberately discard this hint. + | SourceStatementInduction !(Maybe Raw.VarSymbol) + | RecursiveProofInduction + +data SelectedSetInductionFocus + = SelectedInitialSetInduction !InitialSetInductionFocus + | SelectedLeadingSetInduction !(Maybe Raw.VarSymbol) + +data PreparedSetInductionFocus + = PreparedInitialSetInductionFocus + !Exact.ExactLocalId + !Natural + | PreparedLeadingSetInductionFocus + !Exact.ExactLocalId + +data PreparedSetInduction = PreparedCheckedSetInduction + !PreparedSetInductionFocus + !(ScopedCheckedCore ObjectId) + ![ScopedCheckedCore ObjectId] + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedProof + data PreparedProof = PreparedImplicitAuto !PreparedDischarge | PreparedQed !PreparedDischarge @@ -208,10 +295,23 @@ data PreparedProof !(ScopedCheckedCore ObjectId) !PreparedDischarge !PreparedProof - | PreparedSetInduction + | PreparedSetInduction !PreparedSetInduction + | PreparedHave !(ScopedCheckedCore ObjectId) !PreparedDischarge - | PreparedHave + !PreparedProof + | PreparedSuffices + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + !PreparedProof + | PreparedCalculate + !PreparedCalculation + !PreparedProof + | PreparedSince + !(ScopedCheckedCore ObjectId) + !PreparedSinceEvidence !(ScopedCheckedCore ObjectId) !PreparedDischarge !PreparedProof @@ -222,14 +322,29 @@ data PreparedProof | PreparedDefine !Exact.ExactLocalId !(ScopedCheckedCore ObjectId) + !(NonEmpty (ScopedCheckedCore ObjectId)) + !PreparedProof + | PreparedDefineRelational + !Exact.ExactLocalId !(ScopedCheckedCore ObjectId) + !PreparedDischarge + !(NonEmpty (ScopedCheckedCore ObjectId)) !PreparedProof | PreparedDefineFunction !Exact.ExactLocalId !(ScopedCheckedCore ObjectId) !(ScopedCheckedCore ObjectId) !PreparedProof - | PreparedContradiction !PreparedDischarge + | PreparedByCase !PreparedCaseAnalysis + | PreparedByContradiction + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedProof + | PreparedContradiction + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedDischarge data PreparedExactProof = PreparedExactProof !Location @@ -302,14 +417,19 @@ prepareExactProof block explicitProof = context openedGoal (Exact.preparedExactClaimAntecedentCount envelope) + initialInduction <- + prepareInitialSetInductionView + statement + context + (Exact.preparedExactClaimVariables envelope) + identities + antecedents + bodyGoal bodyProof <- case explicitProof of Nothing -> PreparedImplicitAuto - <$> prepareDischargeWith - DirectDischarge - [] - Nothing + <$> prepareDischarge location context locals @@ -320,7 +440,7 @@ prepareExactProof block explicitProof = location context locals - (Just antecedents) + (InitialClaimInduction initialInduction) bodyGoal sourceProof let withAssumptions = @@ -464,16 +584,96 @@ openEnvelopeAntecedents context initialGoal initialCount = conclusion (remaining - 1) +prepareInitialSetInductionView + :: Raw.Stmt + -> Exact.ExactBinderContext + -> [Raw.VarSymbol] + -> [Exact.ExactLocalId] + -> [ScopedCheckedCore ObjectId] + -> ScopedCheckedCore ObjectId + -> Prepare InitialSetInductionView +prepareInitialSetInductionView + statement context variables identities antecedents bodyGoal = do + unless (length variables == length identities) + (impossible + "opened claim binders lost their source identity association") + foci <- traverse checkedFocus (zip variables identities) + let property = foldr implyChecked bodyGoal antecedents + support = Exact.exactBinderContextSupport context + unless + ( scopedCoreContext property + == (snd <$> Vector.toList support) + ) + (impossible + "initial set-induction property changed its checked context") + pure + (InitialSetInductionView + foci support property antecedents bodyGoal + (claimLeadingUniversalName statement)) + where + checkedFocus (variable, identity) = do + index <- + maybe + (impossible + "an opened claim binder is absent from its exact context") + pure + (Exact.exactBinderContextIndex variable context) + case Exact.exactBinderContextSupport context + Vector.!? (fromIntegral index) of + Just (actualIdentity, TySet) + | actualIdentity == identity -> + pure + (InitialSetInductionFocus + variable identity index) + _ -> + impossible + "an initial set-induction focus changed identity or type" + + implyChecked antecedent conclusion = + fromMaybe + (impossible + "an exact claim antecedent changed context") + (implyScopedCore antecedent conclusion) + +claimLeadingUniversalName :: Raw.Stmt -> Maybe Raw.VarSymbol +claimLeadingUniversalName = \case + Raw.StmtFormula + (Raw.FormulaQuantified _location Raw.Universally + (variable :| _rest) _bound _formula) -> + Just variable + Raw.SymbolicForall _location (variable :| _rest) + _bound _suchThat _statement -> + Just variable + Raw.StmtQuantPhrase + _location + (Raw.QuantPhrase Raw.Universally + (Raw.NounPhrase _left _noun variables _right _suchThat)) + _statement -> + listToMaybe variables + Raw.StmtVerbPhrase + (Raw.TermQuantified Raw.Universally _location + (Raw.NounPhrase _left _noun variable _right _suchThat) + :| []) + _verb -> + variable + Raw.StmtNoun + (Raw.TermQuantified Raw.Universally _location + (Raw.NounPhrase _left _noun variable _right _suchThat) + :| []) + _nounPhrase -> + variable + _statement -> + Nothing + prepareProof :: Location -> Exact.ExactBinderContext -> [PreparedLocal] - -- Only the initial proof carries set-induction antecedents. - -> Maybe [ScopedCheckedCore ObjectId] + -> SetInductionBoundary -> ScopedCheckedCore ObjectId -> Raw.Proof -> Prepare PreparedProof -prepareProof fallback context locals inductionAntecedents goal = \case +prepareProof fallback context locals inductionBoundary goal = \case Raw.Omitted location -> pure (PreparedOmitted location goal) Raw.Qed maybeLocation justification -> @@ -485,130 +685,166 @@ 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 + RecursiveProofInduction + 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 (locals <> [local]) - Nothing + RecursiveProofInduction 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 <- + 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 -> + prepareSetInduction + fallback location context locals inductionBoundary goal + variable continuation + 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 Nothing statement justification continuation -> do + claim <- Exact.preparedExactPropositionCore - <$> prepareStatement context' statement - let witnessCount = length (toList variables) - existence = closeTakenWitnesses witnessCount witness - goal' = weakenForTakenWitnesses witnessCount goal + <$> prepareStatement context statement discharge <- prepareDischarge - location context locals existence justification - local <- allocateLocal ExactAssumption context' witness - PreparedTake (toList identities) witness discharge + location context locals claim justification + local <- allocateLocal ExactDerivedClaim context claim + PreparedHave claim discharge <$> prepareProof fallback - context' + context (locals <> [local]) - Nothing - goal' + RecursiveProofInduction + 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)) + Raw.Have location (Just sinceStatement) + statement justification continuation -> do + sinceProposition <- + Exact.preparedExactPropositionCore + <$> prepareStatement context sinceStatement claim <- Exact.preparedExactPropositionCore <$> prepareStatement context statement + (evidence, sinceLocals) <- + case find (localMatches sinceProposition) locals of + Just existing -> + pure (PreparedSinceExisting existing, locals) + Nothing -> do + discharge <- + prepareDischarge + location + context + locals + sinceProposition + Raw.JustificationLocal + local <- + allocateLocal + ExactDerivedClaim context sinceProposition + pure + ( PreparedSinceDischarged discharge local + , locals <> [local] + ) + claimDischarge <- + prepareDischarge + location context sinceLocals claim justification + claimLocal <- + allocateLocal ExactDerivedClaim context claim + PreparedSince + sinceProposition evidence claim claimDischarge + <$> prepareProof + fallback + context + (sinceLocals <> [claimLocal]) + RecursiveProofInduction + goal + continuation + Raw.Suffices location statement justification continuation -> do + reduction <- + Exact.preparedExactPropositionCore + <$> prepareStatement context statement + implication <- + maybe + (impossible + "a checked suffices reduction changed lexical context") + pure + (implyScopedCore reduction goal) discharge <- prepareDischarge - location context locals claim justification - local <- allocateLocal ExactDerivedClaim context claim - PreparedHave claim discharge + location context locals implication justification + PreparedSuffices goal reduction implication discharge + <$> prepareProof + fallback + context + locals + (SourceStatementInduction + (claimLeadingUniversalName statement)) + reduction + continuation + Raw.Calc location quantifier calculation continuation -> do + prepared <- + prepareCalculation + location context locals quantifier calculation + local <- + allocateLocal + ExactDerivedClaim + context + (preparedCalculationResult prepared) + PreparedCalculate prepared <$> prepareProof fallback context (locals <> [local]) - Nothing + RecursiveProofInduction goal continuation Raw.Subclaim location statement subproof continuation -> do @@ -620,7 +856,8 @@ prepareProof fallback context locals inductionAntecedents goal = \case location context locals - Nothing + (SourceStatementInduction + (claimLeadingUniversalName statement)) claim subproof local <- allocateLocal ExactDerivedClaim context claim @@ -629,19 +866,17 @@ prepareProof fallback context locals inductionAntecedents goal = \case fallback context (locals <> [local]) - Nothing + RecursiveProofInduction goal continuation - Raw.Define _location variable expression continuation -> do - body <- - Exact.preparedExactSetExpressionCore - <$> ( liftDriver - (Exact.prepareExactSetExpression - context expression) - >>= either - (throwProof . ExactProofElaborationFailed) - pure - ) + Raw.Define location variable expression continuation -> do + preparedBody <- + liftDriver + (Exact.prepareExactSetExpression context expression) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + let body = Exact.preparedExactSetExpressionCore preparedBody identity <- allocateLocalIdentity context' <- either @@ -650,26 +885,77 @@ prepareProof fallback context locals inductionAntecedents goal = \case (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 + case Exact.preparedExactSetExpressionConstruction preparedBody of + Nothing -> do + 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]) + RecursiveProofInduction + (weakenCheckedScopedCore TySet goal) + continuation + Just (Exact.PreparedUnconditionalSetConstruction construction) -> do + characteristics <- prepareConstructionFoundation + (extensional, equation) <- + maybe + (impossible + "a checked named construction has no definition views") + pure + (namedSetConstructionLocalViews + characteristics construction) + extensionalLocal <- + allocateLocal + ExactLocalConstructionExtensional context' extensional + equationLocal <- + allocateLocal + ExactLocalConstructionEquation context' equation + PreparedDefine identity body (extensional :| [equation]) + <$> prepareProof + fallback context' + (locals <> [extensionalLocal, equationLocal]) + RecursiveProofInduction + (weakenCheckedScopedCore TySet goal) + continuation + Just (Exact.PreparedRelationalSetConstruction construction) -> do + characteristics <- prepareConstructionFoundation + let functionality = + relationalSetConstructionFunctionality construction + discharge <- + prepareDischarge + location context locals functionality + Raw.JustificationEmpty + (extensional, equation) <- + maybe + (impossible + "a checked relational construction has no admitted definition views") + pure + (relationalSetConstructionLocalViews + characteristics construction functionality) + extensionalLocal <- + allocateLocal + ExactLocalConstructionExtensional context' extensional + equationLocal <- + allocateLocal + ExactLocalConstructionEquation context' equation + PreparedDefineRelational + identity body discharge (extensional :| [equation]) + <$> prepareProof + fallback context' + (locals <> [extensionalLocal, equationLocal]) + RecursiveProofInduction + (weakenCheckedScopedCore TySet goal) + continuation Raw.DefineFunction location function argument value bound domain continuation -> do unless (argument == bound) @@ -726,35 +1012,734 @@ prepareProof fallback context locals inductionAntecedents goal = \case fallback functionContext (locals <> [local]) - Nothing + RecursiveProofInduction (weakenCheckedScopedCore TySet goal) continuation + Raw.ByCase location sourceCases -> + prepareByCase + location context locals goal sourceCases + Raw.ByContradiction location continuation -> do + let falsum = falsumScopedCore (scopedCoreContext goal) + negation <- + maybe + (structuralFailure + location + "proof by contradiction requires a proposition goal") + pure + (negateScopedCore goal) + local <- allocateLocal ExactAssumption context negation + prepared <- + prepareProof + location + context + (locals <> [local]) + RecursiveProofInduction + falsum + continuation + validateStructuralComposition + location [goal, negation, falsum] + (\foundation globalType -> + KernelProof.validateDoubleNegationComposition + foundation globalType goal negation falsum) + pure + (PreparedByContradiction + goal negation falsum prepared) Raw.Contradiction location justification -> do - unless - ( scopedCoreType goal == TyProp - && scopedCoreTerm goal == CFalsum - ) - (throwProof - (ExactProofContradictionGoalMismatch location)) - PreparedContradiction - <$> prepareDischargeWith - IndirectContradictionDischarge - [] - Nothing + let falsum = falsumScopedCore (scopedCoreContext goal) + discharge <- + prepareDischarge location context locals - goal + falsum justification + validateStructuralComposition + location [goal, falsum] + (\foundation globalType -> + KernelProof.validateFalsumEliminationComposition + foundation globalType goal falsum) + pure (PreparedContradiction goal falsum discharge) proof -> throwProof (ExactProofUnsupportedStep (proofLocation fallback proof)) where - implyChecked antecedent conclusion = - fromMaybe - (impossible "an exact claim antecedent changed context") - (implyScopedCore antecedent conclusion) + localMatches proposition + (PreparedLocal _ordinal _origin _support local) = + local == proposition + +prepareSetInduction + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> SetInductionBoundary + -> ScopedCheckedCore ObjectId + -> Maybe Raw.Term + -> Raw.Proof + -> Prepare PreparedProof +prepareSetInduction + fallback location context locals boundary goal sourceFocus + continuation = do + selected <- + selectSetInductionFocus + location context boundary goal sourceFocus + case selected of + SelectedInitialSetInduction + (InitialSetInductionFocus _variable identity index) -> do + (foci, expectedSupport, property, antecedents, childTarget) <- + case boundary of + InitialClaimInduction + (InitialSetInductionView + foundFoci support foundProperty + foundAntecedents foundTarget _leadingName) -> + pure + ( foundFoci + , support + , foundProperty + , foundAntecedents + , foundTarget + ) + RecursiveProofInduction -> + impossible + "an initial induction focus escaped its claim boundary" + SourceStatementInduction _leadingName -> + impossible + "an initial induction focus escaped its claim boundary" + unless + ( Exact.exactBinderContextSupport context == expectedSupport + && goal == childTarget + && any (sameInitialFocus identity index) foci + ) + (throwProof + (ExactProofSetInductionGoalMismatch location)) + PreparedSetInduction + <$> prepareCheckedSetInduction + fallback location context locals + (PreparedInitialSetInductionFocus identity index) + index property antecedents childTarget continuation + SelectedLeadingSetInduction sourceName -> do + (binderType, property) <- + maybe + (throwProof + (ExactProofSetInductionGoalMismatch location)) + pure + (openScopedForall goal) + unless (binderType == TySet) + (throwProof + (ExactProofSetInductionGoalMismatch location)) + identity <- allocateLocalIdentity + extendedContext <- + either + (throwProof . ExactProofElaborationFailed) + pure + (case sourceName of + Just variable -> + Exact.extendExactBinderContext + ((identity, variable) :| []) + context + Nothing -> + Exact.extendExactAnonymousBinderContext + identity context) + let expectedResult = weakenCheckedScopedCore TySet goal + prepared <- prepareCheckedSetInduction + fallback location extendedContext locals + (PreparedLeadingSetInductionFocus identity) + 0 property [] property continuation + unless + (preparedSetInductionResult prepared == expectedResult) + (throwProof + (ExactProofSetInductionGoalMismatch location)) + pure (PreparedSetInduction prepared) + where + sameInitialFocus expectedIdentity expectedIndex + (InitialSetInductionFocus _variable identity index) = + identity == expectedIdentity && index == expectedIndex + +prepareCheckedSetInduction + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> PreparedSetInductionFocus + -> Natural + -> ScopedCheckedCore ObjectId + -> [ScopedCheckedCore ObjectId] + -> ScopedCheckedCore ObjectId + -> Raw.Proof + -> Prepare PreparedSetInduction +prepareCheckedSetInduction + fallback location context locals focus selected property antecedents + childTarget continuation = do + (_predicate, hypothesis, _step, result) <- + maybe + (throwProof + (ExactProofSetInductionGoalMismatch location)) + pure + (scopedSetInductionInstance selected property) + validateStructuralComposition + location + (property : hypothesis : result : childTarget : antecedents) + (\foundation globalType -> + KernelProof.validateSetInductionComposition + foundation globalType selected property antecedents + childTarget hypothesis result) + local <- allocateLocal ExactAssumption context hypothesis + child <- + prepareProof + fallback + context + (locals <> [local]) + RecursiveProofInduction + childTarget + continuation + pure + (PreparedCheckedSetInduction + focus property antecedents childTarget hypothesis result child) + +preparedSetInductionResult + :: PreparedSetInduction + -> ScopedCheckedCore ObjectId +preparedSetInductionResult + (PreparedCheckedSetInduction + _focus _property _antecedents _target _hypothesis result _child) = + result + +selectSetInductionFocus + :: Location + -> Exact.ExactBinderContext + -> SetInductionBoundary + -> ScopedCheckedCore ObjectId + -> Maybe Raw.Term + -> Prepare SelectedSetInductionFocus +selectSetInductionFocus location context boundary goal sourceFocus = do + explicit <- traverse simpleVariable sourceFocus + let (initialFoci, retainedLeadingName) = + case boundary of + InitialClaimInduction + (InitialSetInductionView + foci _support _property _antecedents _target + leadingName) -> + (foci, leadingName) + SourceStatementInduction leadingName -> + ([], leadingName) + RecursiveProofInduction -> + ([], Nothing) + leadingAvailable = + case openScopedForall goal of + Just (TySet, _body) -> True + _ -> False + case explicit of + Just variable -> + case find (initialNamed variable) initialFoci of + Just focus -> + pure (SelectedInitialSetInduction focus) + Nothing + | leadingAvailable + , isJust + (Exact.exactBinderContextIndex variable context) -> + throwProof + (ExactProofSetInductionBinderConflict + location variable) + | leadingAvailable -> + pure + (SelectedLeadingSetInduction + (Just variable)) + | isJust + (Exact.exactBinderContextIndex variable context) -> + throwProof + (ExactProofSetInductionActiveBinderIneligible + location variable) + | otherwise -> + throwProof + (ExactProofSetInductionVariableNotActive + location variable) + Nothing -> + case + ( (SelectedInitialSetInduction <$> initialFoci) + <> [ SelectedLeadingSetInduction retainedLeadingName + | leadingAvailable + ] + ) of + [only] -> pure only + _ -> + throwProof + (ExactProofSetInductionFocusAmbiguous location) + where + simpleVariable = \case + Raw.TermExpr (Raw.ExprVar variable) -> + pure variable + _term -> + throwProof + (ExactProofSetInductionVariableRequired location) + + initialNamed variable + (InitialSetInductionFocus candidate _identity _index) = + candidate == variable + +prepareByCase + :: Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> [Raw.Case] + -> Prepare PreparedProof +prepareByCase location context locals goal sourceCases = do + cases <- + maybe + (throwProof (ExactProofEmptyCaseSplit location)) + (traverse prepareCase) + (NonEmpty.nonEmpty sourceCases) + exhaustive <- + foldM disjoin + (preparedCaseAssumption (NonEmpty.head cases)) + (preparedCaseAssumption <$> NonEmpty.tail cases) + discharge <- + prepareDischarge + location context locals exhaustive Raw.JustificationEmpty + validateStructuralComposition + location + (goal : exhaustive : (preparedCaseAssumption <$> toList cases)) + (\foundation globalType -> + KernelProof.validateCaseAnalysisComposition + foundation + globalType + goal + (preparedCaseAssumption <$> cases) + exhaustive) + pure + (PreparedByCase + (PreparedCaseAnalysis goal cases exhaustive discharge)) + where + prepareCase (Raw.Case statement child) = do + assumption <- + Exact.preparedExactPropositionCore + <$> prepareStatement context statement + local <- allocateLocal ExactAssumption context assumption + prepared <- + prepareProof + (locate statement) + context + (locals <> [local]) + RecursiveProofInduction + goal + child + pure (PreparedCase assumption prepared) + + disjoin left right = + maybe + (structuralFailure + location + "case assumptions changed type or lexical context") + pure + (disjoinScopedCore left right) + +preparedCaseAssumption + :: PreparedCase + -> ScopedCheckedCore ObjectId +preparedCaseAssumption (PreparedCase assumption _proof) = + assumption + +preparedCaseProof :: PreparedCase -> PreparedProof +preparedCaseProof (PreparedCase _assumption proof) = + proof + +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]) + RecursiveProofInduction + conclusion + continuation + pure (PreparedFix identities (PreparedAssume constraint prepared)) + +prepareCalculation + :: Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> Maybe Raw.CalcQuantifier + -> Raw.Calc + -> Prepare PreparedCalculation +prepareCalculation location context locals quantifier calculation = do + (identities, calculationContext, calculationGuard) <- + prepareCalculationScope context quantifier + case calculation of + Raw.Equation first destinations -> do + firstChecked <- prepareSetEndpoint calculationContext first + checkedDestinations <- + traverse + (\(destination, justification) -> do + checked <- + prepareSetEndpoint calculationContext destination + pure + ( locate destination + , checked + , justification + )) + destinations + finishCalculation + location context locals TySet identities calculationGuard + firstChecked checkedDestinations + Raw.Biconditionals first destinations -> do + firstChecked <- preparePropositionEndpoint calculationContext first + checkedDestinations <- + traverse + (\(destination, justification) -> do + checked <- + preparePropositionEndpoint + calculationContext destination + pure + ( locate destination + , checked + , justification + )) + destinations + finishCalculation + location context locals TyProp identities calculationGuard + firstChecked checkedDestinations + where + prepareSetEndpoint endpointContext expression = + Exact.preparedExactSetExpressionCore + <$> ( liftDriver + (Exact.prepareExactSetExpression + endpointContext expression) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + + preparePropositionEndpoint endpointContext formula = + Exact.preparedExactPropositionCore + <$> prepareStatement endpointContext (Raw.StmtFormula formula) + +prepareCalculationScope + :: Exact.ExactBinderContext + -> Maybe Raw.CalcQuantifier + -> Prepare + ( [Exact.ExactLocalId] + , Exact.ExactBinderContext + , Maybe (ScopedCheckedCore ObjectId) + ) +prepareCalculationScope context = \case + Nothing -> + pure ([], context, Nothing) + Just (Raw.CalcQuantifier variables bound suchThat) -> do + identities <- traverse (const allocateLocalIdentity) variables + calculationContext <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + (NonEmpty.zip identities variables) + context) + boundGuard <- + prepareSymbolicBoundConstraints + calculationContext variables bound + suchThatGuard <- + traverse + (fmap Exact.preparedExactPropositionCore + . prepareStatement calculationContext) + suchThat + calculationGuard <- + normalizeCalculationGuard + (boundGuard : maybeToList suchThatGuard) + pure (toList identities, calculationContext, calculationGuard) + +normalizeCalculationGuard + :: [ScopedCheckedCore ObjectId] + -> Prepare (Maybe (ScopedCheckedCore ObjectId)) +normalizeCalculationGuard guards = + foldM add Nothing guards + where + add accumulated constraint + | isScopedTruth constraint = pure accumulated + | otherwise = + case accumulated of + Nothing -> pure (Just constraint) + Just previous -> + Just + <$> maybe + (impossible + "checked calculation guards changed context") + pure + (conjoinScopedCore previous constraint) + + isScopedTruth proposition = + scopedCoreType proposition == TyProp + && scopedCoreTerm proposition == CImp CFalsum CFalsum + +finishCalculation + :: Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> CoreType + -> [Exact.ExactLocalId] + -> Maybe (ScopedCheckedCore ObjectId) + -> ScopedCheckedCore ObjectId + -> NonEmpty + ( Location + , ScopedCheckedCore ObjectId + , Raw.Justification + ) + -> Prepare PreparedCalculation +finishCalculation + fallback context locals operandType identities calculationGuard + first destinations = do + links <- prepareCalculationLinks first destinations + let finalEndpoint = preparedCalculationLinkDestination (NonEmpty.last links) + resultOpen <- + calculationEquality first finalEndpoint + result <- + closeCalculationProposition identities calculationGuard resultOpen + pure + (PreparedCheckedCalculation + operandType identities calculationGuard first links result) + where + prepareCalculationLinks previous (destination :| rest) = do + (next, firstLink) <- prepareCalculationLink previous destination + later <- prepareRemainingCalculationLinks next rest + pure (firstLink :| later) + + prepareRemainingCalculationLinks _previous [] = + pure [] + prepareRemainingCalculationLinks previous (destination : rest) = do + (next, link) <- prepareCalculationLink previous destination + (link :) <$> prepareRemainingCalculationLinks next rest + + prepareCalculationLink previous + (destinationLocation, destination, justification) = do + linkOpen <- calculationEquality previous destination + link <- closeCalculationProposition + identities calculationGuard linkOpen + discharge <- + prepareDischarge + (if destinationLocation == Nowhere + then fallback + else destinationLocation) + context + locals + link + justification + pure + ( destination + , PreparedCalculationLink destination discharge + ) + + calculationEquality left right = + maybe + (impossible + "checked calculation endpoints changed type or context") + pure + (equalScopedCore left right) + +closeCalculationProposition + :: [Exact.ExactLocalId] + -> Maybe (ScopedCheckedCore ObjectId) + -> ScopedCheckedCore ObjectId + -> Prepare (ScopedCheckedCore ObjectId) +closeCalculationProposition identities calculationGuard proposition = do + guarded <- + case calculationGuard of + Nothing -> pure proposition + Just constraint -> + maybe + (impossible + "a checked calculation guard changed context") + pure + (implyScopedCore constraint proposition) + pure (closeBinders (length identities) guarded) + where + closeBinders 0 closed = closed + closeBinders remaining open = + closeBinders (remaining - 1) + (fromMaybe + (impossible + "a checked calculation lost a quantified binder") + (closeScopedForall open)) + +preparedCalculationResult + :: PreparedCalculation + -> ScopedCheckedCore ObjectId +preparedCalculationResult + (PreparedCheckedCalculation + _operandType _identities _guard _first _links result) = + result + +preparedCalculationLinkDestination + :: PreparedCalculationLink + -> ScopedCheckedCore ObjectId +preparedCalculationLinkDestination + (PreparedCalculationLink destination _discharge) = + destination + +preparedCalculationLinkDischarge + :: PreparedCalculationLink + -> PreparedDischarge +preparedCalculationLinkDischarge + (PreparedCalculationLink _destination discharge) = + discharge + +preparedDischargeGoal + :: PreparedDischarge + -> ScopedCheckedCore ObjectId +preparedDischargeGoal = \case + PreparedVampireDischarge _location _justification goal _obligation -> + goal + PreparedSetExtensionality _location goal -> + goal + +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]) + RecursiveProofInduction + goal' + continuation -- The discharged existential and the opened witness premise are the same -- checked proposition viewed on opposite sides of existential elimination. @@ -846,6 +1831,21 @@ allocateLocal origin context proposition = do (Exact.exactBinderContextSupport context) proposition) +prepareConstructionFoundation + :: Prepare SetConstructionFoundation +prepareConstructionFoundation = do + familyUnion <- foundation FamilyUnionCharacteristic + separation <- foundation SeparationCharacteristic + replacement <- foundation ReplacementCharacteristic + setChoose <- foundation SetChooseWitness + pure + (setConstructionFoundation + familyUnion separation replacement setChoose) + where + foundation tag = + liftDriver + (Declaration.currentFoundationAxiomLowering tag) + prepareDischarge :: Location -> Exact.ExactBinderContext @@ -855,9 +1855,20 @@ prepareDischarge -> Prepare PreparedDischarge prepareDischarge location context locals goal justification = prepareDischargeWith - DirectDischarge + (dischargeModeFor goal) [] Nothing location context locals goal justification +-- A contradictory-axioms answer can establish falsum, but never an unrelated +-- proposition directly. Derive that distinction from the checked target so +-- every surface proof spelling reaches the same guarded request path. +dischargeModeFor :: ScopedCheckedCore ObjectId -> DischargeMode +dischargeModeFor goal + | scopedCoreType goal == TyProp + , scopedCoreTerm goal == CFalsum = + IndirectContradictionDischarge + | otherwise = + DirectDischarge + data DischargeMode = DirectDischarge | IndirectContradictionDischarge @@ -993,6 +2004,49 @@ prepareStatement context statement = (throwProof . ExactProofElaborationFailed) pure +validateStructuralComposition + :: Location + -> [ScopedCheckedCore ObjectId] + -> ( CheckedFoundation + -> (ObjectId -> Maybe CoreType) + -> Either KernelProof.KernelProofBuildError () + ) + -> Prepare () +validateStructuralComposition location propositions validate = do + foundation <- + liftDriver Declaration.currentFoundationLowering + let identities = + Set.toAscList + (Set.unions + ( canonicalTermGlobals . scopedCoreTerm + <$> propositions + )) + types <- + traverse + (\identity -> do + coreType <- + liftDriver + (Declaration.objectTypeLowering identity) + maybe + (impossible + "a checked structural proof lost a global object") + (\availableType -> pure (identity, availableType)) + coreType) + identities + either + (throwProof + . ExactProofStructuralCompositionFailed location) + pure + (validate foundation + (\identity -> Map.lookup identity (Map.fromList types))) + +structuralFailure :: Location -> Text -> Prepare value +structuralFailure location message = + throwProof + (ExactProofStructuralCompositionFailed + location + (KernelProof.ProofStructuralCompositionMismatch message)) + data CheckedExactProofAuthorization = CheckedExactProofAuthorization !PreparedProof !Bool @@ -1098,16 +2152,36 @@ preparedProofFirstOmission = \case preparedProofFirstOmission continuation PreparedTake _identities _witness _discharge continuation -> preparedProofFirstOmission continuation - PreparedSetInduction _hypothesis _discharge -> Nothing + PreparedSetInduction + (PreparedCheckedSetInduction + _focus _property _antecedents _target + _hypothesis _result child) -> + preparedProofFirstOmission child PreparedHave _claim _discharge continuation -> preparedProofFirstOmission continuation + PreparedSuffices _goal _reduction _implication _discharge continuation -> + preparedProofFirstOmission continuation + PreparedCalculate _calculation continuation -> + preparedProofFirstOmission continuation + PreparedSince _since _evidence _claim _discharge continuation -> + preparedProofFirstOmission continuation PreparedSubclaim _claim subproof continuation -> preparedProofFirstOmission subproof <|> preparedProofFirstOmission continuation PreparedDefine _identity _body _definition continuation -> preparedProofFirstOmission continuation + PreparedDefineRelational + _identity _body _functionality _definitions continuation -> + preparedProofFirstOmission continuation PreparedDefineFunction _identity _graph _definition continuation -> preparedProofFirstOmission continuation + PreparedByCase (PreparedCaseAnalysis _goal cases _exhaustive _discharge) -> + foldr + ((<|>) . preparedProofFirstOmission . preparedCaseProof) + Nothing + cases + PreparedByContradiction _goal _negation _falsum child -> + preparedProofFirstOmission child PreparedContradiction{} -> Nothing plannedProofRequests @@ -1123,17 +2197,41 @@ plannedProofRequests = \case plannedProofRequests continuation PreparedTake _identities _witness discharge continuation -> plannedDischargeRequests discharge <> plannedProofRequests continuation - PreparedSetInduction _hypothesis discharge -> - plannedDischargeRequests discharge + PreparedSetInduction + (PreparedCheckedSetInduction + _focus _property _antecedents _target + _hypothesis _result child) -> + plannedProofRequests child PreparedHave _claim discharge continuation -> plannedDischargeRequests discharge <> plannedProofRequests continuation + PreparedSuffices _goal _reduction _implication discharge continuation -> + plannedDischargeRequests discharge <> plannedProofRequests continuation + PreparedCalculate calculation continuation -> + plannedCalculationRequests calculation + <> plannedProofRequests continuation + PreparedSince _since evidence _claim discharge continuation -> + plannedSinceEvidenceRequests evidence + <> plannedDischargeRequests discharge + <> plannedProofRequests continuation PreparedSubclaim _claim subproof continuation -> plannedProofRequests subproof <> plannedProofRequests continuation PreparedDefine _identity _body _definition continuation -> plannedProofRequests continuation + PreparedDefineRelational + _identity _body functionality _definitions continuation -> + plannedDischargeRequests functionality + <> plannedProofRequests continuation PreparedDefineFunction _identity _graph _definition continuation -> plannedProofRequests continuation - PreparedContradiction discharge -> + PreparedByCase + (PreparedCaseAnalysis _goal cases _exhaustive discharge) -> + concatMap + (plannedProofRequests . preparedCaseProof) + (toList cases) + <> plannedDischargeRequests discharge + PreparedByContradiction _goal _negation _falsum child -> + plannedProofRequests child + PreparedContradiction _goal _falsum discharge -> plannedDischargeRequests discharge plannedDischargeRequests @@ -1144,6 +2242,24 @@ plannedDischargeRequests = \case [Declaration.checkedPlannedVampireRequest location obligation] PreparedSetExtensionality{} -> [] +plannedCalculationRequests + :: PreparedCalculation + -> [Declaration.CheckedPlannedVampireRequest] +plannedCalculationRequests + (PreparedCheckedCalculation + _operandType _identities _guard _first links _result) = + concatMap + (plannedDischargeRequests . preparedCalculationLinkDischarge) + (toList links) + +plannedSinceEvidenceRequests + :: PreparedSinceEvidence + -> [Declaration.CheckedPlannedVampireRequest] +plannedSinceEvidenceRequests = \case + PreparedSinceExisting{} -> [] + PreparedSinceDischarged discharge _local -> + plannedDischargeRequests discharge + executePreparedProof :: PreparedProof -> Declaration.CandidateProof () @@ -1161,19 +2277,45 @@ executePreparedProof = \case PreparedTake _identities _witness discharge continuation -> do executeDischarge discharge executePreparedProof continuation - PreparedSetInduction _hypothesis discharge -> - executeDischarge discharge + PreparedSetInduction + (PreparedCheckedSetInduction + _focus _property _antecedents _target + _hypothesis _result child) -> + executePreparedProof child PreparedHave _claim discharge continuation -> do executeDischarge discharge executePreparedProof continuation + PreparedSuffices goal reduction implication discharge continuation -> do + executeDischarge discharge + executePreparedProof continuation + unless + (implyScopedCore reduction goal == Just implication) + (impossible "a prepared suffices implication diverged") + PreparedCalculate calculation continuation -> do + executePreparedCalculation calculation + executePreparedProof continuation + PreparedSince sinceProposition evidence _claim discharge continuation -> do + executeSinceEvidence sinceProposition evidence + executeDischarge discharge + executePreparedProof continuation PreparedSubclaim _claim subproof continuation -> do executePreparedProof subproof executePreparedProof continuation PreparedDefine _identity _body _definition continuation -> executePreparedProof continuation + PreparedDefineRelational + _identity _body functionality _definitions continuation -> do + executeDischarge functionality + executePreparedProof continuation PreparedDefineFunction _identity _graph _definition continuation -> executePreparedProof continuation - PreparedContradiction discharge -> + PreparedByCase + (PreparedCaseAnalysis _goal cases _exhaustive discharge) -> do + traverse_ (executePreparedProof . preparedCaseProof) cases + executeDischarge discharge + PreparedByContradiction _goal _negation _falsum child -> + executePreparedProof child + PreparedContradiction _goal _falsum discharge -> executeDischarge discharge executeDischarge @@ -1187,6 +2329,39 @@ executeDischarge executeDischarge PreparedSetExtensionality{} = pure () +executePreparedCalculation + :: PreparedCalculation + -> Declaration.CandidateProof () +executePreparedCalculation + (PreparedCheckedCalculation + _operandType _identities _guard _first links _result) = + traverse_ + (executeDischarge . preparedCalculationLinkDischarge) + links + +executeSinceEvidence + :: ScopedCheckedCore ObjectId + -> PreparedSinceEvidence + -> Declaration.CandidateProof () +executeSinceEvidence proposition = \case + PreparedSinceExisting local -> + unless (preparedLocalProposition local == proposition) + (impossible "a structural since premise diverged") + PreparedSinceDischarged discharge local -> do + executeDischarge discharge + unless + ( preparedDischargeGoal discharge == proposition + && preparedLocalProposition local == proposition + ) + (impossible "a discharged since premise diverged") + +preparedLocalProposition + :: PreparedLocal + -> ScopedCheckedCore ObjectId +preparedLocalProposition + (PreparedLocal _ordinal _origin _support proposition) = + proposition + encodePreparedProof :: PreparedProof -> ByteString encodePreparedProof = encodeCache . putPreparedProof @@ -1220,28 +2395,72 @@ putPreparedProof = \case putScopedProposition witness putPreparedDischarge discharge putPreparedProof continuation - PreparedSetInduction hypothesis discharge -> do + PreparedSetInduction + (PreparedCheckedSetInduction + focus property antecedents target hypothesis result child) -> do putCacheTag 0x07 + putPreparedSetInductionFocus focus + putScopedProposition property + putCacheList putScopedProposition antecedents + putScopedProposition target putScopedProposition hypothesis - putPreparedDischarge discharge + putScopedProposition result + putPreparedProof child PreparedHave claim discharge continuation -> do putCacheTag 0x04 putScopedProposition claim putPreparedDischarge discharge putPreparedProof continuation + PreparedSuffices goal reduction implication discharge continuation -> do + putCacheTag 0x0c + putScopedProposition goal + putScopedProposition reduction + putScopedProposition implication + putPreparedDischarge discharge + putPreparedProof continuation + PreparedCalculate calculation continuation -> do + putCacheTag 0x0d + putPreparedCalculation calculation + putPreparedProof continuation + PreparedSince sinceProposition evidence claim discharge continuation -> do + putCacheTag 0x0e + putScopedProposition sinceProposition + putPreparedSinceEvidence evidence + 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 + PreparedDefine identity body definitions continuation -> do putCacheTag 0x09 putCacheNatural (Exact.exactLocalIdValue identity) putScopedTerm body - putScopedProposition definition + putCacheList putScopedProposition (toList definitions) + putPreparedProof continuation + PreparedDefineRelational + identity body functionality definitions continuation -> do + putCacheTag 0x11 + putCacheNatural (Exact.exactLocalIdValue identity) + putScopedTerm body + putPreparedDischarge functionality + putCacheList putScopedProposition (toList definitions) putPreparedProof continuation - PreparedContradiction discharge -> do + PreparedByCase caseAnalysis -> do + putCacheTag 0x0f + putPreparedCaseAnalysis caseAnalysis + PreparedByContradiction goal negation falsum child -> do + putCacheTag 0x10 + putScopedProposition goal + putScopedProposition negation + putScopedProposition falsum + putPreparedProof child + PreparedContradiction goal falsum discharge -> do putCacheTag 0x0a + putScopedProposition goal + putScopedProposition falsum putPreparedDischarge discharge PreparedDefineFunction identity graph definition continuation -> do putCacheTag 0x0b @@ -1250,6 +2469,18 @@ putPreparedProof = \case putScopedProposition definition putPreparedProof continuation +putPreparedSetInductionFocus + :: PreparedSetInductionFocus + -> CachePut +putPreparedSetInductionFocus = \case + PreparedInitialSetInductionFocus identity index -> do + putCacheTag 0x00 + putCacheNatural (Exact.exactLocalIdValue identity) + putCacheNatural index + PreparedLeadingSetInductionFocus identity -> do + putCacheTag 0x01 + putCacheNatural (Exact.exactLocalIdValue identity) + putPreparedDischarge :: PreparedDischarge -> CachePut putPreparedDischarge (PreparedVampireDischarge @@ -1268,6 +2499,55 @@ putPreparedDischargeSyntax justification goal = do putPreparedJustification justification putScopedProposition goal +putPreparedCalculation :: PreparedCalculation -> CachePut +putPreparedCalculation + (PreparedCheckedCalculation + operandType identities calculationGuard first links result) = do + putCoreTypeCache operandType + putCacheList + (putCacheNatural . Exact.exactLocalIdValue) + identities + putCacheMaybe putScopedProposition calculationGuard + putCacheList putScopedTerm + (first : (preparedCalculationLinkDestination <$> toList links)) + putCacheList putPreparedDischarge + (preparedCalculationLinkDischarge <$> toList links) + putScopedProposition result + +putPreparedSinceEvidence :: PreparedSinceEvidence -> CachePut +putPreparedSinceEvidence = \case + PreparedSinceExisting local -> do + putCacheTag 0x00 + putPreparedLocalEvidence local + PreparedSinceDischarged discharge local -> do + putCacheTag 0x01 + putPreparedDischarge discharge + putPreparedLocalEvidence local + +putPreparedCaseAnalysis :: PreparedCaseAnalysis -> CachePut +putPreparedCaseAnalysis + (PreparedCaseAnalysis goal cases exhaustive discharge) = do + putScopedProposition goal + putCacheList putPreparedCase (toList cases) + putScopedProposition exhaustive + putPreparedDischarge discharge + +putPreparedCase :: PreparedCase -> CachePut +putPreparedCase (PreparedCase assumption proof) = do + putScopedProposition assumption + putPreparedProof proof + +putPreparedLocalEvidence :: PreparedLocal -> CachePut +putPreparedLocalEvidence + (PreparedLocal ordinal _origin support proposition) = do + putCacheNatural (Backend.localPremiseOrdinalValue ordinal) + putCacheList + (\(identity, coreType) -> do + putCacheNatural (Exact.exactLocalIdValue identity) + putCoreTypeCache coreType) + (Vector.toList support) + putScopedProposition proposition + implicitAutoProofSyntaxId :: ScopedCheckedCore ObjectId -> ProofSyntaxId diff --git a/source/Checking/Exact/Vocabulary.hs b/source/Checking/Exact/Vocabulary.hs index 5701f64..45a2844 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 ) @@ -59,7 +68,7 @@ fixedSemanticVocabulary = (Raw.TokenCons (Raw.Command "emptyset") Raw.End) , FixedIntrinsic Empty ) - , ( expressionKey (unaryCommandPattern "unions") + , ( expressionKey (Raw.mixfixPattern Raw.UnionsSymbol) , FixedIntrinsic FamilyUnion ) , ( expressionKey (unaryCommandPattern "pow") @@ -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) |