diff options
Diffstat (limited to 'source/Felix/Checking/Exact/Inductive.hs')
| -rw-r--r-- | source/Felix/Checking/Exact/Inductive.hs | 838 |
1 files changed, 838 insertions, 0 deletions
diff --git a/source/Felix/Checking/Exact/Inductive.hs b/source/Felix/Checking/Exact/Inductive.hs new file mode 100644 index 0000000..5817b34 --- /dev/null +++ b/source/Felix/Checking/Exact/Inductive.hs @@ -0,0 +1,838 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Exact preparation and atomic publication of direct set inductives. +module Felix.Checking.Exact.Inductive + ( PreparedExactInductive + , preparedExactInductiveCarrierId + , preparedExactInductiveCarrierType + , preparedExactInductiveCarrierBody + , preparedExactInductiveGuardTargets + , preparedExactInductiveFacts + , prepareExactInductive + , CheckedExactInductiveAuthorization + , lowerPreparedExactInductive + , authorizeCheckedExactInductive + , ExactInductiveError(..) + , exactInductiveErrorLocation + , renderExactInductiveError + ) where + +import Base hiding (Empty) +import Felix.Checking.Authority +import Felix.Checking.Core +import Felix.Checking.Declaration qualified as Declaration +import Felix.Checking.Exact.Global qualified as ExactGlobal +import Felix.Checking.Exact.Vocabulary +import Felix.Checking.Foundation +import Felix.Checking.Identity +import Felix.Checking.Semantic +import Felix.Checking.Typed.Inductive qualified as Typed +import Felix.Cache.Codec +import Felix.Meaning qualified as Meaning +import Felix.Report.Location +import Felix.Syntax.Abstract qualified as Raw +import Felix.Syntax.Interface +import Felix.Syntax.Internal qualified as Internal + +import Control.Monad (unless, when) +import Control.Monad.Except (ExceptT) +import Control.Monad.Except qualified as Except +import Data.Bifunctor (first) +import Data.ByteString (ByteString) +import Data.List qualified as List +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 qualified as Vector + + +data PreparedExactInductive = PreparedExactInductive + !Location + !SemanticGlobalKey + !ObjectId + !(Maybe AssertedObject) + !SemanticName + !DeclarationSyntaxId + !(Typed.PreparedTypedInductive ObjectId) + ![SemanticFactOccurrenceFingerprint] + +data CheckedExactInductiveAuthorization = + CheckedExactInductiveAuthorization + !ObjectId + !(Typed.PreparedTypedInductive ObjectId) + ![SemanticFactOccurrenceFingerprint] + ![(Location, Declaration.PreparedVampireObligation Void ())] + +preparedExactInductiveCarrierId + :: PreparedExactInductive + -> ObjectId +preparedExactInductiveCarrierId + (PreparedExactInductive + _location _key identity _asserted _alias _syntax _typed _guards) = + identity + +preparedExactInductiveCarrierType + :: PreparedExactInductive + -> CoreType +preparedExactInductiveCarrierType + (PreparedExactInductive + _location _key _identity _asserted _alias _syntax typed _guards) = + Typed.typedInductiveCarrierType typed + +preparedExactInductiveCarrierBody + :: PreparedExactInductive + -> FrozenCheckedCore ObjectId +preparedExactInductiveCarrierBody + (PreparedExactInductive + _location _key _identity _asserted _alias _syntax typed _guards) = + Typed.typedInductiveCarrierBody typed + +preparedExactInductiveGuardTargets + :: PreparedExactInductive + -> Vector.Vector (FrozenCheckedCore ObjectId) +preparedExactInductiveGuardTargets + (PreparedExactInductive + _location _key _identity _asserted _alias _syntax typed _guards) = + Typed.typedInductiveGuardTargets typed + +preparedExactInductiveFacts + :: PreparedExactInductive + -> NonEmpty (Typed.PreparedTypedInductiveFact ObjectId) +preparedExactInductiveFacts + (PreparedExactInductive + _location _key _identity _asserted _alias _syntax typed _guards) = + Typed.typedInductiveFacts typed + +data ExactInductiveError + = ExactInductiveUnsupportedBlock !Location + | ExactInductiveOccurrenceMissing !Location + | ExactInductiveOccurrenceAmbiguous !Location + | ExactInductiveHeadMismatch !Location + | ExactInductiveGlossFailed !Location !Meaning.GlossError + | ExactInductiveDuplicateParameter !Location !Internal.VarSymbol + | ExactInductiveDomainFreeVariable !Location !Internal.VarSymbol + | ExactInductiveDomainMentionsCarrier !Location + | ExactInductiveResultShape !Location + | ExactInductiveResultMentionsCarrier !Location + | ExactInductiveRecursiveTermMentionsCarrier !Location + | ExactInductiveRecursiveCarrierWrongArguments !Location + | ExactInductiveRecursiveCarrierOutsideMembership !Location + | ExactInductiveUnsupportedRecursiveCarrierContext !Location + | ExactInductiveFixedSemanticCollision !Location !SemanticGlobalKey + | ExactInductiveGlobalAlreadyVisible !Location !SemanticGlobalKey + | ExactInductiveGlobalNotVisible !Location !Internal.Symbol + | ExactInductiveGlobalAmbiguous !Location !Internal.Symbol + | ExactInductiveUnsupportedSymbol !Location !Internal.Symbol + | ExactInductiveGlobalContentInvalid !Location !CoreCheckError + | ExactInductivePreparationFailed + !Location + !Typed.TypedInductiveError + | ExactInductiveGuardMissing !Location + | ExactInductiveGuardAmbiguous !Location + deriving stock (Show, Eq) + +exactInductiveErrorLocation :: ExactInductiveError -> Location +exactInductiveErrorLocation = \case + ExactInductiveUnsupportedBlock location -> location + ExactInductiveOccurrenceMissing location -> location + ExactInductiveOccurrenceAmbiguous location -> location + ExactInductiveHeadMismatch location -> location + ExactInductiveGlossFailed location _failure -> location + ExactInductiveDuplicateParameter location _parameter -> location + ExactInductiveDomainFreeVariable location _variable -> location + ExactInductiveDomainMentionsCarrier location -> location + ExactInductiveResultShape location -> location + ExactInductiveResultMentionsCarrier location -> location + ExactInductiveRecursiveTermMentionsCarrier location -> location + ExactInductiveRecursiveCarrierWrongArguments location -> location + ExactInductiveRecursiveCarrierOutsideMembership location -> location + ExactInductiveUnsupportedRecursiveCarrierContext location -> location + ExactInductiveFixedSemanticCollision location _key -> location + ExactInductiveGlobalAlreadyVisible location _key -> location + ExactInductiveGlobalNotVisible location _symbol -> location + ExactInductiveGlobalAmbiguous location _symbol -> location + ExactInductiveUnsupportedSymbol location _symbol -> location + ExactInductiveGlobalContentInvalid location _failure -> location + ExactInductivePreparationFailed location _failure -> location + ExactInductiveGuardMissing location -> location + ExactInductiveGuardAmbiguous location -> location + +renderExactInductiveError :: ExactInductiveError -> Text +renderExactInductiveError failure = + locationToText (exactInductiveErrorLocation failure) + <> ": " + <> case failure of + ExactInductiveUnsupportedBlock{} -> + "this inductive source form is not supported by the typed checker" + ExactInductiveOccurrenceMissing{} -> + "the inductive declaration has no associated syntax occurrence" + ExactInductiveOccurrenceAmbiguous{} -> + "the inductive declaration has more than one semantic head" + ExactInductiveHeadMismatch{} -> + "the inductive head does not match its syntax occurrence" + ExactInductiveGlossFailed _location glossFailure -> + "inductive elaboration failed: " <> shown glossFailure + ExactInductiveDuplicateParameter _location parameter -> + "the inductive parameter is repeated: " <> shown parameter + ExactInductiveDomainFreeVariable _location variable -> + "the inductive domain contains an unbound variable: " + <> shown variable + ExactInductiveDomainMentionsCarrier{} -> + "the inductive domain must be independent of its carrier" + ExactInductiveResultShape{} -> + "an inductive result must have the form t \\in F(args)" + ExactInductiveResultMentionsCarrier{} -> + "an inductive result term must not mention its carrier" + ExactInductiveRecursiveTermMentionsCarrier{} -> + "a recursive occurrence must be in the carrier of a membership premise" + 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 + ExactInductiveGlobalAlreadyVisible _location key -> + "the inductive carrier is already visible: " <> shown key + ExactInductiveGlobalNotVisible _location symbol -> + "an inductive source symbol is not visible: " <> shown symbol + ExactInductiveGlobalAmbiguous _location symbol -> + "an inductive source symbol has more than one meaning: " + <> shown symbol + ExactInductiveUnsupportedSymbol _location symbol -> + "this inductive source symbol is not supported: " + <> shown symbol + ExactInductiveGlobalContentInvalid _location coreFailure -> + "an inductive global has invalid checked content: " + <> shown coreFailure + ExactInductivePreparationFailed _location typedFailure -> + "typed inductive preparation failed: " <> shown typedFailure + ExactInductiveGuardMissing{} -> + "an inductive domain guard has no visible authorized fact" + ExactInductiveGuardAmbiguous{} -> + "an inductive domain guard matches more than one visible fact" + where + shown :: Show value => value -> Text + shown = Text.pack . show + +type Prepare = + ExceptT + ExactInductiveError + (Declaration.LoweringDriver) + +prepareExactInductive + :: CheckedFoundation + -> Raw.Block + -> [CanonicalLexicalEntry] + -> Declaration.LoweringDriver + (Either ExactInductiveError PreparedExactInductive) +prepareExactInductive foundation block entries = + Except.runExceptT do + (location, marker, rawInductive) <- + case block of + Raw.BlockInductive blockLocation _title blockMarker inductive -> + pure (blockLocation, blockMarker, inductive) + _ -> + Except.throwError + (ExactInductiveUnsupportedBlock (locate block)) + key <- validateOccurrence location rawInductive entries + when + (isJust (fixedSemanticMeaning key)) + (Except.throwError + (ExactInductiveFixedSemanticCollision location key)) + visible <- + Except.lift + (Declaration.resolveVisibleGlobalLowering key) + when (isJust visible) + (Except.throwError + (ExactInductiveGlobalAlreadyVisible location key)) + internal <- + case Meaning.meaning [block] of + Right + [Internal.BlockInductive + _internalLocation _internalMarker inductive] -> + pure inductive + Left failure -> + Except.throwError + (ExactInductiveGlossFailed location failure) + Right _ -> + Except.throwError + (ExactInductiveUnsupportedBlock location) + direct <- + Except.liftEither + (normalizeDirectInductive internal) + (sourceGlobals, globalTypes) <- + resolveSourceGlobals location internal direct + typed <- + Except.liftEither + (first + (ExactInductivePreparationFailed location) + (Typed.prepareTypedInductive + (requireGlobalType globalTypes) + foundation + (`Map.lookup` sourceGlobals) + marker + direct)) + guards <- + traverse + (resolveGuard location) + (Vector.toList + (Typed.typedInductiveGuardTargets typed)) + theory <- Except.lift Declaration.currentTheoryLowering + let carrierType = Typed.typedInductiveCarrierType typed + carrierBody = Typed.typedInductiveCarrierBody typed + carrierTerm = frozenCoreTerm carrierBody + identity = + transparentObjectId theory carrierType carrierTerm + content = + TransparentObjectContent theory carrierType carrierTerm + alias = case marker of + Raw.Marker name -> semanticName name + available <- + Except.lift + (Declaration.objectAvailableLowering identity) + let asserted + | available = Nothing + | otherwise = Just (assertedObject identity content) + syntax = + declarationSyntaxId + (encodePreparedInductive key alias typed) + pure + (PreparedExactInductive + location + key + identity + asserted + alias + syntax + typed + guards) + where + requireGlobalType types identity = + fromMaybe + (impossible + "prepared inductive global has no checked type") + (Map.lookup identity types) + +validateOccurrence + :: Location + -> Raw.Inductive + -> [CanonicalLexicalEntry] + -> Prepare SemanticGlobalKey +validateOccurrence location rawInductive entries = do + entry <- + case entries of + [] -> + Except.throwError + (ExactInductiveOccurrenceMissing location) + [single] -> pure single + _ -> + Except.throwError + (ExactInductiveOccurrenceAmbiguous location) + key <- + maybe + (Except.throwError + (ExactInductiveHeadMismatch location)) + pure + (semanticGlobalKeyFromLexicalEntry entry) + let Raw.SymbolPattern headSymbol _parameters = + Raw.inductiveSymbolPattern rawInductive + expected = + SemanticExpressionFunction + (Raw.mixfixPattern headSymbol) + unless (key == expected) + (Except.throwError + (ExactInductiveHeadMismatch location)) + pure key + +normalizeDirectInductive + :: Internal.Inductive + -> Either ExactInductiveError Typed.DirectInductive +normalizeDirectInductive inductive = do + case firstDuplicate (Internal.inductiveParams inductive) of + Just duplicate -> + Left + (ExactInductiveDuplicateParameter + (locate duplicate) + duplicate) + Nothing -> pure () + let parameters = Internal.inductiveParams inductive + parameterSet = Set.fromList parameters + domain = Internal.inductiveDomain inductive + carrier = Internal.inductiveSymbol inductive + domainVariables = + orderedUnique + (toList domain) + case find (`Set.notMember` parameterSet) domainVariables of + Just variable -> + Left + (ExactInductiveDomainFreeVariable + (locate variable) + variable) + Nothing -> pure () + when + (Internal.SymbolMixfix carrier + `Set.member` Internal.mentionedSymbols domain) + (Left + (ExactInductiveDomainMentionsCarrier + (termLocation domain))) + clauses <- + traverse + (normalizeClause carrier parameters) + (Internal.inductiveIntros inductive) + pure + (Typed.DirectInductive + parameters + domain + clauses) + +normalizeClause + :: Internal.FunctionSymbol + -> [Internal.VarSymbol] + -> Internal.IntroRule + -> Either ExactInductiveError Typed.DirectInductiveClause +normalizeClause carrier parameters rule = do + conditions <- + traverse + (normalizeCondition carrier parameters) + (Internal.introConditions rule) + result <- + normalizeResult + carrier + parameters + (Internal.introResult rule) + let parameterSet = Set.fromList parameters + variables = + List.filter (`Set.notMember` parameterSet) + (orderedUnique + ( concatMap toList + (Internal.introConditions rule) + <> toList result + )) + pure + (Typed.DirectInductiveClause + variables + conditions + result) + +normalizeResult + :: Internal.FunctionSymbol + -> [Internal.VarSymbol] + -> Internal.Formula + -> Either ExactInductiveError Internal.Term +normalizeResult carrier parameters = \case + Internal.IsElementOf _location result target + | not (matchesCarrier carrier parameters target) -> + Left (ExactInductiveResultShape (termLocation target)) + | Internal.SymbolMixfix carrier + `Set.member` Internal.mentionedSymbols result -> + Left + (ExactInductiveResultMentionsCarrier + (termLocation result)) + | otherwise -> + Right result + formula -> + Left (ExactInductiveResultShape (termLocation formula)) + +normalizeCondition + :: Internal.FunctionSymbol + -> [Internal.VarSymbol] + -> Internal.Formula + -> Either ExactInductiveError Typed.DirectInductiveCondition +normalizeCondition carrier parameters formula + | not + (Internal.SymbolMixfix carrier + `Set.member` Internal.mentionedSymbols formula) = + Right (Typed.DirectSideCondition formula) + | otherwise = + case formula of + Internal.IsElementOf _location recursiveTerm recursiveCarrier + | Internal.SymbolMixfix carrier + `Set.member` + Internal.mentionedSymbols recursiveTerm -> + Left + (ExactInductiveRecursiveTermMentionsCarrier + (termLocation recursiveTerm)) + | otherwise -> do + context <- + first recursiveCarrierContextError + (Typed.prepareRecursiveCarrierContext + carrier parameters recursiveCarrier) + Right + (Typed.DirectRecursiveCondition + recursiveTerm context) + _ -> + Left + (ExactInductiveRecursiveCarrierOutsideMembership + (termLocation formula)) + +recursiveCarrierContextError + :: Typed.RecursiveCarrierContextError + -> ExactInductiveError +recursiveCarrierContextError = \case + Typed.RecursiveCarrierWrongArguments location -> + ExactInductiveRecursiveCarrierWrongArguments location + Typed.RecursiveCarrierUnsupportedContext location -> + ExactInductiveUnsupportedRecursiveCarrierContext location + +matchesCarrier + :: Internal.FunctionSymbol + -> [Internal.VarSymbol] + -> Internal.Term + -> Bool +matchesCarrier carrier parameters = \case + Internal.TermSymbol _location (Internal.SymbolMixfix actual) arguments -> + actual == carrier + && length arguments == length parameters + && and + (zipWith + (\argument parameter -> + argument == Internal.TermVar parameter) + arguments + parameters) + _ -> False + +resolveSourceGlobals + :: Location + -> Internal.Inductive + -> Typed.DirectInductive + -> Prepare + ( Map.Map + Internal.Symbol + (Typed.SourceGlobal ObjectId) + , Map.Map ObjectId CoreType + ) +resolveSourceGlobals location internal direct = + Except.lift + (ExactGlobal.resolveExactSourceGlobals symbols) + >>= Except.liftEither + . first (exactGlobalError location) + where + carrier = Internal.SymbolMixfix (Internal.inductiveSymbol internal) + symbols = + Set.delete carrier (directSymbols direct) + +exactGlobalError + :: Location + -> ExactGlobal.ExactGlobalResolutionError + -> ExactInductiveError +exactGlobalError location = \case + ExactGlobal.ExactGlobalNotVisible symbol -> + ExactInductiveGlobalNotVisible location symbol + ExactGlobal.ExactGlobalAmbiguous symbol -> + ExactInductiveGlobalAmbiguous location symbol + ExactGlobal.ExactGlobalUnsupported symbol -> + ExactInductiveUnsupportedSymbol location symbol + ExactGlobal.ExactGlobalContextualUnsupported symbol -> + ExactInductiveUnsupportedSymbol location symbol + ExactGlobal.ExactGlobalContentInvalid failure -> + ExactInductiveGlobalContentInvalid location failure + +resolveGuard + :: Location + -> FrozenCheckedCore ObjectId + -> Prepare SemanticFactOccurrenceFingerprint +resolveGuard location target = do + matches <- + Except.lift + (Declaration.resolveVisibleFactTargetsLowering target) + case matches of + [] -> + Except.throwError (ExactInductiveGuardMissing location) + [fingerprint] -> + pure fingerprint + _ -> + Except.throwError (ExactInductiveGuardAmbiguous location) + +directSymbols :: Typed.DirectInductive -> Set.Set Internal.Symbol +directSymbols direct = + Internal.mentionedSymbols (Typed.directInductiveDomain direct) + <> foldMap clauseSymbols + (Typed.directInductiveClauses direct) + where + clauseSymbols clause = + foldMap conditionSymbols + (Typed.directClauseConditions clause) + <> Internal.mentionedSymbols + (Typed.directClauseResult clause) + conditionSymbols = \case + Typed.DirectSideCondition formula -> + Internal.mentionedSymbols formula + Typed.DirectRecursiveCondition term context -> + Internal.mentionedSymbols term + <> Typed.recursiveCarrierContextSymbols context + +lowerPreparedExactInductive + :: PreparedExactInductive + -> Declaration.LoweringDriver + (Either + Declaration.DeclarationError + (Declaration.CheckedDeclaration + CheckedExactInductiveAuthorization)) +lowerPreparedExactInductive + (PreparedExactInductive + _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 -> do + prepared <- + Declaration.prepareCandidateSpecLowering + objects + (embedClosedCore [] + (Typed.typedInductiveFactTarget fact)) + SearchEligible + [markerAlias + (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 + objects + [] + [semanticGlobalBinding key (GlobalReference identity)] + [] + stages + (CheckedExactInductiveAuthorization + identity typed guards + (snd <$> monotonicityCandidates))) + where + markerAlias (Raw.Marker name) = + semanticName name + +authorizeCheckedExactInductive + :: CheckedExactInductiveAuthorization + -> [NonEmpty Declaration.ReservedCandidate] + -> Declaration.Declaration () +authorizeCheckedExactInductive + (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 + case NonEmpty.nonEmpty candidates of + Just factCandidates + | NonEmpty.length factCandidates == NonEmpty.length facts -> + sequence_ + (NonEmpty.zipWith + (authorizeFact []) + factCandidates + facts) + _ -> + Declaration.failDeclaration + (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 + (if null monotonicityObligations then 1 else 3) + (length stages)) + where + 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 + -> Typed.PreparedTypedInductive ObjectId + -> ByteString +encodePreparedInductive key alias typed = + encodeCache do + putCacheTag 0x04 + putSemanticGlobalKeyCache key + putCoreTypeCache + (Typed.typedInductiveCarrierType 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 + putCacheText marker + putCanonicalTermCache putObjectIdCache + (frozenCoreTerm + (Typed.typedInductiveFactTarget fact)) + putCacheList + (putCacheBytes . encodeKernelRuleTag) + (toList (Typed.typedInductiveFactRules fact)) + +firstDuplicate :: Ord value => [value] -> Maybe value +firstDuplicate = + go Set.empty + where + go _seen [] = Nothing + go seen (value : remaining) + | value `Set.member` seen = Just value + | otherwise = + go (Set.insert value seen) remaining + +orderedUnique :: Ord value => [value] -> [value] +orderedUnique = + reverse . snd . foldl' step (Set.empty, []) + where + step (seen, values) value + | value `Set.member` seen = (seen, values) + | otherwise = + (Set.insert value seen, value : values) + +termLocation :: Internal.Expr -> Location +termLocation = Internal.exprLocation |