diff options
Diffstat (limited to 'source/Checking/SetConstruction.hs')
| -rw-r--r-- | source/Checking/SetConstruction.hs | 1191 |
1 files changed, 1191 insertions, 0 deletions
diff --git a/source/Checking/SetConstruction.hs b/source/Checking/SetConstruction.hs new file mode 100644 index 0000000..4c4b4bc --- /dev/null +++ b/source/Checking/SetConstruction.hs @@ -0,0 +1,1191 @@ +{-# 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 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 Checking.Core +import Checking.Foundation +import 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)) |