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