Prepare exact inductive declarations

1 files changed, 742 insertions, 0 deletions

diff --git a/source/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs
new file mode 100644
index 0000000..cbb29f0
--- /dev/null
+++ b/source/Checking/Exact/Inductive.hs
@@ -0,0 +1,742 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- | Exact preparation and atomic publication of direct set inductives.
+module Checking.Exact.Inductive
+    ( PreparedExactInductive
+    , preparedExactInductiveCarrierId
+    , preparedExactInductiveCarrierType
+    , preparedExactInductiveCarrierBody
+    , preparedExactInductiveGuardTargets
+    , preparedExactInductiveFacts
+    , prepareExactInductive
+    , commitPreparedExactInductive
+    , ExactInductiveError(..)
+    , exactInductiveErrorLocation
+    , renderExactInductiveError
+    ) where
+
+import Base hiding (Empty)
+import Checking.Authority
+import Checking.Core
+import Checking.Declaration qualified as Declaration
+import Checking.Foundation
+import Checking.Identity
+import Checking.Semantic
+import Checking.Typed.Inductive qualified as Typed
+import Felix.Cache.Codec
+import Meaning qualified
+import Report.Location
+import Syntax.Abstract qualified as Raw
+import Syntax.Interface
+import Syntax.Internal qualified as Internal
+import Syntax.Lexicon
+    ( pattern ConsSymbol
+    , pattern PairSymbol
+    )
+
+import Control.Monad (foldM, 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.Maybe (catMaybes)
+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]
+
+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
+    | ExactInductiveNestedRecursion !Location
+    | ExactInductiveGlobalAlreadyVisible !Location !SemanticGlobalKey
+    | ExactInductiveGlobalNotVisible !Location !Internal.Symbol
+    | ExactInductiveGlobalAmbiguous !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
+    ExactInductiveNestedRecursion location -> location
+    ExactInductiveGlobalAlreadyVisible location _key -> location
+    ExactInductiveGlobalNotVisible location _symbol -> location
+    ExactInductiveGlobalAmbiguous 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"
+            ExactInductiveNestedRecursion{} ->
+                "nested inductive recursion is not supported by the typed checker"
+            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
+            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 failure =
+    ExceptT
+        ExactInductiveError
+        (Declaration.ModuleDriver failure)
+
+prepareExactInductive
+    :: CheckedFoundation
+    -> Raw.Block
+    -> [CanonicalLexicalEntry]
+    -> Declaration.ModuleDriver failure
+        (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
+        visible <-
+            Except.lift
+                (Declaration.resolveVisibleGlobalDriver 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.currentTheoryDriver
+        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.objectAvailableDriver 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 failure 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))
+                | matchesCarrier carrier parameters recursiveCarrier ->
+                    Right
+                        (Typed.DirectRecursiveCondition recursiveTerm)
+                | otherwise ->
+                    Left
+                        (ExactInductiveNestedRecursion
+                            (termLocation recursiveCarrier))
+            _ ->
+                Left
+                    (ExactInductiveNestedRecursion
+                        (termLocation formula))
+
+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 failure
+        ( Map.Map
+            Internal.Symbol
+            (Typed.SourceGlobal ObjectId)
+        , Map.Map ObjectId CoreType
+        )
+resolveSourceGlobals location internal direct =
+    foldM resolve (Map.empty, Map.empty) symbols
+  where
+    carrier = Internal.SymbolMixfix (Internal.inductiveSymbol internal)
+    symbols =
+        Set.toAscList
+            ( Set.delete carrier
+                (directSymbols direct)
+                `Set.difference` fixedInductiveSymbols
+            )
+
+    resolve (resolved, types) symbol = do
+        let keys = semanticKeys symbol
+        when (null keys)
+            (Except.throwError
+                (ExactInductiveGlobalNotVisible location symbol))
+        matches <-
+            catMaybes
+                <$> traverse
+                    (Except.lift
+                        . Declaration.resolveVisibleGlobalContentDriver)
+                    keys
+        case matches of
+            [] ->
+                Except.throwError
+                    (ExactInductiveGlobalNotVisible location symbol)
+            [match] -> do
+                (source, sourceTypes) <-
+                    Except.liftEither
+                        (prepareSourceGlobal location match)
+                pure
+                    ( Map.insert symbol source resolved
+                    , Map.union sourceTypes types
+                    )
+            _ ->
+                Except.throwError
+                    (ExactInductiveGlobalAmbiguous location symbol)
+
+prepareSourceGlobal
+    :: Location
+    -> ( SemanticGlobalTarget
+       , ObjectContent
+       , Map.Map ObjectId CoreType
+       )
+    -> Either
+        ExactInductiveError
+        (Typed.SourceGlobal ObjectId, Map.Map ObjectId CoreType)
+prepareSourceGlobal location (target, content, dependencies) = do
+    body <-
+        case target of
+            GlobalReference _identity ->
+                Right Nothing
+            TransparentExpansion _identity ->
+                case content of
+                    TransparentObjectContent _theory _coreType canonical ->
+                        Just
+                            <$> first
+                                (ExactInductiveGlobalContentInvalid location)
+                                (checkCanonicalCore
+                                    (`Map.lookup` dependencies)
+                                    canonical)
+                    _ ->
+                        impossible
+                            "validated transparent expansion has opaque content"
+    let identity = semanticGlobalTargetObject target
+        types =
+            Map.insert
+                identity
+                (objectContentType content)
+                dependencies
+    pure (Typed.SourceGlobal identity body, types)
+
+resolveGuard
+    :: Location
+    -> FrozenCheckedCore ObjectId
+    -> Prepare failure SemanticFactOccurrenceFingerprint
+resolveGuard location target = do
+    matches <-
+        Except.lift
+            (Declaration.resolveVisibleFactTargetsDriver 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 ->
+            Internal.mentionedSymbols term
+
+fixedInductiveSymbols :: Set.Set Internal.Symbol
+fixedInductiveSymbols =
+    Set.fromList
+        [ Internal.SymbolMixfix ConsSymbol
+        , Internal.SymbolMixfix PairSymbol
+        , Internal.SymbolMixfix (unarySymbol "pow")
+        , Internal.SymbolMixfix (unarySymbol "cumul")
+        , Internal.SymbolPredicate
+            (Internal.PredicateRelation Raw.ElementSymbol)
+        , Internal.SymbolPredicate
+            (Internal.PredicateRelation Raw.EqSymbol)
+        , Internal.SymbolPredicate
+            (Internal.PredicateRelation Raw.NeqSymbol)
+        , Internal.SymbolPredicate
+            (Internal.PredicateRelation Raw.SubseteqSymbol)
+        ]
+  where
+    unarySymbol command =
+        Raw.MixfixItem
+            (Raw.TokenCons (Raw.Command command)
+                (Raw.TokenCons Raw.InvisibleBraceL
+                    (Raw.HoleCons
+                        (Raw.TokenCons Raw.InvisibleBraceR Raw.End))))
+            (Raw.Marker command)
+            Raw.NonAssoc
+
+semanticKeys :: Internal.Symbol -> [SemanticGlobalKey]
+semanticKeys = \case
+    Internal.SymbolMixfix symbol ->
+        [SemanticExpressionFunction (Raw.mixfixPattern symbol)]
+    Internal.SymbolFun item ->
+        let patterns = Raw.lexicalItemSgPlPattern item
+        in [SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns)]
+    Internal.SymbolPredicate predicate ->
+        case predicate of
+            Internal.PredicateAdj item ->
+                [ SemanticLeftAdjective (Raw.lexicalItemPattern item)
+                , SemanticRightAdjective (Raw.lexicalItemPattern item)
+                ]
+            Internal.PredicateVerb item ->
+                let patterns = Raw.lexicalItemSgPlPattern item
+                in [SemanticVerb (Raw.sg patterns) (Raw.pl patterns)]
+            Internal.PredicateNoun item ->
+                let patterns = Raw.lexicalItemSgPlPattern item
+                in [SemanticNoun (Raw.sg patterns) (Raw.pl patterns)]
+            Internal.PredicateRelation relation ->
+                [ SemanticRelation
+                    (Raw.relationSymbolToken relation)
+                    (Raw.relationSymbolParameterArity relation)
+                ]
+            Internal.PredicateSymbol{} -> []
+            Internal.PredicateNounStruct{} -> []
+    Internal.SymbolInteger{} -> []
+
+commitPreparedExactInductive
+    :: PreparedExactInductive
+    -> Declaration.ModuleDriver failure
+        ((), Declaration.CommittedDeclarationBatch)
+commitPreparedExactInductive
+        (PreparedExactInductive
+            _location key identity asserted alias syntax typed guards) =
+    Declaration.commitCompiledDeclaration syntax do
+        traverse_ Declaration.addDeclarationObject asserted
+        Declaration.stageSemanticGlobalBinding
+            key
+            (GlobalReference identity)
+        let facts = Typed.typedInductiveFacts typed
+            candidateInputs =
+                fmap
+                    (\fact ->
+                        ( embedClosedCore []
+                            (Typed.typedInductiveFactTarget fact)
+                        , SearchEligible
+                        , [markerAlias
+                            (Typed.typedInductiveFactMarker fact)]
+                        ))
+                    facts
+        (definitionCandidate, factCandidates) <-
+            Declaration.reserveDefinitionEquationCandidateBatch
+                identity
+                alias
+                candidateInputs
+        Declaration.authorizeCompiledDeclaration do
+            Declaration.authorizeDefinitionEquationCandidate
+                identity
+                definitionCandidate
+            sequence_
+                (NonEmpty.zipWith
+                    authorizeFact
+                    factCandidates
+                    facts)
+  where
+    authorizeFact candidate fact =
+        Declaration.authorizeKernelConstructionCandidate
+            (GuardedFoundationRule
+                (Typed.typedInductiveFactRule fact))
+            candidate do
+                traverse_ Declaration.useAuthorizedFact guards
+                pure (Typed.typedInductiveFactDerivation fact)
+
+    markerAlias (Raw.Marker name) =
+        semanticName name
+
+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))
+        putCacheText (semanticNameText alias)
+        putCacheList putFact
+            (toList (Typed.typedInductiveFacts typed))
+  where
+    putFact fact = do
+        let Raw.Marker marker =
+                Typed.typedInductiveFactMarker fact
+        putCacheText marker
+        putCanonicalTermCache putObjectIdCache
+            (frozenCoreTerm
+                (Typed.typedInductiveFactTarget fact))
+        putCacheBytes
+            (encodeKernelRuleTag
+                (Typed.typedInductiveFactRule 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 = \case
+    Internal.TermVar variable -> locate variable
+    Internal.TermSymbol location _symbol _arguments -> location
+    Internal.TermSymbolStruct _symbol expression ->
+        maybe Nowhere termLocation expression
+    Internal.Apply function _arguments -> termLocation function
+    Internal.TermSep variable _bound _predicate -> locate variable
+    Internal.ReplacePred value _domain _bound _predicate -> locate value
+    Internal.ReplaceFun ((variable, _domain) :| _remaining) _value _condition ->
+        locate variable
+    Internal.Connected _connective left _right -> termLocation left
+    Internal.Lambda{} -> Nowhere
+    Internal.Quantified{} -> Nowhere
+    Internal.PropositionalConstant{} -> Nowhere
+    Internal.Not location _term -> location