diff options
Diffstat (limited to 'source/Checking/Exact/Inductive.hs')
| -rw-r--r-- | source/Checking/Exact/Inductive.hs | 838 |
1 files changed, 0 insertions, 838 deletions
diff --git a/source/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs deleted file mode 100644 index 441c773..0000000 --- a/source/Checking/Exact/Inductive.hs +++ /dev/null @@ -1,838 +0,0 @@ -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE NoImplicitPrelude #-} - --- | Exact preparation and atomic publication of direct set inductives. -module Checking.Exact.Inductive - ( PreparedExactInductive - , preparedExactInductiveCarrierId - , preparedExactInductiveCarrierType - , preparedExactInductiveCarrierBody - , preparedExactInductiveGuardTargets - , preparedExactInductiveFacts - , prepareExactInductive - , CheckedExactInductiveAuthorization - , lowerPreparedExactInductive - , authorizeCheckedExactInductive - , ExactInductiveError(..) - , exactInductiveErrorLocation - , renderExactInductiveError - ) where - -import Base hiding (Empty) -import Checking.Authority -import Checking.Core -import Checking.Declaration qualified as Declaration -import Checking.Exact.Global qualified as ExactGlobal -import Checking.Exact.Vocabulary -import Checking.Foundation -import Checking.Identity -import Checking.Semantic -import Checking.Typed.Inductive qualified as Typed -import Felix.Cache.Codec -import Felix.Meaning qualified as Meaning -import Report.Location -import Syntax.Abstract qualified as Raw -import Syntax.Interface -import 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 |