path: root/source/Felix/Checking/SetConstruction.hs

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

-- | Checked source semantics for named separation and functional replacement.
--
-- A value of 'NamedSetConstruction' is the sole transient owner of the
-- source decomposition.  Its smart constructors validate the complete
-- telescope and derive one canonical term.  Local views, transparent content,
-- direct extensional facts, and cache-scoped descriptors all consume that
-- same checked value.
module Felix.Checking.SetConstruction
    ( NamedSetConstruction
    , checkedSeparationConstruction
    , checkedFunctionalReplacementConstruction
    , namedSetConstructionTerm
    , namedSetConstructionLocalViews
    , namedSetConstructionClosedBody
    , SetConstructionFoundation
    , setConstructionFoundation
    , checkedFoundationSetConstruction
    , NamedSetConstructionFact
    , namedSetConstructionFactProposition
    , namedSetConstructionFactDescriptor
    , namedSetConstructionObjectFact
    , CheckedRelationalSetConstruction
    , checkedRelationalReplacementConstruction
    , relationalSetConstructionTerm
    , relationalSetConstructionFunctionality
    , relationalSetConstructionClosedFunctionality
    , relationalSetConstructionLocalViews
    , relationalSetConstructionClosedBody
    , RelationalSetConstructionFact
    , relationalSetConstructionFactProposition
    , relationalSetConstructionFactDescriptor
    , relationalSetConstructionObjectFact
    ) where

import Base hiding (Empty)
import Felix.Checking.Core
import Felix.Checking.Foundation
import Felix.Checking.Identity
import Felix.Cache.Codec
    ( CacheDigest
    , encodeCache
    , hashCacheFields
    , putCanonicalTermCache
    , putCoreTypeCache
    )

import Data.List.NonEmpty qualified as NonEmpty
import Data.Map.Strict qualified as Map
import Data.Set qualified as Set
import Numeric.Natural (Natural)


-- | The exact fixed rows used by the narrow derived extensionality schema.
-- Proof-local construction obtains these rows through the confined foundation
-- lookup; declaration authorization obtains them from 'CheckedFoundation'.
data SetConstructionFoundation = SetConstructionFoundation
    !(FrozenCheckedCore Void)
    !(FrozenCheckedCore Void)
    !(FrozenCheckedCore Void)
    !(FrozenCheckedCore Void)

setConstructionFoundation
    :: FrozenCheckedCore Void
    -> FrozenCheckedCore Void
    -> FrozenCheckedCore Void
    -> FrozenCheckedCore Void
    -> SetConstructionFoundation
setConstructionFoundation =
    SetConstructionFoundation

checkedFoundationSetConstruction
    :: CheckedFoundation
    -> SetConstructionFoundation
checkedFoundationSetConstruction foundation =
    SetConstructionFoundation
        (foundationAxiomFrozen foundation FamilyUnionCharacteristic)
        (foundationAxiomFrozen foundation SeparationCharacteristic)
        (foundationAxiomFrozen foundation ReplacementCharacteristic)
        (foundationAxiomFrozen foundation SetChooseWitness)

data NamedSetConstruction global = NamedSetConstruction
    ![CoreType]
    !(Map.Map global CoreType)
    !(NamedSetConstructionShape global)
    !(BuiltSetConstruction global)
    deriving stock (Eq)

data NamedSetConstructionShape global
    = SeparationShape
        !(CanonicalTerm global)
        !(CanonicalTerm global)
    | FunctionalReplacementShape
        !(NonEmpty (CanonicalTerm global))
        !(CanonicalTerm global)
        !(Maybe (CanonicalTerm global))
    deriving stock (Eq)

-- | The one canonical build result retained by the checked construction.
-- Characteristic applications describe the exact primitive rows used by the
-- derived theorem schema; the flattened body is the deterministic composition
-- of those rows for the source telescope.
data BuiltSetConstruction global = BuiltSetConstruction
    !(CanonicalTerm global)
    !(CanonicalTerm global)
    ![CheckedCharacteristicApplication global]
    deriving stock (Eq)

data CheckedCharacteristicApplication global =
    CheckedCharacteristicApplication
        !CoreIntrinsicTag
        ![CoreType]
        !(CanonicalTerm global)
        !(NonEmpty (CoreType, CanonicalTerm global))
        !(CanonicalTerm global)
    deriving stock (Eq)

-- | One checked relational replacement.  Unlike the unconditional named
-- constructions above, its flattened membership theorem is available only
-- after the separately checked functionality proposition has authority.
-- This value owns the source telescope, the one canonical choice/replacement
-- term, and the exact primitive characteristic applications used by that
-- narrow derived schema.
data CheckedRelationalSetConstruction global =
    CheckedRelationalSetConstruction
        ![CoreType]
        !(Map.Map global CoreType)
        !(CanonicalTerm global)
        !(CanonicalTerm global)
        !(CanonicalTerm global)
        !(CanonicalTerm global)
        !(CanonicalTerm global)
        ![CheckedCharacteristicApplication global]
    deriving stock (Eq)

-- | Validate one source relational replacement.  The relation is checked in
-- the nearest-first context @[range, domain] <> outer@, matching the source
-- binder order @y x A P@ without retaining source syntax.
checkedRelationalReplacementConstruction
    :: Ord global
    => (global -> Maybe CoreType)
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Maybe (CheckedRelationalSetConstruction global)
checkedRelationalReplacementConstruction globalType domain relation = do
    guard (scopedCoreType domain == TySet)
    guard (scopedCoreType relation == TyProp)
    let context = scopedCoreContext domain
    guard (scopedCoreContext relation == TySet : TySet : context)
    globals <-
        captureGlobalTypes globalType
            [scopedCoreTerm domain, scopedCoreTerm relation]
    let domainTerm = scopedCoreTerm domain
        relationTerm = scopedCoreTerm relation
        domainPredicate = CLam TySet (logicalExists relationTerm)
        restrictedDomain = applyIntrinsic2 Sep domainTerm domainPredicate
        choiceFunction =
            CLam TySet
                (applyIntrinsic SetChoose (CLam TySet relationTerm))
        replacement = applyIntrinsic2 Repl restrictedDomain choiceFunction
        functionality = relationalFunctionality domainTerm relationTerm
        membership = relationalMembership domainTerm relationTerm
        applications =
            [ characteristicApplication
                Sep context restrictedDomain
                [ (TySet, domainTerm)
                , (TyArrow TySet TyProp, domainPredicate)
                ]
            , characteristicApplication
                Repl context replacement
                [ (TySet, restrictedDomain)
                , (TyArrow TySet TySet, choiceFunction)
                ]
            ]
        construction =
            CheckedRelationalSetConstruction
                context globals domainTerm relationTerm replacement
                functionality membership applications
    _ <- checkedRelationalDerived construction context TySet replacement
    _ <- checkedRelationalDerived construction context TyProp functionality
    _ <- checkedRelationalDerived
        construction (TySet : context) TyProp membership
    pure construction

-- | Check one source separation.  The callback supplies the exact visible
-- type of every global used by its already checked components.
checkedSeparationConstruction
    :: Ord global
    => (global -> Maybe CoreType)
    -> ScopedCheckedCore global
    -> ScopedCheckedCore global
    -> Maybe (NamedSetConstruction global)
checkedSeparationConstruction globalType bound predicate = do
    guard (scopedCoreType bound == TySet)
    guard (scopedCoreType predicate == TyProp)
    let context = scopedCoreContext bound
    guard (scopedCoreContext predicate == TySet : context)
    globals <-
        captureGlobalTypes globalType
            [scopedCoreTerm bound, scopedCoreTerm predicate]
    finishConstruction
        context
        globals
        (SeparationShape
            (scopedCoreTerm bound)
            (scopedCoreTerm predicate))

-- | Check source-ordered functional replacement once.  Domain @i@ is checked
-- beneath exactly the preceding @i - 1@ source binders; the value and optional
-- condition are checked beneath the complete telescope.
checkedFunctionalReplacementConstruction
    :: Ord global
    => (global -> Maybe CoreType)
    -> NonEmpty (ScopedCheckedCore global)
    -> ScopedCheckedCore global
    -> Maybe (ScopedCheckedCore global)
    -> Maybe (NamedSetConstruction global)
checkedFunctionalReplacementConstruction globalType domains value condition = do
    let domainList = NonEmpty.toList domains
        firstDomain = NonEmpty.head domains
    guard (scopedCoreType firstDomain == TySet)
    let context = scopedCoreContext firstDomain
        expectedDomainContexts =
            [ replicate index TySet <> context
            | index <- [0 .. length domainList - 1]
            ]
        valueContext = replicate (length domainList) TySet <> context
    guard
        (and
            (zipWith
                (\domain expected ->
                    scopedCoreType domain == TySet
                        && scopedCoreContext domain == expected)
                domainList
                expectedDomainContexts))
    guard
        (scopedCoreType value == TySet
            && scopedCoreContext value == valueContext)
    traverse_
        (\predicate ->
            guard
                (scopedCoreType predicate == TyProp
                    && scopedCoreContext predicate == valueContext))
        condition
    globals <-
        captureGlobalTypes globalType
            ( (scopedCoreTerm <$> domainList)
              <> [scopedCoreTerm value]
              <> maybeToList (scopedCoreTerm <$> condition)
            )
    finishConstruction
        context
        globals
        (FunctionalReplacementShape
            (scopedCoreTerm <$> domains)
            (scopedCoreTerm value)
            (scopedCoreTerm <$> condition))

namedSetConstructionTerm
    :: Ord global
    => NamedSetConstruction global
    -> ScopedCheckedCore global
namedSetConstructionTerm construction =
    fromMaybe
        (impossible "a checked construction lost its canonical term")
        (checkedDerived
            construction
            (constructionContext construction)
            TySet
            (constructionCanonicalTerm construction))

-- | Introduce a fresh named set and return adjacent FOF extensional and exact
-- equation locals.  Weakening is internal so construction-local binders and
-- source-domain order cannot drift at a caller.
namedSetConstructionLocalViews
    :: Ord global
    => SetConstructionFoundation
    -> NamedSetConstruction global
    -> Maybe
        ( ScopedCheckedCore global
        , ScopedCheckedCore global
        )
namedSetConstructionLocalViews foundation construction = do
    weakened <- weakenConstruction TySet construction
    let context = TySet : constructionContext construction
        target = CBound 0
    extensional <- extensionalView foundation target weakened
    equation <- checkedDerived weakened context TyProp
        (CEq TySet target (constructionCanonicalTerm weakened))
    pure (extensional, equation)

-- | Closed transparent content derived from the sole canonical construction
-- term.  This retains the pre-existing object-content identity exactly.
namedSetConstructionClosedBody
    :: Ord global
    => NamedSetConstruction global
    -> FrozenCheckedCore global
namedSetConstructionClosedBody construction =
    fromMaybe
        (impossible "a checked construction did not close")
        (freezeDerived construction closedType closedTerm)
  where
    context = constructionContext construction
    closedType = foldr TyArrow TySet (reverse context)
    closedTerm =
        foldl (flip CLam) (constructionCanonicalTerm construction) context

data NamedSetConstructionFact = NamedSetConstructionFact
    !(FrozenCheckedCore ObjectId)
    !CacheDigest

namedSetConstructionFactProposition
    :: NamedSetConstructionFact
    -> FrozenCheckedCore ObjectId
namedSetConstructionFactProposition
        (NamedSetConstructionFact proposition _descriptor) =
    proposition

namedSetConstructionFactDescriptor
    :: NamedSetConstructionFact
    -> CacheDigest
namedSetConstructionFactDescriptor
        (NamedSetConstructionFact _proposition descriptor) =
    descriptor

-- | Derive the only proposition authorized by
-- @CheckedSetConstructionExtensionality@.  This is a deliberately small
-- trusted theorem schema over the fixed foundation: every primitive
-- characteristic specialization is checked against its exact membership
-- formula before the source telescope is composed.  The caller cannot supply
-- either the resulting proposition or its cache descriptor.
namedSetConstructionObjectFact
    :: SetConstructionFoundation
    -> ObjectId
    -> NamedSetConstruction ObjectId
    -> Maybe NamedSetConstructionFact
namedSetConstructionObjectFact foundation object construction = do
    let context = constructionContext construction
        objectType = foldr TyArrow TySet (reverse context)
    globals <- insertGlobalType object objectType (constructionGlobals construction)
    let withObject = replaceConstructionGlobals globals construction
        target =
            foldl
                CApp
                (CGlobal object)
                [ CBound (fromIntegral index)
                | index <- reverse [0 .. length context - 1]
                ]
    view <- extensionalView foundation target withObject
    proposition <- freezeDerived withObject TyProp
        (foldl
            (flip CForall)
            (scopedCoreTerm view)
            context)
    selfView <- extensionalView
        foundation
        (constructionCanonicalTerm construction)
        construction
    closedSelf <- freezeDerived construction TyProp
        (foldl
            (flip CForall)
            (scopedCoreTerm selfView)
            context)
    let closedBody = namedSetConstructionClosedBody construction
        descriptor =
            hashCacheFields
                "felix-checked-named-set-construction-v1"
                [ encodeCache do
                    putCoreTypeCache (frozenCoreType closedBody)
                    putCanonicalTermCache putObjectIdCache
                        (frozenCoreTerm closedBody)
                , encodeCache do
                    putCanonicalTermCache putObjectIdCache
                        (frozenCoreTerm closedSelf)
                ]
    pure (NamedSetConstructionFact proposition descriptor)

relationalSetConstructionTerm
    :: Ord global
    => CheckedRelationalSetConstruction global
    -> ScopedCheckedCore global
relationalSetConstructionTerm construction =
    fromMaybe
        (impossible "a checked relational construction lost its canonical term")
        (checkedRelationalDerived
            construction
            (relationalConstructionContext construction)
            TySet
            (relationalConstructionCanonicalTerm construction))

-- | The exact source functionality obligation, still scoped by the outer
-- definition parameters.  It is discharged independently before the derived
-- extensional theorem can be authorized.
relationalSetConstructionFunctionality
    :: Ord global
    => CheckedRelationalSetConstruction global
    -> ScopedCheckedCore global
relationalSetConstructionFunctionality construction =
    fromMaybe
        (impossible "a checked relational construction lost functionality")
        (checkedRelationalDerived
            construction
            (relationalConstructionContext construction)
            TyProp
            (relationalConstructionFunctionalityTerm construction))

relationalSetConstructionClosedFunctionality
    :: Ord global
    => CheckedRelationalSetConstruction global
    -> FrozenCheckedCore global
relationalSetConstructionClosedFunctionality =
    closeRelationalFunctionality

-- | Introduce a fresh named set.  Assuming the exact checked functionality
-- proposition, derive its two local views; no arbitrary proposition can
-- unlock the extensional view.  The enclosing proof transaction owns the
-- corresponding authority.
relationalSetConstructionLocalViews
    :: Ord global
    => SetConstructionFoundation
    -> CheckedRelationalSetConstruction global
    -> ScopedCheckedCore global
    -> Maybe
        ( ScopedCheckedCore global
        , ScopedCheckedCore global
        )
relationalSetConstructionLocalViews foundation construction functionality = do
    guard
        (functionality
            == relationalSetConstructionFunctionality construction)
    validateRelationalSchema foundation construction
    let context = TySet : relationalConstructionContext construction
        target = CBound 0
    extensional <- checkedRelationalDerived construction context TyProp
        (CForall TySet
            (CEq TyProp
                (member (CBound 0) (CBound 1))
                (shiftCanonical 1 1
                    (relationalConstructionMembershipTerm construction))))
    equation <- checkedRelationalDerived construction context TyProp
        (CEq TySet
            target
            (shiftCanonical 1 0
                (relationalConstructionCanonicalTerm construction)))
    pure (extensional, equation)

relationalSetConstructionClosedBody
    :: Ord global
    => CheckedRelationalSetConstruction global
    -> FrozenCheckedCore global
relationalSetConstructionClosedBody construction =
    fromMaybe
        (impossible "a checked relational construction did not close")
        (freezeRelationalDerived construction closedType closedTerm)
  where
    context = relationalConstructionContext construction
    closedType = foldr TyArrow TySet (reverse context)
    closedTerm =
        foldl
            (flip CLam)
            (relationalConstructionCanonicalTerm construction)
            context

data RelationalSetConstructionFact = RelationalSetConstructionFact
    !(FrozenCheckedCore ObjectId)
    !CacheDigest

relationalSetConstructionFactProposition
    :: RelationalSetConstructionFact
    -> FrozenCheckedCore ObjectId
relationalSetConstructionFactProposition
        (RelationalSetConstructionFact proposition _descriptor) =
    proposition

relationalSetConstructionFactDescriptor
    :: RelationalSetConstructionFact
    -> CacheDigest
relationalSetConstructionFactDescriptor
        (RelationalSetConstructionFact _proposition descriptor) =
    descriptor

-- | The direct relational schema is a deterministic theorem over the fixed
-- separation, choice-witness, and replacement rows.  The functionality fact
-- is a real strictly-earlier candidate: its exact proposition is checked here
-- and its authority safety is consumed separately by declaration admission.
relationalSetConstructionObjectFact
    :: SetConstructionFoundation
    -> ObjectId
    -> CheckedRelationalSetConstruction ObjectId
    -> FrozenCheckedCore ObjectId
    -> Maybe RelationalSetConstructionFact
relationalSetConstructionObjectFact
        foundation object construction functionality = do
    let expectedFunctionality =
            closeRelationalFunctionality construction
    guard (functionality == expectedFunctionality)
    validateRelationalSchema foundation construction
    let context = relationalConstructionContext construction
        objectType = foldr TyArrow TySet (reverse context)
    globals <- insertGlobalType
        object objectType (relationalConstructionGlobals construction)
    let withObject = replaceRelationalGlobals globals construction
        target =
            foldl
                CApp
                (CGlobal object)
                [ CBound (fromIntegral index)
                | index <- reverse [0 .. length context - 1]
                ]
        membership = relationalConstructionMembershipTerm withObject
    proposition <- freezeRelationalDerived withObject TyProp
        (foldl
            (flip CForall)
            (CForall TySet
                (CEq TyProp
                    (member (CBound 0) (shiftCanonical 1 0 target))
                    membership))
            context)
    closedSelf <- freezeRelationalDerived construction TyProp
        (foldl
            (flip CForall)
            (CForall TySet
                (CEq TyProp
                    (member
                        (CBound 0)
                        (shiftCanonical 1 0
                            (relationalConstructionCanonicalTerm construction)))
                    (relationalConstructionMembershipTerm construction)))
            context)
    let closedBody = relationalSetConstructionClosedBody construction
        descriptor =
            hashCacheFields
                "felix-checked-named-relational-set-construction-v1"
                [ encodeCache do
                    putCoreTypeCache (frozenCoreType closedBody)
                    putCanonicalTermCache putObjectIdCache
                        (frozenCoreTerm closedBody)
                , encodeCache do
                    putCanonicalTermCache putObjectIdCache
                        (frozenCoreTerm expectedFunctionality)
                , encodeCache do
                    putCanonicalTermCache putObjectIdCache
                        (frozenCoreTerm closedSelf)
                ]
    pure (RelationalSetConstructionFact proposition descriptor)

finishConstruction
    :: Ord global
    => [CoreType]
    -> Map.Map global CoreType
    -> NamedSetConstructionShape global
    -> Maybe (NamedSetConstruction global)
finishConstruction context globals shape = do
    let built = buildConstruction context shape
        construction = NamedSetConstruction context globals shape built
    _ <- checkedDerived construction context TySet
        (builtConstructionTerm built)
    _ <- checkedDerived construction (TySet : context) TyProp
        (builtConstructionMembership built)
    pure construction

buildConstruction
    :: Eq global
    => [CoreType]
    -> NamedSetConstructionShape global
    -> BuiltSetConstruction global
buildConstruction context = \case
    SeparationShape bound predicate ->
        let function = CLam TySet predicate
            term = applyIntrinsic2 Sep bound function
            membership =
                logicalAnd
                    (member (CBound 0) (shiftCanonical 1 0 bound))
                    predicate
            application =
                characteristicApplication
                    Sep context term
                    [ (TySet, bound)
                    , (TyArrow TySet TyProp, function)
                    ]
        in BuiltSetConstruction term membership [application]
    FunctionalReplacementShape domains value condition ->
        let (term, applications) =
                buildFunctionalReplacement
                    context
                    domains
                    value
                    condition
            domainList = NonEmpty.toList domains
            binderCount = length domainList
            terminal =
                logicalConjunction
                    ( maybeToList
                        (shiftCanonical 1 (fromIntegral binderCount)
                            <$> condition)
                      <> [ CEq TySet
                            (CBound (fromIntegral binderCount))
                            (shiftCanonical 1
                                (fromIntegral binderCount)
                                value)
                         ]
                    )
            membership =
                foldr
                    (\(depth, domain) rest ->
                        logicalExists
                            (logicalAnd
                                (member
                                    (CBound 0)
                                    (shiftCanonical 1 0
                                        (shiftCanonical 1 depth domain)))
                                rest))
                    terminal
                    (zip [0 :: Natural ..] domainList)
        in BuiltSetConstruction term membership applications

-- The only functional-replacement term builder.  Its result is reused by the
-- transparent body, exact-content matching, characteristic validation, local
-- views, and descriptor derivation.
buildFunctionalReplacement
    :: [CoreType]
    -> NonEmpty (CanonicalTerm global)
    -> CanonicalTerm global
    -> Maybe (CanonicalTerm global)
    -> (CanonicalTerm global, [CheckedCharacteristicApplication global])
buildFunctionalReplacement context (domain :| remaining) value condition =
    case remaining of
        [] ->
            let predicate = CLam TySet <$> condition
                filtered = maybe domain
                    (applyIntrinsic2 Sep domain)
                    predicate
                function = CLam TySet value
                replacement = applyIntrinsic2 Repl filtered function
                separationApplications = case predicate of
                    Nothing -> []
                    Just checkedPredicate ->
                        [ characteristicApplication
                            Sep context filtered
                            [ (TySet, domain)
                            , (TyArrow TySet TyProp, checkedPredicate)
                            ]
                        ]
                replacementApplication =
                    characteristicApplication
                        Repl context replacement
                        [ (TySet, filtered)
                        , (TyArrow TySet TySet, function)
                        ]
            in
                ( replacement
                , separationApplications <> [replacementApplication]
                )
        next : rest ->
            let (nested, nestedApplications) =
                    buildFunctionalReplacement
                        (TySet : context)
                        (next :| rest)
                        value
                        condition
                function = CLam TySet nested
                replacement = applyIntrinsic2 Repl domain function
                union = applyIntrinsic FamilyUnion replacement
            in
                ( union
                , characteristicApplication
                    Repl context replacement
                    [ (TySet, domain)
                    , (TyArrow TySet TySet, function)
                    ]
                  : characteristicApplication
                        FamilyUnion context union
                        [(TySet, replacement)]
                  : nestedApplications
                )

characteristicApplication
    :: CoreIntrinsicTag
    -> [CoreType]
    -> CanonicalTerm global
    -> [(CoreType, CanonicalTerm global)]
    -> CheckedCharacteristicApplication global
characteristicApplication intrinsic context target arguments =
    CheckedCharacteristicApplication
        intrinsic
        context
        target
        (NonEmpty.fromList arguments)
        (expectedCharacteristicBody intrinsic arguments)

expectedCharacteristicBody
    :: CoreIntrinsicTag
    -> [(CoreType, CanonicalTerm global)]
    -> CanonicalTerm global
expectedCharacteristicBody intrinsic arguments =
    case (intrinsic, arguments) of
        (Sep, [(_boundType, bound), (_predicateType, CLam TySet predicate)]) ->
            logicalAnd
                (member (CBound 0) (shiftCanonical 2 0 bound))
                (shiftCanonical 1 1 predicate)
        (Repl, [(_domainType, domain), (_functionType, CLam TySet value)]) ->
            logicalExists
                (logicalAnd
                    (member (CBound 0) (shiftCanonical 3 0 domain))
                    (CEq TySet
                        (CBound 1)
                        (shiftCanonical 2 1 value)))
        (FamilyUnion, [(_familyType, family)]) ->
            logicalExists
                (logicalAnd
                    (member (CBound 0) (shiftCanonical 3 0 family))
                    (member (CBound 1) (CBound 0)))
        _ ->
            impossible "invalid checked set-construction characteristic"

extensionalView
    :: Ord global
    => SetConstructionFoundation
    -> CanonicalTerm global
    -> NamedSetConstruction global
    -> Maybe (ScopedCheckedCore global)
extensionalView foundation target construction = do
    traverse_
        (validateCharacteristic foundation construction)
        (constructionApplications construction)
    checkedDerived construction (constructionContext construction) TyProp
        (CForall TySet
            (CEq TyProp
                (member (CBound 0) (shiftCanonical 1 0 target))
                (constructionMembership construction)))

-- Each primitive step is specialized from the actual fixed row, and the
-- complete normalized membership body is checked.  The final flattened view
-- is then the deterministic composition of these exact primitive schemas.
validateCharacteristic
    :: Ord global
    => SetConstructionFoundation
    -> NamedSetConstruction global
    -> CheckedCharacteristicApplication global
    -> Maybe ()
validateCharacteristic foundation construction
        (CheckedCharacteristicApplication
            intrinsic context targetTerm argumentTerms expectedBody) = do
    row <- characteristicRow foundation intrinsic
    target <- checkedDerived construction context TySet targetTerm
    arguments <- traverse
        (\(coreType, term) ->
            checkedDerived construction context coreType term)
        argumentTerms
    specialized <- scopedCharacteristicDefinition row target arguments
    case scopedCoreTerm specialized of
        CForall TySet
                (CEq TyProp actualMembership actualBody)
            | actualMembership
                == member (CBound 0) (CBound 1)
            , scopedCoreContext specialized
                == TySet : scopedCoreContext target
            , actualBody == expectedBody ->
                pure ()
        _ -> Nothing

characteristicRow
    :: SetConstructionFoundation
    -> CoreIntrinsicTag
    -> Maybe (FrozenCheckedCore Void)
characteristicRow
        (SetConstructionFoundation
            familyUnion separation replacement _setChoose) =
    \case
        FamilyUnion -> Just familyUnion
        Sep -> Just separation
        Repl -> Just replacement
        _ -> Nothing

validateRelationalSchema
    :: Ord global
    => SetConstructionFoundation
    -> CheckedRelationalSetConstruction global
    -> Maybe ()
validateRelationalSchema foundation construction = do
    traverse_
        (validateRelationalCharacteristic foundation construction)
        (relationalConstructionApplications construction)
    validateChoiceWitness foundation construction

validateRelationalCharacteristic
    :: Ord global
    => SetConstructionFoundation
    -> CheckedRelationalSetConstruction global
    -> CheckedCharacteristicApplication global
    -> Maybe ()
validateRelationalCharacteristic foundation construction
        (CheckedCharacteristicApplication
            intrinsic context targetTerm argumentTerms expectedBody) = do
    row <- characteristicRow foundation intrinsic
    target <- checkedRelationalDerived construction context TySet targetTerm
    arguments <- traverse
        (\(coreType, term) ->
            checkedRelationalDerived construction context coreType term)
        argumentTerms
    specialized <- scopedCharacteristicDefinition row target arguments
    case scopedCoreTerm specialized of
        CForall TySet (CEq TyProp actualMembership actualBody)
            | actualMembership == member (CBound 0) (CBound 1)
            , scopedCoreContext specialized
                == TySet : scopedCoreContext target
            , actualBody == expectedBody ->
                pure ()
        _ -> Nothing

validateChoiceWitness
    :: Ord global
    => SetConstructionFoundation
    -> CheckedRelationalSetConstruction global
    -> Maybe ()
validateChoiceWitness
        (SetConstructionFoundation
            _familyUnion _separation _replacement setChoose)
        construction = do
    let context = relationalConstructionContext construction
        relation = relationalConstructionRelation construction
        predicate = CLam TySet relation
        choice = applyIntrinsic SetChoose predicate
        witnessContext = TySet : TySet : context
    target <- checkedRelationalDerived construction witnessContext TySet
        (shiftCanonical 1 0 choice)
    checkedPredicate <-
        checkedRelationalDerived construction witnessContext
            (TyArrow TySet TyProp)
            (shiftCanonical 1 0 predicate)
    witness <- checkedRelationalDerived construction witnessContext TySet
        (CBound 0)
    specialized <-
        scopedCharacteristicDefinition
            setChoose target (checkedPredicate :| [witness])
    guard
        (scopedCoreContext specialized
            == TySet : TySet : TySet : context)
    guard
        (scopedCoreTerm specialized
            == CImp
                (shiftCanonical 1 0 relation)
                (shiftCanonical 1 1 relation))

relationalFunctionality
    :: CanonicalTerm global
    -> CanonicalTerm global
    -> CanonicalTerm global
relationalFunctionality domain relation =
    CForall TySet
        (CImp
            (member (CBound 0) (shiftCanonical 1 0 domain))
            (CForall TySet
                (CForall TySet
                    (CImp
                        (logicalAnd
                            (shiftCanonical 1 0 relation)
                            (shiftCanonical 1 1 relation))
                        (CEq TySet (CBound 1) (CBound 0))))))

relationalMembership
    :: CanonicalTerm global
    -> CanonicalTerm global
    -> CanonicalTerm global
relationalMembership domain relation =
    logicalExists
        (logicalAnd
            (member (CBound 0) (shiftCanonical 2 0 domain))
            (applyRelation
                (shiftCanonical 2 0
                    (CLam TySet (CLam TySet relation)))
                (CBound 0)
                (CBound 1)))
  where
    applyRelation function domainValue rangeValue =
        case function of
            CLam TySet domainBody ->
                case instantiateCanonical domainValue domainBody of
                    CLam TySet rangeBody ->
                        instantiateCanonical rangeValue rangeBody
                    _ -> impossible "a checked relation lost its range binder"
            _ -> impossible "a checked relation lost its domain binder"

weakenConstruction
    :: Ord global
    => CoreType
    -> NamedSetConstruction global
    -> Maybe (NamedSetConstruction global)
weakenConstruction binderType construction =
    finishConstruction
        (binderType : constructionContext construction)
        (constructionGlobals construction)
        (case constructionShape construction of
            SeparationShape bound predicate ->
                SeparationShape
                    (shiftCanonical 1 0 bound)
                    (shiftCanonical 1 1 predicate)
            FunctionalReplacementShape domains value condition ->
                let domainList = NonEmpty.toList domains
                    weakenedDomains =
                        zipWith
                            (\depth domain -> shiftCanonical 1 depth domain)
                            [0..]
                            domainList
                    binderDepth = fromIntegral (length domainList)
                in FunctionalReplacementShape
                    (NonEmpty.fromList weakenedDomains)
                    (shiftCanonical 1 binderDepth value)
                    (shiftCanonical 1 binderDepth <$> condition))

captureGlobalTypes
    :: Ord global
    => (global -> Maybe CoreType)
    -> [CanonicalTerm global]
    -> Maybe (Map.Map global CoreType)
captureGlobalTypes globalType terms =
    Map.fromList <$> traverse capture
        (Set.toAscList (foldMap canonicalTermGlobals terms))
  where
    capture global = do
        coreType <- globalType global
        pure (global, coreType)

insertGlobalType
    :: Ord global
    => global
    -> CoreType
    -> Map.Map global CoreType
    -> Maybe (Map.Map global CoreType)
insertGlobalType global coreType globals =
    case Map.lookup global globals of
        Nothing -> Just (Map.insert global coreType globals)
        Just existing
            | existing == coreType -> Just globals
            | otherwise -> Nothing

checkedDerived
    :: Ord global
    => NamedSetConstruction global
    -> [CoreType]
    -> CoreType
    -> CanonicalTerm global
    -> Maybe (ScopedCheckedCore global)
checkedDerived construction context expected term = do
    checked <- either (const Nothing) Just
        (checkScopedCanonicalCore
            (`Map.lookup` constructionGlobals construction)
            context
            term)
    guard (scopedCoreType checked == expected)
    pure checked

freezeDerived
    :: Ord global
    => NamedSetConstruction global
    -> CoreType
    -> CanonicalTerm global
    -> Maybe (FrozenCheckedCore global)
freezeDerived construction expected term = do
    checked <- checkedDerived construction [] expected term
    closeScopedCore checked

checkedRelationalDerived
    :: Ord global
    => CheckedRelationalSetConstruction global
    -> [CoreType]
    -> CoreType
    -> CanonicalTerm global
    -> Maybe (ScopedCheckedCore global)
checkedRelationalDerived construction context expected term = do
    checked <- either (const Nothing) Just
        (checkScopedCanonicalCore
            (`Map.lookup` relationalConstructionGlobals construction)
            context
            term)
    guard (scopedCoreType checked == expected)
    pure checked

freezeRelationalDerived
    :: Ord global
    => CheckedRelationalSetConstruction global
    -> CoreType
    -> CanonicalTerm global
    -> Maybe (FrozenCheckedCore global)
freezeRelationalDerived construction expected term = do
    checked <- checkedRelationalDerived construction [] expected term
    closeScopedCore checked

closeRelationalFunctionality
    :: Ord global
    => CheckedRelationalSetConstruction global
    -> FrozenCheckedCore global
closeRelationalFunctionality construction =
    fromMaybe
        (impossible "a relational functionality proposition did not close")
        (freezeRelationalDerived construction TyProp
            (foldl
                (flip CForall)
                (relationalConstructionFunctionalityTerm construction)
                (relationalConstructionContext construction)))

replaceRelationalGlobals
    :: Map.Map global CoreType
    -> CheckedRelationalSetConstruction global
    -> CheckedRelationalSetConstruction global
replaceRelationalGlobals globals
        (CheckedRelationalSetConstruction
            context _oldGlobals domain relation term functionality
            membership applications) =
    CheckedRelationalSetConstruction
        context globals domain relation term functionality membership applications

relationalConstructionContext
    :: CheckedRelationalSetConstruction global
    -> [CoreType]
relationalConstructionContext
        (CheckedRelationalSetConstruction
            context _globals _domain _relation _term _functionality
            _membership _applications) =
    context

relationalConstructionGlobals
    :: CheckedRelationalSetConstruction global
    -> Map.Map global CoreType
relationalConstructionGlobals
        (CheckedRelationalSetConstruction
            _context globals _domain _relation _term _functionality
            _membership _applications) =
    globals

relationalConstructionRelation
    :: CheckedRelationalSetConstruction global
    -> CanonicalTerm global
relationalConstructionRelation
        (CheckedRelationalSetConstruction
            _context _globals _domain relation _term _functionality
            _membership _applications) =
    relation

relationalConstructionCanonicalTerm
    :: CheckedRelationalSetConstruction global
    -> CanonicalTerm global
relationalConstructionCanonicalTerm
        (CheckedRelationalSetConstruction
            _context _globals _domain _relation term _functionality
            _membership _applications) =
    term

relationalConstructionFunctionalityTerm
    :: CheckedRelationalSetConstruction global
    -> CanonicalTerm global
relationalConstructionFunctionalityTerm
        (CheckedRelationalSetConstruction
            _context _globals _domain _relation _term functionality
            _membership _applications) =
    functionality

relationalConstructionMembershipTerm
    :: CheckedRelationalSetConstruction global
    -> CanonicalTerm global
relationalConstructionMembershipTerm
        (CheckedRelationalSetConstruction
            _context _globals _domain _relation _term _functionality
            membership _applications) =
    membership

relationalConstructionApplications
    :: CheckedRelationalSetConstruction global
    -> [CheckedCharacteristicApplication global]
relationalConstructionApplications
        (CheckedRelationalSetConstruction
            _context _globals _domain _relation _term _functionality
            _membership applications) =
    applications

replaceConstructionGlobals
    :: Map.Map global CoreType
    -> NamedSetConstruction global
    -> NamedSetConstruction global
replaceConstructionGlobals globals
        (NamedSetConstruction context _oldGlobals shape built) =
    NamedSetConstruction context globals shape built

constructionContext :: NamedSetConstruction global -> [CoreType]
constructionContext (NamedSetConstruction context _globals _shape _built) =
    context

constructionGlobals
    :: NamedSetConstruction global
    -> Map.Map global CoreType
constructionGlobals (NamedSetConstruction _context globals _shape _built) =
    globals

constructionShape
    :: NamedSetConstruction global
    -> NamedSetConstructionShape global
constructionShape (NamedSetConstruction _context _globals shape _built) =
    shape

constructionCanonicalTerm
    :: NamedSetConstruction global
    -> CanonicalTerm global
constructionCanonicalTerm
        (NamedSetConstruction _context _globals _shape built) =
    builtConstructionTerm built

constructionMembership
    :: NamedSetConstruction global
    -> CanonicalTerm global
constructionMembership
        (NamedSetConstruction _context _globals _shape built) =
    builtConstructionMembership built

constructionApplications
    :: NamedSetConstruction global
    -> [CheckedCharacteristicApplication global]
constructionApplications
        (NamedSetConstruction _context _globals _shape built) =
    builtConstructionApplications built

builtConstructionTerm
    :: BuiltSetConstruction global
    -> CanonicalTerm global
builtConstructionTerm (BuiltSetConstruction term _membership _applications) =
    term

builtConstructionMembership
    :: BuiltSetConstruction global
    -> CanonicalTerm global
builtConstructionMembership
        (BuiltSetConstruction _term membership _applications) =
    membership

builtConstructionApplications
    :: BuiltSetConstruction global
    -> [CheckedCharacteristicApplication global]
builtConstructionApplications
        (BuiltSetConstruction _term _membership applications) =
    applications

applyIntrinsic
    :: CoreIntrinsicTag
    -> CanonicalTerm global
    -> CanonicalTerm global
applyIntrinsic intrinsic argument =
    CApp (CIntrinsic intrinsic) argument

applyIntrinsic2
    :: CoreIntrinsicTag
    -> CanonicalTerm global
    -> CanonicalTerm global
    -> CanonicalTerm global
applyIntrinsic2 intrinsic first second =
    CApp (CApp (CIntrinsic intrinsic) first) second

member
    :: CanonicalTerm global
    -> CanonicalTerm global
    -> CanonicalTerm global
member = applyIntrinsic2 Member

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

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

logicalTruth :: CanonicalTerm global
logicalTruth = CImp CFalsum CFalsum

logicalConjunction
    :: Eq global
    => [CanonicalTerm global]
    -> CanonicalTerm global
logicalConjunction =
    foldr combine logicalTruth
  where
    combine proposition remaining
        | proposition == logicalTruth = remaining
        | remaining == logicalTruth = proposition
        | otherwise = logicalAnd proposition remaining

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