path: root/source/Checking/Exact.hs

{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE NoImplicitPrelude #-}

-- | Direct compiler for the first exact monomorphic declaration family.
module Checking.Exact
    ( ExactLocalId
    , exactLocalId
    , exactLocalIdValue
    , ExactBinderContext
    , emptyExactBinderContext
    , extendExactBinderContext
    , extendExactAnonymousBinderContext
    , exactBinderContextSupport
    , exactBinderContextIndex
    , PreparedExactProposition
    , preparedExactPropositionCore
    , prepareExactProposition
    , prepareExactSymbolicBoundConstraints
    , prepareExactSymbolicWitnessConstraints
    , prepareExactNounWitnessConstraints
    , PreparedExactSetExpression
    , preparedExactSetExpressionCore
    , prepareExactSetExpression
    , PreparedExactLocalFunctionGraph
    , preparedExactLocalFunctionGraphCore
    , preparedExactLocalFunctionGraphDomain
    , preparedExactLocalFunctionGraphMap
    , prepareExactLocalFunctionGraph
    , PreparedExactClaimEnvelope
    , preparedExactClaimTarget
    , preparedExactClaimVariables
    , preparedExactClaimContext
    , preparedExactClaimAntecedentCount
    , prepareExactClaimEnvelope
    , PreparedExactDeclaration
    , preparedExactLocation
    , preparedExactGlobalKey
    , preparedExactObjectId
    , preparedExactObject
    , preparedExactSyntaxId
    , preparedExactIsDefinition
    , prepareExactDeclaration
    , lowerPreparedExactBinding
    , authorizeCheckedExactBinding
    , PreparedExactStructure
    , prepareExactStructure
    , CheckedExactStructureAuthorization
    , lowerPreparedExactStructure
    , authorizeCheckedExactStructure
    , PreparedExactSourceAxiom
    , prepareExactSourceAxiom
    , lowerPreparedExactSourceAxiom
    , authorizeCheckedExactSourceAxiom
    , ExactCompileError(..)
    , exactCompileErrorLocation
    , renderExactCompileError
    ) where

import Base hiding (Empty)
import Checking.Core
import Checking.Declaration qualified as Declaration
import Checking.Exact.Vocabulary
import Checking.Identity
import Checking.Semantic
import Felix.Cache.Codec
import Felix.Module
import Report.Location
import Syntax.Abstract qualified as Raw
import Syntax.Interface (CanonicalLexicalEntry(..))
import Syntax.Lexicon qualified as Lexicon

import Control.Monad.Except (ExceptT)
import Control.Monad.Except (MonadError, throwError)
import Control.Monad.Except qualified as Except
import Control.Monad (foldM, unless, when)
import Control.Monad.State.Strict (StateT)
import Control.Monad.State.Strict qualified as State
import Data.ByteString (ByteString)
import Data.Bifunctor (first)
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 (Vector)
import Data.Vector qualified as Vector
import Numeric.Natural (Natural)


-- | A disposable identity allocated in source order within one proof.
newtype ExactLocalId = ExactLocalId Natural
    deriving stock (Show, Eq, Ord)

exactLocalId :: Natural -> ExactLocalId
exactLocalId = ExactLocalId

exactLocalIdValue :: ExactLocalId -> Natural
exactLocalIdValue (ExactLocalId value) = value

data ExactBinder = ExactBinder
    !ExactLocalId
    !(Maybe Raw.VarSymbol)
    !CoreType
    !(Maybe ExactStructureAnnotation)

data ExactStructureAnnotation = ExactStructureAnnotation
    !SemanticStructurePhrase
    !(Maybe ObjectId)
    !(Map.Map Raw.StructSymbol ObjectId)

-- | The active nearest-first binders of one exact proof scope.
newtype ExactBinderContext = ExactBinderContext [ExactBinder]

emptyExactBinderContext :: ExactBinderContext
emptyExactBinderContext = ExactBinderContext []

extendExactBinderContext
    :: NonEmpty (ExactLocalId, Raw.VarSymbol)
    -> ExactBinderContext
    -> Either ExactCompileError ExactBinderContext
extendExactBinderContext additions (ExactBinderContext initial) =
    ExactBinderContext <$> foldM add initial (toList additions)
  where
    add binders (identity, variable)
        | any (sameVariable variable) binders =
            Left (ExactDuplicateLocalBinder (locate variable) variable)
        | any (sameIdentity identity) binders =
            Left (ExactDuplicateLocalIdentity (locate variable) identity)
        | otherwise =
            Right (ExactBinder identity (Just variable) TySet Nothing : binders)

    sameVariable variable (ExactBinder _identity existing _coreType _structure) =
        existing == Just variable

    sameIdentity identity (ExactBinder existing _variable _coreType _structure) =
        existing == identity

-- | Add one proof-owned binder which deliberately has no source-resolvable
-- spelling.  This is used for a nameless singular witness; it participates in
-- checked support and de Bruijn weakening but cannot shadow or be looked up by
-- a later source variable.
extendExactAnonymousBinderContext
    :: ExactLocalId
    -> ExactBinderContext
    -> Either ExactCompileError ExactBinderContext
extendExactAnonymousBinderContext identity (ExactBinderContext binders)
    | any sameIdentity binders =
        Left (ExactDuplicateLocalIdentity Nowhere identity)
    | otherwise =
        Right
            (ExactBinderContext
                (ExactBinder identity Nothing TySet Nothing : binders))
  where
    sameIdentity (ExactBinder existing _variable _coreType _structure) =
        existing == identity

exactBinderContextSupport
    :: ExactBinderContext
    -> Vector (ExactLocalId, CoreType)
exactBinderContextSupport (ExactBinderContext binders) =
    Vector.fromList
        [ (identity, coreType)
        | ExactBinder identity _variable coreType _structure <- binders
        ]

exactBinderContextIndex
    :: Raw.VarSymbol
    -> ExactBinderContext
    -> Maybe Natural
exactBinderContextIndex variable (ExactBinderContext binders) =
    go 0 binders
  where
    go _index [] =
        Nothing
    go index (ExactBinder _identity candidate _coreType _structure : rest)
        | candidate == Just variable = Just index
        | otherwise = go (index + 1) rest

newtype PreparedExactProposition = PreparedExactProposition
    (ScopedCheckedCore ObjectId)

preparedExactPropositionCore
    :: PreparedExactProposition
    -> ScopedCheckedCore ObjectId
preparedExactPropositionCore (PreparedExactProposition proposition) =
    proposition

newtype PreparedExactSetExpression = PreparedExactSetExpression
    (ScopedCheckedCore ObjectId)

preparedExactSetExpressionCore
    :: PreparedExactSetExpression
    -> ScopedCheckedCore ObjectId
preparedExactSetExpressionCore (PreparedExactSetExpression expression) =
    expression

-- | A checked replacement graph and the two checked arguments used to
-- specialize its foundation characteristic. This is transient proof
-- preparation data, not a declaration or durable object.
data PreparedExactLocalFunctionGraph = PreparedExactLocalFunctionGraph
    !(ScopedCheckedCore ObjectId)
    !(ScopedCheckedCore ObjectId)
    !(ScopedCheckedCore ObjectId)

preparedExactLocalFunctionGraphCore
    :: PreparedExactLocalFunctionGraph
    -> ScopedCheckedCore ObjectId
preparedExactLocalFunctionGraphCore
        (PreparedExactLocalFunctionGraph graph _domain _function) =
    graph

preparedExactLocalFunctionGraphDomain
    :: PreparedExactLocalFunctionGraph
    -> ScopedCheckedCore ObjectId
preparedExactLocalFunctionGraphDomain
        (PreparedExactLocalFunctionGraph _graph domain _function) =
    domain

preparedExactLocalFunctionGraphMap
    :: PreparedExactLocalFunctionGraph
    -> ScopedCheckedCore ObjectId
preparedExactLocalFunctionGraphMap
        (PreparedExactLocalFunctionGraph _graph _domain function) =
    function

-- | One authoritative closed proposition prepared from a top-level claim
-- header and conclusion. The remaining fields are transient opening data for
-- the proof compiler.
data PreparedExactClaimEnvelope = PreparedExactClaimEnvelope
    !(ScopedCheckedCore ObjectId)
    ![Raw.VarSymbol]
    !ExactBinderContext
    !Natural

preparedExactClaimTarget
    :: PreparedExactClaimEnvelope
    -> ScopedCheckedCore ObjectId
preparedExactClaimTarget
        (PreparedExactClaimEnvelope target _variables _context _antecedents) =
    target

preparedExactClaimVariables
    :: PreparedExactClaimEnvelope
    -> [Raw.VarSymbol]
preparedExactClaimVariables
        (PreparedExactClaimEnvelope _target variables _context _antecedents) =
    variables

preparedExactClaimContext
    :: PreparedExactClaimEnvelope
    -> ExactBinderContext
preparedExactClaimContext
        (PreparedExactClaimEnvelope _target _variables context _antecedents) =
    context

preparedExactClaimAntecedentCount
    :: PreparedExactClaimEnvelope
    -> Natural
preparedExactClaimAntecedentCount
        (PreparedExactClaimEnvelope _target _variables _context antecedents) =
    antecedents


data ExactDeclarationFamily
    = ExactSignature
    | ExactAbbreviation
    | ExactDefinition
    deriving stock (Show, Eq, Ord)

data PreparedExactDeclaration = PreparedExactDeclaration
    !Location
    !ExactDeclarationFamily
    !SemanticGlobalKey
    !SemanticGlobalTarget
    !(Maybe AssertedObject)
    !(Maybe SemanticName)
    !DeclarationSyntaxId

preparedExactLocation :: PreparedExactDeclaration -> Location
preparedExactLocation
        (PreparedExactDeclaration location _family _key _target _object _alias _syntax) =
    location

preparedExactGlobalKey :: PreparedExactDeclaration -> SemanticGlobalKey
preparedExactGlobalKey
        (PreparedExactDeclaration _location _family key _target _object _alias _syntax) =
    key

preparedExactObjectId :: PreparedExactDeclaration -> ObjectId
preparedExactObjectId
        (PreparedExactDeclaration _location _family _key target _object _alias _syntax) =
    semanticGlobalTargetObject target

preparedExactObject
    :: PreparedExactDeclaration
    -> Maybe AssertedObject
preparedExactObject
        (PreparedExactDeclaration _location _family _key _target object _alias _syntax) =
    object

preparedExactSyntaxId
    :: PreparedExactDeclaration
    -> DeclarationSyntaxId
preparedExactSyntaxId
        (PreparedExactDeclaration _location _family _key _target _object _alias syntax) =
    syntax

preparedExactIsDefinition :: PreparedExactDeclaration -> Bool
preparedExactIsDefinition
        (PreparedExactDeclaration _location family _key _target _object _alias _syntax) =
    family == ExactDefinition

preparedExactGlobalTarget
    :: PreparedExactDeclaration
    -> SemanticGlobalTarget
preparedExactGlobalTarget
        (PreparedExactDeclaration
            _location _family _key target _object _alias _syntax) =
    target

preparedDefinitionAlias
    :: PreparedExactDeclaration
    -> Maybe SemanticName
preparedDefinitionAlias
        (PreparedExactDeclaration
            _location _family _key _target _object alias _syntax) =
    alias

data PreparedExactSourceAxiom = PreparedExactSourceAxiom
    !Location
    !SemanticName
    !(ScopedCheckedCore ObjectId)
    !DeclarationSyntaxId

data PreparedExactStructureFact = PreparedExactStructureFact
    !Location
    !(FrozenCheckedCore ObjectId)
    !SemanticName

data PreparedExactStructure = PreparedExactStructure
    !Location
    ![AssertedObject]
    !ObjectId
    !SemanticStructureDescriptor
    !SemanticName
    ![PreparedExactStructureFact]
    !DeclarationSyntaxId

data CheckedExactStructureAuthorization =
    CheckedExactStructureAuthorization
        !ObjectId
        ![(Location, Declaration.PreparedVampireObligation Void ())]

data ExactCompileError
    = ExactUnsupportedDeclaration !Location
    | ExactUnsupportedDeclarationBody !Location
    | ExactDeclarationOccurrenceMissing !Location
    | ExactDeclarationOccurrenceAmbiguous !Location
    | ExactDeclarationHeadMismatch !Location
    | ExactFixedSemanticCollision !Location !SemanticGlobalKey
    | ExactGlobalAlreadyVisible !Location !SemanticGlobalKey
    | ExactGlobalNotVisible !Location !SemanticGlobalKey
    | ExactDuplicateParameter !Location !Raw.VarSymbol
    | ExactDuplicateLocalBinder !Location !Raw.VarSymbol
    | ExactDuplicateLocalIdentity !Location !ExactLocalId
    | ExactFreeVariable !Location !Raw.VarSymbol
    | ExactApplicationExpectedFunction !Location !CoreType
    | ExactApplicationArgumentMismatch
        !Location !CoreType !CoreType
    | ExactExpressionExpectedSet !Location !CoreType
    | ExactFormulaExpectedProposition !Location !CoreType
    | ExactCoreCheckFailed !Location !CoreCheckError
    | ExactObjectTypeMismatch !Location !CoreType !CoreType
    | ExactUnsupportedHeaderAssumption !Location
    | ExactQuantifiedTermRequiresStatementSubject !Location
    | ExactStructureNotVisible !Location !SemanticStructurePhrase
    | ExactBaseStructureNotAssertable !Location !SemanticStructurePhrase
    | ExactDuplicateStructureAnnotation !Location !Raw.VarSymbol
    | ExactStructureOperationNotAvailable !Location !Raw.StructSymbol
    | ExactStructureOperationAmbiguous
        !Location !Raw.StructSymbol ![ObjectId]
    | ExactContextualExpansionNotAvailable
        !Location !SemanticGlobalKey
    | ExactContextualRequirementConflict
        !Location !Raw.StructSymbol !ObjectId !ObjectId
    | ExactStructureOccurrenceMismatch !Location
    | ExactStructureSelfParent !Location !SemanticStructurePhrase
    | ExactStructureDuplicateParent !Location !SemanticStructurePhrase
    | ExactStructureAlreadyVisible !Location !SemanticStructurePhrase
    | ExactStructureDuplicateOperation !Location !Raw.StructSymbol
    | ExactStructureOperationAlreadyInherited !Location !Raw.StructSymbol
    | ExactStructureOperationConflict
        !Location !Raw.StructSymbol
        !SemanticStructurePhrase !SemanticStructurePhrase
    | ExactStructureHasNoCarrier !Location !SemanticStructurePhrase
    | ExactStructureDescriptorInvalid !Location !SemanticEnvironmentError
    | ExactStructureObjectNotVisible !Location !ObjectId
    deriving stock (Show, Eq)

exactCompileErrorLocation :: ExactCompileError -> Location
exactCompileErrorLocation = \case
    ExactUnsupportedDeclaration location -> location
    ExactUnsupportedDeclarationBody location -> location
    ExactDeclarationOccurrenceMissing location -> location
    ExactDeclarationOccurrenceAmbiguous location -> location
    ExactDeclarationHeadMismatch location -> location
    ExactFixedSemanticCollision location _key -> location
    ExactGlobalAlreadyVisible location _key -> location
    ExactGlobalNotVisible location _key -> location
    ExactDuplicateParameter location _parameter -> location
    ExactDuplicateLocalBinder location _variable -> location
    ExactDuplicateLocalIdentity location _identity -> location
    ExactFreeVariable location _variable -> location
    ExactApplicationExpectedFunction location _actual -> location
    ExactApplicationArgumentMismatch location _expected _actual -> location
    ExactExpressionExpectedSet location _actual -> location
    ExactFormulaExpectedProposition location _actual -> location
    ExactCoreCheckFailed location _failure -> location
    ExactObjectTypeMismatch location _expected _actual -> location
    ExactUnsupportedHeaderAssumption location -> location
    ExactQuantifiedTermRequiresStatementSubject location -> location
    ExactStructureNotVisible location _phrase -> location
    ExactBaseStructureNotAssertable location _phrase -> location
    ExactDuplicateStructureAnnotation location _variable -> location
    ExactStructureOperationNotAvailable location _symbol -> location
    ExactStructureOperationAmbiguous location _symbol _objects -> location
    ExactContextualExpansionNotAvailable location _key -> location
    ExactContextualRequirementConflict location _symbol _first _second -> location
    ExactStructureOccurrenceMismatch location -> location
    ExactStructureSelfParent location _phrase -> location
    ExactStructureDuplicateParent location _phrase -> location
    ExactStructureAlreadyVisible location _phrase -> location
    ExactStructureDuplicateOperation location _symbol -> location
    ExactStructureOperationAlreadyInherited location _symbol -> location
    ExactStructureOperationConflict location _symbol _first _second -> location
    ExactStructureHasNoCarrier location _phrase -> location
    ExactStructureDescriptorInvalid location _failure -> location
    ExactStructureObjectNotVisible location _object -> location

renderExactCompileError :: ExactCompileError -> Text
renderExactCompileError = \case
    ExactUnsupportedDeclaration location ->
        at location <> "this declaration is not yet supported by the typed checker"
    ExactUnsupportedDeclarationBody location ->
        at location <> "this source form is not yet supported by exact elaboration"
    ExactDeclarationOccurrenceMissing location ->
        at location <> "the declaration has no associated syntax occurrence"
    ExactDeclarationOccurrenceAmbiguous location ->
        at location <> "the declaration has more than one semantic head"
    ExactDeclarationHeadMismatch location ->
        at location <> "the parsed declaration head does not match its syntax occurrence"
    ExactFixedSemanticCollision location key ->
        at location <> "the declaration collides with fixed semantics for "
            <> shown key
    ExactGlobalAlreadyVisible location key ->
        at location <> "the global " <> shown key <> " is already declared"
    ExactGlobalNotVisible location key ->
        at location <> "the global " <> shown key <> " is not visible"
    ExactDuplicateParameter location parameter ->
        at location <> "the declaration parameter " <> shown parameter <> " is repeated"
    ExactDuplicateLocalBinder location variable ->
        at location <> "the proof binder " <> shown variable <> " is already active"
    ExactDuplicateLocalIdentity location identity ->
        at location <> "the proof-local identity " <> shown identity <> " is already active"
    ExactFreeVariable location variable ->
        at location <> "the exact source form contains the free variable " <> shown variable
    ExactApplicationExpectedFunction location actual ->
        at location <> "an application expected a function, but found " <> shown actual
    ExactApplicationArgumentMismatch location expected actual ->
        at location <> "an application expected " <> shown expected
            <> ", but found " <> shown actual
    ExactExpressionExpectedSet location actual ->
        at location <> "an expression has type " <> shown actual <> " instead of Set"
    ExactFormulaExpectedProposition location actual ->
        at location <> "a formula has type " <> shown actual <> " instead of Prop"
    ExactCoreCheckFailed location failure ->
        at location <> "the checked declaration core is invalid: " <> shown failure
    ExactObjectTypeMismatch location expected actual ->
        at location <> "the declaration object has type " <> shown actual
            <> " instead of " <> shown expected
    ExactUnsupportedHeaderAssumption location ->
        at location <> "this top-level header assumption is not yet supported by exact elaboration"
    ExactQuantifiedTermRequiresStatementSubject location ->
        at location
            <> "a quantified term must be the sole subject of an exact statement"
    ExactStructureNotVisible location structurePhrase ->
        at location <> "the structure " <> shown structurePhrase <> " is not visible"
    ExactBaseStructureNotAssertable location structurePhrase ->
        at location <> "the metadata-only structure " <> shown structurePhrase
            <> " cannot be asserted"
    ExactDuplicateStructureAnnotation location variable ->
        at location <> "the structure binder " <> shown variable
            <> " is annotated more than once"
    ExactStructureOperationNotAvailable location symbol ->
        at location <> "the structure operation " <> shown symbol
            <> " is not available in the active structure scope"
    ExactStructureOperationAmbiguous location symbol objects ->
        at location <> "the structure operation " <> shown symbol
            <> " is ambiguous between " <> shown objects
    ExactContextualExpansionNotAvailable location key ->
        at location <> "the contextual abbreviation " <> shown key
            <> " has no compatible active structure"
    ExactContextualRequirementConflict location symbol firstObject secondObject ->
        at location <> "the contextual abbreviation requires incompatible "
            <> shown symbol <> " operations " <> shown firstObject
            <> " and " <> shown secondObject
    ExactStructureOccurrenceMismatch location ->
        at location <> "the structure syntax occurrences do not match the declaration"
    ExactStructureSelfParent location structurePhrase ->
        at location <> "the structure " <> shown structurePhrase
            <> " cannot inherit from itself"
    ExactStructureDuplicateParent location structurePhrase ->
        at location <> "the parent structure " <> shown structurePhrase
            <> " is repeated"
    ExactStructureAlreadyVisible location structurePhrase ->
        at location <> "the structure " <> shown structurePhrase
            <> " is already declared"
    ExactStructureDuplicateOperation location symbol ->
        at location <> "the structure operation " <> shown symbol
            <> " is repeated"
    ExactStructureOperationAlreadyInherited location symbol ->
        at location <> "the structure operation " <> shown symbol
            <> " is already inherited"
    ExactStructureOperationConflict location symbol firstOrigin secondOrigin ->
        at location <> "the inherited structure operation " <> shown symbol
            <> " conflicts between " <> shown firstOrigin
            <> " and " <> shown secondOrigin
    ExactStructureHasNoCarrier location structurePhrase ->
        at location <> "the structure " <> shown structurePhrase
            <> " does not inherit the base carrier operation"
    ExactStructureDescriptorInvalid location _failure ->
        at location <> "the canonical structure descriptor is inconsistent"
    ExactStructureObjectNotVisible location identity ->
        at location <> "the structure fact mentions unavailable object "
            <> shown identity
  where
    at location = locationToText location <> ": "
    shown :: Show value => value -> Text
    shown = Text.pack . show

data ElaborationState = ElaborationState
    { elaborationBinders :: !(Map.Map Raw.VarSymbol Natural)
    , elaborationStructures :: !(Map.Map Natural ExactStructureAnnotation)
    , elaborationGlobals :: !(Map.Map ObjectId CoreType)
    , elaborationContextualBinder :: !(Maybe Natural)
    , elaborationContextualRequirements
        :: !(Map.Map Raw.StructSymbol ObjectId)
    }

type Elaborate =
    StateT
        ElaborationState
        (ExceptT ExactCompileError (Declaration.LoweringDriver))

data PreparedHead = PreparedHead
    !SemanticGlobalKey
    ![Raw.VarSymbol]
    !CoreType

data PreparedBody
    = OpaqueBody
    | TransparentBody !(CanonicalTerm ObjectId)
    | ContextualTransparentBody
        !(Map.Map Raw.StructSymbol ObjectId)
        !(CanonicalTerm ObjectId)

prepareExactProposition
    :: ExactBinderContext
    -> Raw.Stmt
    -> Declaration.LoweringDriver
        (Either ExactCompileError PreparedExactProposition)
prepareExactProposition context statement =
    prepareExactPropositionTerm
        context
        (locate statement)
        (compileStatement statement)

-- | Compile the source bound of already-opened symbolic binders.  This is the
-- shared checked constraint seam used by quantified statements and proof
-- binders, so relation signs, carrier casts, and global occurrences are
-- elaborated exactly once by the ordinary expression compiler.
prepareExactSymbolicBoundConstraints
    :: ExactBinderContext
    -> NonEmpty Raw.VarSymbol
    -> Raw.Bound
    -> Declaration.LoweringDriver
        (Either ExactCompileError PreparedExactProposition)
prepareExactSymbolicBoundConstraints context variables bound =
    prepareExactPropositionTerm
        context
        (case bound of
            Raw.Unbounded -> locate (NonEmpty.head variables)
            _ -> locate bound)
        (logicalConjunction
            <$> compileSymbolicBoundConstraintList variables bound)

-- | Compile the opened body used by a symbolic existential witness.  Its
-- grouping is deliberately identical to 'SymbolicExists': all bound
-- constraints form the existential restriction and the stated proposition is
-- its body.
prepareExactSymbolicWitnessConstraints
    :: ExactBinderContext
    -> NonEmpty Raw.VarSymbol
    -> Raw.Bound
    -> Raw.Stmt
    -> Declaration.LoweringDriver
        (Either ExactCompileError PreparedExactProposition)
prepareExactSymbolicWitnessConstraints context variables bound statement =
    prepareExactPropositionTerm context (locate statement) do
        constraints <-
            logicalConjunction
                <$> compileSymbolicBoundConstraintList variables bound
        body <- compileStatement statement
        pure
            (if constraints == logicalTruth
                then body
                else logicalAnd constraints body)

-- | Compile the checked constraint of an already-opened noun witness.  Named
-- binders are resolved normally; a nameless singular noun uses the nearest
-- anonymous binder and therefore introduces no lookup spelling.
prepareExactNounWitnessConstraints
    :: ExactBinderContext
    -> Raw.NounPhrase []
    -> Declaration.LoweringDriver
        (Either ExactCompileError PreparedExactProposition)
prepareExactNounWitnessConstraints context nounPhrase =
    case nounPhrase of
        Raw.NounPhrase left noun variables right suchThat ->
            prepareExactPropositionTerm context (locate noun) do
                subjects <-
                    case NonEmpty.nonEmpty variables of
                        Just binders ->
                            toList
                                <$> traverse compileIntroducedVariable binders
                        Nothing ->
                            pure [CBound 0]
                compileNounPhraseConstraints
                    subjects left noun right suchThat

prepareExactPropositionTerm
    :: ExactBinderContext
    -> Location
    -> Elaborate (CanonicalTerm ObjectId)
    -> Declaration.LoweringDriver
        (Either ExactCompileError PreparedExactProposition)
prepareExactPropositionTerm context location compile =
    Except.runExceptT do
        let initialElaboration = initialElaborationState context
        (term, finalElaboration) <-
            State.runStateT compile initialElaboration
        checked <-
            either
                (Except.throwError . ExactCoreCheckFailed location)
                pure
                (checkScopedCanonicalCore
                    (`Map.lookup` elaborationGlobals finalElaboration)
                    (binderTypes context)
                    term)
        unless (scopedCoreType checked == TyProp)
            (Except.throwError
                (ExactFormulaExpectedProposition
                    location
                    (scopedCoreType checked)))
        pure (PreparedExactProposition checked)

prepareExactSetExpression
    :: ExactBinderContext
    -> Raw.Expr
    -> Declaration.LoweringDriver
        (Either ExactCompileError PreparedExactSetExpression)
prepareExactSetExpression context expression =
    Except.runExceptT do
        let initialElaboration = initialElaborationState context
        (term, finalElaboration) <-
            State.runStateT
                (compileExpressionAsSet expression)
                initialElaboration
        checked <-
            either
                (Except.throwError
                    . ExactCoreCheckFailed (locate expression))
                pure
                (checkScopedCanonicalCore
                    (`Map.lookup` elaborationGlobals finalElaboration)
                    (binderTypes context)
                    term)
        unless (scopedCoreType checked == TySet)
            (Except.throwError
                (ExactExpressionExpectedSet
                    (locate expression)
                    (scopedCoreType checked)))
        pure (PreparedExactSetExpression checked)

prepareExactLocalFunctionGraph
    :: Location
    -> ExactBinderContext
    -> ExactBinderContext
    -> Raw.Expr
    -> Raw.Expr
    -> Declaration.LoweringDriver
        (Either ExactCompileError PreparedExactLocalFunctionGraph)
prepareExactLocalFunctionGraph
        location context argumentContext domainExpression valueExpression =
    Except.runExceptT do
        domain <-
            preparedExactSetExpressionCore
                <$> ( Except.lift
                        (prepareExactSetExpression context domainExpression)
                        >>= Except.liftEither
                    )
        value <-
            preparedExactSetExpressionCore
                <$> ( Except.lift
                        (prepareExactSetExpression
                            argumentContext valueExpression)
                        >>= Except.liftEither
                    )
        pair <- prepareOrderedPair
        case scopedReplacementGraph pair domain value of
            Just (graph, checkedDomain, function) ->
                pure
                    (PreparedExactLocalFunctionGraph
                        graph checkedDomain function)
            Nothing ->
                impossible
                    "checked local-function components did not form a replacement graph"
  where
    prepareOrderedPair = do
        let initialElaboration = initialElaborationState context
            key =
                SemanticExpressionFunction
                    (Raw.mixfixPattern Raw.PairSymbol)
            expected = TySet `TyArrow` (TySet `TyArrow` TySet)
        ((term, actual), finalElaboration) <-
            State.runStateT
                (applyResolvedTyped location key [])
                initialElaboration
        unless (actual == expected)
            (Except.throwError
                (ExactObjectTypeMismatch location expected actual))
        either
            (Except.throwError . ExactCoreCheckFailed location)
            pure
            (checkScopedCanonicalCore
                (`Map.lookup` elaborationGlobals finalElaboration)
                (binderTypes context)
                term)

prepareExactClaimEnvelope
    :: [Raw.Asm]
    -> Raw.Stmt
    -> Declaration.LoweringDriver
        (Either ExactCompileError PreparedExactClaimEnvelope)
prepareExactClaimEnvelope assumptions statement =
    discover [] emptyExactBinderContext
  where
    discover variables context = do
        attempted <- prepareExactClaimAttempt context assumptions statement
        case attempted of
            Left (ExactFreeVariable _location variable)
                | variable `elem` variables ->
                    impossible
                        "exact claim discovery repeated an active free variable"
                | otherwise ->
                    case extendExactBinderContext
                            ( ( exactLocalId
                                    (fromIntegral (length variables))
                              , variable
                              ) :| []
                            )
                            context of
                        Left failure ->
                            pure (Left failure)
                        Right extended ->
                            discover (variables <> [variable]) extended
            Left failure ->
                pure (Left failure)
            Right (target, antecedentCount, structures) ->
                pure
                    (Right
                        (PreparedExactClaimEnvelope
                            target
                            variables
                            (annotateBinderContext structures context)
                            antecedentCount))

prepareExactClaimAttempt
    :: ExactBinderContext
    -> [Raw.Asm]
    -> Raw.Stmt
    -> Declaration.LoweringDriver
        (Either
            ExactCompileError
            ( ScopedCheckedCore ObjectId
            , Natural
            , Map.Map Natural ExactStructureAnnotation
            ))
prepareExactClaimAttempt context assumptions statement =
    Except.runExceptT do
        let initialElaboration = initialElaborationState context
        ((antecedents, conclusion), finalElaboration) <-
            State.runStateT
                ( do
                    antecedents <-
                        concat <$> traverse compileHeaderAssumption assumptions
                    conclusion <- compileStatement statement
                    pure (antecedents, conclusion)
                )
                initialElaboration
        checkedAntecedents <-
            traverse
                (uncurry
                    (checkEnvelopeProposition
                        finalElaboration
                        context))
                antecedents
        checkedConclusion <-
            checkEnvelopeProposition
                finalElaboration
                context
                (locate statement)
                conclusion
        let implication =
                foldr
                    (\antecedent continuation ->
                        fromMaybe
                            (impossible
                                "checked claim antecedents have unequal contexts")
                            (implyScopedCore antecedent continuation))
                    checkedConclusion
                    checkedAntecedents
            closed = closeClaimBinders implication
        unless (null (scopedCoreContext closed))
            (impossible "exact claim closure retained a binder")
        pure
            ( closed
            , fromIntegral (length antecedents)
            , elaborationStructures finalElaboration
            )

checkEnvelopeProposition
    :: ElaborationState
    -> ExactBinderContext
    -> Location
    -> CanonicalTerm ObjectId
    -> ExceptT
        ExactCompileError
        (Declaration.LoweringDriver)
        (ScopedCheckedCore ObjectId)
checkEnvelopeProposition elaboration context location term = do
    checked <-
        either
            (Except.throwError . ExactCoreCheckFailed location)
            pure
            (checkScopedCanonicalCore
                (`Map.lookup` elaborationGlobals elaboration)
                (binderTypes context)
                term)
    unless (scopedCoreType checked == TyProp)
        (Except.throwError
            (ExactFormulaExpectedProposition
                location
                (scopedCoreType checked)))
    pure checked

closeClaimBinders
    :: ScopedCheckedCore global
    -> ScopedCheckedCore global
closeClaimBinders scoped =
    case scopedCoreContext scoped of
        [] -> scoped
        _binder : _remaining ->
            closeClaimBinders
                (fromMaybe
                    (impossible
                        "a checked claim binder could not be closed")
                    (closeScopedForall scoped))

binderIndices :: ExactBinderContext -> Map.Map Raw.VarSymbol Natural
binderIndices (ExactBinderContext binders) =
    Map.fromList
        [ (variable, fromIntegral index)
        | (index, ExactBinder _identity (Just variable) _coreType _structure) <-
            zip [0 :: Int ..] binders
        ]

binderStructures
    :: ExactBinderContext
    -> Map.Map Natural ExactStructureAnnotation
binderStructures (ExactBinderContext binders) =
    Map.fromList
        [ (fromIntegral index, structure)
        | (index, ExactBinder _identity _variable _coreType (Just structure)) <-
            zip [0 :: Int ..] binders
        ]

binderTypes :: ExactBinderContext -> [CoreType]
binderTypes (ExactBinderContext binders) =
    [ coreType
    | ExactBinder _identity _variable coreType _structure <- binders
    ]

initialElaborationState :: ExactBinderContext -> ElaborationState
initialElaborationState context =
    ElaborationState
        (binderIndices context)
        (binderStructures context)
        mempty
        Nothing
        mempty

annotateBinderContext
    :: Map.Map Natural ExactStructureAnnotation
    -> ExactBinderContext
    -> ExactBinderContext
annotateBinderContext structures (ExactBinderContext binders) =
    ExactBinderContext
        [ ExactBinder identity variable coreType
            (Map.lookup (fromIntegral index) structures)
        | (index, ExactBinder identity variable coreType _old) <-
            zip [0 :: Int ..] binders
        ]

compileHeaderAssumption
    :: Raw.Asm
    -> Elaborate [(Location, CanonicalTerm ObjectId)]
compileHeaderAssumption = \case
    Raw.AsmSuppose statement -> do
        proposition <- compileStatement statement
        pure [(locate statement, proposition)]
    Raw.AsmLetNoun variables nounPhrase
        | exactSetNounPhrase nounPhrase -> do
            traverse_ compileIntroducedVariable variables
            pure []
        | otherwise -> do
            subjects <- traverse compileIntroducedVariable variables
            constraints <-
                traverse (`compileNounPhraseMaybe` nounPhrase) subjects
            pure
                [ (locate variable, constraint)
                | (variable, constraint) <-
                    zip (toList variables) (toList constraints)
                ]
    Raw.AsmLetIn variables domain -> do
        variableTerms <- traverse compileIntroducedVariable variables
        domainTerm <- compileExpressionAsSet domain
        traverse
            (\(variable, variableTerm) -> do
                proposition <-
                    compileMembership
                        (locate domain)
                        Raw.Positive
                        variableTerm
                        domainTerm
                pure (locate variable, proposition))
            (zip (toList variables) (toList variableTerms))
    Raw.AsmLetEq variable expression -> do
        variableTerm <- compileIntroducedVariable variable
        expressionTerm <- compileExpressionAsSet expression
        pure
            [ ( locate variable
              , CEq TySet variableTerm expressionTerm
              )
            ]
    Raw.AsmLetThe variable _function ->
        Except.throwError
            (ExactUnsupportedHeaderAssumption (locate variable))
    Raw.AsmLetStruct variable structure -> do
        subject <- compileIntroducedVariable variable
        annotation <-
            resolveStructureAnnotation
                (locate variable)
                structure
        index <-
            maybe
                (impossible "an introduced structure variable is unbound")
                pure
                =<< Map.lookup variable <$> State.gets elaborationBinders
        existing <- State.gets (Map.lookup index . elaborationStructures)
        when
            (isJust existing)
            (Except.throwError
                (ExactDuplicateStructureAnnotation
                    (locate variable) variable))
        State.modify' \state ->
            state
                { elaborationStructures =
                    Map.insert index annotation
                        (elaborationStructures state)
                }
        predicate <-
            maybe
                (impossible "an assertable structure has no predicate")
                pure
                (structureAnnotationPredicate annotation)
        recordExactGlobal
            predicate
            (TyArrow TySet TyProp)
        pure
            [ ( locate variable
              , CApp
                    (CGlobal predicate)
                    subject
              )
            ]

compileIntroducedVariable
    :: Raw.VarSymbol
    -> Elaborate (CanonicalTerm ObjectId)
compileIntroducedVariable variable =
    compileExpressionAsSet (Raw.ExprVar variable)

resolveStructureAnnotation
    :: Location
    -> Raw.StructPhrase
    -> Elaborate ExactStructureAnnotation
resolveStructureAnnotation location rawPhrase = do
    let structurePhrase = semanticStructurePhrase rawPhrase
    resolved <-
        State.lift
            (Except.lift
                (Declaration.resolveVisibleStructureLowering structurePhrase))
    structure <-
        maybe
            (Except.throwError
                (ExactStructureNotVisible location structurePhrase))
            pure
            resolved
    predicate <-
        maybe
            (Except.throwError
                (ExactBaseStructureNotAssertable location structurePhrase))
            pure
            (Declaration.resolvedStructurePredicate structure)
    pure
        (ExactStructureAnnotation
            structurePhrase
            (Just predicate)
            (Declaration.resolvedStructureOperations structure))

structureAnnotationPredicate :: ExactStructureAnnotation -> Maybe ObjectId
structureAnnotationPredicate
        (ExactStructureAnnotation _ predicate _operations) =
    predicate

structureAnnotationOperation
    :: Raw.StructSymbol
    -> ExactStructureAnnotation
    -> Maybe ObjectId
structureAnnotationOperation symbol
        (ExactStructureAnnotation _phrase _predicate operations) =
    Map.lookup symbol operations

recordExactGlobal :: ObjectId -> CoreType -> Elaborate ()
recordExactGlobal identity coreType = do
    existing <- State.gets (Map.lookup identity . elaborationGlobals)
    case existing of
        Nothing ->
            State.modify' \state ->
                state
                    { elaborationGlobals =
                        Map.insert identity coreType
                            (elaborationGlobals state)
                    }
        Just actual
            | actual == coreType -> pure ()
            | otherwise ->
                impossible "one exact global acquired two checked types"

prepareExactSourceAxiom
    :: Raw.Block
    -> Declaration.LoweringDriver
        (Either ExactCompileError PreparedExactSourceAxiom)
prepareExactSourceAxiom = \case
    Raw.BlockAxiom
            location _title (Raw.Marker marker)
            (Raw.Axiom assumptions statement) -> do
            prepared <- prepareExactClaimEnvelope assumptions statement
            pure do
                envelope <- prepared
                let core = preparedExactClaimTarget envelope
                    alias = semanticName marker
                unless (null (scopedCoreContext core))
                    (Left (ExactUnsupportedDeclarationBody location))
                pure
                    (PreparedExactSourceAxiom
                        location
                        alias
                        core
                        (declarationSyntaxId
                            (encodePreparedSourceAxiom core alias)))
    block ->
        pure (Left (ExactUnsupportedDeclaration (locate block)))

lowerPreparedExactSourceAxiom
    :: PreparedExactSourceAxiom
    -> Declaration.LoweringDriver
        (Either
            Declaration.DeclarationError
            (Declaration.CheckedDeclaration ()))
lowerPreparedExactSourceAxiom
        (PreparedExactSourceAxiom _location alias target syntax) =
    fmap
        (\spec ->
            Declaration.checkedCompiledDeclaration
                syntax [] [] [] []
                [ Declaration.checkedCandidate
                    spec
                    Declaration.checkedSourceAxiomPlanning
                    :| []
                ]
                ())
        <$> Declaration.prepareCandidateSpecLowering
            [] target SearchEligible [alias]

authorizeCheckedExactSourceAxiom
    :: ()
    -> [NonEmpty Declaration.ReservedCandidate]
    -> Declaration.Declaration ()
authorizeCheckedExactSourceAxiom () = \case
    [candidate :| []] ->
        Declaration.authorizeSourceAxiomCandidate candidate
    stages ->
        Declaration.failDeclaration
            (Declaration.CheckedAuthorizationCandidateShapeMismatch
                1 (length stages))

prepareExactDeclaration
    :: Raw.Block
    -> [CanonicalLexicalEntry]
    -> Declaration.LoweringDriver
        (Either ExactCompileError PreparedExactDeclaration)
prepareExactDeclaration block entries =
    Except.runExceptT do
        entry <-
            case entries of
                [] -> Except.throwError
                    (ExactDeclarationOccurrenceMissing (locate block))
                [single] -> pure single
                _ -> Except.throwError
                    (ExactDeclarationOccurrenceAmbiguous (locate block))
        key <-
            maybe
                (Except.throwError
                    (ExactUnsupportedDeclaration (locate block)))
                pure
                (semanticGlobalKeyFromLexicalEntry entry)
        when
            (isJust (fixedSemanticMeaning key))
            (Except.throwError
                (ExactFixedSemanticCollision (locate block) key))
        visible <- Except.lift
            (Declaration.resolveVisibleGlobalLowering key)
        when
            (isJust visible)
            (Except.throwError
                (ExactGlobalAlreadyVisible (locate block) key))
        (head', family, rawBody) <-
            prepareHead block key
        slot <- Except.lift Declaration.nextDeclarationSlotLowering
        theory <- Except.lift Declaration.currentTheoryLowering
        (body, globals) <-
            case rawBody of
                Nothing -> pure (OpaqueBody, Map.empty)
                Just buildBody -> do
                    let initialElaboration =
                            ElaborationState
                                mempty mempty mempty Nothing mempty
                    (canonical, finalElaboration) <-
                        State.runStateT buildBody initialElaboration
                    let requirements =
                            elaborationContextualRequirements finalElaboration
                        body
                            | Map.null requirements =
                                TransparentBody canonical
                            | family == ExactAbbreviation =
                                ContextualTransparentBody
                                    requirements
                                    (CLam TySet canonical)
                            | otherwise =
                                impossible
                                    "a non-abbreviation acquired contextual requirements"
                    pure (body, elaborationGlobals finalElaboration)
        let PreparedHead semanticKey _parameters coreType = head'
        unless (semanticKey == key)
            (Except.throwError
                (ExactDeclarationHeadMismatch (locate block)))
        (target, content) <-
            case body of
                OpaqueBody -> do
                    let seed =
                            opaqueDeclarationSeed
                                (declarationSlotModule slot)
                                (declarationSlotOrdinal slot)
                                SignatureDeclaration
                                (generatedObjectSlot 0)
                        content' =
                            OpaqueObjectContent theory seed coreType
                        identity = opaqueObjectId theory seed coreType
                    pure (GlobalReference identity, content')
                TransparentBody canonical -> do
                    checked <-
                        either
                            (Except.throwError
                                . ExactCoreCheckFailed (locate block))
                            pure
                            (checkCanonicalCore
                                (`Map.lookup` globals)
                                canonical)
                    unless
                        (frozenCoreType checked == coreType)
                        (Except.throwError
                            (ExactObjectTypeMismatch
                                (locate block)
                                coreType
                                (frozenCoreType checked)))
                    let content' =
                            TransparentObjectContent
                                theory
                                coreType
                                canonical
                    let identity =
                            transparentObjectId theory coreType canonical
                        semanticTarget =
                            case family of
                                ExactAbbreviation ->
                                    TransparentExpansion identity
                                ExactDefinition -> GlobalReference identity
                                ExactSignature ->
                                    impossible
                                        "a signature acquired a transparent body"
                    pure (semanticTarget, content')
                ContextualTransparentBody requirements canonical -> do
                    let contextualType = TyArrow TySet coreType
                    checked <-
                        either
                            (Except.throwError
                                . ExactCoreCheckFailed (locate block))
                            pure
                            (checkCanonicalCore
                                (`Map.lookup` globals)
                                canonical)
                    unless
                        (frozenCoreType checked == contextualType)
                        (Except.throwError
                            (ExactObjectTypeMismatch
                                (locate block)
                                contextualType
                                (frozenCoreType checked)))
                    let content' =
                            TransparentObjectContent
                                theory
                                contextualType
                                canonical
                        identity =
                            transparentObjectId
                                theory contextualType canonical
                    pure
                        ( ContextualTransparentExpansion
                            identity requirements
                        , content'
                        )
        let targetObject = semanticGlobalTargetObject target
        available <-
            Except.lift (Declaration.objectAvailableLowering targetObject)
        let alias = definitionAlias block
            asserted
                | available = Nothing
                | otherwise = Just (assertedObject targetObject content)
            syntax =
                declarationSyntaxId
                    (encodePreparedSyntax family head' body alias)
        pure
            (PreparedExactDeclaration
                (locate block)
                family
                key
                target
                asserted
                alias
                syntax)

lowerPreparedExactBinding
    :: PreparedExactDeclaration
    -> Declaration.LoweringDriver
        (Either
            Declaration.DeclarationError
            (Declaration.CheckedDeclaration (Maybe ObjectId)))
lowerPreparedExactBinding prepared =
    case preparedDefinitionAlias prepared of
        Nothing ->
            pure
                (Right
                    (checked [] Nothing))
        Just alias ->
            fmap
                (\spec ->
                    checked
                        [ Declaration.checkedCandidate
                            spec
                            (Declaration.checkedDefinitionEquationPlanning
                                identity)
                            :| []
                        ]
                        (Just identity))
                <$> Declaration.prepareDefinitionEquationSpecLowering
                    objects identity alias
  where
    identity = preparedExactObjectId prepared
    objects = maybeToList (preparedExactObject prepared)
    checked stages body =
        Declaration.checkedCompiledDeclaration
            (preparedExactSyntaxId prepared)
            objects
            []
            [semanticGlobalBinding
                (preparedExactGlobalKey prepared)
                (preparedExactGlobalTarget prepared)]
            []
            stages
            body

authorizeCheckedExactBinding
    :: Maybe ObjectId
    -> [NonEmpty Declaration.ReservedCandidate]
    -> Declaration.Declaration ()
authorizeCheckedExactBinding body stages =
    case (body, stages) of
        (Nothing, []) -> pure ()
        (Just identity, [candidate :| []]) ->
            Declaration.authorizeDefinitionEquationCandidate
                identity candidate
        _ ->
            Declaration.failDeclaration
                (Declaration.CheckedAuthorizationCandidateShapeMismatch
                    (if isJust body then 1 else 0)
                    (length stages))

prepareExactStructure
    :: Raw.Block
    -> [CanonicalLexicalEntry]
    -> Declaration.LoweringDriver
        (Either ExactCompileError PreparedExactStructure)
prepareExactStructure block entries =
    Except.runExceptT do
        (location, marker, structure) <-
            case block of
                Raw.BlockStruct location _title (Raw.Marker marker) structure ->
                    pure (location, marker, structure)
                _ -> Except.throwError
                    (ExactUnsupportedDeclaration (locate block))
        validateStructureOccurrences location structure entries
        let structurePhrase =
                semanticStructurePhrase (Raw.structPhrase structure)
            parentPhrases =
                semanticStructurePhrase <$> Raw.structParents structure
        when
            (structurePhrase `elem` parentPhrases)
            (Except.throwError
                (ExactStructureSelfParent location structurePhrase))
        case firstDuplicate parentPhrases of
            Just duplicate ->
                Except.throwError
                    (ExactStructureDuplicateParent location duplicate)
            Nothing -> pure ()
        visible <- Except.lift
            (Declaration.resolveVisibleStructureLowering structurePhrase)
        when
            (isJust visible)
            (Except.throwError
                (ExactStructureAlreadyVisible location structurePhrase))
        parents <- traverse (resolveParent location) parentPhrases
        inherited <-
            foldM mergeParentOperations Map.empty
                (zip parentPhrases parents)
        case firstDuplicate (Raw.structFixes structure) of
            Just duplicate ->
                Except.throwError
                    (ExactStructureDuplicateOperation location duplicate)
            Nothing -> pure ()
        traverse_
            (\symbol ->
                when
                    (Map.member symbol inherited)
                    (Except.throwError
                        (ExactStructureOperationAlreadyInherited
                            location symbol)))
            (Raw.structFixes structure)
        slot <- Except.lift Declaration.nextDeclarationSlotLowering
        theory <- Except.lift Declaration.currentTheoryLowering
        let operationType = TyArrow TySet TySet
            makeOperation index symbol =
                let seed =
                        opaqueDeclarationSeed
                            (declarationSlotModule slot)
                            (declarationSlotOrdinal slot)
                            StructureDeclaration
                            (generatedObjectSlot index)
                    content = OpaqueObjectContent theory seed operationType
                    identity = opaqueObjectId theory seed operationType
                in ( symbol
                   , identity
                   , assertedObject identity content
                   )
            ownOperations =
                zipWith makeOperation [0 ..] (Raw.structFixes structure)
            operationObjects =
                [ asserted
                | (_symbol, _identity, asserted) <- ownOperations
                ]
            completeOperations =
                Map.union
                    (Map.fromList
                        [ (symbol, identity)
                        | (symbol, identity, _asserted) <- ownOperations
                        ])
                    (fst <$> inherited)
        unless
            (Map.member Raw.CarrierSymbol completeOperations)
            (Except.throwError
                (ExactStructureHasNoCarrier location structurePhrase))
        context <-
            either Except.throwError pure
                (extendExactBinderContext
                    ((exactLocalId 0, Raw.structLabel structure) :| [])
                    emptyExactBinderContext)
        let provisionalAnnotation =
                ExactStructureAnnotation
                    structurePhrase Nothing completeOperations
            structureContext =
                annotateBinderContext
                    (Map.singleton 0 provisionalAnnotation)
                    context
        checkedAssumptions <-
            traverse
                (\(assumptionMarker, assumption) -> do
                    prepared <- Except.lift
                        (prepareExactProposition structureContext assumption)
                    proposition <- Except.liftEither prepared
                    pure
                        ( locate assumption
                        , assumptionMarker
                        , preparedExactPropositionCore proposition
                        ))
                (Raw.structAssumes structure)
        parentTerms <-
            fmap catMaybes
                (traverse
                    (\parent ->
                        case Declaration.resolvedStructurePredicate parent of
                            Nothing -> pure Nothing
                            Just predicate ->
                                pure
                                    (Just
                                        (CApp
                                            (CGlobal predicate)
                                            (CBound 0))))
                    parents)
        let assumptionTerms =
                [ scopedCoreTerm proposition
                | (_assumptionLocation, _assumptionMarker, proposition) <-
                    checkedAssumptions
                ]
            predicateBody =
                CLam TySet
                    (logicalConjunction
                        (parentTerms <> assumptionTerms))
            predicateType = TyArrow TySet TyProp
            predicateContent =
                TransparentObjectContent theory predicateType predicateBody
            predicate =
                transparentObjectId theory predicateType predicateBody
        predicateAvailable <-
            Except.lift (Declaration.objectAvailableLowering predicate)
        let predicateObject =
                [ assertedObject predicate predicateContent
                | not predicateAvailable
                ]
            ownBindings =
                [ semanticStructureOperation symbol identity
                | (symbol, identity, _asserted) <- ownOperations
                ]
        descriptor <-
            Except.liftEither
                (first
                    (ExactStructureDescriptorInvalid location)
                    (semanticStructureDescriptor
                        structurePhrase
                        (Just predicate)
                        parentPhrases
                        ownBindings))
        let structureApplication =
                CApp (CGlobal predicate) (CBound 0)
            inheritance =
                [ ( location
                  , semanticName (marker <> "inherit")
                  , CForall TySet
                        (CImp structureApplication
                            (logicalConjunction parentTerms))
                  )
                | not (null parentTerms)
                ]
            projections =
                [ ( assumptionLocation
                  , semanticName assumptionMarker
                  , CForall TySet
                        (CImp structureApplication
                            (scopedCoreTerm proposition))
                  )
                | ( assumptionLocation
                  , Raw.Marker assumptionMarker
                  , proposition
                  ) <- checkedAssumptions
                ]
            generatedTerms = inheritance <> projections
            localTypes =
                Map.fromList
                    ((predicate, predicateType)
                        : [ (identity, operationType)
                          | (_symbol, identity, _asserted) <- ownOperations
                          ])
        resolvedTypes <-
            resolveStructureGlobalTypes
                localTypes
                [ term
                | (_factLocation, _alias, term) <- generatedTerms
                ]
        generated <-
            traverse
                (\(factLocation, alias, term) -> do
                    frozen <-
                        either
                            (Except.throwError
                                . ExactCoreCheckFailed factLocation)
                            pure
                            (checkCanonicalCore
                                (`Map.lookup` resolvedTypes)
                                term)
                    pure
                        (PreparedExactStructureFact
                            factLocation frozen alias))
                generatedTerms
        environment <-
            Except.liftEither
                (first
                    (ExactStructureDescriptorInvalid location)
                    (semanticEnvironmentWithStructures [] [descriptor]))
        let syntax =
                declarationSyntaxId
                    (encodePreparedStructure
                        environment
                        predicate
                        generated)
        pure
            (PreparedExactStructure
                location
                (operationObjects <> predicateObject)
                predicate
                descriptor
                (semanticName marker)
                generated
                syntax)
  where
    resolveParent location structurePhrase = do
        resolved <- Except.lift
            (Declaration.resolveVisibleStructureLowering structurePhrase)
        maybe
            (Except.throwError
                (ExactStructureNotVisible location structurePhrase))
            pure
            resolved

    mergeParentOperations inherited (parentPhrase, parent) =
        foldM
            (insertParentOperation parentPhrase)
            inherited
            (Map.toAscList
                (Declaration.resolvedStructureOperations parent))

    insertParentOperation parentPhrase inherited (symbol, identity) =
        case Map.lookup symbol inherited of
            Nothing ->
                pure
                    (Map.insert symbol (identity, parentPhrase) inherited)
            Just (existing, existingOrigin)
                | existing == identity -> pure inherited
                | otherwise ->
                    Except.throwError
                        (ExactStructureOperationConflict
                            (locate block)
                            symbol
                            existingOrigin
                            parentPhrase)

    resolveStructureGlobalTypes localTypes terms = do
        let dependencies = Set.unions (canonicalTermGlobals <$> terms)
        foldM
            (\types identity ->
                case Map.lookup identity types of
                    Just{} -> pure types
                    Nothing -> do
                        coreType <- Except.lift
                            (Declaration.objectTypeLowering identity)
                        case coreType of
                            Nothing ->
                                Except.throwError
                                    (ExactStructureObjectNotVisible
                                        (locate block) identity)
                            Just actual ->
                                pure (Map.insert identity actual types))
            localTypes
            (Set.toAscList dependencies)

lowerPreparedExactStructure
    :: PreparedExactStructure
    -> Declaration.LoweringDriver
        (Either
            Declaration.DeclarationError
            (Declaration.CheckedDeclaration
                CheckedExactStructureAuthorization))
lowerPreparedExactStructure
        (PreparedExactStructure
            _location objects predicate descriptor alias generatedFacts syntax) =
    Except.runExceptT do
        definition <-
            Except.lift
                (Declaration.preparePointwiseDefinitionEquationSpecLowering
                    objects predicate alias)
                >>= Except.liftEither
        generatedCandidates <-
            traverse
                (\(PreparedExactStructureFact
                        factLocation target factAlias) -> do
                    generatedSpec <- Except.lift
                        (Declaration.prepareFrozenCandidateSpecLowering
                            objects target SearchEligible [factAlias])
                        >>= Except.liftEither
                    obligation <- Except.lift
                        (Declaration.prepareStagedCandidateVampireLowering
                            factLocation objects definition generatedSpec)
                        >>= Except.liftEither
                    pure
                        ( Declaration.checkedCandidate generatedSpec
                            (Declaration.checkedSourceProofPlanning
                                [ Declaration.checkedPlannedVampireRequest
                                    factLocation obligation
                                ]
                                [ Declaration.plannedEarlierCandidate 0 0
                                ])
                        , (factLocation, obligation)
                        ))
                generatedFacts
        let generatedAuthorizations =
                snd <$> generatedCandidates
            stages =
                [ Declaration.checkedCandidate definition
                    (Declaration.checkedDefinitionEquationPlanning predicate)
                    :| []
                ]
                    <> maybeToList
                        (NonEmpty.nonEmpty
                            (fst <$> generatedCandidates))
            body =
                CheckedExactStructureAuthorization
                    predicate
                    generatedAuthorizations
        pure
            (Declaration.checkedCompiledDeclaration
                syntax objects [] [] [descriptor] stages
                body)

authorizeCheckedExactStructure
    :: CheckedExactStructureAuthorization
    -> [NonEmpty Declaration.ReservedCandidate]
    -> Declaration.Declaration ()
authorizeCheckedExactStructure
        (CheckedExactStructureAuthorization predicate obligations)
        stages =
    case (obligations, stages) of
        ([], [definition :| []]) ->
            Declaration.authorizeDefinitionEquationCandidate
                predicate definition
        (_, [definition :| [], generatedCandidates])
            | length obligations == NonEmpty.length generatedCandidates -> do
                Declaration.authorizeDefinitionEquationCandidate
                    predicate definition
                Declaration.authorizeVampireCandidateBatch
                    (NonEmpty.zipWith
                        (\candidate (factLocation, obligation) ->
                            ( factLocation
                            , candidate
                            , do
                                void
                                    (Declaration.useStagedCandidate
                                        definition)
                                pure obligation
                            ))
                        generatedCandidates
                        (NonEmpty.fromList obligations))
        _ ->
            Declaration.failDeclaration
                (Declaration.CheckedAuthorizationCandidateShapeMismatch
                    (if null obligations then 1 else 2)
                    (length stages))

validateStructureOccurrences
    :: Location
    -> Raw.StructDefn
    -> [CanonicalLexicalEntry]
    -> ExceptT ExactCompileError (Declaration.LoweringDriver) ()
validateStructureOccurrences location structure entries = do
    let Raw.LexicalItemSgPl forms structureMarker =
            Raw.structPhrase structure
        expected =
            CanonicalStructureNoun
                (Raw.sg forms)
                (Raw.pl forms)
                structureMarker
                : [ CanonicalStructureOperation command
                  | Raw.StructSymbol command <- Raw.structFixes structure
                  ]
    unless
        (entries == expected)
        (Except.throwError
            (ExactStructureOccurrenceMismatch location))

encodePreparedStructure
    :: SemanticEnvironmentDelta
    -> ObjectId
    -> [PreparedExactStructureFact]
    -> ByteString
encodePreparedStructure environment predicate generated =
    encodeCache do
        putCacheTag 0x04
        putSemanticEnvironmentDeltaCache environment
        putObjectIdCache predicate
        putCacheList
            (\(PreparedExactStructureFact _location target alias) -> do
                putCanonicalTermCache putObjectIdCache
                    (frozenCoreTerm target)
                putCacheText (semanticNameText alias))
            generated

prepareHead
    :: Raw.Block
    -> SemanticGlobalKey
    -> ExceptT
        ExactCompileError
        (Declaration.LoweringDriver)
        ( PreparedHead
        , ExactDeclarationFamily
        , Maybe (Elaborate (CanonicalTerm ObjectId))
        )
prepareHead block key =
    case block of
        Raw.BlockSig location _title _marker assumptions signature -> do
            unless (null assumptions)
                (Except.throwError
                    (ExactUnsupportedDeclarationBody location))
            head' <- prepareSignature location key signature
            pure (head', ExactSignature, Nothing)
        Raw.BlockAbbr location _title _marker abbreviation -> do
            (head', buildBody) <-
                prepareAbbreviation location key abbreviation
            pure (head', ExactAbbreviation, Just buildBody)
        Raw.BlockDefn location _title _marker definition -> do
            (head', buildBody) <-
                prepareDefinition location key definition
            pure (head', ExactDefinition, Just buildBody)
        _ ->
            Except.throwError (ExactUnsupportedDeclaration (locate block))

prepareSignature
    :: Location
    -> SemanticGlobalKey
    -> Raw.Signature
    -> ExceptT
        ExactCompileError
        (Declaration.LoweringDriver)
        PreparedHead
prepareSignature location key = \case
    Raw.SignatureAdj subject (Raw.Adj _ item arguments) -> do
        ensureAdjectiveKey location item key
        makePreparedHead
            location key (subject : arguments) TyProp
    Raw.SignatureSymbolic (Raw.SymbolPattern symbol parameters) nounPhrase -> do
        unless
            ( key
                == SemanticExpressionFunction
                    (Raw.mixfixPattern symbol)
            )
            (Except.throwError (ExactDeclarationHeadMismatch location))
        unless
            (exactSetNounPhrase nounPhrase)
            (Except.throwError (ExactUnsupportedDeclarationBody location))
        makePreparedHead location key parameters TySet
    _ ->
        Except.throwError (ExactUnsupportedDeclaration location)

prepareAbbreviation
    :: Location
    -> SemanticGlobalKey
    -> Raw.Abbreviation
    -> ExceptT
        ExactCompileError
        (Declaration.LoweringDriver)
        ( PreparedHead
        , Elaborate (CanonicalTerm ObjectId)
        )
prepareAbbreviation location key = \case
    Raw.AbbreviationEq (Raw.SymbolPattern symbol parameters) expression -> do
        ensureExpressionKey location symbol key
        makeContextualTransparentHead
            location key parameters TySet
            (compileExpressionAsSet expression)
    Raw.AbbreviationFun (Raw.Fun _ item parameters) term -> do
        ensureFunctionPhraseKey location item key
        makeContextualTransparentHead
            location key parameters TySet
            (compileTermAsSet term)
    Raw.AbbreviationAdj subject (Raw.Adj _ item arguments) statement -> do
        ensureAdjectiveKey location item key
        makeContextualTransparentHead
            location key (subject : arguments) TyProp
            (compileStatement statement)
    Raw.AbbreviationVerb subject (Raw.Verb _ item arguments) statement -> do
        ensureVerbKey location item key
        makeContextualTransparentHead
            location key (subject : arguments) TyProp
            (compileStatement statement)
    Raw.AbbreviationNoun subject (Raw.Noun _ item arguments) statement -> do
        ensureNounKey location item key
        makeContextualTransparentHead
            location key (subject : arguments) TyProp
            (compileStatement statement)
    Raw.AbbreviationRel left relation parameters right statement -> do
        ensureRelationKey location relation key
        makeContextualTransparentHead
            location key (parameters <> [left, right]) TyProp
            (compileStatement statement)

prepareDefinition
    :: Location
    -> SemanticGlobalKey
    -> Raw.Defn
    -> ExceptT
        ExactCompileError
        (Declaration.LoweringDriver)
        ( PreparedHead
        , Elaborate (CanonicalTerm ObjectId)
        )
prepareDefinition location key = \case
    Raw.Defn assumptions head' statement -> do
        unless (null assumptions)
            (Except.throwError
                (ExactUnsupportedDeclarationBody location))
        (parameters, resultType) <-
            definitionHead location key head'
        makeTransparentHead
            location key parameters resultType
            (compileStatement statement)
    Raw.DefnFun assumptions (Raw.Fun _ item parameters) symbolic term -> do
        unless (null assumptions && isNothing symbolic)
            (Except.throwError
                (ExactUnsupportedDeclarationBody location))
        ensureFunctionPhraseKey location item key
        makeTransparentHead
            location key parameters TySet
            (compileTermAsSet term)
    Raw.DefnOp (Raw.SymbolPattern symbol parameters) expression -> do
        ensureExpressionKey location symbol key
        makeTransparentHead
            location key parameters TySet
            (compileExpressionAsSet expression)

definitionHead
    :: Location
    -> SemanticGlobalKey
    -> Raw.DefnHead
    -> ExceptT
        ExactCompileError
        (Declaration.LoweringDriver)
        ([Raw.VarSymbol], CoreType)
definitionHead location key = \case
    Raw.DefnAdj annotation subject (Raw.Adj _ item arguments) -> do
        unless (isNothing annotation)
            (Except.throwError
                (ExactUnsupportedDeclarationBody location))
        ensureAdjectiveKey location item key
        pure (subject : arguments, TyProp)
    Raw.DefnVerb annotation subject (Raw.Verb _ item arguments) -> do
        unless (isNothing annotation)
            (Except.throwError
                (ExactUnsupportedDeclarationBody location))
        ensureVerbKey location item key
        pure (subject : arguments, TyProp)
    Raw.DefnNoun subject (Raw.Noun _ item arguments) -> do
        ensureNounKey location item key
        pure (subject : arguments, TyProp)
    Raw.DefnRel left relation parameters right -> do
        ensureRelationKey location relation key
        pure (parameters <> [left, right], TyProp)
    Raw.DefnSymbolicPredicate
            (Raw.PrefixPredicate command arity)
            _marker
            parameters -> do
        unless
            ( key
                == SemanticPrefixPredicate
                    command
                    (fromIntegral arity)
            )
            (Except.throwError (ExactDeclarationHeadMismatch location))
        pure (toList parameters, TyProp)

makeTransparentHead
    :: Location
    -> SemanticGlobalKey
    -> [Raw.VarSymbol]
    -> CoreType
    -> Elaborate (CanonicalTerm ObjectId)
    -> ExceptT
        ExactCompileError
        (Declaration.LoweringDriver)
        ( PreparedHead
        , Elaborate (CanonicalTerm ObjectId)
        )
makeTransparentHead location key parameters resultType body = do
    (prepared, binders) <-
        prepareParameters location key parameters resultType
    let close = do
            State.modify' (\state -> state{elaborationBinders = binders})
            body' <- body
            pure (foldr (const (CLam TySet)) body' parameters)
    pure (prepared, close)

makeContextualTransparentHead
    :: Location
    -> SemanticGlobalKey
    -> [Raw.VarSymbol]
    -> CoreType
    -> Elaborate (CanonicalTerm ObjectId)
    -> ExceptT
        ExactCompileError
        (Declaration.LoweringDriver)
        ( PreparedHead
        , Elaborate (CanonicalTerm ObjectId)
        )
makeContextualTransparentHead location key parameters resultType body = do
    (prepared, binders) <-
        prepareParameters location key parameters resultType
    let close = do
            State.modify' \state ->
                state
                    { elaborationBinders = binders
                    , elaborationContextualBinder =
                        Just (fromIntegral (length parameters))
                    }
            body' <- body
            pure (foldr (const (CLam TySet)) body' parameters)
    pure (prepared, close)

makePreparedHead
    :: Location
    -> SemanticGlobalKey
    -> [Raw.VarSymbol]
    -> CoreType
    -> ExceptT
        ExactCompileError
        (Declaration.LoweringDriver)
        PreparedHead
makePreparedHead location key parameters resultType = do
    (prepared, _binders) <-
        prepareParameters location key parameters resultType
    pure prepared

prepareParameters
    :: Location
    -> SemanticGlobalKey
    -> [Raw.VarSymbol]
    -> CoreType
    -> ExceptT
        ExactCompileError
        (Declaration.LoweringDriver)
        ( PreparedHead
        , Map.Map Raw.VarSymbol Natural
        )
prepareParameters
        location key parameters resultType = do
    case firstDuplicate parameters of
        Just duplicate ->
            Except.throwError
                (ExactDuplicateParameter location duplicate)
        Nothing -> pure ()
    let indices =
            reverse (take (length parameters) [0 ..])
        binders =
            Map.fromList
                (zip parameters indices)
        coreType = foldr (const (TyArrow TySet)) resultType parameters
    pure
        ( PreparedHead key parameters coreType
        , binders
        )

compileExpressionAsSet
    :: Raw.Expr
    -> Elaborate (CanonicalTerm ObjectId)
compileExpressionAsSet expression = do
    (term, actual) <- compileExpression expression
    unless (actual == TySet)
        (Except.throwError
            (ExactExpressionExpectedSet (locate expression) actual))
    pure term

compileTermAsSet
    :: Raw.Term
    -> Elaborate (CanonicalTerm ObjectId)
compileTermAsSet = \case
    Raw.TermExpr expression ->
        compileExpressionAsSet expression
    Raw.TermFun (Raw.Fun location item arguments) -> do
        let patterns = Raw.lexicalItemSgPlPattern item
            key = SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns)
        compiled <- traverse compileTermAsSet arguments
        applyResolved location key compiled
    Raw.TermQuantified _quantifier location _nounPhrase ->
        Except.throwError
            (ExactQuantifiedTermRequiresStatementSubject location)
    term ->
        Except.throwError
            (ExactUnsupportedDeclarationBody (locate term))

compileExpression
    :: Raw.Expr
    -> Elaborate (CanonicalTerm ObjectId, CoreType)
compileExpression = \case
    Raw.ExprVar variable -> do
        binders <- State.gets elaborationBinders
        case Map.lookup variable binders of
            Just index ->
                pure (CBound index, TySet)
            Nothing ->
                Except.throwError
                    (ExactFreeVariable (locate variable) variable)
    Raw.ExprInteger _location integer ->
        pure (COpaqueInteger (toInteger integer), TySet)
    Raw.ExprOp location symbol arguments -> do
        let key =
                SemanticExpressionFunction
                    (Raw.mixfixPattern symbol)
        compiled <- traverse compileExpression arguments
        case fixedSemanticMeaning key of
            Just (FixedIntrinsic intrinsic) ->
                applyTyped
                    location
                    (CIntrinsic intrinsic)
                    (coreIntrinsicType intrinsic)
                    compiled
            Just (FixedNegatedIntrinsic _intrinsic) ->
                impossible
                    "expression key resolved to a negated intrinsic"
            Just FixedEquality ->
                impossible
                    "expression key resolved to fixed equality"
            Just FixedDisequality ->
                impossible
                    "expression key resolved to fixed disequality"
            Nothing ->
                applyResolvedTyped
                    location
                    key
                    compiled
    Raw.ExprStructOp location symbol maybeArgument ->
        compileStructureOperation location symbol maybeArgument
    Raw.ExprFiniteSet _location elements -> do
        compiled <- traverse compileExpressionAsSet elements
        pure
            ( foldr
                canonicalSetInsert
                (CIntrinsic Empty)
                compiled
            , TySet
            )
    Raw.ExprSep _location variable bound predicate -> do
        bound' <- compileExpressionAsSet bound
        predicate' <-
            withSetBinders (variable :| [])
                (compileStatement predicate)
        pure
            ( CApp
                (CApp (CIntrinsic Sep) bound')
                (CLam TySet predicate')
            , TySet
            )
    Raw.ExprReplace _location value bounds condition -> do
        replacement <- compileReplacement value bounds condition
        pure (replacement, TySet)
    Raw.ExprReplacePred location _value _variable _bound _predicate ->
        Except.throwError
            (ExactUnsupportedDeclarationBody location)

compileStructureOperation
    :: Location
    -> Raw.StructSymbol
    -> Maybe Raw.Expr
    -> Elaborate (CanonicalTerm ObjectId, CoreType)
compileStructureOperation location symbol maybeArgument = do
    (argument, object) <-
        case maybeArgument of
            Just expression -> do
                term <- compileExpressionAsSet expression
                structures <- State.gets elaborationStructures
                case termStructureAnnotation term structures of
                    Just annotation -> do
                        object <-
                            maybe
                                (Except.throwError
                                    (ExactStructureOperationNotAvailable
                                        location symbol))
                                pure
                                (structureAnnotationOperation
                                    symbol annotation)
                        pure (term, object)
                    Nothing -> do
                        object <-
                            resolveUniqueStructureOperation location symbol
                        pure (term, object)
            Nothing -> do
                structures <- State.gets elaborationStructures
                case
                    [ (CBound index, object)
                    | (index, structure) <- Map.toAscList structures
                    , Just object <-
                        [structureAnnotationOperation symbol structure]
                    ] of
                    firstMatch : _ -> pure firstMatch
                    [] -> do
                        contextual <- State.gets elaborationContextualBinder
                        case contextual of
                            Nothing ->
                                Except.throwError
                                    (ExactStructureOperationNotAvailable
                                        location symbol)
                            Just index -> do
                                object <-
                                    resolveUniqueStructureOperation
                                        location symbol
                                recordContextualRequirement
                                    location symbol object
                                pure (CBound index, object)
    recordExactGlobal object (TyArrow TySet TySet)
    pure (CApp (CGlobal object) argument, TySet)
  where
    termStructureAnnotation term structures =
        case term of
            CBound index -> Map.lookup index structures
            _ -> Nothing

resolveUniqueStructureOperation
    :: Location
    -> Raw.StructSymbol
    -> Elaborate ObjectId
resolveUniqueStructureOperation location symbol = do
    objects <-
        State.lift
            (Except.lift
                (Declaration.resolveVisibleStructureOperationObjectsLowering
                    symbol))
    case objects of
        [] ->
            Except.throwError
                (ExactStructureOperationNotAvailable location symbol)
        [object] -> pure object
        _ ->
            Except.throwError
                (ExactStructureOperationAmbiguous location symbol objects)

recordContextualRequirement
    :: Location
    -> Raw.StructSymbol
    -> ObjectId
    -> Elaborate ()
recordContextualRequirement location symbol object = do
    existing <-
        State.gets
            (Map.lookup symbol . elaborationContextualRequirements)
    case existing of
        Nothing ->
            State.modify' \state ->
                state
                    { elaborationContextualRequirements =
                        Map.insert symbol object
                            (elaborationContextualRequirements state)
                    }
        Just actual
            | actual == object -> pure ()
            | otherwise ->
                Except.throwError
                    (ExactContextualRequirementConflict
                        location symbol actual object)

structureCarrierCast
    :: Location
    -> CanonicalTerm ObjectId
    -> Elaborate (CanonicalTerm ObjectId)
structureCarrierCast location term =
    case term of
        CBound index -> do
            annotation <- State.gets (Map.lookup index . elaborationStructures)
            case annotation of
                Nothing -> pure term
                Just structure -> do
                    carrier <-
                        maybe
                            (Except.throwError
                                (ExactStructureOperationNotAvailable
                                    location Raw.CarrierSymbol))
                            pure
                            (structureAnnotationOperation
                                Raw.CarrierSymbol structure)
                    recordExactGlobal carrier (TyArrow TySet TySet)
                    pure (CApp (CGlobal carrier) term)
        _ -> pure term

compileMembership
    :: Location
    -> Raw.Sign
    -> CanonicalTerm ObjectId
    -> CanonicalTerm ObjectId
    -> Elaborate (CanonicalTerm ObjectId)
compileMembership location sign element set = do
    checkedSet <- structureCarrierCast location set
    let proposition =
            CApp
                (CApp (CIntrinsic Member) element)
                checkedSet
    pure case sign of
        Raw.Positive -> proposition
        Raw.Negative -> logicalNot proposition

compileReplacement
    :: Raw.Expr
    -> NonEmpty (Raw.VarSymbol, Raw.Expr)
    -> Maybe Raw.Stmt
    -> Elaborate (CanonicalTerm ObjectId)
compileReplacement value ((variable, domain) :| remaining) condition = do
    domain' <- compileExpressionAsSet domain
    case remaining of
        [] -> do
            (value', condition') <-
                withSetBinders (variable :| []) do
                    value' <- compileExpressionAsSet value
                    condition' <- traverse compileStatement condition
                    pure (value', condition')
            let filteredDomain =
                    case condition' of
                        Nothing -> domain'
                        Just predicate ->
                            CApp
                                (CApp (CIntrinsic Sep) domain')
                                (CLam TySet predicate)
            pure
                (CApp
                    (CApp (CIntrinsic Repl) filteredDomain)
                    (CLam TySet value'))
        next : rest -> do
            nested <-
                withSetBinders (variable :| [])
                    (compileReplacement value (next :| rest) condition)
            pure
                (CApp
                    (CIntrinsic FamilyUnion)
                    (CApp
                        (CApp (CIntrinsic Repl) domain')
                        (CLam TySet nested)))

compileStatement
    :: Raw.Stmt
    -> Elaborate (CanonicalTerm ObjectId)
compileStatement = \case
    Raw.StmtFormula formula ->
        compileFormula formula
    Raw.StmtVerbPhrase
            (Raw.TermQuantified quantifier _location nounPhrase :| [])
            verbPhrase ->
        compileQuantifiedTermSubject quantifier nounPhrase
            (`compileVerbPhrase` verbPhrase)
    Raw.StmtVerbPhrase terms verbPhrase -> do
        subjects <- traverse compileTermAsSet terms
        logicalConjunction
            <$> traverse (`compileVerbPhrase` verbPhrase) subjects
    Raw.StmtNoun
            (Raw.TermQuantified quantifier _location quantified :| [])
            nounPhrase ->
        compileQuantifiedTermSubject quantifier quantified
            (`compileNounPhraseMaybe` nounPhrase)
    Raw.StmtNoun terms nounPhrase -> do
        subjects <- traverse compileTermAsSet terms
        logicalConjunction
            <$> traverse (`compileNounPhraseMaybe` nounPhrase) subjects
    Raw.StmtExists _location nounPhrase ->
        compileExistentialNounPhrase nounPhrase
    Raw.StmtQuantPhrase
            _location
            (Raw.QuantPhrase quantifier nounPhrase)
            statement ->
        compileQuantifiedNounPhrase quantifier nounPhrase statement
    Raw.StmtConnected connective location left right ->
        compileConnective
            (fromMaybe (locate left) location)
            connective
            compileStatement
            left
            right
    Raw.StmtNeg _location statement ->
        logicalNot <$> compileStatement statement
    Raw.SymbolicQuantified
            _location quantifier variables bound suchThat statement ->
        compileSymbolicQuantified
            quantifier variables bound suchThat (compileStatement statement)
    Raw.StmtStruct term rawPhrase -> do
        subject <- compileTermAsSet term
        annotation <-
            resolveStructureAnnotation (locate term) rawPhrase
        predicate <-
            maybe
                (impossible "an assertable structure has no predicate")
                pure
                (structureAnnotationPredicate annotation)
        recordExactGlobal
            predicate
            (TyArrow TySet TyProp)
        pure
            (CApp
                (CGlobal predicate)
                subject)

compileQuantifiedTermSubject
    :: Raw.Quantifier
    -> Raw.NounPhrase Maybe
    -> (CanonicalTerm ObjectId
        -> Elaborate (CanonicalTerm ObjectId))
    -> Elaborate (CanonicalTerm ObjectId)
compileQuantifiedTermSubject quantifier
        (Raw.NounPhrase left noun named right suchThat)
        compileBody =
    case named of
        Nothing ->
            withAnonymousSetBinder compileFor
        Just variable ->
            withSetBinders (variable :| []) do
                subject <- compileIntroducedVariable variable
                compileFor subject
  where
    compileFor subject = do
        constraints <-
            compileNounPhraseConstraints
                [subject] left noun right suchThat
        body <- compileBody subject
        pure (quantifyNounPhrase quantifier 1 constraints body)

compileSymbolicQuantified
    :: Raw.Quantifier
    -> NonEmpty Raw.VarSymbol
    -> Raw.Bound
    -> Maybe Raw.Stmt
    -> Elaborate (CanonicalTerm ObjectId)
    -> Elaborate (CanonicalTerm ObjectId)
compileSymbolicQuantified quantifier variables bound suchThat compileBody =
    withSetBinders variables do
        boundConstraints <-
            compileSymbolicBoundConstraintList variables bound
        suchThatConstraints <-
            maybeToList <$> traverse compileStatement suchThat
        body <- compileBody
        pure
            (quantifyNounPhrase
                quantifier
                (length (toList variables))
                (logicalConjunction
                    (boundConstraints <> suchThatConstraints))
                body)

compileSymbolicBoundConstraintList
    :: NonEmpty Raw.VarSymbol
    -> Raw.Bound
    -> Elaborate [CanonicalTerm ObjectId]
compileSymbolicBoundConstraintList variables = \case
    Raw.Unbounded ->
        pure []
    Raw.Bounded _location sign relation domain -> do
        subjects <- traverse compileIntroducedVariable variables
        domain' <- compileExpressionAsSet domain
        traverse
            (\subject -> do
                proposition <-
                    compileAtomicRelationTerms subject relation domain'
                pure case sign of
                    Raw.Positive -> proposition
                    Raw.Negative -> logicalNot proposition)
            (toList subjects)

compileAtomicRelationTerms
    :: CanonicalTerm ObjectId
    -> Raw.Relation
    -> CanonicalTerm ObjectId
    -> Elaborate (CanonicalTerm ObjectId)
compileAtomicRelationTerms left relation right =
    case relation of
        Raw.Relation location symbol parameters -> do
            let key =
                    SemanticRelation
                        (Raw.relationSymbolToken symbol)
                        (Raw.relationSymbolParameterArity symbol)
            compiledParameters <- traverse compileExpressionAsSet parameters
            case fixedSemanticMeaning key of
                Just FixedEquality
                    | null parameters -> pure (CEq TySet left right)
                Just FixedDisequality
                    | null parameters ->
                        pure (logicalNot (CEq TySet left right))
                Just (FixedIntrinsic Member)
                    | null parameters ->
                        compileMembership location Raw.Positive left right
                Just (FixedNegatedIntrinsic Member)
                    | null parameters ->
                        compileMembership location Raw.Negative left right
                Just (FixedIntrinsic intrinsic) -> do
                    (term, actual) <-
                        applyTyped
                            location
                            (CIntrinsic intrinsic)
                            (coreIntrinsicType intrinsic)
                            ((\term -> (term, TySet))
                                <$> (compiledParameters <> [left, right]))
                    unless (actual == TyProp)
                        (Except.throwError
                            (ExactFormulaExpectedProposition location actual))
                    pure term
                Just (FixedNegatedIntrinsic intrinsic) -> do
                    (term, actual) <-
                        applyTyped
                            location
                            (CIntrinsic intrinsic)
                            (coreIntrinsicType intrinsic)
                            ((\term -> (term, TySet))
                                <$> (compiledParameters <> [left, right]))
                    unless (actual == TyProp)
                        (Except.throwError
                            (ExactFormulaExpectedProposition location actual))
                    pure (logicalNot term)
                _ -> do
                    (term, actual) <-
                        applyResolvedTyped
                            location key
                            ((\term -> (term, TySet))
                                <$> (compiledParameters <> [left, right]))
                    unless (actual == TyProp)
                        (Except.throwError
                            (ExactFormulaExpectedProposition location actual))
                    pure term
        Raw.RelationExpr location expression ->
            compileRelationExpression location expression left right

compileVerbPhrase
    :: CanonicalTerm ObjectId
    -> Raw.VerbPhrase
    -> Elaborate (CanonicalTerm ObjectId)
compileVerbPhrase subject = \case
    Raw.VPVerb verb ->
        compileVerb subject verb
    Raw.VPVerbNot verb ->
        logicalNot <$> compileVerb subject verb
    Raw.VPAdj adjectives ->
        logicalConjunction
            <$> traverse (compileAdjective subject) adjectives
    Raw.VPAdjNot adjectives ->
        logicalNot . logicalConjunction
            <$> traverse (compileAdjective subject) adjectives

compileVerb
    :: CanonicalTerm ObjectId
    -> Raw.Verb
    -> Elaborate (CanonicalTerm ObjectId)
compileVerb subject (Raw.Verb location item arguments) = do
    let patterns = Raw.lexicalItemSgPlPattern item
    compiled <- traverse compileTermAsSet arguments
    applyResolvedPredicate
        location
        (SemanticVerb (Raw.sg patterns) (Raw.pl patterns))
        (subject : compiled)

compileAdjective
    :: CanonicalTerm ObjectId
    -> Raw.Adj
    -> Elaborate (CanonicalTerm ObjectId)
compileAdjective subject (Raw.Adj location item arguments) = do
    compiled <- traverse compileTermAsSet arguments
    applyResolvedPredicateChoice
        location
        ( SemanticRightAdjective (Raw.lexicalItemPattern item)
            :| [SemanticLeftAdjective (Raw.lexicalItemPattern item)]
        )
        (subject : compiled)

compileLeftAdjective
    :: CanonicalTerm ObjectId
    -> Raw.AdjL
    -> Elaborate (CanonicalTerm ObjectId)
compileLeftAdjective subject (Raw.AdjL location item arguments) = do
    compiled <- traverse compileTermAsSet arguments
    applyResolvedPredicate
        location
        (SemanticLeftAdjective (Raw.lexicalItemPattern item))
        (subject : compiled)

compileRightAttribute
    :: CanonicalTerm ObjectId
    -> Raw.AdjR
    -> Elaborate (CanonicalTerm ObjectId)
compileRightAttribute subject = \case
    Raw.AdjR location item arguments -> do
        compiled <- traverse compileTermAsSet arguments
        applyResolvedPredicate
            location
            (SemanticRightAdjective (Raw.lexicalItemPattern item))
            (subject : compiled)
    Raw.AttrRThat verbPhrase ->
        compileVerbPhrase subject verbPhrase

compileNoun
    :: CanonicalTerm ObjectId
    -> Raw.Noun
    -> Elaborate (CanonicalTerm ObjectId)
compileNoun subject (Raw.Noun location item arguments)
    | Lexicon.isBuiltinSetNoun item =
        pure logicalTruth
    | otherwise = do
        let patterns = Raw.lexicalItemSgPlPattern item
            key = SemanticNoun (Raw.sg patterns) (Raw.pl patterns)
        compiled <- traverse compileTermAsSet arguments
        case fixedSemanticMeaning key of
            Just (FixedIntrinsic Member) ->
                case compiled of
                    [set] ->
                        compileMembership location Raw.Positive subject set
                    _ ->
                        impossible
                            "the fixed element noun does not have one argument"
            Just (FixedIntrinsic intrinsic) -> do
                (term, actual) <-
                    applyTyped
                        location
                        (CIntrinsic intrinsic)
                        (coreIntrinsicType intrinsic)
                        ((\argument -> (argument, TySet))
                            <$> (subject : compiled))
                unless (actual == TyProp)
                    (Except.throwError
                        (ExactFormulaExpectedProposition location actual))
                pure term
            Just{} ->
                impossible "a fixed noun is not a predicate intrinsic"
            Nothing ->
                applyResolvedPredicate location key (subject : compiled)

compileNounPhraseConstraints
    :: [CanonicalTerm ObjectId]
    -> [Raw.AdjL]
    -> Raw.Noun
    -> [Raw.AdjR]
    -> Maybe Raw.Stmt
    -> Elaborate (CanonicalTerm ObjectId)
compileNounPhraseConstraints subjects left noun right suchThat = do
    nounConstraints <- traverse (`compileNoun` noun) subjects
    leftConstraints <- concat
        <$> traverse
            (\subject -> traverse (compileLeftAdjective subject) left)
            subjects
    rightConstraints <- concat
        <$> traverse
            (\subject -> traverse (compileRightAttribute subject) right)
            subjects
    suchThatConstraint <- traverse compileStatement suchThat
    pure
        (logicalConjunction
            ( nounConstraints
                <> leftConstraints
                <> rightConstraints
                <> maybeToList suchThatConstraint
            ))

compileNounPhraseMaybe
    :: CanonicalTerm ObjectId
    -> Raw.NounPhrase Maybe
    -> Elaborate (CanonicalTerm ObjectId)
compileNounPhraseMaybe subject
        (Raw.NounPhrase left noun named right suchThat) =
    case named of
        Nothing ->
            compileNounPhraseConstraints
                [subject] left noun right suchThat
        Just variable -> do
            abstracted <-
                withSetBinders (variable :| [])
                    (compileNounPhraseConstraints
                        [CBound 0] left noun right suchThat)
            pure (instantiateCanonical subject abstracted)

compileExistentialNounPhrase
    :: Raw.NounPhrase []
    -> Elaborate (CanonicalTerm ObjectId)
compileExistentialNounPhrase
        (Raw.NounPhrase left noun variables right suchThat) =
    case NonEmpty.nonEmpty variables of
        Just binders ->
            withSetBinders binders do
                subjects <- traverse compileIntroducedVariable binders
                constraints <-
                    compileNounPhraseConstraints
                        (toList subjects) left noun right suchThat
                pure
                    (foldr
                        (const logicalExists)
                        constraints
                        binders)
        Nothing ->
            withAnonymousSetBinder \subject ->
                logicalExists
                    <$> compileNounPhraseConstraints
                        [subject] left noun right suchThat

compileQuantifiedNounPhrase
    :: Raw.Quantifier
    -> Raw.NounPhrase []
    -> Raw.Stmt
    -> Elaborate (CanonicalTerm ObjectId)
compileQuantifiedNounPhrase quantifier
        (Raw.NounPhrase left noun variables right suchThat)
        statement =
    case NonEmpty.nonEmpty variables of
        Just binders ->
            withSetBinders binders do
                subjects <- traverse compileIntroducedVariable binders
                constraints <-
                    compileNounPhraseConstraints
                        (toList subjects) left noun right suchThat
                body <- compileStatement statement
                pure
                    (quantifyNounPhrase
                        quantifier
                        (length (toList binders))
                        constraints
                        body)
        Nothing ->
            withAnonymousSetBinder \subject -> do
                constraints <-
                    compileNounPhraseConstraints
                        [subject] left noun right suchThat
                body <- compileStatement statement
                pure (quantifyNounPhrase quantifier 1 constraints body)

quantifyNounPhrase
    :: Raw.Quantifier
    -> Int
    -> CanonicalTerm ObjectId
    -> CanonicalTerm ObjectId
    -> CanonicalTerm ObjectId
quantifyNounPhrase quantifier binderCount constraints body =
    case quantifier of
        Raw.Universally ->
            quantify
                (if constraints == logicalTruth
                    then body
                    else CImp constraints body)
        Raw.Existentially ->
            quantify
                (if constraints == logicalTruth
                    then body
                    else logicalAnd constraints body)
        Raw.Nonexistentially ->
            logicalNot
                (quantify
                    (if constraints == logicalTruth
                        then body
                        else logicalAnd constraints body))
  where
    quantify scoped =
        foldr (const binder) scoped [1 .. binderCount]
    binder = case quantifier of
        Raw.Universally -> CForall TySet
        Raw.Existentially -> logicalExists
        Raw.Nonexistentially -> logicalExists

withAnonymousSetBinder
    :: (CanonicalTerm ObjectId -> Elaborate value)
    -> Elaborate value
withAnonymousSetBinder action = do
    outer <- State.gets elaborationBinders
    outerStructures <- State.gets elaborationStructures
    outerContextual <- State.gets elaborationContextualBinder
    State.modify' \state ->
        state
            { elaborationBinders = (+ 1) <$> outer
            , elaborationStructures =
                Map.mapKeysMonotonic (+ 1) outerStructures
            , elaborationContextualBinder = (+ 1) <$> outerContextual
            }
    result <- action (CBound 0)
    State.modify' \state ->
        state
            { elaborationBinders = outer
            , elaborationStructures = outerStructures
            , elaborationContextualBinder = outerContextual
            }
    pure result

withSetBinders
    :: NonEmpty Raw.VarSymbol
    -> Elaborate value
    -> Elaborate value
withSetBinders variables action = do
    outer <- State.gets elaborationBinders
    outerStructures <- State.gets elaborationStructures
    outerContextual <- State.gets elaborationContextualBinder
    case firstDuplicate (toList variables) of
        Just duplicate ->
            Except.throwError
                (ExactDuplicateLocalBinder
                    (locate duplicate)
                    duplicate)
        Nothing -> pure ()
    case find (`Map.member` outer) (toList variables) of
        Just shadowed ->
            Except.throwError
                (ExactDuplicateLocalBinder
                    (locate shadowed)
                    shadowed)
        Nothing -> pure ()
    let binderCount = fromIntegral (length (toList variables))
        shifted = (+ binderCount) <$> outer
        introduced =
            Map.fromList
                (zip
                    (toList variables)
                    (reverse [0 .. binderCount - 1]))
    State.modify' \state ->
        state
            { elaborationBinders = introduced <> shifted
            , elaborationStructures =
                Map.mapKeysMonotonic (+ binderCount) outerStructures
            , elaborationContextualBinder =
                (+ binderCount) <$> outerContextual
            }
    result <- action
    State.modify' \state ->
        state
            { elaborationBinders = outer
            , elaborationStructures = outerStructures
            , elaborationContextualBinder = outerContextual
            }
    pure result

compileFormula
    :: Raw.Formula
    -> Elaborate (CanonicalTerm ObjectId)
compileFormula = \case
    Raw.FormulaChain chain ->
        compileRelationChain chain
    Raw.PropositionalConstant _ Raw.IsBottom ->
        pure CFalsum
    Raw.PropositionalConstant _ Raw.IsTop ->
        pure (CImp CFalsum CFalsum)
    Raw.FormulaNeg _ formula ->
        logicalNot <$> compileFormula formula
    Raw.FormulaPredicate
            location
            (Raw.PrefixPredicate command arity)
            _marker
            arguments -> do
        compiled <- traverse compileExpression arguments
        (term, actual) <-
            applyResolvedTyped
                location
                (SemanticPrefixPredicate
                    command
                    (fromIntegral arity))
                (toList compiled)
        unless (actual == TyProp)
            (Except.throwError
                (ExactFormulaExpectedProposition location actual))
        pure term
    Raw.Connected location connective left right ->
        compileConnective
            location
            connective
            compileFormula
            left
            right
    Raw.FormulaQuantified
            _location quantifier variables bound formula ->
        compileSymbolicQuantified
            quantifier variables bound Nothing (compileFormula formula)
compileConnective
    :: Location
    -> Raw.Connective
    -> (input -> Elaborate (CanonicalTerm ObjectId))
    -> input
    -> input
    -> Elaborate (CanonicalTerm ObjectId)
compileConnective _location connective compile left right = do
    left' <- compile left
    right' <- compile right
    case connective of
        Raw.Conjunction ->
            pure (logicalAnd left' right')
        Raw.Disjunction ->
            pure (logicalOr left' right')
        Raw.Implication ->
            pure (CImp left' right')
        Raw.Equivalence ->
            pure (CEq TyProp left' right')
        Raw.ExclusiveOr ->
            pure
                (logicalAnd
                    (logicalOr left' right')
                    (logicalNot (logicalAnd left' right')))
        Raw.NegatedDisjunction ->
            pure (logicalNot (logicalOr left' right'))

logicalAnd
    :: CanonicalTerm global
    -> CanonicalTerm global
    -> CanonicalTerm global
logicalAnd left right =
    logicalNot (CImp left (logicalNot right))

logicalTruth :: CanonicalTerm global
logicalTruth =
    CImp CFalsum CFalsum

logicalConjunction
    :: (Foldable collection, Eq global)
    => collection (CanonicalTerm global)
    -> CanonicalTerm global
logicalConjunction =
    foldr combine logicalTruth
  where
    combine proposition remaining
        | proposition == logicalTruth = remaining
        | remaining == logicalTruth = proposition
        | otherwise = logicalAnd proposition remaining

logicalOr
    :: CanonicalTerm global
    -> CanonicalTerm global
    -> CanonicalTerm global
logicalOr left right =
    CImp (logicalNot left) right

logicalExists
    :: CanonicalTerm global
    -> CanonicalTerm global
logicalExists body =
    logicalNot (CForall TySet (logicalNot body))

compileAtomicRelation
    :: NonEmpty Raw.Expr
    -> Raw.Relation
    -> NonEmpty Raw.Expr
    -> Elaborate (CanonicalTerm ObjectId)
compileAtomicRelation left relation right =
    case (toList left, relation, toList right) of
        ([leftExpression], Raw.Relation location symbol parameters, [rightExpression]) -> do
            let key =
                    SemanticRelation
                        (Raw.relationSymbolToken symbol)
                        (Raw.relationSymbolParameterArity symbol)
            case fixedSemanticMeaning key of
                Just FixedEquality
                    | null parameters -> do
                        left' <- compileExpressionAsSet leftExpression
                        right' <- compileExpressionAsSet rightExpression
                        pure (CEq TySet left' right')
                    | otherwise ->
                        Except.throwError
                            (ExactUnsupportedDeclarationBody location)
                Just FixedDisequality
                    | null parameters -> do
                        left' <- compileExpressionAsSet leftExpression
                        right' <- compileExpressionAsSet rightExpression
                        pure (logicalNot (CEq TySet left' right'))
                    | otherwise ->
                        Except.throwError
                            (ExactUnsupportedDeclarationBody location)
                Just (FixedIntrinsic Member)
                    | null parameters -> do
                        left' <- compileExpressionAsSet leftExpression
                        right' <- compileExpressionAsSet rightExpression
                        compileMembership
                            location Raw.Positive left' right'
                Just (FixedNegatedIntrinsic Member)
                    | null parameters -> do
                        left' <- compileExpressionAsSet leftExpression
                        right' <- compileExpressionAsSet rightExpression
                        compileMembership
                            location Raw.Negative left' right'
                Just (FixedIntrinsic intrinsic) -> do
                    compiled <- traverse compileExpression
                        (parameters <> [leftExpression, rightExpression])
                    (term, actual) <-
                        applyTyped
                            location
                            (CIntrinsic intrinsic)
                            (coreIntrinsicType intrinsic)
                            compiled
                    unless (actual == TyProp)
                        (Except.throwError
                            (ExactFormulaExpectedProposition location actual))
                    pure term
                Just (FixedNegatedIntrinsic intrinsic) -> do
                    compiled <- traverse compileExpression
                        (parameters <> [leftExpression, rightExpression])
                    (term, actual) <-
                        applyTyped
                            location
                            (CIntrinsic intrinsic)
                            (coreIntrinsicType intrinsic)
                            compiled
                    unless (actual == TyProp)
                        (Except.throwError
                            (ExactFormulaExpectedProposition location actual))
                    pure (logicalNot term)
                Nothing -> do
                    compiled <- traverse compileExpression
                        (parameters <> [leftExpression, rightExpression])
                    (term, actual) <-
                        applyResolvedTyped location key compiled
                    unless (actual == TyProp)
                        (Except.throwError
                            (ExactFormulaExpectedProposition location actual))
                    pure term
        ([leftExpression], Raw.RelationExpr location expression, [rightExpression]) -> do
            left' <- compileExpressionAsSet leftExpression
            right' <- compileExpressionAsSet rightExpression
            compileRelationExpression location expression left' right'
        _ ->
            Except.throwError
                (ExactUnsupportedDeclarationBody (locate relation))

compileRelationExpression
    :: Location
    -> Raw.Expr
    -> CanonicalTerm ObjectId
    -> CanonicalTerm ObjectId
    -> Elaborate (CanonicalTerm ObjectId)
compileRelationExpression location expression left right = do
    relation <- compileExpressionAsSet expression
    pair <-
        applyResolved
            location
            (SemanticExpressionFunction
                (Raw.mixfixPattern Raw.PairSymbol))
            [left, right]
    compileMembership location Raw.Positive pair relation

compileRelationChain
    :: Raw.Chain
    -> Elaborate (CanonicalTerm ObjectId)
compileRelationChain chain =
    logicalConjunction <$> traverse compileLink (chainLinks chain)
  where
    compileLink (sign, relation, left, right) = do
        proposition <-
            compileAtomicRelation
                (left :| []) relation (right :| [])
        pure case sign of
            Raw.Positive -> proposition
            Raw.Negative -> logicalNot proposition

    chainLinks = \case
        Raw.ChainBase left sign relation right ->
            [ (sign, relation, leftExpression, rightExpression)
            | leftExpression <- toList left
            , rightExpression <- toList right
            ]
        Raw.ChainCons left sign relation rest ->
            let firstRight = chainFirstLeft rest
            in
                [ (sign, relation, leftExpression, rightExpression)
                | leftExpression <- toList left
                , rightExpression <- toList firstRight
                ]
                <> chainLinks rest

    chainFirstLeft = \case
        Raw.ChainBase left _sign _relation _right -> left
        Raw.ChainCons left _sign _relation _rest -> left

applyResolved
    :: Location
    -> SemanticGlobalKey
    -> [CanonicalTerm ObjectId]
    -> Elaborate (CanonicalTerm ObjectId)
applyResolved location key arguments = do
    (term, actual) <-
        applyResolvedTyped
            location key ((\argument -> (argument, TySet)) <$> arguments)
    unless (actual == TySet)
        (Except.throwError
            (ExactExpressionExpectedSet location actual))
    pure term

applyResolvedPredicate
    :: Location
    -> SemanticGlobalKey
    -> [CanonicalTerm ObjectId]
    -> Elaborate (CanonicalTerm ObjectId)
applyResolvedPredicate location key =
    applyResolvedPredicateChoice location (key :| [])

applyResolvedPredicateChoice
    :: Location
    -> NonEmpty SemanticGlobalKey
    -> [CanonicalTerm ObjectId]
    -> Elaborate (CanonicalTerm ObjectId)
applyResolvedPredicateChoice location keys arguments = do
    case firstFixedMeaning (toList keys) of
        Just meaning ->
            maybe
                (impossible
                    "a fixed equality predicate has an invalid source arity")
                pure
                (lowerFixedEqualityPredicate meaning arguments)
        Nothing -> do
            visible <- for (toList keys) \key -> do
                found <-
                    State.lift
                        (Except.lift
                            (Declaration.resolveVisibleGlobalLowering key))
                pure ((\target -> (key, target)) <$> found)
            case catMaybes visible of
                [(key, _target)] -> do
                    (term, actual) <-
                        applyResolvedTyped
                            location key
                            ((\argument -> (argument, TySet)) <$> arguments)
                    unless (actual == TyProp)
                        (Except.throwError
                            (ExactFormulaExpectedProposition location actual))
                    pure term
                [] ->
                    Except.throwError
                        (ExactGlobalNotVisible location (NonEmpty.head keys))
                _ ->
                    impossible
                        "one adjective surface resolves to several exact globals"
  where
    firstFixedMeaning =
        foldr
            (\key found -> fixedSemanticMeaning key <|> found)
            Nothing

applyResolvedTyped
    :: Location
    -> SemanticGlobalKey
    -> [(CanonicalTerm ObjectId, CoreType)]
    -> Elaborate (CanonicalTerm ObjectId, CoreType)
applyResolvedTyped location key arguments = do
    visible <-
        State.lift
            (Except.lift
                (Declaration.resolveVisibleGlobalContentLowering key))
    (target, content, dependencies) <-
        maybe
            (Except.throwError (ExactGlobalNotVisible location key))
            pure
            visible
    case target of
        GlobalReference identity -> do
            let coreType = objectContentType content
            State.modify' \state ->
                state
                    { elaborationGlobals =
                        Map.insert
                            identity coreType
                            (elaborationGlobals state)
                    }
            applyTyped location (CGlobal identity) coreType arguments
        TransparentExpansion _identity ->
            case content of
                TransparentObjectContent _theory coreType body -> do
                    State.modify' \state ->
                        state
                            { elaborationGlobals =
                                Map.union
                                    dependencies
                                    (elaborationGlobals state)
                            }
                    applyExpandedTyped
                        location body coreType arguments
                _ ->
                    impossible
                        "validated transparent expansion has opaque content"
        ContextualTransparentExpansion _identity requirements ->
            case content of
                TransparentObjectContent _theory coreType body -> do
                    State.modify' \state ->
                        state
                            { elaborationGlobals =
                                Map.union
                                    dependencies
                                    (elaborationGlobals state)
                            }
                    contextArgument <-
                        resolveContextualExpansionArgument
                            location key requirements
                    applyExpandedTyped
                        location body coreType
                        ((contextArgument, TySet) : arguments)
                _ ->
                    impossible
                        "validated contextual expansion has opaque content"

resolveContextualExpansionArgument
    :: Location
    -> SemanticGlobalKey
    -> Map.Map Raw.StructSymbol ObjectId
    -> Elaborate (CanonicalTerm ObjectId)
resolveContextualExpansionArgument location key requirements = do
    contextual <- State.gets elaborationContextualBinder
    case contextual of
        Just index -> do
            traverse_
                (uncurry (recordContextualRequirement location))
                (Map.toAscList requirements)
            pure (CBound index)
        Nothing -> do
            structures <- State.gets elaborationStructures
            case
                [ CBound index
                | (index, structure) <- Map.toAscList structures
                , all
                    (\(symbol, object) ->
                        structureAnnotationOperation symbol structure
                            == Just object)
                    (Map.toAscList requirements)
                ] of
                firstMatch : _ -> pure firstMatch
                [] ->
                    Except.throwError
                        (ExactContextualExpansionNotAvailable location key)

applyExpandedTyped
    :: Location
    -> CanonicalTerm ObjectId
    -> CoreType
    -> [(CanonicalTerm ObjectId, CoreType)]
    -> Elaborate (CanonicalTerm ObjectId, CoreType)
applyExpandedTyped location body coreType arguments =
    foldM step (body, coreType) arguments
  where
    step (current, currentType) (argument, argumentType) =
        case currentType of
            TyArrow expected result
                | expected == argumentType ->
                    pure
                        ( case current of
                            CLam binderType lambdaBody
                                | binderType == expected ->
                                    instantiateCanonical
                                        argument lambdaBody
                            _ -> CApp current argument
                        , result
                        )
                | otherwise ->
                    Except.throwError
                        (ExactApplicationArgumentMismatch
                            location expected argumentType)
            actual ->
                Except.throwError
                    (ExactApplicationExpectedFunction location actual)

applyTyped
    :: Location
    -> CanonicalTerm ObjectId
    -> CoreType
    -> [(CanonicalTerm ObjectId, CoreType)]
    -> Elaborate (CanonicalTerm ObjectId, CoreType)
applyTyped location function functionType arguments =
    foldM step (function, functionType) arguments
  where
    step (currentFunction, currentType) (argument, argumentType) =
        case currentType of
            TyArrow expected result
                | expected == argumentType ->
                    pure (CApp currentFunction argument, result)
                | otherwise ->
                    Except.throwError
                        (ExactApplicationArgumentMismatch
                            location expected argumentType)
            actual ->
                Except.throwError
                    (ExactApplicationExpectedFunction location actual)

logicalNot :: CanonicalTerm global -> CanonicalTerm global
logicalNot proposition =
    CImp proposition CFalsum

ensureExpressionKey
    :: MonadError ExactCompileError monad
    => Location
    -> Raw.FunctionSymbol
    -> SemanticGlobalKey
    -> monad ()
ensureExpressionKey location symbol key =
    unless
        (key == SemanticExpressionFunction (Raw.mixfixPattern symbol))
        (throwError (ExactDeclarationHeadMismatch location))

ensureAdjectiveKey
    :: MonadError ExactCompileError monad
    => Location
    -> Raw.LexicalItem
    -> SemanticGlobalKey
    -> monad ()
ensureAdjectiveKey location item key =
    unless
        ( key == SemanticLeftAdjective (Raw.lexicalItemPattern item)
          || key == SemanticRightAdjective (Raw.lexicalItemPattern item)
        )
        (throwError (ExactDeclarationHeadMismatch location))

ensureFunctionPhraseKey
    :: MonadError ExactCompileError monad
    => Location
    -> Raw.LexicalItemSgPl
    -> SemanticGlobalKey
    -> monad ()
ensureFunctionPhraseKey location item key =
    let patterns = Raw.lexicalItemSgPlPattern item
    in unless
        (key == SemanticFunctionPhrase (Raw.sg patterns) (Raw.pl patterns))
        (throwError (ExactDeclarationHeadMismatch location))

ensureNounKey
    :: MonadError ExactCompileError monad
    => Location
    -> Raw.LexicalItemSgPl
    -> SemanticGlobalKey
    -> monad ()
ensureNounKey location item key =
    let patterns = Raw.lexicalItemSgPlPattern item
    in unless
        (key == SemanticNoun (Raw.sg patterns) (Raw.pl patterns))
        (throwError (ExactDeclarationHeadMismatch location))

ensureVerbKey
    :: MonadError ExactCompileError monad
    => Location
    -> Raw.LexicalItemSgPl
    -> SemanticGlobalKey
    -> monad ()
ensureVerbKey location item key =
    let patterns = Raw.lexicalItemSgPlPattern item
    in unless
        (key == SemanticVerb (Raw.sg patterns) (Raw.pl patterns))
        (throwError (ExactDeclarationHeadMismatch location))

ensureRelationKey
    :: MonadError ExactCompileError monad
    => Location
    -> Raw.RelationSymbol
    -> SemanticGlobalKey
    -> monad ()
ensureRelationKey location relation key =
    unless
        ( key
            == SemanticRelation
                (Raw.relationSymbolToken relation)
                (Raw.relationSymbolParameterArity relation)
        )
        (throwError (ExactDeclarationHeadMismatch location))

exactSetNounPhrase :: Raw.NounPhrase Maybe -> Bool
exactSetNounPhrase = \case
    Raw.NounPhrase
            []
            (Raw.Noun _ item [])
            Nothing
            []
            Nothing ->
        Lexicon.isBuiltinSetNoun item
    _ -> False

encodePreparedSyntax
    :: ExactDeclarationFamily
    -> PreparedHead
    -> PreparedBody
    -> Maybe SemanticName
    -> ByteString
encodePreparedSyntax
        family (PreparedHead key _parameters coreType) body alias =
    encodeCache do
        putCacheTag case family of
            ExactSignature -> 0x00
            ExactAbbreviation -> 0x01
            ExactDefinition -> 0x02
        putSemanticGlobalKeyCache key
        putCoreTypeCache coreType
        case body of
            OpaqueBody -> putCacheTag 0x00
            TransparentBody canonical -> do
                putCacheTag 0x01
                putCanonicalTermCache putObjectIdCache canonical
            ContextualTransparentBody requirements canonical -> do
                putCacheTag 0x02
                putCanonicalCacheMap
                    (\(Raw.StructSymbol symbol) -> putCacheText symbol)
                    putObjectIdCache
                    requirements
                putCanonicalTermCache putObjectIdCache canonical
        putCacheMaybe
            (putCacheText . semanticNameText)
            alias

encodePreparedSourceAxiom
    :: ScopedCheckedCore ObjectId
    -> SemanticName
    -> ByteString
encodePreparedSourceAxiom proposition alias =
    encodeCache do
        putCacheTag 0x03
        putCanonicalTermCache putObjectIdCache
            (scopedCoreTerm proposition)
        putCacheText (semanticNameText alias)

definitionAlias :: Raw.Block -> Maybe SemanticName
definitionAlias = \case
    Raw.BlockDefn _location _title (Raw.Marker marker) _definition ->
        Just (semanticName marker)
    _ -> Nothing

firstDuplicate :: Ord value => [value] -> Maybe value
firstDuplicate =
    go Set.empty
  where
    go _seen [] = Nothing
    go seen (value : rest)
        | value `Set.member` seen = Just value
        | otherwise = go (Set.insert value seen) rest