summaryrefslogtreecommitdiff
path: root/source/Checking/Exact/Inductive.hs
diff options
context:
space:
mode:
Diffstat (limited to 'source/Checking/Exact/Inductive.hs')
-rw-r--r--source/Checking/Exact/Inductive.hs214
1 files changed, 180 insertions, 34 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
generated by cgit v1.2.3 (git 2.39.1) at 2026-08-06 10:18:05 +0000