diff options
Diffstat (limited to 'source/Checking')
| -rw-r--r-- | source/Checking/Authority.hs | 9 | ||||
| -rw-r--r-- | source/Checking/Backend/Problem.hs | 211 | ||||
| -rw-r--r-- | source/Checking/Core.hs | 230 | ||||
| -rw-r--r-- | source/Checking/Declaration.hs | 299 | ||||
| -rw-r--r-- | source/Checking/Exact.hs | 1256 | ||||
| -rw-r--r-- | source/Checking/Exact/Inductive.hs | 214 | ||||
| -rw-r--r-- | source/Checking/Exact/Proof.hs | 1652 | ||||
| -rw-r--r-- | source/Checking/Exact/Vocabulary.hs | 30 | ||||
| -rw-r--r-- | source/Checking/FinalPrelude.hs | 237 | ||||
| -rw-r--r-- | source/Checking/Kernel/Proof.hs | 277 | ||||
| -rw-r--r-- | source/Checking/Module.hs | 3 | ||||
| -rw-r--r-- | source/Checking/SetConstruction.hs | 1191 | ||||
| -rw-r--r-- | source/Checking/Typed/Inductive.hs | 944 |
13 files changed, 5809 insertions, 744 deletions
diff --git a/source/Checking/Authority.hs b/source/Checking/Authority.hs index 2fa21f2..fb6cea0 100644 --- a/source/Checking/Authority.hs +++ b/source/Checking/Authority.hs @@ -230,6 +230,7 @@ data KernelConstructionDescriptor = FoundationLeaf !FoundationAxiomTag | GuardedFoundationRules !GuardedRuleSet | CheckedDefinitionEquation !ObjectId + | CheckedSetConstructionExtensionality !ObjectId !CacheDigest deriving stock (Show, Eq, Ord, Generic) -- | Exact semantic members of one trusted datatype compilation. @@ -487,6 +488,10 @@ putKernelDescriptor = \case CheckedDefinitionEquation identity -> do putCacheTag 0x02 putObjectIdCache identity + CheckedSetConstructionExtensionality identity construction -> do + putCacheTag 0x03 + putObjectIdCache identity + putCacheDigest construction getKernelDescriptor :: CacheGet KernelConstructionDescriptor getKernelDescriptor = @@ -503,6 +508,10 @@ getKernelDescriptor = (fail "cache guarded-rule tags are not in canonical order") pure (GuardedFoundationRules (guardedRuleSet rules)) 0x02 -> CheckedDefinitionEquation <$> getObjectIdCache + 0x03 -> + CheckedSetConstructionExtensionality + <$> getObjectIdCache + <*> getCacheDigest tag -> fail ("unknown cache kernel-construction tag " <> show tag) diff --git a/source/Checking/Backend/Problem.hs b/source/Checking/Backend/Problem.hs index 61a31d2..8d3a071 100644 --- a/source/Checking/Backend/Problem.hs +++ b/source/Checking/Backend/Problem.hs @@ -38,8 +38,8 @@ module Checking.Backend.Problem , typedProblemAuxiliaryTag , typedProblemAuxiliaryProposition , typedProblemAuxiliaryCapability - , GlobalPremiseMode(..) , LocalPremisePolicy(..) + , HigherOrderJustificationPolicy(..) , selectTypedLocalPremises , TypedProblemRoute(..) , TypedProblem @@ -806,34 +806,43 @@ typedProblemAuxiliaryCapability capability -data GlobalPremiseMode - = ImplicitFofPremises - | ExplicitGlobalPremises - | NoGlobalPremises - deriving stock (Show, Eq) - +-- | Source justification policy for premise selection. Higher-order routing +-- is validated separately after the complete selected problem is known. data LocalPremisePolicy = FirstOrderLocals - | AllLocals + | CompleteLocals + deriving stock (Show, Eq) + +-- | Whether selected higher-order components must be justified by one of the +-- two approved inline construction forms. Premise selection has already +-- happened when this policy is applied. +data HigherOrderJustificationPolicy + = ImplicitConstructionJustification + | ExplicitHigherOrderJustification deriving stock (Show, Eq) selectTypedLocalPremises :: LocalPremisePolicy -> [TypedLocalPremise local origin global] -> Vector (TypedLocalPremise local origin global) -selectTypedLocalPremises localPolicy availableLocals = +selectTypedLocalPremises selection availableLocals = Vector.fromList (List.sortOn typedLocalPremiseOrdinal - (case localPolicy of + (case selection of FirstOrderLocals -> List.filter (isFofCapability . typedLocalPremiseCapability) availableLocals - AllLocals -> + CompleteLocals -> availableLocals)) +data ImplicitHigherOrderConstruction + = ImplicitSeparation + | ImplicitFunctionalReplacement + deriving stock (Show, Eq, Ord) + data TypedProblemRoute = RouteFof | RouteTh0 @@ -855,9 +864,6 @@ data TypedProblemError local global !(BackendClassificationError global) | TypedProblemExplicitHigherOrderJustificationRequired !(NonEmpty BackendFofExclusion) - | TypedProblemInvalidPolicyCombination - !GlobalPremiseMode - !LocalPremisePolicy | TypedProblemDuplicateLocalPremiseOrdinal !LocalPremiseOrdinal | TypedProblemLocalTypeMismatch @@ -873,8 +879,8 @@ planTypedProblem -> SupportedProposition local global -> [TypedLocalPremise local origin global] -> [TypedFoundationAuxiliaryInput global] - -> GlobalPremiseMode -> LocalPremisePolicy + -> HigherOrderJustificationPolicy -> Either (TypedProblemError local global) (TypedProblem ref local origin global) @@ -884,11 +890,8 @@ planTypedProblem claim availableLocals auxiliaries - globalPolicy - localPolicy = do - validatePolicyCombination - globalPolicy localPolicy + higherOrderPolicy = do validateLocalPremiseOrdinals availableLocals claimCapability <- @@ -906,19 +909,15 @@ planTypedProblem prepareAuxiliary [0..] auxiliaries - case globalPolicy of - ImplicitFofPremises -> - case implicitTh0Requirement - claimCapability - (typedProblemAuxiliaryCapability - <$> preparedAuxiliaries) of - Nothing -> - pure () - Just exclusions -> - Left - (TypedProblemExplicitHigherOrderJustificationRequired - exclusions) - _ -> + case higherOrderPolicy of + ImplicitConstructionJustification -> + validateImplicitHigherOrderAdmission + claim + claimCapability + selectedFacts + selectedLocals + preparedAuxiliaries + ExplicitHigherOrderJustification -> pure () let selectedFofCapabilities = isFofCapability claimCapability @@ -956,23 +955,6 @@ planTypedProblem globalTypes localTypes) where - implicitTh0Requirement claimCapability - auxiliaryCapabilities = - case claimCapability of - RequiresTh0 exclusions -> - Just exclusions - FofProjectable{} -> - firstAuxiliaryRequirement - auxiliaryCapabilities - - firstAuxiliaryRequirement = \case - [] -> - Nothing - FofProjectable{} : remaining -> - firstAuxiliaryRequirement remaining - RequiresTh0 exclusions : _remaining -> - Just exclusions - prepareAuxiliary ordinal (TypedFoundationAuxiliaryInput @@ -985,25 +967,120 @@ planTypedProblem proposition capability -validatePolicyCombination - :: GlobalPremiseMode - -> LocalPremisePolicy - -> Either - (TypedProblemError local global) - () -validatePolicyCombination globalPolicy localPolicy = - case (globalPolicy, localPolicy) of - (ImplicitFofPremises, FirstOrderLocals) -> - Right () - (ExplicitGlobalPremises, FirstOrderLocals) -> - Right () - (NoGlobalPremises, AllLocals) -> - Right () +-- | Implicit automation admits higher-order routing only for a checked +-- proposition that itself contains one of the two approved set constructions. +-- This classification selects no premise and grants no authority. +implicitConstructionAdmission + :: SupportedProposition local global + -> FofCapability projection + -> Maybe (Set ImplicitHigherOrderConstruction) +implicitConstructionAdmission proposition capability = + case capability of + FofProjectable{} -> + Nothing + RequiresTh0 exclusions + | Set.null constructions -> + Nothing + | all (admittedExclusion constructions) exclusions -> + Just constructions + | otherwise -> + Nothing + where + dependencies = + foundationAxiomDependencies + (supportedPropositionTerm proposition) + constructions = + Set.fromList + ( [ ImplicitSeparation + | SeparationCharacteristic `Set.member` dependencies + ] + <> [ ImplicitFunctionalReplacement + | ReplacementCharacteristic `Set.member` dependencies + ] + ) + + admittedExclusion allowed = \case + StructuralFofExclusion HigherOrderLambda -> + True + StructuralFofExclusion (HigherOrderIntrinsic Sep) -> + ImplicitSeparation `Set.member` allowed + StructuralFofExclusion (HigherOrderIntrinsic Repl) -> + ImplicitFunctionalReplacement `Set.member` allowed + -- The checked proposition is the deliberate granularity: its typed + -- global occurrences neither select another fact nor grant authority. + HigherOrderGlobalType{} -> + True + StructuralFofExclusion{} -> + False + HigherOrderAmbientLocal{} -> + False + +validateImplicitHigherOrderAdmission + :: SupportedProposition local global + -> FofCapability claimProjection + -> Vector (TypedBackendFact ref global) + -> Vector (TypedLocalPremise local origin global) + -> [TypedProblemAuxiliary global] + -> Either (TypedProblemError local global) () +validateImplicitHigherOrderAdmission + claim claimCapability selectedFacts selectedLocals auxiliaries = do + claimConstructions <- + admittedPropositionConstructions claim claimCapability + traverse_ requireFirstOrderGlobal selectedFacts + localConstructions <- + foldM + (\admitted premise -> + (admitted <>) + <$> admittedPropositionConstructions + (typedLocalPremiseProposition premise) + (typedLocalPremiseCapability premise)) + Set.empty + (Vector.toList selectedLocals) + let admitted = claimConstructions <> localConstructions + traverse_ (requireAdmittedAuxiliary admitted) auxiliaries + where + admittedPropositionConstructions proposition = \case + FofProjectable{} -> + Right Set.empty + RequiresTh0 exclusions -> + maybe + (Left + (TypedProblemExplicitHigherOrderJustificationRequired + exclusions)) + Right + (implicitConstructionAdmission + proposition + (RequiresTh0 exclusions)) + + requireFirstOrderGlobal fact = + case typedBackendFactCapability fact of + FofProjectable{} -> + Right () + RequiresTh0 exclusions -> + Left + (TypedProblemExplicitHigherOrderJustificationRequired + exclusions) + + requireAdmittedAuxiliary admitted auxiliary = + case typedProblemAuxiliaryCapability auxiliary of + FofProjectable{} -> + Right () + RequiresTh0 exclusions + | auxiliaryAdmitted admitted + (typedProblemAuxiliaryTag auxiliary) -> + Right () + | otherwise -> + Left + (TypedProblemExplicitHigherOrderJustificationRequired + exclusions) + + auxiliaryAdmitted admitted = \case + SeparationCharacteristic -> + ImplicitSeparation `Set.member` admitted + ReplacementCharacteristic -> + ImplicitFunctionalReplacement `Set.member` admitted _ -> - Left - (TypedProblemInvalidPolicyCombination - globalPolicy - localPolicy) + False validateLocalPremiseOrdinals :: [TypedLocalPremise local origin global] diff --git a/source/Checking/Core.hs b/source/Checking/Core.hs index 4b7478f..bf5bf3b 100644 --- a/source/Checking/Core.hs +++ b/source/Checking/Core.hs @@ -52,14 +52,22 @@ module Checking.Core , scopedCharacteristicDefinition , scopedReplacementGraph , implyScopedCore + , equalScopedCore + , conjoinScopedCore + , disjoinScopedCore + , negateScopedCore + , falsumScopedCore , splitScopedSetEquality - , scopedSetInductionHypothesis + , scopedSetInductionInstance , closeScopedForall , closeScopedExists , openScopedForall , openScopedImplication + , openScopedAssumption , closeScopedCore + , betaNormalizeCanonical , instantiateCanonical + , shiftCanonical , mapCanonicalGlobals , canonicalTermGlobals , checkCanonicalCore @@ -463,7 +471,8 @@ data CanonicalTerm global -- | The fixed checked-core interpretation of set insertion. -- --- Finite-set notation and typed 'ConsSymbol' lowering share this form. +-- Finite-set notation uses this intrinsic HOTG adjunction directly. The +-- ordinary source-owned @cons@ function is not consulted during lowering. canonicalSetInsert :: CanonicalTerm global -> CanonicalTerm global @@ -904,6 +913,90 @@ implyScopedCore implyScopedCore _premise _conclusion = Nothing +-- | Form an equality between checked operands under the same lexical +-- context. This preserves the checked-core invariant without requiring a +-- caller to recover global types merely to combine already checked terms. +equalScopedCore + :: ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe (ScopedCheckedCore global) +equalScopedCore + (ScopedCheckedCore leftContext leftType left) + (ScopedCheckedCore rightContext rightType right) + | leftContext == rightContext + , leftType == rightType = + Just + (ScopedCheckedCore + leftContext + TyProp + (CEq leftType left right)) +equalScopedCore _left _right = + Nothing + +-- | Conjoin two checked propositions under the same lexical context. Truth +-- is normalized away so callers can build an optional source guard without +-- retaining an inert conjunct. +conjoinScopedCore + :: Eq global + => ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe (ScopedCheckedCore global) +conjoinScopedCore + left@(ScopedCheckedCore leftContext TyProp leftTerm) + right@(ScopedCheckedCore rightContext TyProp rightTerm) + | leftContext == rightContext + , leftTerm == truth = Just right + | leftContext == rightContext + , rightTerm == truth = Just left + | leftContext == rightContext = + Just + (ScopedCheckedCore + leftContext + TyProp + (CImp + (CImp leftTerm (CImp rightTerm CFalsum)) + CFalsum)) + where + truth = CImp CFalsum CFalsum +conjoinScopedCore _left _right = + Nothing + +-- | Disjoin two checked propositions under the same lexical context using +-- the fixed classical encoding owned by the checked core. +disjoinScopedCore + :: ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe (ScopedCheckedCore global) +disjoinScopedCore + (ScopedCheckedCore leftContext TyProp left) + (ScopedCheckedCore rightContext TyProp right) + | leftContext == rightContext = + Just + (ScopedCheckedCore + leftContext + TyProp + (CImp (CImp left CFalsum) right)) +disjoinScopedCore _left _right = + Nothing + +-- | Negate a checked proposition without changing its lexical context. +negateScopedCore + :: ScopedCheckedCore global + -> Maybe (ScopedCheckedCore global) +negateScopedCore (ScopedCheckedCore context TyProp proposition) = + Just + (ScopedCheckedCore + context + TyProp + (CImp proposition CFalsum)) +negateScopedCore _proposition = + Nothing + +-- | Checked falsum at an already established lexical context. +falsumScopedCore :: [CoreType] -> ScopedCheckedCore global +falsumScopedCore context = + ScopedCheckedCore context TyProp CFalsum + -- | Split a checked set equality into its two extensionality directions. splitScopedSetEquality :: ScopedCheckedCore global @@ -934,30 +1027,61 @@ splitScopedSetEquality splitScopedSetEquality _proposition = Nothing --- | Form the set-induction hypothesis for one set-valued ambient binder. -scopedSetInductionHypothesis +-- | Derive the exact predicate, member-wise hypothesis, induction step, and +-- binder-level result for one set-valued ambient binder. The selected binder +-- is replaced by the newly introduced set variable; every other ambient +-- binder remains a parameter. +scopedSetInductionInstance :: Natural -> ScopedCheckedCore global - -> Maybe (ScopedCheckedCore global) -scopedSetInductionHypothesis selected + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + , ScopedCheckedCore global + , ScopedCheckedCore global + ) +scopedSetInductionInstance selected (ScopedCheckedCore context TyProp property) | binderTypeAt selected context == Just TySet = - Just - (ScopedCheckedCore - context - TyProp - (CForall - TySet - (CImp - (CApp - (CApp - (CIntrinsic Member) - (CBound 0)) - (CBound (selected + 1))) - (replaceSelectedWithNearest - 0 property)))) + Just (predicate, hypothesis, step, result) where - replaceSelectedWithNearest depth = \case + abstractedProperty = abstractSelected 0 property + predicate = + ScopedCheckedCore + context + (TySet `TyArrow` TyProp) + (CLam TySet abstractedProperty) + hypothesis = + ScopedCheckedCore + context + TyProp + (CForall + TySet + (CImp + (CApp + (CApp + (CIntrinsic Member) + (CBound 0)) + (CBound (selected + 1))) + abstractedProperty)) + step = + ScopedCheckedCore + context + TyProp + (CForall + TySet + (CImp + (abstractSelected + 0 + (scopedCoreTerm hypothesis)) + abstractedProperty)) + result = + ScopedCheckedCore + context + TyProp + (CForall TySet abstractedProperty) + + abstractSelected depth = \case CBound index | index == depth + selected -> CBound depth @@ -973,25 +1097,25 @@ scopedSetInductionHypothesis selected COpaqueInteger integer CApp function argument -> CApp - (replaceSelectedWithNearest depth function) - (replaceSelectedWithNearest depth argument) + (abstractSelected depth function) + (abstractSelected depth argument) CLam binderType body -> CLam binderType - (replaceSelectedWithNearest (depth + 1) body) + (abstractSelected (depth + 1) body) CFalsum -> CFalsum CImp premise conclusion -> CImp - (replaceSelectedWithNearest depth premise) - (replaceSelectedWithNearest depth conclusion) + (abstractSelected depth premise) + (abstractSelected depth conclusion) CEq operandType left right -> CEq operandType - (replaceSelectedWithNearest depth left) - (replaceSelectedWithNearest depth right) + (abstractSelected depth left) + (abstractSelected depth right) CForall binderType body -> CForall binderType - (replaceSelectedWithNearest (depth + 1) body) -scopedSetInductionHypothesis _selected _property = + (abstractSelected (depth + 1) body) +scopedSetInductionInstance _selected _property = Nothing -- | Close the nearest checked binder as one leading universal. @@ -1058,6 +1182,52 @@ openScopedImplication openScopedImplication _scoped = Nothing +-- | Open a checked proof assumption against the current goal. Besides a +-- direct implication antecedent, the source language historically permits +-- either immediate side of one binary conjunction antecedent to be assumed +-- first. The other side remains the next implication antecedent. This is a +-- deliberately shallow structural rule: it neither flattens conjunctions nor +-- treats disjunction as an eliminable assumption. +openScopedAssumption + :: Eq global + => ScopedCheckedCore global + -> ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + ) +openScopedAssumption supplied goal = do + (antecedent, conclusion) <- openScopedImplication goal + if supplied == antecedent + then pure (antecedent, conclusion) + else do + (left, right) <- splitScopedConjunction antecedent + if supplied == left + then do + remaining <- implyScopedCore right conclusion + pure (left, remaining) + else if supplied == right + then do + remaining <- implyScopedCore left conclusion + pure (right, remaining) + else Nothing + +splitScopedConjunction + :: ScopedCheckedCore global + -> Maybe + ( ScopedCheckedCore global + , ScopedCheckedCore global + ) +splitScopedConjunction + (ScopedCheckedCore context TyProp + (CImp (CImp left (CImp right CFalsum)) CFalsum)) = + Just + ( ScopedCheckedCore context TyProp left + , ScopedCheckedCore context TyProp right + ) +splitScopedConjunction _scoped = + Nothing + closeScopedCore :: ScopedCheckedCore global -> Maybe (FrozenCheckedCore global) diff --git a/source/Checking/Declaration.hs b/source/Checking/Declaration.hs index 65b7675..6d5dab4 100644 --- a/source/Checking/Declaration.hs +++ b/source/Checking/Declaration.hs @@ -35,6 +35,7 @@ module Checking.Declaration , runProspectiveLoweringDriver , nextDeclarationSlotLowering , currentTheoryLowering + , currentFoundationLowering , currentFoundationAxiomLowering , resolveVisibleFactAliasLowering , resolveVisibleFactTargetsLowering @@ -71,6 +72,8 @@ module Checking.Declaration , checkedSourceAxiomPlanning , checkedDatatypePlanning , checkedKernelPlanning + , checkedKernelPlanningWithStaged + , checkedStagedKernelPlanning , checkedSourceProofPlanning , checkedOmittedPlanning , CheckedPlannedVampireRequest @@ -95,6 +98,9 @@ module Checking.Declaration , prepareCandidateSpecLowering , prepareFrozenCandidateSpecLowering , prepareDefinitionEquationSpecLowering + , prepareDefinitionEquationSpecWithEligibilityLowering + , prepareNamedSetConstructionSpecLowering + , prepareRelationalSetConstructionSpecLowering , preparePointwiseDefinitionEquationSpecLowering , prepareStagedCandidateVampireLowering , ReservedCandidate @@ -127,6 +133,8 @@ module Checking.Declaration , authorizeKernelProofCandidate , authorizeKernelConstructionCandidate , authorizeDefinitionEquationCandidate + , authorizeNamedSetConstructionCandidate + , authorizeRelationalSetConstructionCandidate , acceptVampireObligation , acceptPreparedVampireObligation , acceptCurrentCandidateVampire @@ -172,7 +180,9 @@ import Checking.Identity import Checking.Kernel.Derivation import Checking.Semantic import Checking.Materialization qualified as Materialization -import Felix.Cache.Codec (encodeCache) +import Checking.SetConstruction +import Felix.Cache.Codec + ( encodeCache ) import Felix.Module import Provers qualified import Report.Location @@ -1338,6 +1348,10 @@ currentTheoryLowering :: LoweringDriver TheoryId currentTheoryLowering = withLoweringBuilder logicalBuilderTheory +currentFoundationLowering :: LoweringDriver CheckedFoundation +currentFoundationLowering = + withLoweringBuilder logicalBuilderFoundation + currentFoundationAxiomLowering :: FoundationAxiomTag -> LoweringDriver (FrozenCheckedCore Void) @@ -1515,6 +1529,29 @@ checkedKernelPlanning descriptor facts = [] [] +checkedKernelPlanningWithStaged + :: KernelConstructionDescriptor + -> [SemanticFactOccurrenceFingerprint] + -> [PlannedCandidatePosition] + -> CandidatePlanningSpec +checkedKernelPlanningWithStaged descriptor facts staged = + CandidatePlanningSpec + (PlanningKernelConstruction descriptor) + facts + staged + [] + +checkedStagedKernelPlanning + :: KernelConstructionDescriptor + -> [PlannedCandidatePosition] + -> CandidatePlanningSpec +checkedStagedKernelPlanning descriptor staged = + CandidatePlanningSpec + (PlanningKernelConstruction descriptor) + [] + staged + [] + checkedSourceProofPlanning :: [CheckedPlannedVampireRequest] -> [PlannedCandidatePosition] @@ -1672,9 +1709,74 @@ prepareDefinitionEquationSpecLowering -> SemanticName -> LoweringDriver (Either DeclarationError CandidateSpec) prepareDefinitionEquationSpecLowering objects identity alias = + prepareDefinitionEquationSpecWithEligibilityLowering + objects identity SearchEligible alias + +prepareDefinitionEquationSpecWithEligibilityLowering + :: [AssertedObject] + -> ObjectId + -> FactSearchEligibility + -> SemanticName + -> LoweringDriver (Either DeclarationError CandidateSpec) +prepareDefinitionEquationSpecWithEligibilityLowering + objects identity eligibility alias = prepareCandidateSpecWithLoweringClosure objects (\closure -> - prepareDefinitionEquationSpec closure identity alias) + prepareDefinitionEquationSpecWithEligibility + closure identity eligibility alias) + +-- | Prepare the unaliased first-order view of one checked, named set +-- construction. The returned descriptor binds direct authorization to the +-- transparent object and the complete checked source decomposition. +prepareNamedSetConstructionSpecLowering + :: [AssertedObject] + -> ObjectId + -> NamedSetConstruction ObjectId + -> LoweringDriver + (Either + DeclarationError + (CandidateSpec, KernelConstructionDescriptor)) +prepareNamedSetConstructionSpecLowering objects identity construction = + withLoweringBuilder \builder -> do + closure <- + first DeclarationObjectValidationFailed + (extendObjectClosure + (logicalBuilderObjectClosure builder) + objects) + (proposition, descriptor) <- + prepareNamedSetConstruction + (logicalBuilderFoundation builder) + closure identity construction + spec <- + prepareFrozenCandidateSpec + closure proposition SearchEligible [] + pure (spec, descriptor) + +prepareRelationalSetConstructionSpecLowering + :: [AssertedObject] + -> ObjectId + -> CheckedRelationalSetConstruction ObjectId + -> FrozenCheckedCore ObjectId + -> LoweringDriver + (Either + DeclarationError + (CandidateSpec, KernelConstructionDescriptor)) +prepareRelationalSetConstructionSpecLowering + objects identity construction functionality = + withLoweringBuilder \builder -> do + closure <- + first DeclarationObjectValidationFailed + (extendObjectClosure + (logicalBuilderObjectClosure builder) + objects) + (proposition, descriptor) <- + prepareRelationalSetConstruction + (logicalBuilderFoundation builder) + closure identity construction functionality + spec <- + prepareFrozenCandidateSpec + closure proposition SearchEligible [] + pure (spec, descriptor) preparePointwiseDefinitionEquationSpecLowering :: [AssertedObject] @@ -1860,8 +1962,8 @@ prepareCandidateSpecWithDriverClosure objects prepare = ModuleDriver do prepareCandidateSpecWithLoweringClosure :: [AssertedObject] - -> (CheckedObjectClosure -> Either DeclarationError CandidateSpec) - -> LoweringDriver (Either DeclarationError CandidateSpec) + -> (CheckedObjectClosure -> Either DeclarationError value) + -> LoweringDriver (Either DeclarationError value) prepareCandidateSpecWithLoweringClosure objects prepare = withLoweringBuilder \builder -> do closure <- @@ -2100,6 +2202,17 @@ prepareDefinitionEquationSpec -> SemanticName -> Either DeclarationError CandidateSpec prepareDefinitionEquationSpec closure identity alias = do + prepareDefinitionEquationSpecWithEligibility + closure identity SearchEligible alias + +prepareDefinitionEquationSpecWithEligibility + :: CheckedObjectClosure + -> ObjectId + -> FactSearchEligibility + -> SemanticName + -> Either DeclarationError CandidateSpec +prepareDefinitionEquationSpecWithEligibility + closure identity eligibility alias = do content <- maybe (Left (DefinitionEquationObjectMissing identity)) @@ -2116,7 +2229,70 @@ prepareDefinitionEquationSpec closure identity alias = do (validatePropositionContent closure (CEq coreType (CGlobal identity) body)) - pure (candidateSpec proposition SearchEligible [alias]) + pure (candidateSpec proposition eligibility [alias]) + +prepareNamedSetConstruction + :: CheckedFoundation + -> CheckedObjectClosure + -> ObjectId + -> NamedSetConstruction ObjectId + -> Either + DeclarationError + (FrozenCheckedCore ObjectId, KernelConstructionDescriptor) +prepareNamedSetConstruction foundation closure identity construction = do + let expectedContent = namedSetConstructionClosedBody construction + case lookupCheckedObjectContent identity closure of + Just (TransparentObjectContent _theory coreType body) + | coreType == frozenCoreType expectedContent + , body == frozenCoreTerm expectedContent -> pure () + _ -> Left KernelConstructionDescriptorMismatch + derived <- + maybe + (Left KernelConstructionDescriptorMismatch) + Right + (namedSetConstructionObjectFact + (checkedFoundationSetConstruction foundation) + identity + construction) + pure + ( namedSetConstructionFactProposition derived + , CheckedSetConstructionExtensionality + identity + (namedSetConstructionFactDescriptor derived) + ) + +prepareRelationalSetConstruction + :: CheckedFoundation + -> CheckedObjectClosure + -> ObjectId + -> CheckedRelationalSetConstruction ObjectId + -> FrozenCheckedCore ObjectId + -> Either + DeclarationError + (FrozenCheckedCore ObjectId, KernelConstructionDescriptor) +prepareRelationalSetConstruction + foundation closure identity construction functionality = do + let expectedContent = relationalSetConstructionClosedBody construction + case lookupCheckedObjectContent identity closure of + Just (TransparentObjectContent _theory coreType body) + | coreType == frozenCoreType expectedContent + , body == frozenCoreTerm expectedContent -> pure () + _ -> Left KernelConstructionDescriptorMismatch + derived <- + maybe + (Left KernelConstructionDescriptorMismatch) + Right + (relationalSetConstructionObjectFact + (checkedFoundationSetConstruction foundation) + identity + construction + functionality) + pure + ( relationalSetConstructionFactProposition derived + , CheckedSetConstructionExtensionality + identity + (relationalSetConstructionFactDescriptor derived) + ) preparePointwiseDefinitionEquationSpec :: CheckedObjectClosure @@ -2817,20 +2993,30 @@ prepareVampireObligationWith globalType builder selection - let (globalMode, localPolicy) = + let localPremisePolicy = case selection of VampireImplicitPremises -> - ( Backend.ImplicitFofPremises - , Backend.FirstOrderLocals - ) + Backend.FirstOrderLocals + VampireExplicitPremises{} + | any + (\fact -> + case Backend.typedBackendFactCapability fact of + Backend.FofProjectable{} -> False + Backend.RequiresTh0{} -> True) + selected -> + Backend.CompleteLocals + | otherwise -> + Backend.FirstOrderLocals + VampireLocalPremises -> + Backend.CompleteLocals + higherOrderPolicy = + case selection of + VampireImplicitPremises -> + Backend.ImplicitConstructionJustification VampireExplicitPremises{} -> - ( Backend.ExplicitGlobalPremises - , Backend.FirstOrderLocals - ) + Backend.ExplicitHigherOrderJustification VampireLocalPremises -> - ( Backend.NoGlobalPremises - , Backend.AllLocals - ) + Backend.ExplicitHigherOrderJustification propositionDependencies = foundationAxiomDependencies . Backend.supportedPropositionTerm @@ -2846,7 +3032,7 @@ prepareVampireObligationWith (propositionDependencies . Backend.typedLocalPremiseProposition) (Backend.selectTypedLocalPremises - localPolicy + localPremisePolicy locals) ) auxiliaries = @@ -2861,8 +3047,8 @@ prepareVampireObligationWith claim locals auxiliaries - globalMode - localPolicy) + localPremisePolicy + higherOrderPolicy) task <- first VampireObligationEncodingFailed (Provers.prepareTypedProverTask @@ -3617,6 +3803,81 @@ authorizeDefinitionEquationCandidate identity candidate = (candidateProofSafety initial) initial +-- | Authorize only the extensional fact deterministically derived from the +-- checked source construction and its committed transparent object. +authorizeNamedSetConstructionCandidate + :: ObjectId + -> NamedSetConstruction ObjectId + -> ReservedCandidate + -> Declaration () +authorizeNamedSetConstructionCandidate identity construction candidate = + authorizeOneCandidate candidate \initial -> do + let builder = candidateProofBuilder initial + (expected, descriptor) <- + Except.liftEither + (prepareNamedSetConstruction + (logicalBuilderFoundation builder) + (candidateProofObjectClosure initial) + identity + construction) + when (isNothing (candidateProofCachedValidation initial)) do + unless + (frozenCoreTerm expected + == frozenCoreTerm + (checkedPropositionTerm + (candidateCheckedProposition candidate)) + ) + (Except.throwError + KernelConstructionDescriptorMismatch) + completeCandidateWithValidation + candidate + (CheckedKernelConstruction descriptor) + (candidateProofSafety initial) + initial + +-- | Authorize the relational extensional view only after consuming the exact +-- strictly-earlier functionality candidate. The consumed candidate supplies +-- both real authority safety and the proposition rechecked by the confined +-- construction schema; a caller cannot substitute an arbitrary theorem. +authorizeRelationalSetConstructionCandidate + :: ObjectId + -> CheckedRelationalSetConstruction ObjectId + -> ReservedCandidate + -> ReservedCandidate + -> Declaration () +authorizeRelationalSetConstructionCandidate + identity construction functionality candidate = + authorizeOneCandidate candidate \initial -> do + (_used, final) <- + State.runStateT + (runCandidateProof (useStagedCandidate functionality)) + initial + let builder = candidateProofBuilder final + functionalityTerm = + checkedPropositionTerm + (candidateCheckedProposition functionality) + (expected, descriptor) <- + Except.liftEither + (prepareRelationalSetConstruction + (logicalBuilderFoundation builder) + (candidateProofObjectClosure final) + identity + construction + functionalityTerm) + when (isNothing (candidateProofCachedValidation final)) do + unless + (frozenCoreTerm expected + == frozenCoreTerm + (checkedPropositionTerm + (candidateCheckedProposition candidate))) + (Except.throwError + KernelConstructionDescriptorMismatch) + completeCandidateWithValidation + candidate + (CheckedKernelConstruction descriptor) + (candidateProofSafety final) + final + authorizeSourceAxiomCandidate :: ReservedCandidate -> Declaration () @@ -4685,6 +4946,8 @@ validateKernelConstruction descriptor proposition replayed proofState = && noFoundation && noRules && matchesDefinitionEquation identity proposition proofState + CheckedSetConstructionExtensionality{} -> + False matchesDefinitionEquation :: ObjectId diff --git a/source/Checking/Exact.hs b/source/Checking/Exact.hs index d0278f5..47e3859 100644 --- a/source/Checking/Exact.hs +++ b/source/Checking/Exact.hs @@ -9,13 +9,19 @@ module Checking.Exact , ExactBinderContext , emptyExactBinderContext , extendExactBinderContext + , extendExactAnonymousBinderContext , exactBinderContextSupport , exactBinderContextIndex , PreparedExactProposition , preparedExactPropositionCore , prepareExactProposition + , prepareExactSymbolicBoundConstraints + , prepareExactSymbolicWitnessConstraints + , prepareExactNounWitnessConstraints , PreparedExactSetExpression + , PreparedExactSetConstruction(..) , preparedExactSetExpressionCore + , preparedExactSetExpressionConstruction , prepareExactSetExpression , PreparedExactLocalFunctionGraph , preparedExactLocalFunctionGraphCore @@ -37,6 +43,7 @@ module Checking.Exact , preparedExactIsDefinition , prepareExactDeclaration , lowerPreparedExactBinding + , CheckedExactBindingAuthorization , authorizeCheckedExactBinding , PreparedExactStructure , prepareExactStructure @@ -57,6 +64,7 @@ import Checking.Core import Checking.Declaration qualified as Declaration import Checking.Exact.Vocabulary import Checking.Identity +import Checking.SetConstruction import Checking.Semantic import Felix.Cache.Codec import Felix.Module @@ -95,7 +103,7 @@ exactLocalIdValue (ExactLocalId value) = value data ExactBinder = ExactBinder !ExactLocalId - !Raw.VarSymbol + !(Maybe Raw.VarSymbol) !CoreType !(Maybe ExactStructureAnnotation) @@ -123,14 +131,33 @@ extendExactBinderContext additions (ExactBinderContext initial) = | any (sameIdentity identity) binders = Left (ExactDuplicateLocalIdentity (locate variable) identity) | otherwise = - Right (ExactBinder identity variable TySet Nothing : binders) + Right (ExactBinder identity (Just variable) TySet Nothing : binders) sameVariable variable (ExactBinder _identity existing _coreType _structure) = - existing == variable + existing == Just variable sameIdentity identity (ExactBinder existing _variable _coreType _structure) = existing == identity +-- | Add one proof-owned binder which deliberately has no source-resolvable +-- spelling. This is used for a nameless singular witness; it participates in +-- checked support and de Bruijn weakening but cannot shadow or be looked up by +-- a later source variable. +extendExactAnonymousBinderContext + :: ExactLocalId + -> ExactBinderContext + -> Either ExactCompileError ExactBinderContext +extendExactAnonymousBinderContext identity (ExactBinderContext binders) + | any sameIdentity binders = + Left (ExactDuplicateLocalIdentity Nowhere identity) + | otherwise = + Right + (ExactBinderContext + (ExactBinder identity Nothing TySet Nothing : binders)) + where + sameIdentity (ExactBinder existing _variable _coreType _structure) = + existing == identity + exactBinderContextSupport :: ExactBinderContext -> Vector (ExactLocalId, CoreType) @@ -150,7 +177,7 @@ exactBinderContextIndex variable (ExactBinderContext binders) = go _index [] = Nothing go index (ExactBinder _identity candidate _coreType _structure : rest) - | candidate == variable = Just index + | candidate == Just variable = Just index | otherwise = go (index + 1) rest newtype PreparedExactProposition = PreparedExactProposition @@ -162,15 +189,29 @@ preparedExactPropositionCore preparedExactPropositionCore (PreparedExactProposition proposition) = proposition -newtype PreparedExactSetExpression = PreparedExactSetExpression - (ScopedCheckedCore ObjectId) +data PreparedExactSetExpression = PreparedExactSetExpression + !(ScopedCheckedCore ObjectId) + !(Maybe PreparedExactSetConstruction) + +data PreparedExactSetConstruction + = PreparedUnconditionalSetConstruction + !(NamedSetConstruction ObjectId) + | PreparedRelationalSetConstruction + !(CheckedRelationalSetConstruction ObjectId) preparedExactSetExpressionCore :: PreparedExactSetExpression -> ScopedCheckedCore ObjectId -preparedExactSetExpressionCore (PreparedExactSetExpression expression) = +preparedExactSetExpressionCore (PreparedExactSetExpression expression _construction) = expression +preparedExactSetExpressionConstruction + :: PreparedExactSetExpression + -> Maybe PreparedExactSetConstruction +preparedExactSetExpressionConstruction + (PreparedExactSetExpression _expression construction) = + construction + -- | A checked replacement graph and the two checked arguments used to -- specialize its foundation characteristic. This is transient proof -- preparation data, not a declaration or durable object. @@ -251,40 +292,41 @@ data PreparedExactDeclaration = PreparedExactDeclaration !SemanticGlobalTarget !(Maybe AssertedObject) !(Maybe SemanticName) + !(Maybe PreparedExactSetConstruction) !DeclarationSyntaxId preparedExactLocation :: PreparedExactDeclaration -> Location preparedExactLocation - (PreparedExactDeclaration location _family _key _target _object _alias _syntax) = + (PreparedExactDeclaration location _family _key _target _object _alias _construction _syntax) = location preparedExactGlobalKey :: PreparedExactDeclaration -> SemanticGlobalKey preparedExactGlobalKey - (PreparedExactDeclaration _location _family key _target _object _alias _syntax) = + (PreparedExactDeclaration _location _family key _target _object _alias _construction _syntax) = key preparedExactObjectId :: PreparedExactDeclaration -> ObjectId preparedExactObjectId - (PreparedExactDeclaration _location _family _key target _object _alias _syntax) = + (PreparedExactDeclaration _location _family _key target _object _alias _construction _syntax) = semanticGlobalTargetObject target preparedExactObject :: PreparedExactDeclaration -> Maybe AssertedObject preparedExactObject - (PreparedExactDeclaration _location _family _key _target object _alias _syntax) = + (PreparedExactDeclaration _location _family _key _target object _alias _construction _syntax) = object preparedExactSyntaxId :: PreparedExactDeclaration -> DeclarationSyntaxId preparedExactSyntaxId - (PreparedExactDeclaration _location _family _key _target _object _alias syntax) = + (PreparedExactDeclaration _location _family _key _target _object _alias _construction syntax) = syntax preparedExactIsDefinition :: PreparedExactDeclaration -> Bool preparedExactIsDefinition - (PreparedExactDeclaration _location family _key _target _object _alias _syntax) = + (PreparedExactDeclaration _location family _key _target _object _alias _construction _syntax) = family == ExactDefinition preparedExactGlobalTarget @@ -292,7 +334,7 @@ preparedExactGlobalTarget -> SemanticGlobalTarget preparedExactGlobalTarget (PreparedExactDeclaration - _location _family _key target _object _alias _syntax) = + _location _family _key target _object _alias _construction _syntax) = target preparedDefinitionAlias @@ -300,9 +342,17 @@ preparedDefinitionAlias -> Maybe SemanticName preparedDefinitionAlias (PreparedExactDeclaration - _location _family _key _target _object alias _syntax) = + _location _family _key _target _object alias _construction _syntax) = alias +preparedDefinitionConstruction + :: PreparedExactDeclaration + -> Maybe PreparedExactSetConstruction +preparedDefinitionConstruction + (PreparedExactDeclaration + _location _family _key _target _object _alias construction _syntax) = + construction + data PreparedExactSourceAxiom = PreparedExactSourceAxiom !Location !SemanticName @@ -331,6 +381,11 @@ data CheckedExactStructureAuthorization = data ExactCompileError = ExactUnsupportedDeclaration !Location | ExactUnsupportedDeclarationBody !Location + | ExactNonCanonicalSetDefinitionAnnotation !Location + | ExactGuardedTransparentDefinition !Location + | ExactGuardedOpaqueSignature !Location + | ExactDefinitionCombinedSymbolicAlias !Location + | ExactRelationalReplacementRequiresNamedDefinition !Location | ExactDeclarationOccurrenceMissing !Location | ExactDeclarationOccurrenceAmbiguous !Location | ExactDeclarationHeadMismatch !Location @@ -349,7 +404,7 @@ data ExactCompileError | ExactCoreCheckFailed !Location !CoreCheckError | ExactObjectTypeMismatch !Location !CoreType !CoreType | ExactUnsupportedHeaderAssumption !Location - | ExactQuantifiedTermRequiresStatementSubject !Location + | ExactQuantifiedTermRequiresPropositionContext !Location | ExactStructureNotVisible !Location !SemanticStructurePhrase | ExactBaseStructureNotAssertable !Location !SemanticStructurePhrase | ExactDuplicateStructureAnnotation !Location !Raw.VarSymbol @@ -378,6 +433,11 @@ exactCompileErrorLocation :: ExactCompileError -> Location exactCompileErrorLocation = \case ExactUnsupportedDeclaration location -> location ExactUnsupportedDeclarationBody location -> location + ExactNonCanonicalSetDefinitionAnnotation location -> location + ExactGuardedTransparentDefinition location -> location + ExactGuardedOpaqueSignature location -> location + ExactDefinitionCombinedSymbolicAlias location -> location + ExactRelationalReplacementRequiresNamedDefinition location -> location ExactDeclarationOccurrenceMissing location -> location ExactDeclarationOccurrenceAmbiguous location -> location ExactDeclarationHeadMismatch location -> location @@ -395,7 +455,7 @@ exactCompileErrorLocation = \case ExactCoreCheckFailed location _failure -> location ExactObjectTypeMismatch location _expected _actual -> location ExactUnsupportedHeaderAssumption location -> location - ExactQuantifiedTermRequiresStatementSubject location -> location + ExactQuantifiedTermRequiresPropositionContext location -> location ExactStructureNotVisible location _phrase -> location ExactBaseStructureNotAssertable location _phrase -> location ExactDuplicateStructureAnnotation location _variable -> location @@ -420,6 +480,25 @@ renderExactCompileError = \case at location <> "this declaration is not yet supported by the typed checker" ExactUnsupportedDeclarationBody location -> at location <> "this source form is not yet supported by exact elaboration" + ExactNonCanonicalSetDefinitionAnnotation location -> + at location + <> "only the unmodified built-in noun `set` is a harmless definition annotation; " + <> "state a total condition in the definiens, or, where a corresponding opaque signature form exists, use it with a following explicit axiom; otherwise migrate the spelling or leave it unsupported" + ExactGuardedTransparentDefinition location -> + at location + <> "a transparent definition cannot have a header assumption; " + <> "state a total condition in the definiens, or, where a corresponding opaque signature form exists, use it with a following explicit axiom; otherwise migrate the spelling or leave it unsupported" + ExactGuardedOpaqueSignature location -> + at location + <> "an opaque signature cannot have a header assumption; " + <> "state the condition in a following explicit axiom" + ExactDefinitionCombinedSymbolicAlias location -> + at location + <> "a functional definition cannot declare a symbolic equivalent at the same time; " + <> "define the symbolic operator first, then define the functional phrase as an abbreviation applying it" + ExactRelationalReplacementRequiresNamedDefinition location -> + at location + <> "relational replacement is supported only as the outer body of a named definition" ExactDeclarationOccurrenceMissing location -> at location <> "the declaration has no associated syntax occurrence" ExactDeclarationOccurrenceAmbiguous location -> @@ -457,9 +536,9 @@ renderExactCompileError = \case <> " instead of " <> shown expected ExactUnsupportedHeaderAssumption location -> at location <> "this top-level header assumption is not yet supported by exact elaboration" - ExactQuantifiedTermRequiresStatementSubject location -> + ExactQuantifiedTermRequiresPropositionContext location -> at location - <> "a quantified term must be the sole subject of an exact statement" + <> "a quantified term requires a containing proposition" ExactStructureNotVisible location structurePhrase -> at location <> "the structure " <> shown structurePhrase <> " is not visible" ExactBaseStructureNotAssertable location structurePhrase -> @@ -517,6 +596,9 @@ renderExactCompileError = \case data ElaborationState = ElaborationState { elaborationBinders :: !(Map.Map Raw.VarSymbol Natural) + -- Counts every active de Bruijn binder, including anonymous and + -- contextual binders which have no entry in 'elaborationBinders'. + , elaborationBinderDepth :: !Natural , elaborationStructures :: !(Map.Map Natural ExactStructureAnnotation) , elaborationGlobals :: !(Map.Map ObjectId CoreType) , elaborationContextualBinder :: !(Maybe Natural) @@ -536,27 +618,117 @@ data PreparedHead = PreparedHead data PreparedBody = OpaqueBody - | TransparentBody !(CanonicalTerm ObjectId) + | TransparentBody + !(CanonicalTerm ObjectId) + !(Maybe PreparedExactSetConstruction) | ContextualTransparentBody !(Map.Map Raw.StructSymbol ObjectId) !(CanonicalTerm ObjectId) +data CompiledBody = CompiledBody + !(CanonicalTerm ObjectId) + !(Maybe CompiledNamedSetConstruction) + +data CompiledNamedSetConstruction + = CompiledSeparationConstruction + !(CanonicalTerm ObjectId) + !(CanonicalTerm ObjectId) + | CompiledFunctionalReplacementConstruction + !(NonEmpty (CanonicalTerm ObjectId)) + !(CanonicalTerm ObjectId) + !(Maybe (CanonicalTerm ObjectId)) + | CompiledRelationalReplacementConstruction + !(CanonicalTerm ObjectId) + !(CanonicalTerm ObjectId) + prepareExactProposition :: ExactBinderContext -> Raw.Stmt -> Declaration.LoweringDriver (Either ExactCompileError PreparedExactProposition) prepareExactProposition context statement = + prepareExactPropositionTerm + context + (locate statement) + (compileStatement statement) + +-- | Compile the source bound of already-opened symbolic binders. This is the +-- shared checked constraint seam used by quantified statements and proof +-- binders, so relation signs, carrier casts, and global occurrences are +-- elaborated exactly once by the ordinary expression compiler. +prepareExactSymbolicBoundConstraints + :: ExactBinderContext + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactSymbolicBoundConstraints context variables bound = + prepareExactPropositionTerm + context + (case bound of + Raw.Unbounded -> locate (NonEmpty.head variables) + _ -> locate bound) + (logicalConjunction + <$> compileSymbolicBoundConstraintList variables bound) + +-- | Compile the opened body used by a symbolic existential witness. Its +-- grouping is deliberately identical to 'SymbolicExists': all bound +-- constraints form the existential restriction and the stated proposition is +-- its body. +prepareExactSymbolicWitnessConstraints + :: ExactBinderContext + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Raw.Stmt + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactSymbolicWitnessConstraints context variables bound statement = + prepareExactPropositionTerm context (locate statement) do + constraints <- + logicalConjunction + <$> compileSymbolicBoundConstraintList variables bound + body <- compileStatement statement + pure + (if constraints == logicalTruth + then body + else logicalAnd constraints body) + +-- | Compile the checked constraint of an already-opened noun witness. Named +-- binders are resolved normally; a nameless singular noun uses the nearest +-- anonymous binder and therefore introduces no lookup spelling. +prepareExactNounWitnessConstraints + :: ExactBinderContext + -> Raw.NounPhrase [] + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactNounWitnessConstraints context nounPhrase = + case nounPhrase of + Raw.NounPhrase left noun variables right suchThat -> + prepareExactPropositionTerm context (locate noun) do + subjects <- + case NonEmpty.nonEmpty variables of + Just binders -> + toList + <$> traverse compileIntroducedVariable binders + Nothing -> + pure [CBound 0] + compileNounPhraseConstraints + subjects left noun right suchThat + +prepareExactPropositionTerm + :: ExactBinderContext + -> Location + -> Elaborate (CanonicalTerm ObjectId) + -> Declaration.LoweringDriver + (Either ExactCompileError PreparedExactProposition) +prepareExactPropositionTerm context location compile = Except.runExceptT do let initialElaboration = initialElaborationState context (term, finalElaboration) <- - State.runStateT - (compileStatement statement) - initialElaboration + State.runStateT compile initialElaboration checked <- either - (Except.throwError - . ExactCoreCheckFailed (locate statement)) + (Except.throwError . ExactCoreCheckFailed location) pure (checkScopedCanonicalCore (`Map.lookup` elaborationGlobals finalElaboration) @@ -565,7 +737,7 @@ prepareExactProposition context statement = unless (scopedCoreType checked == TyProp) (Except.throwError (ExactFormulaExpectedProposition - (locate statement) + location (scopedCoreType checked))) pure (PreparedExactProposition checked) @@ -577,10 +749,11 @@ prepareExactSetExpression prepareExactSetExpression context expression = Except.runExceptT do let initialElaboration = initialElaborationState context - (term, finalElaboration) <- + (compiled, finalElaboration) <- State.runStateT - (compileExpressionAsSet expression) + (compileNamedSetExpression expression) initialElaboration + let CompiledBody term rawConstruction = compiled checked <- either (Except.throwError @@ -595,7 +768,107 @@ prepareExactSetExpression context expression = (ExactExpressionExpectedSet (locate expression) (scopedCoreType checked))) - pure (PreparedExactSetExpression checked) + construction <- + Except.liftEither + (traverse + (checkCompiledNamedSetConstruction + (`Map.lookup` elaborationGlobals finalElaboration) + (binderTypes context)) + rawConstruction) + traverse_ + (\checkedConstruction -> + unless + (preparedSetConstructionTerm checkedConstruction == checked) + (impossible + "exact named construction disagrees with its checked expression")) + construction + pure (PreparedExactSetExpression checked construction) + +checkCompiledNamedSetConstruction + :: (ObjectId -> Maybe CoreType) + -> [CoreType] + -> CompiledNamedSetConstruction + -> Either ExactCompileError PreparedExactSetConstruction +checkCompiledNamedSetConstruction globalType context = \case + CompiledSeparationConstruction bound predicate -> do + checkedBound <- checkAt context TySet bound + checkedPredicate <- checkAt (TySet : context) TyProp predicate + maybe + (Left + (ExactCoreCheckFailed + Nowhere + (ExpectedCoreType TySet TyProp))) + (Right . PreparedUnconditionalSetConstruction) + (checkedSeparationConstruction + globalType checkedBound checkedPredicate) + CompiledFunctionalReplacementConstruction domains value condition -> do + let domainList = NonEmpty.toList domains + fullContext = replicate (length domainList) TySet <> context + checkedDomains <- + traverse + (\(depth, domain) -> + checkAt + (replicate depth TySet <> context) + TySet + domain) + (zip [0..] domainList) + checkedValue <- checkAt fullContext TySet value + checkedCondition <- traverse (checkAt fullContext TyProp) condition + maybe + (Left + (ExactCoreCheckFailed + Nowhere + (ExpectedCoreType TySet TyProp))) + (Right . PreparedUnconditionalSetConstruction) + (checkedFunctionalReplacementConstruction + globalType + (NonEmpty.fromList checkedDomains) + checkedValue + checkedCondition) + CompiledRelationalReplacementConstruction domain relation -> do + checkedDomain <- checkAt context TySet domain + checkedRelation <- checkAt (TySet : TySet : context) TyProp relation + maybe + (Left + (ExactCoreCheckFailed + Nowhere + (ExpectedCoreType TySet TyProp))) + (Right . PreparedRelationalSetConstruction) + (checkedRelationalReplacementConstruction + globalType checkedDomain checkedRelation) + where + checkAt expectedContext expectedType term = do + checked <- + first + (ExactCoreCheckFailed Nowhere) + (checkScopedCanonicalCore globalType expectedContext term) + unless + (scopedCoreType checked == expectedType) + (Left + (ExactCoreCheckFailed + Nowhere + (ExpectedCoreType + expectedType + (scopedCoreType checked)))) + pure checked + +preparedSetConstructionTerm + :: PreparedExactSetConstruction + -> ScopedCheckedCore ObjectId +preparedSetConstructionTerm = \case + PreparedUnconditionalSetConstruction construction -> + namedSetConstructionTerm construction + PreparedRelationalSetConstruction construction -> + relationalSetConstructionTerm construction + +preparedSetConstructionClosedBody + :: PreparedExactSetConstruction + -> FrozenCheckedCore ObjectId +preparedSetConstructionClosedBody = \case + PreparedUnconditionalSetConstruction construction -> + namedSetConstructionClosedBody construction + PreparedRelationalSetConstruction construction -> + relationalSetConstructionClosedBody construction prepareExactLocalFunctionGraph :: Location @@ -786,7 +1059,7 @@ binderIndices :: ExactBinderContext -> Map.Map Raw.VarSymbol Natural binderIndices (ExactBinderContext binders) = Map.fromList [ (variable, fromIntegral index) - | (index, ExactBinder _identity variable _coreType _structure) <- + | (index, ExactBinder _identity (Just variable) _coreType _structure) <- zip [0 :: Int ..] binders ] @@ -809,11 +1082,14 @@ binderTypes (ExactBinderContext binders) = initialElaborationState :: ExactBinderContext -> ElaborationState initialElaborationState context = ElaborationState - (binderIndices context) - (binderStructures context) - mempty - Nothing - mempty + { elaborationBinders = binderIndices context + , elaborationBinderDepth = + fromIntegral (length (binderTypes context)) + , elaborationStructures = binderStructures context + , elaborationGlobals = mempty + , elaborationContextualBinder = Nothing + , elaborationContextualRequirements = mempty + } annotateBinderContext :: Map.Map Natural ExactStructureAnnotation @@ -849,18 +1125,17 @@ compileHeaderAssumption = \case ] Raw.AsmLetIn variables domain -> do variableTerms <- traverse compileIntroducedVariable variables - domainTerm <- - compileExpressionAsSet domain - >>= structureCarrierCast (locate domain) - pure - [ ( locate variable - , CApp - (CApp (CIntrinsic Member) variableTerm) - domainTerm - ) - | (variable, variableTerm) <- - zip (toList variables) (toList variableTerms) - ] + domainTerm <- compileExpressionAsSet domain + traverse + (\(variable, variableTerm) -> do + proposition <- + compileMembership + (locate domain) + Raw.Positive + variableTerm + domainTerm + pure (locate variable, proposition)) + (zip (toList variables) (toList variableTerms)) Raw.AsmLetEq variable expression -> do variableTerm <- compileIntroducedVariable variable expressionTerm <- compileExpressionAsSet expression @@ -1072,14 +1347,39 @@ prepareExactDeclaration block entries = Just buildBody -> do let initialElaboration = ElaborationState - mempty mempty mempty Nothing mempty - (canonical, finalElaboration) <- + { elaborationBinders = mempty + , elaborationBinderDepth = 0 + , elaborationStructures = mempty + , elaborationGlobals = mempty + , elaborationContextualBinder = Nothing + , elaborationContextualRequirements = mempty + } + (CompiledBody canonical rawConstruction, finalElaboration) <- State.runStateT buildBody initialElaboration + let PreparedHead _semanticKey parameters _coreType = head' + construction <- + Except.liftEither + (traverse + (checkCompiledNamedSetConstruction + (`Map.lookup` + elaborationGlobals finalElaboration) + (replicate (length parameters) TySet)) + rawConstruction) + traverse_ + (\checkedConstruction -> + unless + (frozenCoreTerm + (preparedSetConstructionClosedBody + checkedConstruction) + == canonical) + (impossible + "exact named construction disagrees with its transparent body")) + construction let requirements = elaborationContextualRequirements finalElaboration body | Map.null requirements = - TransparentBody canonical + TransparentBody canonical construction | family == ExactAbbreviation = ContextualTransparentBody requirements @@ -1105,7 +1405,7 @@ prepareExactDeclaration block entries = OpaqueObjectContent theory seed coreType identity = opaqueObjectId theory seed coreType pure (GlobalReference identity, content') - TransparentBody canonical -> do + TransparentBody canonical _construction -> do checked <- either (Except.throwError @@ -1185,6 +1485,11 @@ prepareExactDeclaration block entries = target asserted alias + (case family of + ExactDefinition -> case body of + TransparentBody _canonical construction -> construction + _ -> Nothing + _ -> Nothing) syntax) lowerPreparedExactBinding @@ -1192,29 +1497,114 @@ lowerPreparedExactBinding -> Declaration.LoweringDriver (Either Declaration.DeclarationError - (Declaration.CheckedDeclaration (Maybe ObjectId))) + (Declaration.CheckedDeclaration CheckedExactBindingAuthorization)) lowerPreparedExactBinding prepared = case preparedDefinitionAlias prepared of Nothing -> pure (Right - (checked [] Nothing)) - Just alias -> - fmap - (\spec -> - checked - [ Declaration.checkedCandidate - spec - (Declaration.checkedDefinitionEquationPlanning - identity) - :| [] - ] - (Just identity)) - <$> Declaration.prepareDefinitionEquationSpecLowering - objects identity alias + (checked [] CheckedExactBindingNone)) + Just alias -> case preparedDefinitionConstruction prepared of + Nothing -> + fmap + (\spec -> + checked + [ Declaration.checkedCandidate + spec + (Declaration.checkedDefinitionEquationPlanning + identity) + :| [] + ] + (CheckedExactBindingDefinition identity)) + <$> Declaration.prepareDefinitionEquationSpecLowering + objects identity alias + Just (PreparedUnconditionalSetConstruction construction) -> + Except.runExceptT do + equation <- + Except.lift + (Declaration.prepareDefinitionEquationSpecWithEligibilityLowering + objects identity SearchIneligible alias) + >>= Except.liftEither + (extensional, descriptor) <- + Except.lift + (Declaration.prepareNamedSetConstructionSpecLowering + objects identity construction) + >>= Except.liftEither + pure + (checked + [ Declaration.checkedCandidate + equation + (Declaration.checkedDefinitionEquationPlanning + identity) + :| [ Declaration.checkedCandidate + extensional + (Declaration.checkedKernelPlanning + descriptor []) + ] + ] + (CheckedExactBindingConstruction + identity construction)) + Just (PreparedRelationalSetConstruction construction) -> + Except.runExceptT do + equation <- + Except.lift + (Declaration.prepareDefinitionEquationSpecWithEligibilityLowering + objects identity SearchIneligible alias) + >>= Except.liftEither + let functionality = + relationalSetConstructionClosedFunctionality + construction + functionalityScoped = + embedClosedCore [] functionality + functionalitySpec <- + Except.lift + (Declaration.prepareFrozenCandidateSpecLowering + objects functionality SearchIneligible []) + >>= Except.liftEither + obligation <- + Except.lift + (Declaration.prepareScopedVampireObligationLowering + Vector.empty + functionalityScoped + [] + [] + Declaration.VampireImplicitPremises) + >>= either + (Except.throwError + . Declaration.ProofObligationFailedAt location + . Declaration.CurrentCandidateVampirePreparationFailed) + pure + (extensional, descriptor) <- + Except.lift + (Declaration.prepareRelationalSetConstructionSpecLowering + objects identity construction functionality) + >>= Except.liftEither + pure + (checked + [ Declaration.checkedCandidate + equation + (Declaration.checkedDefinitionEquationPlanning + identity) + :| [ Declaration.checkedCandidate + functionalitySpec + (Declaration.checkedSourceProofPlanning + [Declaration.checkedPlannedVampireRequest + location obligation] + []) + ] + , Declaration.checkedCandidate + extensional + (Declaration.checkedStagedKernelPlanning + descriptor + [Declaration.plannedEarlierCandidate 0 1]) + :| [] + ] + (CheckedExactBindingRelationalConstruction + identity construction obligation)) where identity = preparedExactObjectId prepared objects = maybeToList (preparedExactObject prepared) + location = preparedExactLocation prepared checked stages body = Declaration.checkedCompiledDeclaration (preparedExactSyntaxId prepared) @@ -1227,20 +1617,53 @@ lowerPreparedExactBinding prepared = stages body +data CheckedExactBindingAuthorization + = CheckedExactBindingNone + | CheckedExactBindingDefinition !ObjectId + | CheckedExactBindingConstruction + !ObjectId + !(NamedSetConstruction ObjectId) + | CheckedExactBindingRelationalConstruction + !ObjectId + !(CheckedRelationalSetConstruction ObjectId) + !(Declaration.PreparedVampireObligation Void ()) + authorizeCheckedExactBinding - :: Maybe ObjectId + :: CheckedExactBindingAuthorization -> [NonEmpty Declaration.ReservedCandidate] -> Declaration.Declaration () authorizeCheckedExactBinding body stages = case (body, stages) of - (Nothing, []) -> pure () - (Just identity, [candidate :| []]) -> + (CheckedExactBindingNone, []) -> pure () + (CheckedExactBindingDefinition identity, [candidate :| []]) -> Declaration.authorizeDefinitionEquationCandidate identity candidate + ( CheckedExactBindingConstruction identity construction + , [equation :| [extensional]] + ) -> do + Declaration.authorizeDefinitionEquationCandidate + identity equation + Declaration.authorizeNamedSetConstructionCandidate + identity construction extensional + ( CheckedExactBindingRelationalConstruction + identity construction obligation + , [equation :| [functionality], extensional :| []] + ) -> do + Declaration.authorizeDefinitionEquationCandidate + identity equation + Declaration.authorizeVampireCandidate + functionality + (Declaration.acceptPreparedVampireObligation obligation) + Declaration.authorizeRelationalSetConstructionCandidate + identity construction functionality extensional _ -> Declaration.failDeclaration (Declaration.CheckedAuthorizationCandidateShapeMismatch - (if isJust body then 1 else 0) + (case body of + CheckedExactBindingNone -> 0 + CheckedExactBindingDefinition{} -> 1 + CheckedExactBindingConstruction{} -> 1 + CheckedExactBindingRelationalConstruction{} -> 2) (length stages)) prepareExactStructure @@ -1656,14 +2079,12 @@ prepareHead (Declaration.LoweringDriver) ( PreparedHead , ExactDeclarationFamily - , Maybe (Elaborate (CanonicalTerm ObjectId)) + , Maybe (Elaborate CompiledBody) ) prepareHead block key = case block of Raw.BlockSig location _title _marker assumptions signature -> do - unless (null assumptions) - (Except.throwError - (ExactUnsupportedDeclarationBody location)) + rejectHeaderAssumptions ExactGuardedOpaqueSignature assumptions head' <- prepareSignature location key signature pure (head', ExactSignature, Nothing) Raw.BlockAbbr location _title _marker abbreviation -> do @@ -1712,39 +2133,39 @@ prepareAbbreviation ExactCompileError (Declaration.LoweringDriver) ( PreparedHead - , Elaborate (CanonicalTerm ObjectId) + , Elaborate CompiledBody ) prepareAbbreviation location key = \case Raw.AbbreviationEq (Raw.SymbolPattern symbol parameters) expression -> do ensureExpressionKey location symbol key makeContextualTransparentHead location key parameters TySet - (compileExpressionAsSet expression) + (ordinaryCompiledBody <$> compileExpressionAsSet expression) Raw.AbbreviationFun (Raw.Fun _ item parameters) term -> do ensureFunctionPhraseKey location item key makeContextualTransparentHead location key parameters TySet - (compileTermAsSet term) + (ordinaryCompiledBody <$> compileTermAsSet term) Raw.AbbreviationAdj subject (Raw.Adj _ item arguments) statement -> do ensureAdjectiveKey location item key makeContextualTransparentHead location key (subject : arguments) TyProp - (compileStatement statement) + (ordinaryCompiledBody <$> compileStatement statement) Raw.AbbreviationVerb subject (Raw.Verb _ item arguments) statement -> do ensureVerbKey location item key makeContextualTransparentHead location key (subject : arguments) TyProp - (compileStatement statement) + (ordinaryCompiledBody <$> compileStatement statement) Raw.AbbreviationNoun subject (Raw.Noun _ item arguments) statement -> do ensureNounKey location item key makeContextualTransparentHead location key (subject : arguments) TyProp - (compileStatement statement) + (ordinaryCompiledBody <$> compileStatement statement) Raw.AbbreviationRel left relation parameters right statement -> do ensureRelationKey location relation key makeContextualTransparentHead location key (parameters <> [left, right]) TyProp - (compileStatement statement) + (ordinaryCompiledBody <$> compileStatement statement) prepareDefinition :: Location @@ -1754,31 +2175,32 @@ prepareDefinition ExactCompileError (Declaration.LoweringDriver) ( PreparedHead - , Elaborate (CanonicalTerm ObjectId) + , Elaborate CompiledBody ) prepareDefinition location key = \case Raw.Defn assumptions head' statement -> do - unless (null assumptions) - (Except.throwError - (ExactUnsupportedDeclarationBody location)) + rejectHeaderAssumptions ExactGuardedTransparentDefinition assumptions (parameters, resultType) <- definitionHead location key head' makeTransparentHead location key parameters resultType - (compileStatement statement) + (ordinaryCompiledBody <$> compileStatement statement) Raw.DefnFun assumptions (Raw.Fun _ item parameters) symbolic term -> do - unless (null assumptions && isNothing symbolic) + rejectHeaderAssumptions ExactGuardedTransparentDefinition assumptions + traverse_ (Except.throwError - (ExactUnsupportedDeclarationBody location)) + . ExactDefinitionCombinedSymbolicAlias + . locate) + symbolic ensureFunctionPhraseKey location item key makeTransparentHead location key parameters TySet - (compileTermAsSet term) + (compileNamedSetTerm term) Raw.DefnOp (Raw.SymbolPattern symbol parameters) expression -> do ensureExpressionKey location symbol key makeTransparentHead location key parameters TySet - (compileExpressionAsSet expression) + (compileNamedSetExpression expression) definitionHead :: Location @@ -1790,15 +2212,11 @@ definitionHead ([Raw.VarSymbol], CoreType) definitionHead location key = \case Raw.DefnAdj annotation subject (Raw.Adj _ item arguments) -> do - unless (isNothing annotation) - (Except.throwError - (ExactUnsupportedDeclarationBody location)) + validateDefinitionAnnotation annotation ensureAdjectiveKey location item key pure (subject : arguments, TyProp) Raw.DefnVerb annotation subject (Raw.Verb _ item arguments) -> do - unless (isNothing annotation) - (Except.throwError - (ExactUnsupportedDeclarationBody location)) + validateDefinitionAnnotation annotation ensureVerbKey location item key pure (subject : arguments, TyProp) Raw.DefnNoun subject (Raw.Noun _ item arguments) -> do @@ -1820,25 +2238,67 @@ definitionHead location key = \case (Except.throwError (ExactDeclarationHeadMismatch location)) pure (toList parameters, TyProp) +validateDefinitionAnnotation + :: MonadError ExactCompileError monad + => Maybe (Raw.NounPhrase Maybe) + -> monad () +validateDefinitionAnnotation = traverse_ \nounPhrase -> + unless (exactSetNounPhrase nounPhrase) + (throwError + (ExactNonCanonicalSetDefinitionAnnotation + (exactNounPhraseLocation nounPhrase))) + +rejectHeaderAssumptions + :: MonadError ExactCompileError monad + => (Location -> ExactCompileError) + -> [Raw.Asm] + -> monad () +rejectHeaderAssumptions makeError = \case + [] -> pure () + assumption : _ -> + throwError (makeError (exactAssumptionLocation assumption)) + +exactAssumptionLocation :: Raw.Asm -> Location +exactAssumptionLocation = \case + Raw.AsmSuppose statement -> locate statement + Raw.AsmLetNoun variables _nounPhrase -> locate variables + Raw.AsmLetIn variables _expression -> locate variables + Raw.AsmLetThe variable _function -> locate variable + Raw.AsmLetEq variable _expression -> locate variable + Raw.AsmLetStruct variable _structure -> locate variable + +exactNounPhraseLocation :: Raw.NounPhraseOf t argument -> Location +exactNounPhraseLocation + (Raw.NounPhrase _left noun _variables _right _suchThat) = + locate noun + makeTransparentHead :: Location -> SemanticGlobalKey -> [Raw.VarSymbol] -> CoreType - -> Elaborate (CanonicalTerm ObjectId) + -> Elaborate CompiledBody -> ExceptT ExactCompileError (Declaration.LoweringDriver) ( PreparedHead - , Elaborate (CanonicalTerm ObjectId) + , Elaborate CompiledBody ) makeTransparentHead location key parameters resultType body = do (prepared, binders) <- prepareParameters location key parameters resultType let close = do - State.modify' (\state -> state{elaborationBinders = binders}) - body' <- body - pure (foldr (const (CLam TySet)) body' parameters) + State.modify' \state -> + state + { elaborationBinders = binders + , elaborationBinderDepth = + fromIntegral (length parameters) + } + CompiledBody body' construction <- body + pure + (CompiledBody + (foldr (const (CLam TySet)) body' parameters) + construction) pure (prepared, close) makeContextualTransparentHead @@ -1846,12 +2306,12 @@ makeContextualTransparentHead -> SemanticGlobalKey -> [Raw.VarSymbol] -> CoreType - -> Elaborate (CanonicalTerm ObjectId) + -> Elaborate CompiledBody -> ExceptT ExactCompileError (Declaration.LoweringDriver) ( PreparedHead - , Elaborate (CanonicalTerm ObjectId) + , Elaborate CompiledBody ) makeContextualTransparentHead location key parameters resultType body = do (prepared, binders) <- @@ -1860,11 +2320,16 @@ makeContextualTransparentHead location key parameters resultType body = do State.modify' \state -> state { elaborationBinders = binders + , elaborationBinderDepth = + fromIntegral (length parameters) + 1 , elaborationContextualBinder = Just (fromIntegral (length parameters)) } - body' <- body - pure (foldr (const (CLam TySet)) body' parameters) + CompiledBody body' _construction <- body + pure + (CompiledBody + (foldr (const (CLam TySet)) body' parameters) + Nothing) pure (prepared, close) makePreparedHead @@ -1920,6 +2385,53 @@ compileExpressionAsSet expression = do (ExactExpressionExpectedSet (locate expression) actual)) pure term +-- | Compile one set expression once while retaining the checked-source shape +-- needed only when that expression is subsequently named by a definition. +-- Nested constructions remain ordinary exact terms. +compileNamedSetExpression + :: Raw.Expr + -> Elaborate CompiledBody +compileNamedSetExpression = \case + Raw.ExprSep _location variable bound predicate -> do + (term, bound', predicate') <- + compileSeparation variable bound predicate + pure + (CompiledBody term + (Just + (CompiledSeparationConstruction + bound' predicate'))) + Raw.ExprReplace _location value bounds condition -> do + replacement <- + compileFunctionalReplacement value bounds condition + pure + (CompiledBody + (compiledFunctionalReplacementTerm replacement) + (Just + (CompiledFunctionalReplacementConstruction + (compiledFunctionalReplacementDomains replacement) + (compiledFunctionalReplacementValue replacement) + (compiledFunctionalReplacementCondition replacement)))) + Raw.ExprReplacePred _location range domainVariable bound predicate -> do + (term, domain, relation) <- + compileRelationalReplacement + range domainVariable bound predicate + pure + (CompiledBody term + (Just + (CompiledRelationalReplacementConstruction + domain relation))) + expression -> + (`CompiledBody` Nothing) + <$> compileExpressionAsSet expression + +compileNamedSetTerm :: Raw.Term -> Elaborate CompiledBody +compileNamedSetTerm = \case + Raw.TermExpr expression -> compileNamedSetExpression expression + term -> ordinaryCompiledBody <$> compileTermAsSet term + +ordinaryCompiledBody :: CanonicalTerm ObjectId -> CompiledBody +ordinaryCompiledBody term = CompiledBody term Nothing + compileTermAsSet :: Raw.Term -> Elaborate (CanonicalTerm ObjectId) @@ -1933,11 +2445,73 @@ compileTermAsSet = \case applyResolved location key compiled Raw.TermQuantified _quantifier location _nounPhrase -> Except.throwError - (ExactQuantifiedTermRequiresStatementSubject location) + (ExactQuantifiedTermRequiresPropositionContext location) term -> Except.throwError (ExactUnsupportedDeclarationBody (locate term)) +-- | Compile a source term only at a proposition consumer. Indefinite terms +-- own the continuation, so their noun constraints and quantifier surround +-- exactly the proposition which consumes the resulting set. Function-phrase +-- arguments recurse through the same seam and therefore never masquerade as +-- independently set-valued terms. +compileTermInProposition + :: Raw.Term + -> (CanonicalTerm ObjectId + -> Elaborate (CanonicalTerm ObjectId)) + -> Elaborate (CanonicalTerm ObjectId) +compileTermInProposition term continuation = + case term of + Raw.TermExpr expression -> + compileExpressionAsSet expression >>= continuation + Raw.TermFun (Raw.Fun location item arguments) -> do + let patterns = Raw.lexicalItemSgPlPattern item + key = + SemanticFunctionPhrase + (Raw.sg patterns) + (Raw.pl patterns) + compileTermsInProposition arguments \compiled -> do + value <- applyResolved location key compiled + continuation value + Raw.TermQuantified quantifier _location nounPhrase -> + compileQuantifiedTermInProposition + quantifier nounPhrase continuation + Raw.TermIota location _variable _statement -> + Except.throwError (ExactUnsupportedDeclarationBody location) + +-- | Compile source-ordered proposition terms. The first source occurrence +-- receives the outermost continuation and therefore the widest scope. +compileTermsInProposition + :: [Raw.Term] + -> ([CanonicalTerm ObjectId] + -> Elaborate (CanonicalTerm ObjectId)) + -> Elaborate (CanonicalTerm ObjectId) +compileTermsInProposition terms continuation = + case terms of + [] -> continuation [] + term : remaining -> + compileTermInProposition term \compiled -> do + compiledDepth <- State.gets elaborationBinderDepth + compileTermsInProposition remaining \rest -> do + compiled' <- + weakenElaboratedTermFrom compiledDepth compiled + continuation (compiled' : rest) + +weakenElaboratedTermFrom + :: Natural + -> CanonicalTerm ObjectId + -> Elaborate (CanonicalTerm ObjectId) +weakenElaboratedTermFrom originalDepth term = do + currentDepth <- State.gets elaborationBinderDepth + when (currentDepth < originalDepth) + (impossible + "a proposition-term continuation escaped its binder scope") + pure + (shiftCanonical + (currentDepth - originalDepth) + 0 + term) + compileExpression :: Raw.Expr -> Elaborate (CanonicalTerm ObjectId, CoreType) @@ -1990,22 +2564,16 @@ compileExpression = \case , TySet ) Raw.ExprSep _location variable bound predicate -> do - bound' <- compileExpressionAsSet bound - predicate' <- - withSetBinders (variable :| []) - (compileStatement predicate) - pure - ( CApp - (CApp (CIntrinsic Sep) bound') - (CLam TySet predicate') - , TySet - ) + (term, _bound, _predicate) <- + compileSeparation variable bound predicate + pure (term, TySet) Raw.ExprReplace _location value bounds condition -> do - replacement <- compileReplacement value bounds condition - pure (replacement, TySet) + replacement <- + compileFunctionalReplacement value bounds condition + pure (compiledFunctionalReplacementTerm replacement, TySet) Raw.ExprReplacePred location _value _variable _bound _predicate -> Except.throwError - (ExactUnsupportedDeclarationBody location) + (ExactRelationalReplacementRequiresNamedDefinition location) compileStructureOperation :: Location @@ -2130,12 +2698,113 @@ structureCarrierCast location term = pure (CApp (CGlobal carrier) term) _ -> pure term -compileReplacement +compileMembership + :: Location + -> Raw.Sign + -> CanonicalTerm ObjectId + -> CanonicalTerm ObjectId + -> Elaborate (CanonicalTerm ObjectId) +compileMembership location sign element set = do + checkedSet <- structureCarrierCast location set + let proposition = + CApp + (CApp (CIntrinsic Member) element) + checkedSet + pure case sign of + Raw.Positive -> proposition + Raw.Negative -> logicalNot proposition + +compileSeparation + :: Raw.VarSymbol + -> Raw.Expr + -> Raw.Stmt + -> Elaborate + ( CanonicalTerm ObjectId + , CanonicalTerm ObjectId + , CanonicalTerm ObjectId + ) +compileSeparation variable bound predicate = do + bound' <- compileExpressionAsSet bound + predicate' <- + withSetBinders (variable :| []) + (compileStatement predicate) + pure + ( CApp + (CApp (CIntrinsic Sep) bound') + (CLam TySet predicate') + , bound' + , predicate' + ) + +compileRelationalReplacement + :: Raw.VarSymbol + -> Raw.VarSymbol + -> Raw.Expr + -> Raw.Stmt + -> Elaborate + ( CanonicalTerm ObjectId + , CanonicalTerm ObjectId + , CanonicalTerm ObjectId + ) +compileRelationalReplacement range domainVariable bound predicate = do + domain <- compileExpressionAsSet bound + relation <- + withSetBinders (domainVariable :| [range]) + (compileStatement predicate) + let restrictedDomain = + CApp + (CApp (CIntrinsic Sep) domain) + (CLam TySet (logicalExists relation)) + choiceFunction = + CLam TySet + (CApp (CIntrinsic SetChoose) (CLam TySet relation)) + replacement = + CApp + (CApp (CIntrinsic Repl) restrictedDomain) + choiceFunction + pure (replacement, domain, relation) + +data CompiledFunctionalReplacement = CompiledFunctionalReplacement + !(CanonicalTerm ObjectId) + !(NonEmpty (CanonicalTerm ObjectId)) + !(CanonicalTerm ObjectId) + !(Maybe (CanonicalTerm ObjectId)) + +compiledFunctionalReplacementTerm + :: CompiledFunctionalReplacement + -> CanonicalTerm ObjectId +compiledFunctionalReplacementTerm + (CompiledFunctionalReplacement term _domains _value _condition) = + term + +compiledFunctionalReplacementDomains + :: CompiledFunctionalReplacement + -> NonEmpty (CanonicalTerm ObjectId) +compiledFunctionalReplacementDomains + (CompiledFunctionalReplacement _term domains _value _condition) = + domains + +compiledFunctionalReplacementValue + :: CompiledFunctionalReplacement + -> CanonicalTerm ObjectId +compiledFunctionalReplacementValue + (CompiledFunctionalReplacement _term _domains value _condition) = + value + +compiledFunctionalReplacementCondition + :: CompiledFunctionalReplacement + -> Maybe (CanonicalTerm ObjectId) +compiledFunctionalReplacementCondition + (CompiledFunctionalReplacement _term _domains _value condition) = + condition + +compileFunctionalReplacement :: Raw.Expr -> NonEmpty (Raw.VarSymbol, Raw.Expr) -> Maybe Raw.Stmt - -> Elaborate (CanonicalTerm ObjectId) -compileReplacement value ((variable, domain) :| remaining) condition = do + -> Elaborate CompiledFunctionalReplacement +compileFunctionalReplacement + value ((variable, domain) :| remaining) condition = do domain' <- compileExpressionAsSet domain case remaining of [] -> do @@ -2152,19 +2821,31 @@ compileReplacement value ((variable, domain) :| remaining) condition = do (CApp (CIntrinsic Sep) domain') (CLam TySet predicate) pure - (CApp - (CApp (CIntrinsic Repl) filteredDomain) - (CLam TySet value')) + (CompiledFunctionalReplacement + (CApp + (CApp (CIntrinsic Repl) filteredDomain) + (CLam TySet value')) + (domain' :| []) + value' + condition') next : rest -> do nested <- withSetBinders (variable :| []) - (compileReplacement value (next :| rest) condition) + (compileFunctionalReplacement + value (next :| rest) condition) pure - (CApp - (CIntrinsic FamilyUnion) + (CompiledFunctionalReplacement (CApp - (CApp (CIntrinsic Repl) domain') - (CLam TySet nested))) + (CIntrinsic FamilyUnion) + (CApp + (CApp (CIntrinsic Repl) domain') + (CLam TySet + (compiledFunctionalReplacementTerm nested)))) + (domain' + NonEmpty.<| + compiledFunctionalReplacementDomains nested) + (compiledFunctionalReplacementValue nested) + (compiledFunctionalReplacementCondition nested)) compileStatement :: Raw.Stmt @@ -2172,24 +2853,14 @@ compileStatement compileStatement = \case Raw.StmtFormula formula -> compileFormula formula - Raw.StmtVerbPhrase - (Raw.TermQuantified quantifier _location nounPhrase :| []) - verbPhrase -> - compileQuantifiedTermSubject quantifier nounPhrase - (`compileVerbPhrase` verbPhrase) - Raw.StmtVerbPhrase terms verbPhrase -> do - subjects <- traverse compileTermAsSet terms - logicalConjunction - <$> traverse (`compileVerbPhrase` verbPhrase) subjects - Raw.StmtNoun - (Raw.TermQuantified quantifier _location quantified :| []) - nounPhrase -> - compileQuantifiedTermSubject quantifier quantified - (`compileNounPhraseMaybe` nounPhrase) - Raw.StmtNoun terms nounPhrase -> do - subjects <- traverse compileTermAsSet terms - logicalConjunction - <$> traverse (`compileNounPhraseMaybe` nounPhrase) subjects + Raw.StmtVerbPhrase terms verbPhrase -> + compileTermsInProposition (toList terms) \subjects -> + logicalConjunction + <$> traverse (`compileVerbPhrase` verbPhrase) subjects + Raw.StmtNoun terms nounPhrase -> + compileTermsInProposition (toList terms) \subjects -> + logicalConjunction + <$> traverse (`compileNounPhraseMaybe` nounPhrase) subjects Raw.StmtExists _location nounPhrase -> compileExistentialNounPhrase nounPhrase Raw.StmtQuantPhrase @@ -2210,30 +2881,30 @@ compileStatement = \case _location quantifier variables bound suchThat statement -> compileSymbolicQuantified quantifier variables bound suchThat (compileStatement statement) - Raw.StmtStruct term rawPhrase -> do - subject <- compileTermAsSet term - annotation <- - resolveStructureAnnotation (locate term) rawPhrase - predicate <- - maybe - (impossible "an assertable structure has no predicate") - pure - (structureAnnotationPredicate annotation) - recordExactGlobal - predicate - (TyArrow TySet TyProp) - pure - (CApp - (CGlobal predicate) - subject) + Raw.StmtStruct term rawPhrase -> + compileTermInProposition term \subject -> do + annotation <- + resolveStructureAnnotation (locate term) rawPhrase + predicate <- + maybe + (impossible "an assertable structure has no predicate") + pure + (structureAnnotationPredicate annotation) + recordExactGlobal + predicate + (TyArrow TySet TyProp) + pure + (CApp + (CGlobal predicate) + subject) -compileQuantifiedTermSubject +compileQuantifiedTermInProposition :: Raw.Quantifier -> Raw.NounPhrase Maybe -> (CanonicalTerm ObjectId -> Elaborate (CanonicalTerm ObjectId)) -> Elaborate (CanonicalTerm ObjectId) -compileQuantifiedTermSubject quantifier +compileQuantifiedTermInProposition quantifier (Raw.NounPhrase left noun named right suchThat) compileBody = case named of @@ -2260,21 +2931,8 @@ compileSymbolicQuantified -> Elaborate (CanonicalTerm ObjectId) compileSymbolicQuantified quantifier variables bound suchThat compileBody = withSetBinders variables do - subjects <- traverse compileIntroducedVariable variables - boundConstraints <- case bound of - Raw.Unbounded -> - pure [] - Raw.Bounded _location sign relation domain -> do - domain' <- compileExpressionAsSet domain - traverse - (\subject -> do - proposition <- - compileAtomicRelationTerms - subject relation domain' - pure case sign of - Raw.Positive -> proposition - Raw.Negative -> logicalNot proposition) - (toList subjects) + boundConstraints <- + compileSymbolicBoundConstraintList variables bound suchThatConstraints <- maybeToList <$> traverse compileStatement suchThat body <- compileBody @@ -2286,6 +2944,25 @@ compileSymbolicQuantified quantifier variables bound suchThat compileBody = (boundConstraints <> suchThatConstraints)) body) +compileSymbolicBoundConstraintList + :: NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Elaborate [CanonicalTerm ObjectId] +compileSymbolicBoundConstraintList variables = \case + Raw.Unbounded -> + pure [] + Raw.Bounded _location sign relation domain -> do + subjects <- traverse compileIntroducedVariable variables + domain' <- compileExpressionAsSet domain + traverse + (\subject -> do + proposition <- + compileAtomicRelationTerms subject relation domain' + pure case sign of + Raw.Positive -> proposition + Raw.Negative -> logicalNot proposition) + (toList subjects) + compileAtomicRelationTerms :: CanonicalTerm ObjectId -> Raw.Relation @@ -2299,16 +2976,18 @@ compileAtomicRelationTerms left relation right = (Raw.relationSymbolToken symbol) (Raw.relationSymbolParameterArity symbol) compiledParameters <- traverse compileExpressionAsSet parameters - checkedRight <- - if symbol == Raw.ElementSymbol && null parameters - then structureCarrierCast location right - else pure right case fixedSemanticMeaning key of Just FixedEquality | null parameters -> pure (CEq TySet left right) Just FixedDisequality | null parameters -> pure (logicalNot (CEq TySet left right)) + Just (FixedIntrinsic Member) + | null parameters -> + compileMembership location Raw.Positive left right + Just (FixedNegatedIntrinsic Member) + | null parameters -> + compileMembership location Raw.Negative left right Just (FixedIntrinsic intrinsic) -> do (term, actual) <- applyTyped @@ -2316,7 +2995,7 @@ compileAtomicRelationTerms left relation right = (CIntrinsic intrinsic) (coreIntrinsicType intrinsic) ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, checkedRight])) + <$> (compiledParameters <> [left, right])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -2328,7 +3007,7 @@ compileAtomicRelationTerms left relation right = (CIntrinsic intrinsic) (coreIntrinsicType intrinsic) ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, checkedRight])) + <$> (compiledParameters <> [left, right])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -2338,7 +3017,7 @@ compileAtomicRelationTerms left relation right = applyResolvedTyped location key ((\term -> (term, TySet)) - <$> (compiledParameters <> [left, checkedRight])) + <$> (compiledParameters <> [left, right])) unless (actual == TyProp) (Except.throwError (ExactFormulaExpectedProposition location actual)) @@ -2362,53 +3041,67 @@ compileVerbPhrase subject = \case logicalNot . logicalConjunction <$> traverse (compileAdjective subject) adjectives +compilePredicateArguments + :: CanonicalTerm ObjectId + -> [Raw.Term] + -> ( CanonicalTerm ObjectId + -> [CanonicalTerm ObjectId] + -> Elaborate (CanonicalTerm ObjectId) + ) + -> Elaborate (CanonicalTerm ObjectId) +compilePredicateArguments subject arguments continuation = do + subjectDepth <- State.gets elaborationBinderDepth + compileTermsInProposition arguments \compiled -> do + subject' <- weakenElaboratedTermFrom subjectDepth subject + continuation subject' compiled + compileVerb :: CanonicalTerm ObjectId -> Raw.Verb -> Elaborate (CanonicalTerm ObjectId) compileVerb subject (Raw.Verb location item arguments) = do let patterns = Raw.lexicalItemSgPlPattern item - compiled <- traverse compileTermAsSet arguments - applyResolvedPredicate - location - (SemanticVerb (Raw.sg patterns) (Raw.pl patterns)) - (subject : compiled) + compilePredicateArguments subject arguments \subject' compiled -> + applyResolvedPredicate + location + (SemanticVerb (Raw.sg patterns) (Raw.pl patterns)) + (subject' : compiled) compileAdjective :: CanonicalTerm ObjectId -> Raw.Adj -> Elaborate (CanonicalTerm ObjectId) -compileAdjective subject (Raw.Adj location item arguments) = do - compiled <- traverse compileTermAsSet arguments - applyResolvedPredicateChoice - location - ( SemanticRightAdjective (Raw.lexicalItemPattern item) - :| [SemanticLeftAdjective (Raw.lexicalItemPattern item)] - ) - (subject : compiled) +compileAdjective subject (Raw.Adj location item arguments) = + compilePredicateArguments subject arguments \subject' compiled -> + applyResolvedPredicateChoice + location + ( SemanticRightAdjective (Raw.lexicalItemPattern item) + :| [SemanticLeftAdjective (Raw.lexicalItemPattern item)] + ) + (subject' : compiled) compileLeftAdjective :: CanonicalTerm ObjectId -> Raw.AdjL -> Elaborate (CanonicalTerm ObjectId) -compileLeftAdjective subject (Raw.AdjL location item arguments) = do - compiled <- traverse compileTermAsSet arguments - applyResolvedPredicate - location - (SemanticLeftAdjective (Raw.lexicalItemPattern item)) - (subject : compiled) +compileLeftAdjective subject (Raw.AdjL location item arguments) = + compilePredicateArguments subject arguments \subject' compiled -> + applyResolvedPredicate + location + (SemanticLeftAdjective (Raw.lexicalItemPattern item)) + (subject' : compiled) compileRightAttribute :: CanonicalTerm ObjectId -> Raw.AdjR -> Elaborate (CanonicalTerm ObjectId) compileRightAttribute subject = \case - Raw.AdjR location item arguments -> do - compiled <- traverse compileTermAsSet arguments - applyResolvedPredicate - location - (SemanticRightAdjective (Raw.lexicalItemPattern item)) - (subject : compiled) + Raw.AdjR location item arguments -> + compilePredicateArguments subject arguments \subject' compiled -> + applyResolvedPredicate + location + (SemanticRightAdjective (Raw.lexicalItemPattern item)) + (subject' : compiled) Raw.AttrRThat verbPhrase -> compileVerbPhrase subject verbPhrase @@ -2422,24 +3115,33 @@ compileNoun subject (Raw.Noun location item arguments) | otherwise = do let patterns = Raw.lexicalItemSgPlPattern item key = SemanticNoun (Raw.sg patterns) (Raw.pl patterns) - compiled <- traverse compileTermAsSet arguments - case fixedSemanticMeaning key of - Just (FixedIntrinsic intrinsic) -> do - (term, actual) <- - applyTyped - location - (CIntrinsic intrinsic) - (coreIntrinsicType intrinsic) - ((\argument -> (argument, TySet)) - <$> (subject : compiled)) - unless (actual == TyProp) - (Except.throwError - (ExactFormulaExpectedProposition location actual)) - pure term - Just{} -> - impossible "a fixed noun is not a predicate intrinsic" - Nothing -> - applyResolvedPredicate location key (subject : compiled) + compilePredicateArguments subject arguments \subject' compiled -> + case fixedSemanticMeaning key of + Just (FixedIntrinsic Member) -> + case compiled of + [set] -> + compileMembership + location Raw.Positive subject' set + _ -> + impossible + "the fixed element noun does not have one argument" + Just (FixedIntrinsic intrinsic) -> do + (term, actual) <- + applyTyped + location + (CIntrinsic intrinsic) + (coreIntrinsicType intrinsic) + ((\argument -> (argument, TySet)) + <$> (subject' : compiled)) + unless (actual == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition location actual)) + pure term + Just{} -> + impossible "a fixed noun is not a predicate intrinsic" + Nothing -> + applyResolvedPredicate + location key (subject' : compiled) compileNounPhraseConstraints :: [CanonicalTerm ObjectId] @@ -2574,11 +3276,13 @@ withAnonymousSetBinder -> Elaborate value withAnonymousSetBinder action = do outer <- State.gets elaborationBinders + outerDepth <- State.gets elaborationBinderDepth outerStructures <- State.gets elaborationStructures outerContextual <- State.gets elaborationContextualBinder State.modify' \state -> state { elaborationBinders = (+ 1) <$> outer + , elaborationBinderDepth = outerDepth + 1 , elaborationStructures = Map.mapKeysMonotonic (+ 1) outerStructures , elaborationContextualBinder = (+ 1) <$> outerContextual @@ -2587,6 +3291,7 @@ withAnonymousSetBinder action = do State.modify' \state -> state { elaborationBinders = outer + , elaborationBinderDepth = outerDepth , elaborationStructures = outerStructures , elaborationContextualBinder = outerContextual } @@ -2598,6 +3303,7 @@ withSetBinders -> Elaborate value withSetBinders variables action = do outer <- State.gets elaborationBinders + outerDepth <- State.gets elaborationBinderDepth outerStructures <- State.gets elaborationStructures outerContextual <- State.gets elaborationContextualBinder case firstDuplicate (toList variables) of @@ -2624,6 +3330,7 @@ withSetBinders variables action = do State.modify' \state -> state { elaborationBinders = introduced <> shifted + , elaborationBinderDepth = outerDepth + binderCount , elaborationStructures = Map.mapKeysMonotonic (+ binderCount) outerStructures , elaborationContextualBinder = @@ -2633,6 +3340,7 @@ withSetBinders variables action = do State.modify' \state -> state { elaborationBinders = outer + , elaborationBinderDepth = outerDepth , elaborationStructures = outerStructures , elaborationContextualBinder = outerContextual } @@ -2770,6 +3478,18 @@ compileAtomicRelation left relation right = | otherwise -> Except.throwError (ExactUnsupportedDeclarationBody location) + Just (FixedIntrinsic Member) + | null parameters -> do + left' <- compileExpressionAsSet leftExpression + right' <- compileExpressionAsSet rightExpression + compileMembership + location Raw.Positive left' right' + Just (FixedNegatedIntrinsic Member) + | null parameters -> do + left' <- compileExpressionAsSet leftExpression + right' <- compileExpressionAsSet rightExpression + compileMembership + location Raw.Negative left' right' Just (FixedIntrinsic intrinsic) -> do compiled <- traverse compileExpression (parameters <> [leftExpression, rightExpression]) @@ -2827,10 +3547,7 @@ compileRelationExpression location expression left right = do (SemanticExpressionFunction (Raw.mixfixPattern Raw.PairSymbol)) [left, right] - pure - (CApp - (CApp (CIntrinsic Member) pair) - relation) + compileMembership location Raw.Positive pair relation compileRelationChain :: Raw.Chain @@ -2884,14 +3601,8 @@ applyResolvedPredicate -> SemanticGlobalKey -> [CanonicalTerm ObjectId] -> Elaborate (CanonicalTerm ObjectId) -applyResolvedPredicate location key arguments = do - (term, actual) <- - applyResolvedTyped - location key ((\argument -> (argument, TySet)) <$> arguments) - unless (actual == TyProp) - (Except.throwError - (ExactFormulaExpectedProposition location actual)) - pure term +applyResolvedPredicate location key = + applyResolvedPredicateChoice location (key :| []) applyResolvedPredicateChoice :: Location @@ -2899,28 +3610,41 @@ applyResolvedPredicateChoice -> [CanonicalTerm ObjectId] -> Elaborate (CanonicalTerm ObjectId) applyResolvedPredicateChoice location keys arguments = do - visible <- for (toList keys) \key -> do - found <- - State.lift - (Except.lift - (Declaration.resolveVisibleGlobalLowering key)) - pure ((\target -> (key, target)) <$> found) - case catMaybes visible of - [(key, _target)] -> do - (term, actual) <- - applyResolvedTyped - location key - ((\argument -> (argument, TySet)) <$> arguments) - unless (actual == TyProp) - (Except.throwError - (ExactFormulaExpectedProposition location actual)) - pure term - [] -> - Except.throwError - (ExactGlobalNotVisible location (NonEmpty.head keys)) - _ -> - impossible - "one adjective surface resolves to several exact globals" + case firstFixedMeaning (toList keys) of + Just meaning -> + maybe + (impossible + "a fixed equality predicate has an invalid source arity") + pure + (lowerFixedEqualityPredicate meaning arguments) + Nothing -> do + visible <- for (toList keys) \key -> do + found <- + State.lift + (Except.lift + (Declaration.resolveVisibleGlobalLowering key)) + pure ((\target -> (key, target)) <$> found) + case catMaybes visible of + [(key, _target)] -> do + (term, actual) <- + applyResolvedTyped + location key + ((\argument -> (argument, TySet)) <$> arguments) + unless (actual == TyProp) + (Except.throwError + (ExactFormulaExpectedProposition location actual)) + pure term + [] -> + Except.throwError + (ExactGlobalNotVisible location (NonEmpty.head keys)) + _ -> + impossible + "one adjective surface resolves to several exact globals" + where + firstFixedMeaning = + foldr + (\key found -> fixedSemanticMeaning key <|> found) + Nothing applyResolvedTyped :: Location @@ -3171,7 +3895,7 @@ encodePreparedSyntax putCoreTypeCache coreType case body of OpaqueBody -> putCacheTag 0x00 - TransparentBody canonical -> do + TransparentBody canonical _construction -> do putCacheTag 0x01 putCanonicalTermCache putObjectIdCache canonical ContextualTransparentBody requirements canonical -> do diff --git a/source/Checking/Exact/Inductive.hs b/source/Checking/Exact/Inductive.hs index 6764ec8..74208fc 100644 --- a/source/Checking/Exact/Inductive.hs +++ b/source/Checking/Exact/Inductive.hs @@ -63,6 +63,7 @@ data CheckedExactInductiveAuthorization = !ObjectId !(Typed.PreparedTypedInductive ObjectId) ![SemanticFactOccurrenceFingerprint] + ![(Location, Declaration.PreparedVampireObligation Void ())] preparedExactInductiveCarrierId :: PreparedExactInductive @@ -116,7 +117,9 @@ data ExactInductiveError | ExactInductiveResultShape !Location | ExactInductiveResultMentionsCarrier !Location | ExactInductiveRecursiveTermMentionsCarrier !Location - | ExactInductiveNestedRecursion !Location + | ExactInductiveRecursiveCarrierWrongArguments !Location + | ExactInductiveRecursiveCarrierOutsideMembership !Location + | ExactInductiveUnsupportedRecursiveCarrierContext !Location | ExactInductiveFixedSemanticCollision !Location !SemanticGlobalKey | ExactInductiveGlobalAlreadyVisible !Location !SemanticGlobalKey | ExactInductiveGlobalNotVisible !Location !Internal.Symbol @@ -143,7 +146,9 @@ exactInductiveErrorLocation = \case ExactInductiveResultShape location -> location ExactInductiveResultMentionsCarrier location -> location ExactInductiveRecursiveTermMentionsCarrier location -> location - ExactInductiveNestedRecursion location -> location + ExactInductiveRecursiveCarrierWrongArguments location -> location + ExactInductiveRecursiveCarrierOutsideMembership location -> location + ExactInductiveUnsupportedRecursiveCarrierContext location -> location ExactInductiveFixedSemanticCollision location _key -> location ExactInductiveGlobalAlreadyVisible location _key -> location ExactInductiveGlobalNotVisible location _symbol -> location @@ -182,8 +187,12 @@ renderExactInductiveError failure = "an inductive result term must not mention its carrier" ExactInductiveRecursiveTermMentionsCarrier{} -> "a recursive occurrence must be in the carrier of a membership premise" - ExactInductiveNestedRecursion{} -> - "nested inductive recursion is not supported by the typed checker" + ExactInductiveRecursiveCarrierWrongArguments{} -> + "the inductive carrier occurs with arguments other than its declared parameters" + ExactInductiveRecursiveCarrierOutsideMembership{} -> + "an inductive carrier occurrence must be in the set operand of a membership premise" + ExactInductiveUnsupportedRecursiveCarrierContext{} -> + "this recursive carrier context is outside the supported first-order set-term fragment" ExactInductiveFixedSemanticCollision _location key -> "the inductive carrier collides with fixed semantics for " <> shown key @@ -448,18 +457,28 @@ normalizeCondition carrier parameters formula Left (ExactInductiveRecursiveTermMentionsCarrier (termLocation recursiveTerm)) - | matchesCarrier carrier parameters recursiveCarrier -> + | otherwise -> do + context <- + first recursiveCarrierContextError + (Typed.prepareRecursiveCarrierContext + carrier parameters recursiveCarrier) Right - (Typed.DirectRecursiveCondition recursiveTerm) - | otherwise -> - Left - (ExactInductiveNestedRecursion - (termLocation recursiveCarrier)) + (Typed.DirectRecursiveCondition + recursiveTerm context) _ -> Left - (ExactInductiveNestedRecursion + (ExactInductiveRecursiveCarrierOutsideMembership (termLocation formula)) +recursiveCarrierContextError + :: Typed.RecursiveCarrierContextError + -> ExactInductiveError +recursiveCarrierContextError = \case + Typed.RecursiveCarrierWrongArguments location -> + ExactInductiveRecursiveCarrierWrongArguments location + Typed.RecursiveCarrierUnsupportedContext location -> + ExactInductiveUnsupportedRecursiveCarrierContext location + matchesCarrier :: Internal.FunctionSymbol -> [Internal.VarSymbol] @@ -543,8 +562,9 @@ directSymbols direct = conditionSymbols = \case Typed.DirectSideCondition formula -> Internal.mentionedSymbols formula - Typed.DirectRecursiveCondition term -> + Typed.DirectRecursiveCondition term context -> Internal.mentionedSymbols term + <> Typed.recursiveCarrierContextSymbols context lowerPreparedExactInductive :: PreparedExactInductive @@ -558,34 +578,107 @@ lowerPreparedExactInductive _location key identity asserted alias syntax typed guards) = do let facts = Typed.typedInductiveFacts typed + monotonicities = + Vector.toList + (Typed.typedInductiveMonotonicities typed) objects = maybeToList asserted definition <- Declaration.prepareDefinitionEquationSpecLowering objects identity alias + preparedMonotonicities <- + traverse + (\monotonicity -> Except.runExceptT do + let factLocation = + Typed.typedInductiveMonotonicityLocation + monotonicity + target = + Typed.typedInductiveMonotonicityTarget + monotonicity + spec <- + Except.lift + (Declaration.prepareFrozenCandidateSpecLowering + objects target SearchIneligible []) + >>= Except.liftEither + obligation <- + Except.lift + (Declaration.prepareScopedVampireObligationLowering + Vector.empty + (embedClosedCore [] target) + [] + [] + Declaration.VampireImplicitPremises) + >>= either + (Except.throwError + . Declaration.ProofObligationFailedAt + factLocation + . Declaration.CurrentCandidateVampirePreparationFailed) + pure + pure + ( Declaration.checkedCandidate + spec + (Declaration.checkedSourceProofPlanning + [ Declaration.checkedPlannedVampireRequest + factLocation obligation + ] + []) + , (factLocation, obligation) + )) + monotonicities preparedCandidates <- traverse - (\fact -> - fmap - (fmap - (\spec -> - Declaration.checkedCandidate spec - (Declaration.checkedKernelPlanning - (GuardedFoundationRules - (guardedRuleSet - (Typed.typedInductiveFactRules - fact))) - guards))) - (Declaration.prepareCandidateSpecLowering + (\fact -> do + prepared <- + Declaration.prepareCandidateSpecLowering objects (embedClosedCore [] (Typed.typedInductiveFactTarget fact)) SearchEligible [markerAlias - (Typed.typedInductiveFactMarker fact)])) + (Typed.typedInductiveFactMarker fact)] + let descriptor = + GuardedFoundationRules + (guardedRuleSet + (Typed.typedInductiveFactRules fact)) + planning + | null monotonicities = + Declaration.checkedKernelPlanning + descriptor guards + | otherwise = + Declaration.checkedKernelPlanningWithStaged + descriptor + guards + (if Typed.typedInductiveFactRequiresMonotonicities + fact + then + [ Declaration.plannedEarlierCandidate + 1 index + | (index, _target) <- + zip [0 ..] monotonicities + ] + else []) + pure + (fmap + (\spec -> + Declaration.checkedCandidate spec planning) + prepared)) facts pure do definitionSpec <- definition + monotonicityCandidates <- sequence preparedMonotonicities factCandidates <- sequence preparedCandidates + let stages + | null monotonicityCandidates = + [ Declaration.checkedCandidate definitionSpec + (Declaration.checkedDefinitionEquationPlanning identity) + :| toList factCandidates + ] + | otherwise = + [ Declaration.checkedCandidate definitionSpec + (Declaration.checkedDefinitionEquationPlanning identity) + :| [] + , NonEmpty.fromList (fst <$> monotonicityCandidates) + , factCandidates + ] pure (Declaration.checkedCompiledDeclaration syntax @@ -593,12 +686,10 @@ lowerPreparedExactInductive [] [semanticGlobalBinding key (GlobalReference identity)] [] - [ Declaration.checkedCandidate definitionSpec - (Declaration.checkedDefinitionEquationPlanning identity) - :| toList factCandidates - ] + stages (CheckedExactInductiveAuthorization - identity typed guards)) + identity typed guards + (snd <$> monotonicityCandidates))) where markerAlias (Raw.Marker name) = semanticName name @@ -608,8 +699,12 @@ authorizeCheckedExactInductive -> [NonEmpty Declaration.ReservedCandidate] -> Declaration.Declaration () authorizeCheckedExactInductive - (CheckedExactInductiveAuthorization identity typed guards) = \case + (CheckedExactInductiveAuthorization + identity typed guards monotonicityObligations) = \case [definitionCandidate :| candidates] -> do + unless (null monotonicityObligations) + (Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch 3 1)) Declaration.authorizeDefinitionEquationCandidate identity definitionCandidate let facts = Typed.typedInductiveFacts typed @@ -618,7 +713,7 @@ authorizeCheckedExactInductive | NonEmpty.length factCandidates == NonEmpty.length facts -> sequence_ (NonEmpty.zipWith - authorizeFact + (authorizeFact []) factCandidates facts) _ -> @@ -626,20 +721,60 @@ authorizeCheckedExactInductive (Declaration.CheckedAuthorizationCandidateShapeMismatch (1 + NonEmpty.length facts) (1 + length candidates)) + [ definitionCandidate :| [] + , monotonicityCandidates + , factCandidates + ] + | NonEmpty.length monotonicityCandidates + == length monotonicityObligations + , NonEmpty.length factCandidates + == NonEmpty.length (Typed.typedInductiveFacts typed) -> do + obligations <- + maybe + (Declaration.failDeclaration + (Declaration.CheckedAuthorizationCandidateShapeMismatch + 1 0)) + pure + (NonEmpty.nonEmpty monotonicityObligations) + Declaration.authorizeDefinitionEquationCandidate + identity definitionCandidate + Declaration.authorizeVampireCandidateBatch + (NonEmpty.zipWith + (\candidate (factLocation, obligation) -> + (factLocation, candidate, pure obligation)) + monotonicityCandidates + obligations) + sequence_ + (NonEmpty.zipWith + (\candidate fact -> + authorizeFact + (if Typed.typedInductiveFactRequiresMonotonicities + fact + then NonEmpty.toList monotonicityCandidates + else []) + candidate + fact) + factCandidates + (Typed.typedInductiveFacts typed)) stages -> Declaration.failDeclaration (Declaration.CheckedAuthorizationCandidateShapeMismatch - 1 (length stages)) + (if null monotonicityObligations then 1 else 3) + (length stages)) where - authorizeFact candidate fact = + authorizeFact monotonicityCandidates candidate fact = Declaration.authorizeKernelConstructionCandidate (GuardedFoundationRules (guardedRuleSet (Typed.typedInductiveFactRules fact))) candidate do traverse_ Declaration.useAuthorizedFact guards + traverse_ + Declaration.useStagedCandidate + monotonicityCandidates pure (Typed.typedInductiveFactDerivation fact) + encodePreparedInductive :: SemanticGlobalKey -> SemanticName @@ -654,10 +789,21 @@ encodePreparedInductive key alias typed = putCanonicalTermCache putObjectIdCache (frozenCoreTerm (Typed.typedInductiveCarrierBody typed)) + putCacheList putFrozenTerm + (Vector.toList + (Typed.typedInductiveContextInventory typed)) + putCacheList + (putFrozenTerm + . Typed.typedInductiveMonotonicityTarget) + (Vector.toList + (Typed.typedInductiveMonotonicities typed)) putCacheText (semanticNameText alias) putCacheList putFact (toList (Typed.typedInductiveFacts typed)) where + putFrozenTerm = + putCanonicalTermCache putObjectIdCache . frozenCoreTerm + putFact fact = do let Raw.Marker marker = Typed.typedInductiveFactMarker fact diff --git a/source/Checking/Exact/Proof.hs b/source/Checking/Exact/Proof.hs index 40911b0..92ff500 100644 --- a/source/Checking/Exact/Proof.hs +++ b/source/Checking/Exact/Proof.hs @@ -35,6 +35,8 @@ import Checking.Exact qualified as Exact import Checking.Foundation import Checking.Identity import Checking.Kernel.Derivation (foundationFactDerivation) +import Checking.Kernel.Proof qualified as KernelProof +import Checking.SetConstruction import Checking.Semantic import Felix.Cache.Codec import Report.Location @@ -47,28 +49,34 @@ import Control.Monad.State.Strict (StateT) import Control.Monad.State.Strict qualified as State import Data.ByteString (ByteString) import Data.List.NonEmpty qualified as NonEmpty +import Data.Map.Strict qualified as Map import Data.Set qualified as Set import Data.Text qualified as Text import Data.Vector (Vector) +import Data.Vector qualified as Vector import Numeric.Natural (Natural) data ExactProofError = ExactProofUnsupportedClaim !Location | ExactProofUnsupportedStep !Location - | ExactProofBoundedFixNotSupported !Location - | ExactProofBoundedTakeNotSupported !Location | ExactProofSetInductionVariableRequired !Location | ExactProofSetInductionVariableNotActive !Location !Raw.VarSymbol - | ExactProofSetInductionNotOutermost !Location + | ExactProofSetInductionFocusAmbiguous !Location + | ExactProofSetInductionActiveBinderIneligible + !Location !Raw.VarSymbol + | ExactProofSetInductionBinderConflict + !Location !Raw.VarSymbol | ExactProofSetInductionGoalMismatch !Location | ExactProofSetExtensionalityGoalMismatch !Location | ExactProofSetExtensionalityDirectionsUnavailable !Location | ExactProofExpectedUniversalGoal !Location | ExactProofExpectedImplicationGoal !Location | ExactProofGoalStatementMismatch !Location - | ExactProofContradictionGoalMismatch !Location + | ExactProofEmptyCaseSplit !Location + | ExactProofStructuralCompositionFailed + !Location !KernelProof.KernelProofBuildError | ExactProofLocalFunctionBinderMismatch !Location | ExactProofLocalFunctionNameConflict !Location | ExactProofUnknownReference !Location !Raw.Marker @@ -86,19 +94,22 @@ exactProofErrorLocation :: ExactProofError -> Location exactProofErrorLocation = \case ExactProofUnsupportedClaim location -> location ExactProofUnsupportedStep location -> location - ExactProofBoundedFixNotSupported location -> location - ExactProofBoundedTakeNotSupported location -> location ExactProofSetInductionVariableRequired location -> location ExactProofSetInductionVariableNotActive location _variable -> location - ExactProofSetInductionNotOutermost location -> location + ExactProofSetInductionFocusAmbiguous location -> location + ExactProofSetInductionActiveBinderIneligible location _variable -> + location + ExactProofSetInductionBinderConflict location _variable -> + location ExactProofSetInductionGoalMismatch location -> location ExactProofSetExtensionalityGoalMismatch location -> location ExactProofSetExtensionalityDirectionsUnavailable location -> location ExactProofExpectedUniversalGoal location -> location ExactProofExpectedImplicationGoal location -> location ExactProofGoalStatementMismatch location -> location - ExactProofContradictionGoalMismatch location -> location + ExactProofEmptyCaseSplit location -> location + ExactProofStructuralCompositionFailed location _failure -> location ExactProofLocalFunctionBinderMismatch location -> location ExactProofLocalFunctionNameConflict location -> location ExactProofUnknownReference location _marker -> location @@ -115,17 +126,20 @@ renderExactProofError = \case at location <> "this claim is not yet supported by the typed checker" ExactProofUnsupportedStep location -> at location <> "this proof step is not yet supported by the typed checker" - ExactProofBoundedFixNotSupported location -> - at location <> "bounded proof binders are not yet supported" - ExactProofBoundedTakeNotSupported location -> - at location <> "bounded proof witnesses are not yet supported" ExactProofSetInductionVariableRequired location -> at location <> "exact set induction requires a named set variable" ExactProofSetInductionVariableNotActive location variable -> at location <> "the set-induction variable " <> shown variable - <> " is not an active exact binder" - ExactProofSetInductionNotOutermost location -> - at location <> "set induction must currently be outermost" + <> " is not an eligible exact focus" + ExactProofSetInductionFocusAmbiguous location -> + at location + <> "set induction without an explicit variable has no unique focus" + ExactProofSetInductionActiveBinderIneligible location variable -> + at location <> "the active binder " <> shown variable + <> " is not an eligible set-induction focus" + ExactProofSetInductionBinderConflict location variable -> + at location <> "the leading set-induction binder " <> shown variable + <> " conflicts with an active exact binder" ExactProofSetInductionGoalMismatch location -> at location <> "the set-induction variable does not belong to this goal" ExactProofSetExtensionalityGoalMismatch location -> @@ -139,8 +153,10 @@ renderExactProofError = \case at location <> "this assume step requires an implication goal" ExactProofGoalStatementMismatch location -> at location <> "the proof step does not match the current goal" - ExactProofContradictionGoalMismatch location -> - at location <> "contradiction requires falsum as the current goal" + ExactProofEmptyCaseSplit location -> + at location <> "case analysis requires at least one case" + ExactProofStructuralCompositionFailed location failure -> + at location <> "invalid structural proof composition: " <> shown failure ExactProofLocalFunctionBinderMismatch location -> at location <> "the function argument must match its domain binder" ExactProofLocalFunctionNameConflict location -> @@ -167,6 +183,8 @@ data ExactLocalOrigin = ExactAssumption | ExactDerivedClaim | ExactLocalDefinition + | ExactLocalConstructionExtensional + | ExactLocalConstructionEquation deriving stock (Show, Eq, Ord) data PreparedLocal = PreparedLocal @@ -193,6 +211,75 @@ data PreparedDischarge !Location !(ScopedCheckedCore ObjectId) +data PreparedCalculationLink = PreparedCalculationLink + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + +-- The private constructor stores every destination with the discharge derived +-- from its immediately preceding endpoint. Planning and admission can +-- therefore traverse one immutable sequence without re-associating shapes. +data PreparedCalculation = PreparedCheckedCalculation + !CoreType + ![Exact.ExactLocalId] + !(Maybe (ScopedCheckedCore ObjectId)) + !(ScopedCheckedCore ObjectId) + !(NonEmpty PreparedCalculationLink) + !(ScopedCheckedCore ObjectId) + +data PreparedSinceEvidence + = PreparedSinceExisting !PreparedLocal + | PreparedSinceDischarged !PreparedDischarge !PreparedLocal + +data PreparedCase = PreparedCase + !(ScopedCheckedCore ObjectId) + !PreparedProof + +data PreparedCaseAnalysis = PreparedCaseAnalysis + !(ScopedCheckedCore ObjectId) + !(NonEmpty PreparedCase) + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + +data InitialSetInductionFocus = InitialSetInductionFocus + !Raw.VarSymbol + !Exact.ExactLocalId + !Natural + +data InitialSetInductionView = InitialSetInductionView + ![InitialSetInductionFocus] + !(Vector (Exact.ExactLocalId, CoreType)) + !(ScopedCheckedCore ObjectId) + ![ScopedCheckedCore ObjectId] + !(ScopedCheckedCore ObjectId) + !(Maybe Raw.VarSymbol) + +data SetInductionBoundary + = InitialClaimInduction !InitialSetInductionView + -- A direct source-statement goal may retain only its leading binder name. + -- Recursive proof transformations deliberately discard this hint. + | SourceStatementInduction !(Maybe Raw.VarSymbol) + | RecursiveProofInduction + +data SelectedSetInductionFocus + = SelectedInitialSetInduction !InitialSetInductionFocus + | SelectedLeadingSetInduction !(Maybe Raw.VarSymbol) + +data PreparedSetInductionFocus + = PreparedInitialSetInductionFocus + !Exact.ExactLocalId + !Natural + | PreparedLeadingSetInductionFocus + !Exact.ExactLocalId + +data PreparedSetInduction = PreparedCheckedSetInduction + !PreparedSetInductionFocus + !(ScopedCheckedCore ObjectId) + ![ScopedCheckedCore ObjectId] + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedProof + data PreparedProof = PreparedImplicitAuto !PreparedDischarge | PreparedQed !PreparedDischarge @@ -208,10 +295,23 @@ data PreparedProof !(ScopedCheckedCore ObjectId) !PreparedDischarge !PreparedProof - | PreparedSetInduction + | PreparedSetInduction !PreparedSetInduction + | PreparedHave !(ScopedCheckedCore ObjectId) !PreparedDischarge - | PreparedHave + !PreparedProof + | PreparedSuffices + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedDischarge + !PreparedProof + | PreparedCalculate + !PreparedCalculation + !PreparedProof + | PreparedSince + !(ScopedCheckedCore ObjectId) + !PreparedSinceEvidence !(ScopedCheckedCore ObjectId) !PreparedDischarge !PreparedProof @@ -222,14 +322,29 @@ data PreparedProof | PreparedDefine !Exact.ExactLocalId !(ScopedCheckedCore ObjectId) + !(NonEmpty (ScopedCheckedCore ObjectId)) + !PreparedProof + | PreparedDefineRelational + !Exact.ExactLocalId !(ScopedCheckedCore ObjectId) + !PreparedDischarge + !(NonEmpty (ScopedCheckedCore ObjectId)) !PreparedProof | PreparedDefineFunction !Exact.ExactLocalId !(ScopedCheckedCore ObjectId) !(ScopedCheckedCore ObjectId) !PreparedProof - | PreparedContradiction !PreparedDischarge + | PreparedByCase !PreparedCaseAnalysis + | PreparedByContradiction + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedProof + | PreparedContradiction + !(ScopedCheckedCore ObjectId) + !(ScopedCheckedCore ObjectId) + !PreparedDischarge data PreparedExactProof = PreparedExactProof !Location @@ -302,14 +417,19 @@ prepareExactProof block explicitProof = context openedGoal (Exact.preparedExactClaimAntecedentCount envelope) + initialInduction <- + prepareInitialSetInductionView + statement + context + (Exact.preparedExactClaimVariables envelope) + identities + antecedents + bodyGoal bodyProof <- case explicitProof of Nothing -> PreparedImplicitAuto - <$> prepareDischargeWith - DirectDischarge - [] - Nothing + <$> prepareDischarge location context locals @@ -320,7 +440,7 @@ prepareExactProof block explicitProof = location context locals - (Just antecedents) + (InitialClaimInduction initialInduction) bodyGoal sourceProof let withAssumptions = @@ -464,16 +584,96 @@ openEnvelopeAntecedents context initialGoal initialCount = conclusion (remaining - 1) +prepareInitialSetInductionView + :: Raw.Stmt + -> Exact.ExactBinderContext + -> [Raw.VarSymbol] + -> [Exact.ExactLocalId] + -> [ScopedCheckedCore ObjectId] + -> ScopedCheckedCore ObjectId + -> Prepare InitialSetInductionView +prepareInitialSetInductionView + statement context variables identities antecedents bodyGoal = do + unless (length variables == length identities) + (impossible + "opened claim binders lost their source identity association") + foci <- traverse checkedFocus (zip variables identities) + let property = foldr implyChecked bodyGoal antecedents + support = Exact.exactBinderContextSupport context + unless + ( scopedCoreContext property + == (snd <$> Vector.toList support) + ) + (impossible + "initial set-induction property changed its checked context") + pure + (InitialSetInductionView + foci support property antecedents bodyGoal + (claimLeadingUniversalName statement)) + where + checkedFocus (variable, identity) = do + index <- + maybe + (impossible + "an opened claim binder is absent from its exact context") + pure + (Exact.exactBinderContextIndex variable context) + case Exact.exactBinderContextSupport context + Vector.!? (fromIntegral index) of + Just (actualIdentity, TySet) + | actualIdentity == identity -> + pure + (InitialSetInductionFocus + variable identity index) + _ -> + impossible + "an initial set-induction focus changed identity or type" + + implyChecked antecedent conclusion = + fromMaybe + (impossible + "an exact claim antecedent changed context") + (implyScopedCore antecedent conclusion) + +claimLeadingUniversalName :: Raw.Stmt -> Maybe Raw.VarSymbol +claimLeadingUniversalName = \case + Raw.StmtFormula + (Raw.FormulaQuantified _location Raw.Universally + (variable :| _rest) _bound _formula) -> + Just variable + Raw.SymbolicForall _location (variable :| _rest) + _bound _suchThat _statement -> + Just variable + Raw.StmtQuantPhrase + _location + (Raw.QuantPhrase Raw.Universally + (Raw.NounPhrase _left _noun variables _right _suchThat)) + _statement -> + listToMaybe variables + Raw.StmtVerbPhrase + (Raw.TermQuantified Raw.Universally _location + (Raw.NounPhrase _left _noun variable _right _suchThat) + :| []) + _verb -> + variable + Raw.StmtNoun + (Raw.TermQuantified Raw.Universally _location + (Raw.NounPhrase _left _noun variable _right _suchThat) + :| []) + _nounPhrase -> + variable + _statement -> + Nothing + prepareProof :: Location -> Exact.ExactBinderContext -> [PreparedLocal] - -- Only the initial proof carries set-induction antecedents. - -> Maybe [ScopedCheckedCore ObjectId] + -> SetInductionBoundary -> ScopedCheckedCore ObjectId -> Raw.Proof -> Prepare PreparedProof -prepareProof fallback context locals inductionAntecedents goal = \case +prepareProof fallback context locals inductionBoundary goal = \case Raw.Omitted location -> pure (PreparedOmitted location goal) Raw.Qed maybeLocation justification -> @@ -485,130 +685,166 @@ prepareProof fallback context locals inductionAntecedents goal = \case goal justification Raw.FixSymbolic location variables bound continuation -> do - unless (bound == Raw.Unbounded) - (throwProof - (ExactProofBoundedFixNotSupported location)) (context', goal', identities) <- openFixedVariables context goal variables - PreparedFix identities - <$> prepareProof - fallback - context' - locals - Nothing - goal' - continuation + case bound of + Raw.Unbounded -> + PreparedFix identities + <$> prepareProof + fallback + context' + locals + RecursiveProofInduction + goal' + continuation + _ -> do + constraint <- + prepareSymbolicBoundConstraints + context' variables bound + prepareGuardedFix + fallback location context' locals goal' + identities constraint continuation + Raw.FixSuchThat location variables statement continuation -> do + (context', goal', identities) <- + openFixedVariables context goal variables + constraint <- + Exact.preparedExactPropositionCore + <$> prepareStatement context' statement + prepareGuardedFix + fallback location context' locals goal' + identities constraint continuation Raw.Assume location statement continuation -> do - (antecedent, conclusion) <- + supplied <- prepareStatement context statement + when (isNothing (openScopedImplication goal)) + (throwProof (ExactProofExpectedImplicationGoal location)) + (assumption, conclusion) <- maybe - (throwProof - (ExactProofExpectedImplicationGoal location)) + (throwProof (ExactProofGoalStatementMismatch location)) pure - (openScopedImplication goal) - supplied <- prepareStatement context statement - unless - (Exact.preparedExactPropositionCore supplied - == antecedent) - (throwProof - (ExactProofGoalStatementMismatch location)) - local <- allocateLocal ExactAssumption context antecedent - PreparedAssume antecedent + (openScopedAssumption + (Exact.preparedExactPropositionCore supplied) + goal) + local <- allocateLocal ExactAssumption context assumption + PreparedAssume assumption <$> prepareProof fallback context (locals <> [local]) - Nothing + RecursiveProofInduction conclusion continuation Raw.TakeVar location variables bound statement justification continuation -> do - unless (bound == Raw.Unbounded) - (throwProof - (ExactProofBoundedTakeNotSupported location)) - identities <- - traverse (const allocateLocalIdentity) variables - context' <- - either - (throwProof . ExactProofElaborationFailed) - pure - (Exact.extendExactBinderContext - (NonEmpty.zip identities variables) - context) - witness <- + prepareSymbolicTake + fallback location context locals goal variables bound statement + justification continuation + Raw.TakeNoun location nounPhrase justification continuation -> + prepareNounTake + fallback location context locals goal nounPhrase + justification continuation + Raw.BySetInduction location variable continuation -> + prepareSetInduction + fallback location context locals inductionBoundary goal + variable continuation + Raw.Have location Nothing + (Raw.SymbolicExists _existential variables bound statement) + justification continuation -> + prepareSymbolicTake + fallback location context locals goal variables bound statement + justification continuation + Raw.Have location Nothing statement justification continuation -> do + claim <- Exact.preparedExactPropositionCore - <$> prepareStatement context' statement - let witnessCount = length (toList variables) - existence = closeTakenWitnesses witnessCount witness - goal' = weakenForTakenWitnesses witnessCount goal + <$> prepareStatement context statement discharge <- prepareDischarge - location context locals existence justification - local <- allocateLocal ExactAssumption context' witness - PreparedTake (toList identities) witness discharge + location context locals claim justification + local <- allocateLocal ExactDerivedClaim context claim + PreparedHave claim discharge <$> prepareProof fallback - context' + context (locals <> [local]) - Nothing - goal' + RecursiveProofInduction + goal continuation - Raw.BySetInduction location variable continuation -> - case (inductionAntecedents, continuation) of - (Nothing, _proof) -> - throwProof - (ExactProofSetInductionNotOutermost location) - (Just antecedents, Raw.Qed maybeLocation justification) -> do - sourceVariable <- - case variable of - Just (Raw.TermExpr (Raw.ExprVar candidate)) -> - pure candidate - _ -> - throwProof - (ExactProofSetInductionVariableRequired - location) - selected <- - maybe - (throwProof - (ExactProofSetInductionVariableNotActive - location - sourceVariable)) - pure - (Exact.exactBinderContextIndex - sourceVariable context) - let property = - foldr implyChecked goal antecedents - hypothesis <- - maybe - (throwProof - (ExactProofSetInductionGoalMismatch - location)) - pure - (scopedSetInductionHypothesis selected property) - local <- allocateLocal ExactAssumption context hypothesis - PreparedSetInduction hypothesis - <$> prepareDischarge - (fromMaybe location maybeLocation) - context - (locals <> [local]) - goal - justification - (Just _antecedents, _proof) -> - throwProof (ExactProofUnsupportedStep location) - Raw.Have location since statement justification continuation -> do - when (isJust since) - (throwProof (ExactProofUnsupportedStep location)) + Raw.Have location (Just sinceStatement) + statement justification continuation -> do + sinceProposition <- + Exact.preparedExactPropositionCore + <$> prepareStatement context sinceStatement claim <- Exact.preparedExactPropositionCore <$> prepareStatement context statement + (evidence, sinceLocals) <- + case find (localMatches sinceProposition) locals of + Just existing -> + pure (PreparedSinceExisting existing, locals) + Nothing -> do + discharge <- + prepareDischarge + location + context + locals + sinceProposition + Raw.JustificationLocal + local <- + allocateLocal + ExactDerivedClaim context sinceProposition + pure + ( PreparedSinceDischarged discharge local + , locals <> [local] + ) + claimDischarge <- + prepareDischarge + location context sinceLocals claim justification + claimLocal <- + allocateLocal ExactDerivedClaim context claim + PreparedSince + sinceProposition evidence claim claimDischarge + <$> prepareProof + fallback + context + (sinceLocals <> [claimLocal]) + RecursiveProofInduction + goal + continuation + Raw.Suffices location statement justification continuation -> do + reduction <- + Exact.preparedExactPropositionCore + <$> prepareStatement context statement + implication <- + maybe + (impossible + "a checked suffices reduction changed lexical context") + pure + (implyScopedCore reduction goal) discharge <- prepareDischarge - location context locals claim justification - local <- allocateLocal ExactDerivedClaim context claim - PreparedHave claim discharge + location context locals implication justification + PreparedSuffices goal reduction implication discharge + <$> prepareProof + fallback + context + locals + (SourceStatementInduction + (claimLeadingUniversalName statement)) + reduction + continuation + Raw.Calc location quantifier calculation continuation -> do + prepared <- + prepareCalculation + location context locals quantifier calculation + local <- + allocateLocal + ExactDerivedClaim + context + (preparedCalculationResult prepared) + PreparedCalculate prepared <$> prepareProof fallback context (locals <> [local]) - Nothing + RecursiveProofInduction goal continuation Raw.Subclaim location statement subproof continuation -> do @@ -620,7 +856,8 @@ prepareProof fallback context locals inductionAntecedents goal = \case location context locals - Nothing + (SourceStatementInduction + (claimLeadingUniversalName statement)) claim subproof local <- allocateLocal ExactDerivedClaim context claim @@ -629,19 +866,17 @@ prepareProof fallback context locals inductionAntecedents goal = \case fallback context (locals <> [local]) - Nothing + RecursiveProofInduction goal continuation - Raw.Define _location variable expression continuation -> do - body <- - Exact.preparedExactSetExpressionCore - <$> ( liftDriver - (Exact.prepareExactSetExpression - context expression) - >>= either - (throwProof . ExactProofElaborationFailed) - pure - ) + Raw.Define location variable expression continuation -> do + preparedBody <- + liftDriver + (Exact.prepareExactSetExpression context expression) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + let body = Exact.preparedExactSetExpressionCore preparedBody identity <- allocateLocalIdentity context' <- either @@ -650,26 +885,77 @@ prepareProof fallback context locals inductionAntecedents goal = \case (Exact.extendExactBinderContext ((identity, variable) :| []) context) - separationCharacteristic <- - liftDriver - (Declaration.currentFoundationAxiomLowering - SeparationCharacteristic) - definition <- - maybe - (impossible - "an exact set expression did not form a local definition") - pure - (scopedSetDefinition separationCharacteristic body) - local <- - allocateLocal ExactLocalDefinition context' definition - PreparedDefine identity body definition - <$> prepareProof - fallback - context' - (locals <> [local]) - Nothing - (weakenCheckedScopedCore TySet goal) - continuation + case Exact.preparedExactSetExpressionConstruction preparedBody of + Nothing -> do + separationCharacteristic <- + liftDriver + (Declaration.currentFoundationAxiomLowering + SeparationCharacteristic) + definition <- + maybe + (impossible + "an exact set expression did not form a local definition") + pure + (scopedSetDefinition separationCharacteristic body) + local <- + allocateLocal ExactLocalDefinition context' definition + PreparedDefine identity body (definition :| []) + <$> prepareProof + fallback context' (locals <> [local]) + RecursiveProofInduction + (weakenCheckedScopedCore TySet goal) + continuation + Just (Exact.PreparedUnconditionalSetConstruction construction) -> do + characteristics <- prepareConstructionFoundation + (extensional, equation) <- + maybe + (impossible + "a checked named construction has no definition views") + pure + (namedSetConstructionLocalViews + characteristics construction) + extensionalLocal <- + allocateLocal + ExactLocalConstructionExtensional context' extensional + equationLocal <- + allocateLocal + ExactLocalConstructionEquation context' equation + PreparedDefine identity body (extensional :| [equation]) + <$> prepareProof + fallback context' + (locals <> [extensionalLocal, equationLocal]) + RecursiveProofInduction + (weakenCheckedScopedCore TySet goal) + continuation + Just (Exact.PreparedRelationalSetConstruction construction) -> do + characteristics <- prepareConstructionFoundation + let functionality = + relationalSetConstructionFunctionality construction + discharge <- + prepareDischarge + location context locals functionality + Raw.JustificationEmpty + (extensional, equation) <- + maybe + (impossible + "a checked relational construction has no admitted definition views") + pure + (relationalSetConstructionLocalViews + characteristics construction functionality) + extensionalLocal <- + allocateLocal + ExactLocalConstructionExtensional context' extensional + equationLocal <- + allocateLocal + ExactLocalConstructionEquation context' equation + PreparedDefineRelational + identity body discharge (extensional :| [equation]) + <$> prepareProof + fallback context' + (locals <> [extensionalLocal, equationLocal]) + RecursiveProofInduction + (weakenCheckedScopedCore TySet goal) + continuation Raw.DefineFunction location function argument value bound domain continuation -> do unless (argument == bound) @@ -726,35 +1012,734 @@ prepareProof fallback context locals inductionAntecedents goal = \case fallback functionContext (locals <> [local]) - Nothing + RecursiveProofInduction (weakenCheckedScopedCore TySet goal) continuation + Raw.ByCase location sourceCases -> + prepareByCase + location context locals goal sourceCases + Raw.ByContradiction location continuation -> do + let falsum = falsumScopedCore (scopedCoreContext goal) + negation <- + maybe + (structuralFailure + location + "proof by contradiction requires a proposition goal") + pure + (negateScopedCore goal) + local <- allocateLocal ExactAssumption context negation + prepared <- + prepareProof + location + context + (locals <> [local]) + RecursiveProofInduction + falsum + continuation + validateStructuralComposition + location [goal, negation, falsum] + (\foundation globalType -> + KernelProof.validateDoubleNegationComposition + foundation globalType goal negation falsum) + pure + (PreparedByContradiction + goal negation falsum prepared) Raw.Contradiction location justification -> do - unless - ( scopedCoreType goal == TyProp - && scopedCoreTerm goal == CFalsum - ) - (throwProof - (ExactProofContradictionGoalMismatch location)) - PreparedContradiction - <$> prepareDischargeWith - IndirectContradictionDischarge - [] - Nothing + let falsum = falsumScopedCore (scopedCoreContext goal) + discharge <- + prepareDischarge location context locals - goal + falsum justification + validateStructuralComposition + location [goal, falsum] + (\foundation globalType -> + KernelProof.validateFalsumEliminationComposition + foundation globalType goal falsum) + pure (PreparedContradiction goal falsum discharge) proof -> throwProof (ExactProofUnsupportedStep (proofLocation fallback proof)) where - implyChecked antecedent conclusion = - fromMaybe - (impossible "an exact claim antecedent changed context") - (implyScopedCore antecedent conclusion) + localMatches proposition + (PreparedLocal _ordinal _origin _support local) = + local == proposition + +prepareSetInduction + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> SetInductionBoundary + -> ScopedCheckedCore ObjectId + -> Maybe Raw.Term + -> Raw.Proof + -> Prepare PreparedProof +prepareSetInduction + fallback location context locals boundary goal sourceFocus + continuation = do + selected <- + selectSetInductionFocus + location context boundary goal sourceFocus + case selected of + SelectedInitialSetInduction + (InitialSetInductionFocus _variable identity index) -> do + (foci, expectedSupport, property, antecedents, childTarget) <- + case boundary of + InitialClaimInduction + (InitialSetInductionView + foundFoci support foundProperty + foundAntecedents foundTarget _leadingName) -> + pure + ( foundFoci + , support + , foundProperty + , foundAntecedents + , foundTarget + ) + RecursiveProofInduction -> + impossible + "an initial induction focus escaped its claim boundary" + SourceStatementInduction _leadingName -> + impossible + "an initial induction focus escaped its claim boundary" + unless + ( Exact.exactBinderContextSupport context == expectedSupport + && goal == childTarget + && any (sameInitialFocus identity index) foci + ) + (throwProof + (ExactProofSetInductionGoalMismatch location)) + PreparedSetInduction + <$> prepareCheckedSetInduction + fallback location context locals + (PreparedInitialSetInductionFocus identity index) + index property antecedents childTarget continuation + SelectedLeadingSetInduction sourceName -> do + (binderType, property) <- + maybe + (throwProof + (ExactProofSetInductionGoalMismatch location)) + pure + (openScopedForall goal) + unless (binderType == TySet) + (throwProof + (ExactProofSetInductionGoalMismatch location)) + identity <- allocateLocalIdentity + extendedContext <- + either + (throwProof . ExactProofElaborationFailed) + pure + (case sourceName of + Just variable -> + Exact.extendExactBinderContext + ((identity, variable) :| []) + context + Nothing -> + Exact.extendExactAnonymousBinderContext + identity context) + let expectedResult = weakenCheckedScopedCore TySet goal + prepared <- prepareCheckedSetInduction + fallback location extendedContext locals + (PreparedLeadingSetInductionFocus identity) + 0 property [] property continuation + unless + (preparedSetInductionResult prepared == expectedResult) + (throwProof + (ExactProofSetInductionGoalMismatch location)) + pure (PreparedSetInduction prepared) + where + sameInitialFocus expectedIdentity expectedIndex + (InitialSetInductionFocus _variable identity index) = + identity == expectedIdentity && index == expectedIndex + +prepareCheckedSetInduction + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> PreparedSetInductionFocus + -> Natural + -> ScopedCheckedCore ObjectId + -> [ScopedCheckedCore ObjectId] + -> ScopedCheckedCore ObjectId + -> Raw.Proof + -> Prepare PreparedSetInduction +prepareCheckedSetInduction + fallback location context locals focus selected property antecedents + childTarget continuation = do + (_predicate, hypothesis, _step, result) <- + maybe + (throwProof + (ExactProofSetInductionGoalMismatch location)) + pure + (scopedSetInductionInstance selected property) + validateStructuralComposition + location + (property : hypothesis : result : childTarget : antecedents) + (\foundation globalType -> + KernelProof.validateSetInductionComposition + foundation globalType selected property antecedents + childTarget hypothesis result) + local <- allocateLocal ExactAssumption context hypothesis + child <- + prepareProof + fallback + context + (locals <> [local]) + RecursiveProofInduction + childTarget + continuation + pure + (PreparedCheckedSetInduction + focus property antecedents childTarget hypothesis result child) + +preparedSetInductionResult + :: PreparedSetInduction + -> ScopedCheckedCore ObjectId +preparedSetInductionResult + (PreparedCheckedSetInduction + _focus _property _antecedents _target _hypothesis result _child) = + result + +selectSetInductionFocus + :: Location + -> Exact.ExactBinderContext + -> SetInductionBoundary + -> ScopedCheckedCore ObjectId + -> Maybe Raw.Term + -> Prepare SelectedSetInductionFocus +selectSetInductionFocus location context boundary goal sourceFocus = do + explicit <- traverse simpleVariable sourceFocus + let (initialFoci, retainedLeadingName) = + case boundary of + InitialClaimInduction + (InitialSetInductionView + foci _support _property _antecedents _target + leadingName) -> + (foci, leadingName) + SourceStatementInduction leadingName -> + ([], leadingName) + RecursiveProofInduction -> + ([], Nothing) + leadingAvailable = + case openScopedForall goal of + Just (TySet, _body) -> True + _ -> False + case explicit of + Just variable -> + case find (initialNamed variable) initialFoci of + Just focus -> + pure (SelectedInitialSetInduction focus) + Nothing + | leadingAvailable + , isJust + (Exact.exactBinderContextIndex variable context) -> + throwProof + (ExactProofSetInductionBinderConflict + location variable) + | leadingAvailable -> + pure + (SelectedLeadingSetInduction + (Just variable)) + | isJust + (Exact.exactBinderContextIndex variable context) -> + throwProof + (ExactProofSetInductionActiveBinderIneligible + location variable) + | otherwise -> + throwProof + (ExactProofSetInductionVariableNotActive + location variable) + Nothing -> + case + ( (SelectedInitialSetInduction <$> initialFoci) + <> [ SelectedLeadingSetInduction retainedLeadingName + | leadingAvailable + ] + ) of + [only] -> pure only + _ -> + throwProof + (ExactProofSetInductionFocusAmbiguous location) + where + simpleVariable = \case + Raw.TermExpr (Raw.ExprVar variable) -> + pure variable + _term -> + throwProof + (ExactProofSetInductionVariableRequired location) + + initialNamed variable + (InitialSetInductionFocus candidate _identity _index) = + candidate == variable + +prepareByCase + :: Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> [Raw.Case] + -> Prepare PreparedProof +prepareByCase location context locals goal sourceCases = do + cases <- + maybe + (throwProof (ExactProofEmptyCaseSplit location)) + (traverse prepareCase) + (NonEmpty.nonEmpty sourceCases) + exhaustive <- + foldM disjoin + (preparedCaseAssumption (NonEmpty.head cases)) + (preparedCaseAssumption <$> NonEmpty.tail cases) + discharge <- + prepareDischarge + location context locals exhaustive Raw.JustificationEmpty + validateStructuralComposition + location + (goal : exhaustive : (preparedCaseAssumption <$> toList cases)) + (\foundation globalType -> + KernelProof.validateCaseAnalysisComposition + foundation + globalType + goal + (preparedCaseAssumption <$> cases) + exhaustive) + pure + (PreparedByCase + (PreparedCaseAnalysis goal cases exhaustive discharge)) + where + prepareCase (Raw.Case statement child) = do + assumption <- + Exact.preparedExactPropositionCore + <$> prepareStatement context statement + local <- allocateLocal ExactAssumption context assumption + prepared <- + prepareProof + (locate statement) + context + (locals <> [local]) + RecursiveProofInduction + goal + child + pure (PreparedCase assumption prepared) + + disjoin left right = + maybe + (structuralFailure + location + "case assumptions changed type or lexical context") + pure + (disjoinScopedCore left right) + +preparedCaseAssumption + :: PreparedCase + -> ScopedCheckedCore ObjectId +preparedCaseAssumption (PreparedCase assumption _proof) = + assumption + +preparedCaseProof :: PreparedCase -> PreparedProof +preparedCaseProof (PreparedCase _assumption proof) = + proof + +prepareGuardedFix + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> [Exact.ExactLocalId] + -> ScopedCheckedCore ObjectId + -> Raw.Proof + -> Prepare PreparedProof +prepareGuardedFix + fallback location context locals goal identities constraint continuation = do + (antecedent, conclusion) <- + maybe + (throwProof (ExactProofExpectedImplicationGoal location)) + pure + (openScopedImplication goal) + unless (constraint == antecedent) + (throwProof (ExactProofGoalStatementMismatch location)) + local <- allocateLocal ExactAssumption context constraint + prepared <- + prepareProof + fallback + context + (locals <> [local]) + RecursiveProofInduction + conclusion + continuation + pure (PreparedFix identities (PreparedAssume constraint prepared)) + +prepareCalculation + :: Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> Maybe Raw.CalcQuantifier + -> Raw.Calc + -> Prepare PreparedCalculation +prepareCalculation location context locals quantifier calculation = do + (identities, calculationContext, calculationGuard) <- + prepareCalculationScope context quantifier + case calculation of + Raw.Equation first destinations -> do + firstChecked <- prepareSetEndpoint calculationContext first + checkedDestinations <- + traverse + (\(destination, justification) -> do + checked <- + prepareSetEndpoint calculationContext destination + pure + ( locate destination + , checked + , justification + )) + destinations + finishCalculation + location context locals TySet identities calculationGuard + firstChecked checkedDestinations + Raw.Biconditionals first destinations -> do + firstChecked <- preparePropositionEndpoint calculationContext first + checkedDestinations <- + traverse + (\(destination, justification) -> do + checked <- + preparePropositionEndpoint + calculationContext destination + pure + ( locate destination + , checked + , justification + )) + destinations + finishCalculation + location context locals TyProp identities calculationGuard + firstChecked checkedDestinations + where + prepareSetEndpoint endpointContext expression = + Exact.preparedExactSetExpressionCore + <$> ( liftDriver + (Exact.prepareExactSetExpression + endpointContext expression) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + + preparePropositionEndpoint endpointContext formula = + Exact.preparedExactPropositionCore + <$> prepareStatement endpointContext (Raw.StmtFormula formula) + +prepareCalculationScope + :: Exact.ExactBinderContext + -> Maybe Raw.CalcQuantifier + -> Prepare + ( [Exact.ExactLocalId] + , Exact.ExactBinderContext + , Maybe (ScopedCheckedCore ObjectId) + ) +prepareCalculationScope context = \case + Nothing -> + pure ([], context, Nothing) + Just (Raw.CalcQuantifier variables bound suchThat) -> do + identities <- traverse (const allocateLocalIdentity) variables + calculationContext <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + (NonEmpty.zip identities variables) + context) + boundGuard <- + prepareSymbolicBoundConstraints + calculationContext variables bound + suchThatGuard <- + traverse + (fmap Exact.preparedExactPropositionCore + . prepareStatement calculationContext) + suchThat + calculationGuard <- + normalizeCalculationGuard + (boundGuard : maybeToList suchThatGuard) + pure (toList identities, calculationContext, calculationGuard) + +normalizeCalculationGuard + :: [ScopedCheckedCore ObjectId] + -> Prepare (Maybe (ScopedCheckedCore ObjectId)) +normalizeCalculationGuard guards = + foldM add Nothing guards + where + add accumulated constraint + | isScopedTruth constraint = pure accumulated + | otherwise = + case accumulated of + Nothing -> pure (Just constraint) + Just previous -> + Just + <$> maybe + (impossible + "checked calculation guards changed context") + pure + (conjoinScopedCore previous constraint) + + isScopedTruth proposition = + scopedCoreType proposition == TyProp + && scopedCoreTerm proposition == CImp CFalsum CFalsum + +finishCalculation + :: Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> CoreType + -> [Exact.ExactLocalId] + -> Maybe (ScopedCheckedCore ObjectId) + -> ScopedCheckedCore ObjectId + -> NonEmpty + ( Location + , ScopedCheckedCore ObjectId + , Raw.Justification + ) + -> Prepare PreparedCalculation +finishCalculation + fallback context locals operandType identities calculationGuard + first destinations = do + links <- prepareCalculationLinks first destinations + let finalEndpoint = preparedCalculationLinkDestination (NonEmpty.last links) + resultOpen <- + calculationEquality first finalEndpoint + result <- + closeCalculationProposition identities calculationGuard resultOpen + pure + (PreparedCheckedCalculation + operandType identities calculationGuard first links result) + where + prepareCalculationLinks previous (destination :| rest) = do + (next, firstLink) <- prepareCalculationLink previous destination + later <- prepareRemainingCalculationLinks next rest + pure (firstLink :| later) + + prepareRemainingCalculationLinks _previous [] = + pure [] + prepareRemainingCalculationLinks previous (destination : rest) = do + (next, link) <- prepareCalculationLink previous destination + (link :) <$> prepareRemainingCalculationLinks next rest + + prepareCalculationLink previous + (destinationLocation, destination, justification) = do + linkOpen <- calculationEquality previous destination + link <- closeCalculationProposition + identities calculationGuard linkOpen + discharge <- + prepareDischarge + (if destinationLocation == Nowhere + then fallback + else destinationLocation) + context + locals + link + justification + pure + ( destination + , PreparedCalculationLink destination discharge + ) + + calculationEquality left right = + maybe + (impossible + "checked calculation endpoints changed type or context") + pure + (equalScopedCore left right) + +closeCalculationProposition + :: [Exact.ExactLocalId] + -> Maybe (ScopedCheckedCore ObjectId) + -> ScopedCheckedCore ObjectId + -> Prepare (ScopedCheckedCore ObjectId) +closeCalculationProposition identities calculationGuard proposition = do + guarded <- + case calculationGuard of + Nothing -> pure proposition + Just constraint -> + maybe + (impossible + "a checked calculation guard changed context") + pure + (implyScopedCore constraint proposition) + pure (closeBinders (length identities) guarded) + where + closeBinders 0 closed = closed + closeBinders remaining open = + closeBinders (remaining - 1) + (fromMaybe + (impossible + "a checked calculation lost a quantified binder") + (closeScopedForall open)) + +preparedCalculationResult + :: PreparedCalculation + -> ScopedCheckedCore ObjectId +preparedCalculationResult + (PreparedCheckedCalculation + _operandType _identities _guard _first _links result) = + result + +preparedCalculationLinkDestination + :: PreparedCalculationLink + -> ScopedCheckedCore ObjectId +preparedCalculationLinkDestination + (PreparedCalculationLink destination _discharge) = + destination + +preparedCalculationLinkDischarge + :: PreparedCalculationLink + -> PreparedDischarge +preparedCalculationLinkDischarge + (PreparedCalculationLink _destination discharge) = + discharge + +preparedDischargeGoal + :: PreparedDischarge + -> ScopedCheckedCore ObjectId +preparedDischargeGoal = \case + PreparedVampireDischarge _location _justification goal _obligation -> + goal + PreparedSetExtensionality _location goal -> + goal + +prepareSymbolicBoundConstraints + :: Exact.ExactBinderContext + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Prepare (ScopedCheckedCore ObjectId) +prepareSymbolicBoundConstraints context variables bound = + Exact.preparedExactPropositionCore + <$> ( liftDriver + (Exact.prepareExactSymbolicBoundConstraints + context variables bound) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + +prepareSymbolicTake + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> NonEmpty Raw.VarSymbol + -> Raw.Bound + -> Raw.Stmt + -> Raw.Justification + -> Raw.Proof + -> Prepare PreparedProof +prepareSymbolicTake + fallback location context locals goal variables bound statement + justification continuation = do + identities <- traverse (const allocateLocalIdentity) variables + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + (NonEmpty.zip identities variables) + context) + witness <- + Exact.preparedExactPropositionCore + <$> ( liftDriver + (Exact.prepareExactSymbolicWitnessConstraints + context' variables bound statement) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + prepareTake + fallback location context locals goal context' + (toList identities) witness justification continuation + +prepareNounTake + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> Raw.NounPhrase [] + -> Raw.Justification + -> Raw.Proof + -> Prepare PreparedProof +prepareNounTake + fallback location context locals goal nounPhrase + justification continuation = do + (identities, context') <- + case nounPhrase of + Raw.NounPhrase _left _noun variables _right _suchThat -> + case NonEmpty.nonEmpty variables of + Just binders -> do + identities <- + traverse (const allocateLocalIdentity) binders + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactBinderContext + (NonEmpty.zip identities binders) + context) + pure (toList identities, context') + Nothing -> do + identity <- allocateLocalIdentity + context' <- + either + (throwProof . ExactProofElaborationFailed) + pure + (Exact.extendExactAnonymousBinderContext + identity context) + pure ([identity], context') + witness <- + Exact.preparedExactPropositionCore + <$> ( liftDriver + (Exact.prepareExactNounWitnessConstraints + context' nounPhrase) + >>= either + (throwProof . ExactProofElaborationFailed) + pure + ) + prepareTake + fallback location context locals goal context' + identities witness justification continuation + +prepareTake + :: Location + -> Location + -> Exact.ExactBinderContext + -> [PreparedLocal] + -> ScopedCheckedCore ObjectId + -> Exact.ExactBinderContext + -> [Exact.ExactLocalId] + -> ScopedCheckedCore ObjectId + -> Raw.Justification + -> Raw.Proof + -> Prepare PreparedProof +prepareTake + fallback location context locals goal witnessContext + identities witness justification continuation = do + let witnessCount = length identities + existence = closeTakenWitnesses witnessCount witness + goal' = weakenForTakenWitnesses witnessCount goal + discharge <- + prepareDischarge + location context locals existence justification + local <- allocateLocal ExactAssumption witnessContext witness + PreparedTake identities witness discharge + <$> prepareProof + fallback + witnessContext + (locals <> [local]) + RecursiveProofInduction + goal' + continuation -- The discharged existential and the opened witness premise are the same -- checked proposition viewed on opposite sides of existential elimination. @@ -846,6 +1831,21 @@ allocateLocal origin context proposition = do (Exact.exactBinderContextSupport context) proposition) +prepareConstructionFoundation + :: Prepare SetConstructionFoundation +prepareConstructionFoundation = do + familyUnion <- foundation FamilyUnionCharacteristic + separation <- foundation SeparationCharacteristic + replacement <- foundation ReplacementCharacteristic + setChoose <- foundation SetChooseWitness + pure + (setConstructionFoundation + familyUnion separation replacement setChoose) + where + foundation tag = + liftDriver + (Declaration.currentFoundationAxiomLowering tag) + prepareDischarge :: Location -> Exact.ExactBinderContext @@ -855,9 +1855,20 @@ prepareDischarge -> Prepare PreparedDischarge prepareDischarge location context locals goal justification = prepareDischargeWith - DirectDischarge + (dischargeModeFor goal) [] Nothing location context locals goal justification +-- A contradictory-axioms answer can establish falsum, but never an unrelated +-- proposition directly. Derive that distinction from the checked target so +-- every surface proof spelling reaches the same guarded request path. +dischargeModeFor :: ScopedCheckedCore ObjectId -> DischargeMode +dischargeModeFor goal + | scopedCoreType goal == TyProp + , scopedCoreTerm goal == CFalsum = + IndirectContradictionDischarge + | otherwise = + DirectDischarge + data DischargeMode = DirectDischarge | IndirectContradictionDischarge @@ -993,6 +2004,49 @@ prepareStatement context statement = (throwProof . ExactProofElaborationFailed) pure +validateStructuralComposition + :: Location + -> [ScopedCheckedCore ObjectId] + -> ( CheckedFoundation + -> (ObjectId -> Maybe CoreType) + -> Either KernelProof.KernelProofBuildError () + ) + -> Prepare () +validateStructuralComposition location propositions validate = do + foundation <- + liftDriver Declaration.currentFoundationLowering + let identities = + Set.toAscList + (Set.unions + ( canonicalTermGlobals . scopedCoreTerm + <$> propositions + )) + types <- + traverse + (\identity -> do + coreType <- + liftDriver + (Declaration.objectTypeLowering identity) + maybe + (impossible + "a checked structural proof lost a global object") + (\availableType -> pure (identity, availableType)) + coreType) + identities + either + (throwProof + . ExactProofStructuralCompositionFailed location) + pure + (validate foundation + (\identity -> Map.lookup identity (Map.fromList types))) + +structuralFailure :: Location -> Text -> Prepare value +structuralFailure location message = + throwProof + (ExactProofStructuralCompositionFailed + location + (KernelProof.ProofStructuralCompositionMismatch message)) + data CheckedExactProofAuthorization = CheckedExactProofAuthorization !PreparedProof !Bool @@ -1098,16 +2152,36 @@ preparedProofFirstOmission = \case preparedProofFirstOmission continuation PreparedTake _identities _witness _discharge continuation -> preparedProofFirstOmission continuation - PreparedSetInduction _hypothesis _discharge -> Nothing + PreparedSetInduction + (PreparedCheckedSetInduction + _focus _property _antecedents _target + _hypothesis _result child) -> + preparedProofFirstOmission child PreparedHave _claim _discharge continuation -> preparedProofFirstOmission continuation + PreparedSuffices _goal _reduction _implication _discharge continuation -> + preparedProofFirstOmission continuation + PreparedCalculate _calculation continuation -> + preparedProofFirstOmission continuation + PreparedSince _since _evidence _claim _discharge continuation -> + preparedProofFirstOmission continuation PreparedSubclaim _claim subproof continuation -> preparedProofFirstOmission subproof <|> preparedProofFirstOmission continuation PreparedDefine _identity _body _definition continuation -> preparedProofFirstOmission continuation + PreparedDefineRelational + _identity _body _functionality _definitions continuation -> + preparedProofFirstOmission continuation PreparedDefineFunction _identity _graph _definition continuation -> preparedProofFirstOmission continuation + PreparedByCase (PreparedCaseAnalysis _goal cases _exhaustive _discharge) -> + foldr + ((<|>) . preparedProofFirstOmission . preparedCaseProof) + Nothing + cases + PreparedByContradiction _goal _negation _falsum child -> + preparedProofFirstOmission child PreparedContradiction{} -> Nothing plannedProofRequests @@ -1123,17 +2197,41 @@ plannedProofRequests = \case plannedProofRequests continuation PreparedTake _identities _witness discharge continuation -> plannedDischargeRequests discharge <> plannedProofRequests continuation - PreparedSetInduction _hypothesis discharge -> - plannedDischargeRequests discharge + PreparedSetInduction + (PreparedCheckedSetInduction + _focus _property _antecedents _target + _hypothesis _result child) -> + plannedProofRequests child PreparedHave _claim discharge continuation -> plannedDischargeRequests discharge <> plannedProofRequests continuation + PreparedSuffices _goal _reduction _implication discharge continuation -> + plannedDischargeRequests discharge <> plannedProofRequests continuation + PreparedCalculate calculation continuation -> + plannedCalculationRequests calculation + <> plannedProofRequests continuation + PreparedSince _since evidence _claim discharge continuation -> + plannedSinceEvidenceRequests evidence + <> plannedDischargeRequests discharge + <> plannedProofRequests continuation PreparedSubclaim _claim subproof continuation -> plannedProofRequests subproof <> plannedProofRequests continuation PreparedDefine _identity _body _definition continuation -> plannedProofRequests continuation + PreparedDefineRelational + _identity _body functionality _definitions continuation -> + plannedDischargeRequests functionality + <> plannedProofRequests continuation PreparedDefineFunction _identity _graph _definition continuation -> plannedProofRequests continuation - PreparedContradiction discharge -> + PreparedByCase + (PreparedCaseAnalysis _goal cases _exhaustive discharge) -> + concatMap + (plannedProofRequests . preparedCaseProof) + (toList cases) + <> plannedDischargeRequests discharge + PreparedByContradiction _goal _negation _falsum child -> + plannedProofRequests child + PreparedContradiction _goal _falsum discharge -> plannedDischargeRequests discharge plannedDischargeRequests @@ -1144,6 +2242,24 @@ plannedDischargeRequests = \case [Declaration.checkedPlannedVampireRequest location obligation] PreparedSetExtensionality{} -> [] +plannedCalculationRequests + :: PreparedCalculation + -> [Declaration.CheckedPlannedVampireRequest] +plannedCalculationRequests + (PreparedCheckedCalculation + _operandType _identities _guard _first links _result) = + concatMap + (plannedDischargeRequests . preparedCalculationLinkDischarge) + (toList links) + +plannedSinceEvidenceRequests + :: PreparedSinceEvidence + -> [Declaration.CheckedPlannedVampireRequest] +plannedSinceEvidenceRequests = \case + PreparedSinceExisting{} -> [] + PreparedSinceDischarged discharge _local -> + plannedDischargeRequests discharge + executePreparedProof :: PreparedProof -> Declaration.CandidateProof () @@ -1161,19 +2277,45 @@ executePreparedProof = \case PreparedTake _identities _witness discharge continuation -> do executeDischarge discharge executePreparedProof continuation - PreparedSetInduction _hypothesis discharge -> - executeDischarge discharge + PreparedSetInduction + (PreparedCheckedSetInduction + _focus _property _antecedents _target + _hypothesis _result child) -> + executePreparedProof child PreparedHave _claim discharge continuation -> do executeDischarge discharge executePreparedProof continuation + PreparedSuffices goal reduction implication discharge continuation -> do + executeDischarge discharge + executePreparedProof continuation + unless + (implyScopedCore reduction goal == Just implication) + (impossible "a prepared suffices implication diverged") + PreparedCalculate calculation continuation -> do + executePreparedCalculation calculation + executePreparedProof continuation + PreparedSince sinceProposition evidence _claim discharge continuation -> do + executeSinceEvidence sinceProposition evidence + executeDischarge discharge + executePreparedProof continuation PreparedSubclaim _claim subproof continuation -> do executePreparedProof subproof executePreparedProof continuation PreparedDefine _identity _body _definition continuation -> executePreparedProof continuation + PreparedDefineRelational + _identity _body functionality _definitions continuation -> do + executeDischarge functionality + executePreparedProof continuation PreparedDefineFunction _identity _graph _definition continuation -> executePreparedProof continuation - PreparedContradiction discharge -> + PreparedByCase + (PreparedCaseAnalysis _goal cases _exhaustive discharge) -> do + traverse_ (executePreparedProof . preparedCaseProof) cases + executeDischarge discharge + PreparedByContradiction _goal _negation _falsum child -> + executePreparedProof child + PreparedContradiction _goal _falsum discharge -> executeDischarge discharge executeDischarge @@ -1187,6 +2329,39 @@ executeDischarge executeDischarge PreparedSetExtensionality{} = pure () +executePreparedCalculation + :: PreparedCalculation + -> Declaration.CandidateProof () +executePreparedCalculation + (PreparedCheckedCalculation + _operandType _identities _guard _first links _result) = + traverse_ + (executeDischarge . preparedCalculationLinkDischarge) + links + +executeSinceEvidence + :: ScopedCheckedCore ObjectId + -> PreparedSinceEvidence + -> Declaration.CandidateProof () +executeSinceEvidence proposition = \case + PreparedSinceExisting local -> + unless (preparedLocalProposition local == proposition) + (impossible "a structural since premise diverged") + PreparedSinceDischarged discharge local -> do + executeDischarge discharge + unless + ( preparedDischargeGoal discharge == proposition + && preparedLocalProposition local == proposition + ) + (impossible "a discharged since premise diverged") + +preparedLocalProposition + :: PreparedLocal + -> ScopedCheckedCore ObjectId +preparedLocalProposition + (PreparedLocal _ordinal _origin _support proposition) = + proposition + encodePreparedProof :: PreparedProof -> ByteString encodePreparedProof = encodeCache . putPreparedProof @@ -1220,28 +2395,72 @@ putPreparedProof = \case putScopedProposition witness putPreparedDischarge discharge putPreparedProof continuation - PreparedSetInduction hypothesis discharge -> do + PreparedSetInduction + (PreparedCheckedSetInduction + focus property antecedents target hypothesis result child) -> do putCacheTag 0x07 + putPreparedSetInductionFocus focus + putScopedProposition property + putCacheList putScopedProposition antecedents + putScopedProposition target putScopedProposition hypothesis - putPreparedDischarge discharge + putScopedProposition result + putPreparedProof child PreparedHave claim discharge continuation -> do putCacheTag 0x04 putScopedProposition claim putPreparedDischarge discharge putPreparedProof continuation + PreparedSuffices goal reduction implication discharge continuation -> do + putCacheTag 0x0c + putScopedProposition goal + putScopedProposition reduction + putScopedProposition implication + putPreparedDischarge discharge + putPreparedProof continuation + PreparedCalculate calculation continuation -> do + putCacheTag 0x0d + putPreparedCalculation calculation + putPreparedProof continuation + PreparedSince sinceProposition evidence claim discharge continuation -> do + putCacheTag 0x0e + putScopedProposition sinceProposition + putPreparedSinceEvidence evidence + putScopedProposition claim + putPreparedDischarge discharge + putPreparedProof continuation PreparedSubclaim claim subproof continuation -> do putCacheTag 0x05 putScopedProposition claim putPreparedProof subproof putPreparedProof continuation - PreparedDefine identity body definition continuation -> do + PreparedDefine identity body definitions continuation -> do putCacheTag 0x09 putCacheNatural (Exact.exactLocalIdValue identity) putScopedTerm body - putScopedProposition definition + putCacheList putScopedProposition (toList definitions) + putPreparedProof continuation + PreparedDefineRelational + identity body functionality definitions continuation -> do + putCacheTag 0x11 + putCacheNatural (Exact.exactLocalIdValue identity) + putScopedTerm body + putPreparedDischarge functionality + putCacheList putScopedProposition (toList definitions) putPreparedProof continuation - PreparedContradiction discharge -> do + PreparedByCase caseAnalysis -> do + putCacheTag 0x0f + putPreparedCaseAnalysis caseAnalysis + PreparedByContradiction goal negation falsum child -> do + putCacheTag 0x10 + putScopedProposition goal + putScopedProposition negation + putScopedProposition falsum + putPreparedProof child + PreparedContradiction goal falsum discharge -> do putCacheTag 0x0a + putScopedProposition goal + putScopedProposition falsum putPreparedDischarge discharge PreparedDefineFunction identity graph definition continuation -> do putCacheTag 0x0b @@ -1250,6 +2469,18 @@ putPreparedProof = \case putScopedProposition definition putPreparedProof continuation +putPreparedSetInductionFocus + :: PreparedSetInductionFocus + -> CachePut +putPreparedSetInductionFocus = \case + PreparedInitialSetInductionFocus identity index -> do + putCacheTag 0x00 + putCacheNatural (Exact.exactLocalIdValue identity) + putCacheNatural index + PreparedLeadingSetInductionFocus identity -> do + putCacheTag 0x01 + putCacheNatural (Exact.exactLocalIdValue identity) + putPreparedDischarge :: PreparedDischarge -> CachePut putPreparedDischarge (PreparedVampireDischarge @@ -1268,6 +2499,55 @@ putPreparedDischargeSyntax justification goal = do putPreparedJustification justification putScopedProposition goal +putPreparedCalculation :: PreparedCalculation -> CachePut +putPreparedCalculation + (PreparedCheckedCalculation + operandType identities calculationGuard first links result) = do + putCoreTypeCache operandType + putCacheList + (putCacheNatural . Exact.exactLocalIdValue) + identities + putCacheMaybe putScopedProposition calculationGuard + putCacheList putScopedTerm + (first : (preparedCalculationLinkDestination <$> toList links)) + putCacheList putPreparedDischarge + (preparedCalculationLinkDischarge <$> toList links) + putScopedProposition result + +putPreparedSinceEvidence :: PreparedSinceEvidence -> CachePut +putPreparedSinceEvidence = \case + PreparedSinceExisting local -> do + putCacheTag 0x00 + putPreparedLocalEvidence local + PreparedSinceDischarged discharge local -> do + putCacheTag 0x01 + putPreparedDischarge discharge + putPreparedLocalEvidence local + +putPreparedCaseAnalysis :: PreparedCaseAnalysis -> CachePut +putPreparedCaseAnalysis + (PreparedCaseAnalysis goal cases exhaustive discharge) = do + putScopedProposition goal + putCacheList putPreparedCase (toList cases) + putScopedProposition exhaustive + putPreparedDischarge discharge + +putPreparedCase :: PreparedCase -> CachePut +putPreparedCase (PreparedCase assumption proof) = do + putScopedProposition assumption + putPreparedProof proof + +putPreparedLocalEvidence :: PreparedLocal -> CachePut +putPreparedLocalEvidence + (PreparedLocal ordinal _origin support proposition) = do + putCacheNatural (Backend.localPremiseOrdinalValue ordinal) + putCacheList + (\(identity, coreType) -> do + putCacheNatural (Exact.exactLocalIdValue identity) + putCoreTypeCache coreType) + (Vector.toList support) + putScopedProposition proposition + implicitAutoProofSyntaxId :: ScopedCheckedCore ObjectId -> ProofSyntaxId diff --git a/source/Checking/Exact/Vocabulary.hs b/source/Checking/Exact/Vocabulary.hs index 5701f64..45a2844 100644 --- a/source/Checking/Exact/Vocabulary.hs +++ b/source/Checking/Exact/Vocabulary.hs @@ -5,6 +5,7 @@ module Checking.Exact.Vocabulary ( FixedSemanticMeaning(..) , fixedSemanticMeaning + , lowerFixedEqualityPredicate , ExactSymbolClass(..) , classifyExactSymbol , FixedSetTermDispatch(..) @@ -43,6 +44,14 @@ fixedSemanticVocabulary = [ ( relationKey Raw.EqSymbol , FixedEquality ) + , ( SemanticRightAdjective + (Raw.lexicalItemPattern + Lexicon.builtinEqualityRightAdjective) + , FixedEquality + ) + , ( verbKey Lexicon.builtinEqualityVerb + , FixedEquality + ) , ( relationKey Raw.ElementSymbol , FixedIntrinsic Member ) @@ -59,7 +68,7 @@ fixedSemanticVocabulary = (Raw.TokenCons (Raw.Command "emptyset") Raw.End) , FixedIntrinsic Empty ) - , ( expressionKey (unaryCommandPattern "unions") + , ( expressionKey (Raw.mixfixPattern Raw.UnionsSymbol) , FixedIntrinsic FamilyUnion ) , ( expressionKey (unaryCommandPattern "pow") @@ -80,8 +89,27 @@ fixedSemanticVocabulary = nounKey item = let patterns = Raw.lexicalItemSgPlPattern item in SemanticNoun (Raw.sg patterns) (Raw.pl patterns) + verbKey item = + let patterns = Raw.lexicalItemSgPlPattern item + in SemanticVerb (Raw.sg patterns) (Raw.pl patterns) expressionKey = SemanticExpressionFunction +-- | Lower the fixed proposition meanings shared by raw exact elaboration and +-- the reusable internal-formula path. Membership deliberately retains its +-- carrier-aware source lowering and is not handled here. +lowerFixedEqualityPredicate + :: FixedSemanticMeaning + -> [CanonicalTerm global] + -> Maybe (CanonicalTerm global) +lowerFixedEqualityPredicate meaning arguments = + case (meaning, arguments) of + (FixedEquality, [left, right]) -> + Just (CEq TySet left right) + (FixedDisequality, [left, right]) -> + Just (CImp (CEq TySet left right) CFalsum) + _ -> + Nothing + unaryCommandPattern :: Text -> Raw.Pattern unaryCommandPattern command = Raw.TokenCons (Raw.Command command) diff --git a/source/Checking/FinalPrelude.hs b/source/Checking/FinalPrelude.hs index 5951acc..acb3c7b 100644 --- a/source/Checking/FinalPrelude.hs +++ b/source/Checking/FinalPrelude.hs @@ -19,6 +19,7 @@ module Checking.FinalPrelude , FinalPreludeBuildResult(..) , buildFinalPreludeCandidate , buildParsedFinalPreludeCandidate + , validateOmegaFactInventory ) where import Base hiding (Empty) @@ -29,9 +30,11 @@ import Checking.Exact qualified as Exact import Checking.Exact.Proof qualified as ExactProof import Checking.Foundation import Checking.Identity +import Checking.SetConstruction import Checking.Semantic import Checking.Semantic qualified as Semantic import Felix.Module +import Felix.Cache.Codec (CacheDigest) import Felix.Parse import Felix.Prelude qualified as Prelude import Felix.Source (ImportRef) @@ -164,7 +167,8 @@ data FinalPreludeBuildResult data PlannedPreludeDeclaration = PlannedPreludeBinding - !(Declaration.PlannedDeclaration (Maybe ObjectId)) + !(Declaration.PlannedDeclaration + Exact.CheckedExactBindingAuthorization) | PlannedPreludeFoundation !(Declaration.PlannedDeclaration ExactProof.CheckedFinalPreludeFoundationAuthorization) @@ -540,6 +544,19 @@ resolveAndValidatePublicRoles foundation objects declarations = do omegaBody let omegaId = definitionViewObject omega + omegaConstruction <- + expectedOmegaConstruction objects omegaBody + omegaDerived <- + maybe + (Left + (FinalPreludeFactContentMismatch + "prelude_omega")) + Right + (namedSetConstructionObjectFact + (checkedFoundationSetConstruction foundation) + omegaId + omegaConstruction) + naturals <- expectDefinition foundation objects declarations @@ -557,12 +574,14 @@ resolveAndValidatePublicRoles foundation objects declarations = do (infinity, infinityTarget) <- expectClaim declarations "prelude_infinity" validateInfinityTarget objects inductiveId infinityTarget + omegaDeclaration <- findDeclaration "prelude_omega" declarations omegaEquation <- - fst - <$> expectFactTarget - declarations - "prelude_omega" - (CEq TySet (CGlobal omegaId) omegaBody) + validateOmegaDeclaration + objects + omegaId + omegaBody + omegaDerived + omegaDeclaration let inductiveOmega = CApp (CGlobal inductiveId) (CGlobal omegaId) minimalOmega = expectedMinimality inductiveId omegaId @@ -606,6 +625,159 @@ resolveAndValidatePublicRoles foundation objects declarations = do PreludeInfinityTheorem)) pure roles +expectedOmegaConstruction + :: CheckedObjectClosure + -> CanonicalTerm ObjectId + -> Either + FinalPreludeValidationError + (NamedSetConstruction ObjectId) +expectedOmegaConstruction objects = \case + CApp (CApp (CIntrinsic Sep) bound) (CLam TySet predicate) -> do + checkedBound <- checked [] bound + checkedPredicate <- checked [TySet] predicate + maybe + (Left + (FinalPreludeFactContentMismatch + "prelude_omega")) + Right + (checkedSeparationConstruction + (`lookupCheckedObjectType` objects) + checkedBound + checkedPredicate) + _ -> + Left + (FinalPreludeFactContentMismatch + "prelude_omega") + where + checked context term = + first + (const + (FinalPreludeFactContentMismatch + "prelude_omega")) + (checkScopedCanonicalCore + (`lookupCheckedObjectType` objects) + context + term) + +validateOmegaDeclaration + :: CheckedObjectClosure + -> ObjectId + -> CanonicalTerm ObjectId + -> NamedSetConstructionFact + -> PreludeDeclaration + -> Either FinalPreludeValidationError TheoremRef +validateOmegaDeclaration objects omegaId omegaBody derived declaration = do + let batch = declarationBatch declaration + delta = Declaration.committedBatchDelta batch + omegaContent <- case lookupCheckedObjectContent omegaId objects of + Just content@TransparentObjectContent{} -> pure content + _ -> + Left + (FinalPreludeFactContentMismatch + "prelude_omega") + unless + ( declarationDeltaObjects delta == [omegaId] + && case Declaration.committedBatchObjects batch of + [asserted] -> + assertedObjectId asserted == omegaId + && assertedObjectContent asserted == omegaContent + _ -> False + && null (Declaration.committedBatchProofValidations batch) + ) + (Left + (FinalPreludeFactContentMismatch + "prelude_omega")) + certificates <- + maybe + (Left + (FinalPreludeFactContentMismatch + "prelude_omega")) + (Right . declarationValidationRecordCertificates) + (Declaration.committedBatchDeclarationValidation batch) + validateOmegaFactInventory + omegaId + omegaBody + (namedSetConstructionFactProposition derived) + (namedSetConstructionFactDescriptor derived) + (declarationDeltaFacts delta) + (declarationDeltaAliases delta) + (Declaration.committedBatchPropositions batch) + certificates + +-- | Purpose-specific audit of the distinguished Omega definition. It is +-- deliberately not a general declaration manifest: the confined prelude has +-- exactly one declaration whose public role requires this two-fact shape. +-- The explicit arguments also provide a narrow pure seam for corruption +-- regression tests. +validateOmegaFactInventory + :: ObjectId + -> CanonicalTerm ObjectId + -> FrozenCheckedCore ObjectId + -> CacheDigest + -> [SemanticFactOccurrence] + -> [SemanticAlias] + -> [CheckedPropositionContent] + -> [Authority.ValidationCertificate] + -> Either FinalPreludeValidationError TheoremRef +validateOmegaFactInventory + omegaId omegaBody expectedExtensional expectedDescriptor + facts aliases propositions certificates = do + (equationOccurrence, extensionalOccurrence) <- + case facts of + [equation, extensional] -> Right (equation, extensional) + _ -> mismatch + (equationCertificate, extensionalCertificate) <- + case certificates of + [equation, extensional] -> Right (equation, extensional) + _ -> mismatch + case aliases of + [alias] + | semanticAliasName alias == semanticName "prelude_omega" + , semanticAliasTarget alias + == semanticFactFingerprint equationOccurrence -> + pure () + _ -> mismatch + equation <- propositionFor equationOccurrence + extensional <- propositionFor extensionalOccurrence + unless + ( length propositions == 2 + && semanticFactSearchEligibility equationOccurrence + == SearchIneligible + && frozenCoreTerm (checkedPropositionTerm equation) + == CEq TySet (CGlobal omegaId) omegaBody + && Authority.validationTarget equationCertificate + == semanticFactAuthority equationOccurrence + && Authority.validationDirectAuthorization equationCertificate + == Authority.CheckedKernelConstruction + (Authority.CheckedDefinitionEquation omegaId) + && semanticFactSearchEligibility extensionalOccurrence + == SearchEligible + && checkedPropositionTerm extensional == expectedExtensional + && Authority.validationTarget extensionalCertificate + == semanticFactAuthority extensionalOccurrence + && Authority.validationDirectAuthorization extensionalCertificate + == Authority.CheckedKernelConstruction + (Authority.CheckedSetConstructionExtensionality + omegaId expectedDescriptor) + ) + mismatch + pure + (Authority.factAuthorityTheorem + (semanticFactAuthority equationOccurrence)) + where + mismatch = + Left + (FinalPreludeFactContentMismatch + "prelude_omega") + + propositionFor occurrence = + case List.filter + ((== semanticFactProposition occurrence) + . checkedPropositionId) + propositions of + [proposition] -> Right proposition + _ -> mismatch + validatePackagedPreludeInput :: Prelude.ReservedParsedPrelude -> ModuleSyntaxInterface @@ -805,6 +977,16 @@ validateDeclarationAuthority foundation objects declaration = do (Left (FinalPreludeAuthorityMismatch slot)) _ -> Left (FinalPreludeAuthorityMismatch slot) + Authority.CheckedKernelConstruction + (Authority.CheckedSetConstructionExtensionality + identity _descriptor) -> + case lookupCheckedObjectContent identity objects of + Just TransparentObjectContent{} + | semanticFactSearchEligibility occurrence + == SearchEligible -> + pure () + _ -> + Left (FinalPreludeAuthorityMismatch slot) Authority.CheckedSourceProof requests -> unless ( not (null requests) @@ -900,17 +1082,34 @@ expectFact (TheoremRef, CanonicalTerm ObjectId) expectFact declarations marker = do declaration <- findDeclaration marker declarations + unless + (length + (declarationDeltaFacts + (Declaration.committedBatchDelta + (declarationBatch declaration))) == 1) + (Left (FinalPreludeFactContentMismatch marker)) + expectAliasedFact declaration marker + +expectAliasedFact + :: PreludeDeclaration + -> Text + -> Either + FinalPreludeValidationError + (TheoremRef, CanonicalTerm ObjectId) +expectAliasedFact declaration marker = do let batch = declarationBatch declaration delta = Declaration.committedBatchDelta batch expectedAlias = semanticName marker - occurrence <- case declarationDeltaFacts delta of + fingerprint <- case declarationDeltaAliases delta of + [alias] + | semanticAliasName alias == expectedAlias -> + Right (semanticAliasTarget alias) + _ -> Left (FinalPreludeFactContentMismatch marker) + occurrence <- case List.filter + ((== fingerprint) . semanticFactFingerprint) + (declarationDeltaFacts delta) of [single] -> Right single _ -> Left (FinalPreludeFactContentMismatch marker) - unless - (declarationDeltaAliases delta - == [semanticAlias expectedAlias - (semanticFactFingerprint occurrence)]) - (Left (FinalPreludeFactContentMismatch marker)) proposition <- maybe (Left (FinalPreludeFactContentMismatch marker)) @@ -925,20 +1124,6 @@ expectFact declarations marker = do , frozenCoreTerm (checkedPropositionTerm proposition) ) -expectFactTarget - :: [PreludeDeclaration] - -> Text - -> CanonicalTerm ObjectId - -> Either - FinalPreludeValidationError - (TheoremRef, CanonicalTerm ObjectId) -expectFactTarget declarations marker expected = do - result@(_theorem, actual) <- expectFact declarations marker - unless - (actual == expected) - (Left (FinalPreludeFactContentMismatch marker)) - pure result - validateInfinityTarget :: CheckedObjectClosure -> ObjectId diff --git a/source/Checking/Kernel/Proof.hs b/source/Checking/Kernel/Proof.hs index 42324d1..5fc0d96 100644 --- a/source/Checking/Kernel/Proof.hs +++ b/source/Checking/Kernel/Proof.hs @@ -33,6 +33,10 @@ module Checking.Kernel.Proof , disjunctionLeftProof , disjunctionRightProof , disjunctionEliminationProof + , validateCaseAnalysisComposition + , validateDoubleNegationComposition + , validateFalsumEliminationComposition + , validateSetInductionComposition , existentialTerm , existentialIntroductionProof , existentialEliminationProof @@ -52,7 +56,9 @@ import Checking.Kernel.SetLfp qualified as SetLfp import Control.Monad (unless) import Data.Bifunctor (first) import Data.List qualified as List +import Data.List.NonEmpty qualified as NonEmpty import Data.Text qualified as Text +import Numeric.Natural (Natural) data ProofContext global = ProofContext @@ -108,6 +114,7 @@ data KernelProofBuildError | ProofExpectedUnaryBinder | ProofSetLfpRuleFailed !Text | ProofConversionPlanFailed !Text + | ProofStructuralCompositionMismatch !Text deriving stock (Show, Eq) scopedTerm @@ -881,6 +888,276 @@ disjunctionEliminationProof result doubleNegation +-- | Validate the one structural rule used by exact source case analysis. +-- The branch proofs and the exhaustive disjunction are represented here by +-- exact hypotheses; the kernel combinators must derive the owned goal from +-- precisely those propositions. No derived proof escapes this check. +validateCaseAnalysisComposition + :: Eq global + => CheckedFoundation + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> NonEmpty (ScopedCheckedCore global) + -> ScopedCheckedCore global + -> Either KernelProofBuildError () +validateCaseAnalysisComposition + foundation globalType goal cases exhaustive = do + validatePropositionContext "case goal" lexicalContext goal + traverse_ + (validatePropositionContext "case assumption" lexicalContext) + cases + validatePropositionContext + "case exhaustiveness target" lexicalContext exhaustive + let expectedExhaustive = + foldl1 + (\left right -> + CImp + (CImp left CFalsum) + right) + (scopedCoreTerm <$> cases) + unless (scopedCoreTerm exhaustive == expectedExhaustive) + (Left + (ProofStructuralCompositionMismatch + "case exhaustiveness is not the source-ordered disjunction")) + branchImplications <- + traverse + (checkedImplication lexicalContext goal) + cases + let context = + ProofContext + foundation + globalType + lexicalContext + (exhaustive : toList branchImplications) + exhaustiveProof <- hypothesisProof context exhaustive + result <- + eliminateCases + context goal cases exhaustiveProof + unless (builtProofStatement result == goal) + (Left + (ProofStructuralCompositionMismatch + "case elimination did not derive the owned goal")) + where + lexicalContext = scopedCoreContext goal + + checkedImplication expectedContext conclusion antecedent = + case implyScopedCore antecedent conclusion of + Just implication + | scopedCoreContext implication == expectedContext -> + pure implication + _ -> + Left + (ProofStructuralCompositionMismatch + "case branch implication changed context") + + eliminateCases context result (only :| []) caseProof = do + branchImplication <- + scopedTerm context + (CImp + (scopedCoreTerm only) + (scopedCoreTerm result)) + >>= hypothesisProof context + implicationEliminationProof context branchImplication caseProof + eliminateCases context result (firstCase :| rest) disjunctionProof = do + let allCases = firstCase :| rest + leftCases = NonEmpty.fromList (NonEmpty.init allCases) + rightCase = NonEmpty.last allCases + leftTerm = + foldl1 disjunctionTerm + (scopedCoreTerm <$> leftCases) + disjunctionEliminationProof + context + leftTerm + (scopedCoreTerm rightCase) + disjunctionProof + result + (\extended leftProof -> + eliminateCases extended result leftCases leftProof) + (\extended rightProof -> do + branchImplication <- + scopedTerm extended + (CImp + (scopedCoreTerm rightCase) + (scopedCoreTerm result)) + >>= hypothesisProof extended + implicationEliminationProof + extended branchImplication rightProof) + +-- | Validate the exact classical closing step for a proof by contradiction. +-- The only classical input is the confined 'DoubleNegationElim' foundation +-- row already consumed by 'doubleNegationEliminationProof'. +validateDoubleNegationComposition + :: Eq global + => CheckedFoundation + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either KernelProofBuildError () +validateDoubleNegationComposition + foundation globalType goal negation falsum = do + let lexicalContext = scopedCoreContext goal + validatePropositionContext "contradiction goal" lexicalContext goal + validatePropositionContext + "contradiction negation" lexicalContext negation + validatePropositionContext "contradiction falsum" lexicalContext falsum + unless (scopedCoreTerm falsum == CFalsum) + (Left + (ProofStructuralCompositionMismatch + "proof by contradiction did not target falsum")) + expectedNegation <- + checkedNegation lexicalContext goal + unless (negation == expectedNegation) + (Left + (ProofStructuralCompositionMismatch + "proof by contradiction did not own the exact negated goal")) + doubleNegation <- + checkedNegation lexicalContext negation + let context = + ProofContext + foundation globalType lexicalContext [doubleNegation] + hypothesis <- hypothesisProof context doubleNegation + result <- doubleNegationEliminationProof context goal hypothesis + unless (builtProofStatement result == goal) + (Left + (ProofStructuralCompositionMismatch + "double-negation elimination did not derive the owned goal")) + +-- | Validate the exact ex-falso closing step used after a terminal indirect +-- contradiction discharge. +validateFalsumEliminationComposition + :: Eq global + => CheckedFoundation + -> (global -> Maybe CoreType) + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either KernelProofBuildError () +validateFalsumEliminationComposition foundation globalType goal falsum = do + let lexicalContext = scopedCoreContext goal + validatePropositionContext "contradiction goal" lexicalContext goal + validatePropositionContext "contradiction falsum" lexicalContext falsum + unless (scopedCoreTerm falsum == CFalsum) + (Left + (ProofStructuralCompositionMismatch + "falsum elimination did not receive falsum")) + let context = + ProofContext foundation globalType lexicalContext [falsum] + hypothesis <- hypothesisProof context falsum + result <- falsumEliminationProof context hypothesis goal + unless (builtProofStatement result == goal) + (Left + (ProofStructuralCompositionMismatch + "falsum elimination did not derive the owned goal")) + +-- | Validate the exact structural instance used by source set induction. +-- The admitted child is represented by its generalized step proposition; +-- the checked foundation row must specialize to that exact premise and the +-- owned binder-level result. No induction principle becomes an ATP premise. +validateSetInductionComposition + :: Eq global + => CheckedFoundation + -> (global -> Maybe CoreType) + -> Natural + -> ScopedCheckedCore global + -> [ScopedCheckedCore global] + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> ScopedCheckedCore global + -> Either KernelProofBuildError () +validateSetInductionComposition + foundation globalType selected property antecedents childTarget + hypothesis result = do + let lexicalContext = scopedCoreContext property + traverse_ + (validatePropositionContext + "set-induction antecedent" lexicalContext) + antecedents + validatePropositionContext + "set-induction property" lexicalContext property + validatePropositionContext + "set-induction child target" lexicalContext childTarget + validatePropositionContext + "set-induction hypothesis" lexicalContext hypothesis + validatePropositionContext + "set-induction result" lexicalContext result + expectedProperty <- + foldrM implyChecked childTarget antecedents + unless (property == expectedProperty) + (Left + (ProofStructuralCompositionMismatch + "set-induction property does not own the child target and guards")) + (predicate, expectedHypothesis, step, expectedResult) <- + maybe + (Left + (ProofStructuralCompositionMismatch + "set-induction focus is not a set-valued ambient binder")) + pure + (scopedSetInductionInstance selected property) + unless (hypothesis == expectedHypothesis) + (Left + (ProofStructuralCompositionMismatch + "set-induction hypothesis does not match the owned property")) + unless (result == expectedResult) + (Left + (ProofStructuralCompositionMismatch + "set-induction result does not close the owned property")) + let context = + ProofContext foundation globalType lexicalContext [step] + stepProof <- hypothesisProof context step + axiom <- foundationProof context SetInduction + instanceProof <- forallEliminationProof context axiom predicate + expectedInstance <- + maybe + (Left + (ProofStructuralCompositionMismatch + "set-induction instance changed lexical context")) + pure + (implyScopedCore step result) + convertedInstance <- + conversionProof context instanceProof expectedInstance + resultProof <- + implicationEliminationProof context convertedInstance stepProof + unless (builtProofStatement resultProof == result) + (Left + (ProofStructuralCompositionMismatch + "set-induction foundation instance did not derive the owned result")) + where + implyChecked antecedent conclusion = + maybe + (Left + (ProofStructuralCompositionMismatch + "set-induction guard changed lexical context")) + pure + (implyScopedCore antecedent conclusion) + +validatePropositionContext + :: Text + -> [CoreType] + -> ScopedCheckedCore global + -> Either KernelProofBuildError () +validatePropositionContext label expected proposition = + unless + ( scopedCoreType proposition == TyProp + && scopedCoreContext proposition == expected + ) + (Left + (ProofStructuralCompositionMismatch + (label <> " has the wrong type or lexical context"))) + +checkedNegation + :: [CoreType] + -> ScopedCheckedCore global + -> Either KernelProofBuildError (ScopedCheckedCore global) +checkedNegation expectedContext proposition = + case negateScopedCore proposition of + Just negation + | scopedCoreContext negation == expectedContext -> + pure negation + _ -> + Left + (ProofStructuralCompositionMismatch + "classical negation changed context") + existentialTerm :: CoreType -> CanonicalTerm global diff --git a/source/Checking/Module.hs b/source/Checking/Module.hs index 453059a..d0e1d52 100644 --- a/source/Checking/Module.hs +++ b/source/Checking/Module.hs @@ -678,7 +678,8 @@ data TypedModuleResult data PlannedTypedDeclaration = PlannedBinding - !(Declaration.PlannedDeclaration (Maybe ObjectId)) + !(Declaration.PlannedDeclaration + Exact.CheckedExactBindingAuthorization) | PlannedSourceAxiom !(Declaration.PlannedDeclaration ()) | PlannedInductive 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)) diff --git a/source/Checking/Typed/Inductive.hs b/source/Checking/Typed/Inductive.hs index 7a895c6..eb6c0f7 100644 --- a/source/Checking/Typed/Inductive.hs +++ b/source/Checking/Typed/Inductive.hs @@ -8,16 +8,27 @@ module Checking.Typed.Inductive ( DirectInductive(..) , DirectInductiveClause(..) , DirectInductiveCondition(..) + , RecursiveCarrierContext + , RecursiveCarrierContextError(..) + , prepareRecursiveCarrierContext + , directRecursiveCarrierContext + , recursiveCarrierContextSymbols , SourceGlobal(..) , PreparedTypedInductive , typedInductiveCarrierType , typedInductiveCarrierBody , typedInductiveGuardTargets + , PreparedTypedInductiveMonotonicity + , typedInductiveMonotonicities + , typedInductiveMonotonicityLocation + , typedInductiveMonotonicityTarget + , typedInductiveContextInventory , PreparedTypedInductiveFact , typedInductiveFacts , typedInductiveFactMarker , typedInductiveFactTarget , typedInductiveFactRules + , typedInductiveFactRequiresMonotonicities , typedInductiveFactDerivation , prepareTypedClosedTerm , prepareTypedClosedFormula @@ -31,6 +42,7 @@ import Checking.Exact.Vocabulary import Checking.Foundation import Checking.Kernel.Derivation import Checking.Kernel.Proof +import Report.Location (Location) import Syntax.Internal import Control.Monad ((<=<), foldM) @@ -63,7 +75,73 @@ data DirectInductiveClause = DirectInductiveClause data DirectInductiveCondition = DirectSideCondition !Formula - | DirectRecursiveCondition !Term + | DirectRecursiveCondition !Term !RecursiveCarrierContext + +data RecursiveCarrierVariable + = RecursiveCarrierHole + | RecursiveCarrierSourceVariable !VarSymbol + deriving stock (Show, Eq, Ord) + +-- | A validated, capture-free one-hole carrier context in the same +-- first-order set-term fragment lowered by this module. The source carrier +-- application itself has been replaced, so the inductive symbol cannot +-- survive inside this value. +data RecursiveCarrierContext = RecursiveCarrierContext + !Location + !(ExprOf RecursiveCarrierVariable) + deriving stock (Show, Eq, Ord) + +data RecursiveCarrierContextError + = RecursiveCarrierWrongArguments !Location + | RecursiveCarrierUnsupportedContext !Location + deriving stock (Show, Eq) + +prepareRecursiveCarrierContext + :: FunctionSymbol + -> [VarSymbol] + -> Term + -> Either RecursiveCarrierContextError RecursiveCarrierContext +prepareRecursiveCarrierContext carrier parameters source = + RecursiveCarrierContext (exprLocation source) <$> go source + where + carrierSymbol = SymbolMixfix carrier + + go = \case + TermVar variable -> + pure + (TermVar + (RecursiveCarrierSourceVariable variable)) + TermSymbol location symbol arguments + | symbol == carrierSymbol -> + if sameCarrierArguments arguments parameters + then pure (TermVar RecursiveCarrierHole) + else Left (RecursiveCarrierWrongArguments location) + | otherwise -> + TermSymbol location symbol <$> traverse go arguments + unsupported -> + Left + (RecursiveCarrierUnsupportedContext + (exprLocation unsupported)) + + sameCarrierArguments arguments variables = + length arguments == length variables + && and + (zipWith + (\argument variable -> + argument == TermVar variable) + arguments + variables) + +recursiveCarrierContextSymbols + :: RecursiveCarrierContext + -> Set Symbol +recursiveCarrierContextSymbols + (RecursiveCarrierContext _location source) = + mentionedSymbols source + +directRecursiveCarrierContext :: Location -> RecursiveCarrierContext +directRecursiveCarrierContext location = + RecursiveCarrierContext location (TermVar RecursiveCarrierHole) data SourceGlobal global = SourceGlobal !global @@ -93,8 +171,80 @@ data PreparedTypedInductive global = PreparedTypedInductive !CoreType !(FrozenCheckedCore global) !(Vector (FrozenCheckedCore global)) + !(Vector (PreparedTypedInductiveMonotonicity global)) + !(Vector (FrozenCheckedCore global)) !(NonEmpty (PreparedTypedInductiveFact global)) +data PreparedTypedInductiveMonotonicity global = + PreparedTypedInductiveMonotonicity + !Location + !(FrozenCheckedCore global) + +typedInductiveMonotonicities + :: PreparedTypedInductive global + -> Vector (PreparedTypedInductiveMonotonicity global) +typedInductiveMonotonicities + (PreparedTypedInductive + _carrierType + _body + _guards + monotonicities + _contexts + _facts) = + monotonicities + +typedInductiveMonotonicityLocation + :: PreparedTypedInductiveMonotonicity global + -> Location +typedInductiveMonotonicityLocation + (PreparedTypedInductiveMonotonicity location _target) = + location + +typedInductiveMonotonicityTarget + :: PreparedTypedInductiveMonotonicity global + -> FrozenCheckedCore global +typedInductiveMonotonicityTarget + (PreparedTypedInductiveMonotonicity _location target) = + target + +typedInductiveContextInventory + :: PreparedTypedInductive global + -> Vector (FrozenCheckedCore global) +typedInductiveContextInventory + (PreparedTypedInductive + _carrierType _body _guards _monotonicities contexts _facts) = + contexts + +data CheckedRecursiveCarrierContext global = + CheckedRecursiveCarrierContext + ![VarSymbol] + !(FrozenCheckedCore global) + +data PreparedInductiveSource global = PreparedInductiveSource + { preparedInductiveParams :: ![VarSymbol] + , preparedInductiveDomain :: !Term + , preparedInductiveClauses + :: !(NonEmpty (PreparedInductiveClause global)) + } + +data PreparedInductiveClause global = PreparedInductiveClause + { preparedClauseVariables :: ![VarSymbol] + , preparedClauseConditions + :: ![PreparedInductiveCondition global] + , preparedClauseResult :: !Term + } + +data PreparedInductiveCondition global + = PreparedSideCondition !Formula + | PreparedDirectRecursiveCondition + !Term + !(CheckedRecursiveCarrierContext global) + | PreparedNestedRecursiveCondition + !Term + !(CheckedRecursiveCarrierContext global) + !ImportIx + !(FrozenCheckedCore global) + data PreparedInductiveGuard global = PreparedFoundationGuard !FoundationAxiomTag | PreparedImportedGuard @@ -109,6 +259,8 @@ typedInductiveCarrierType carrierType _body _guards + _monotonicities + _contexts _facts) = carrierType @@ -120,6 +272,8 @@ typedInductiveCarrierBody _carrierType body _guards + _monotonicities + _contexts _facts) = body @@ -131,6 +285,8 @@ typedInductiveGuardTargets _carrierType _body guards + _monotonicities + _contexts _facts) = guards @@ -139,6 +295,7 @@ newtype PreparedTypedInductiveFact global = ( Marker , FrozenCheckedCore global , NonEmpty KernelRuleTag + , Bool , KernelDerivation global ) @@ -150,6 +307,8 @@ typedInductiveFacts _carrierType _body _guards + _monotonicities + _contexts facts) = facts @@ -158,7 +317,7 @@ typedInductiveFactMarker -> Marker typedInductiveFactMarker (PreparedTypedInductiveFact - (marker, _target, _rule, _derivation)) = + (marker, _target, _rule, _monotonicities, _derivation)) = marker typedInductiveFactTarget @@ -166,7 +325,7 @@ typedInductiveFactTarget -> FrozenCheckedCore global typedInductiveFactTarget (PreparedTypedInductiveFact - (_marker, target, _rule, _derivation)) = + (_marker, target, _rule, _monotonicities, _derivation)) = target typedInductiveFactRules @@ -174,15 +333,23 @@ typedInductiveFactRules -> NonEmpty KernelRuleTag typedInductiveFactRules (PreparedTypedInductiveFact - (_marker, _target, rules, _derivation)) = + (_marker, _target, rules, _monotonicities, _derivation)) = rules +typedInductiveFactRequiresMonotonicities + :: PreparedTypedInductiveFact global + -> Bool +typedInductiveFactRequiresMonotonicities + (PreparedTypedInductiveFact + (_marker, _target, _rules, required, _derivation)) = + required + typedInductiveFactDerivation :: PreparedTypedInductiveFact global -> KernelDerivation global typedInductiveFactDerivation (PreparedTypedInductiveFact - (_marker, _target, _rule, derivation)) = + (_marker, _target, _rule, _monotonicities, derivation)) = derivation -- | Lower one closed source formula through the exact primitive/global @@ -326,13 +493,9 @@ prepareTypedInductiveInternal resolveGlobal marker inductive = do - carrierBody <- - prepareCarrierBody - resolveGlobal - inductive guards <- traverse - (prepareGuardTarget + (prepareDirectGuardTarget resolveGlobal inductive) (directInductiveClauses @@ -340,12 +503,27 @@ prepareTypedInductiveInternal let preparedGuards = assignGuardSources foundation (NonEmpty.toList guards) + nextImport = + fromIntegral + (length + [ () + | PreparedImportedGuard{} <- preparedGuards + ]) + (preparedSource, monotonicities, contexts) <- + prepareInductiveSource + resolveGlobal + nextImport + inductive + carrierBody <- + prepareCarrierBody + resolveGlobal + preparedSource facts <- prepareFacts foundation resolveGlobal marker - inductive + preparedSource (case preparedGuards of firstGuard : remainingGuards -> firstGuard :| remainingGuards @@ -361,6 +539,8 @@ prepareTypedInductiveInternal | PreparedImportedGuard _index target <- preparedGuards ]) + (Vector.fromList monotonicities) + (Vector.fromList contexts) facts) where carrierType = @@ -385,34 +565,264 @@ mapPreparedTypedInductive -> PreparedTypedInductive left -> PreparedTypedInductive right mapPreparedTypedInductive transform - (PreparedTypedInductive carrierType body guards facts) = + (PreparedTypedInductive + carrierType body guards monotonicities contexts facts) = PreparedTypedInductive carrierType (mapFrozenGlobals transform body) (mapFrozenGlobals transform <$> guards) + (mapMonotonicity transform <$> monotonicities) + (mapFrozenGlobals transform <$> contexts) (mapPreparedFact transform <$> facts) where + mapMonotonicity mapGlobal + (PreparedTypedInductiveMonotonicity location target) = + PreparedTypedInductiveMonotonicity + location + (mapFrozenGlobals mapGlobal target) + mapPreparedFact mapGlobal (PreparedTypedInductiveFact - (marker, target, rule, derivation)) = + (marker, target, rule, requiresMonotonicities, derivation)) = PreparedTypedInductiveFact ( marker , mapFrozenGlobals mapGlobal target , rule + , requiresMonotonicities , mapKernelDerivationGlobals mapGlobal derivation ) -prepareCarrierBody +data MonotonicityInventory global = MonotonicityInventory + ![(FrozenCheckedCore global, ImportIx)] + !Natural + ![PreparedTypedInductiveMonotonicity global] + ![FrozenCheckedCore global] + +prepareInductiveSource :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> Natural -> DirectInductive -> Either TypedInductiveError + ( PreparedInductiveSource (InductiveGlobal global) + , [PreparedTypedInductiveMonotonicity (InductiveGlobal global)] + , [FrozenCheckedCore (InductiveGlobal global)] + ) +prepareInductiveSource resolveGlobal firstImport inductive = do + (final, clauses) <- + prepareClauses + (MonotonicityInventory [] firstImport [] []) + (NonEmpty.toList (directInductiveClauses inductive)) + let MonotonicityInventory + _targets _next monotonicities contexts = final + pure + ( PreparedInductiveSource + (directInductiveParams inductive) + (directInductiveDomain inductive) + (NonEmpty.fromList clauses) + , reverse monotonicities + , reverse contexts + ) + where + variablesFor clause = + directInductiveParams inductive + <> directClauseVariables clause + + prepareClauses inventory = \case + [] -> pure (inventory, []) + clause : remaining -> do + (afterClause, preparedClause) <- + prepareClause inventory clause + (final, preparedRemaining) <- + prepareClauses afterClause remaining + pure (final, preparedClause : preparedRemaining) + + prepareClause inventory clause = do + (next, conditions) <- + prepareConditions inventory clause + (directClauseConditions clause) + pure + ( next + , PreparedInductiveClause + (directClauseVariables clause) + conditions + (directClauseResult clause) + ) + + prepareConditions inventory _clause [] = + pure (inventory, []) + prepareConditions inventory clause (condition : remaining) = do + (next, prepared) <- + prepareCondition inventory clause condition + (final, preparedRemaining) <- + prepareConditions next clause remaining + pure (final, prepared : preparedRemaining) + + prepareCondition inventory _clause (DirectSideCondition formula) = + pure (inventory, PreparedSideCondition formula) + prepareCondition + (MonotonicityInventory targets next facts contexts) + clause + (DirectRecursiveCondition recursiveTerm sourceContext) = do + checkedContext <- + prepareRecursiveCarrierTemplate + resolveGlobal + (variablesFor clause) + sourceContext + let template = checkedRecursiveCarrierTemplate checkedContext + withContext currentFacts = + MonotonicityInventory + targets next currentFacts (template : contexts) + if recursiveCarrierContextIsDirect sourceContext + then pure + ( withContext facts + , PreparedDirectRecursiveCondition + recursiveTerm checkedContext + ) + else do + target <- + prepareRecursiveCarrierMonotonicityTarget + checkedContext + let RecursiveCarrierContext location _source = sourceContext + case List.lookup target targets of + Just index -> + pure + ( MonotonicityInventory + targets next facts (template : contexts) + , PreparedNestedRecursiveCondition + recursiveTerm checkedContext index target + ) + Nothing -> + let index = importIx next + in pure + ( MonotonicityInventory + ((target, index) : targets) + (next + 1) + (PreparedTypedInductiveMonotonicity + location target : facts) + (template : contexts) + , PreparedNestedRecursiveCondition + recursiveTerm checkedContext index target + ) + +checkedRecursiveCarrierTemplate + :: CheckedRecursiveCarrierContext global + -> FrozenCheckedCore global +checkedRecursiveCarrierTemplate + (CheckedRecursiveCarrierContext _variables template) = + template + +recursiveCarrierContextIsDirect :: RecursiveCarrierContext -> Bool +recursiveCarrierContextIsDirect + (RecursiveCarrierContext _location source) = + source == TermVar RecursiveCarrierHole + +prepareRecursiveCarrierTemplate + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> [VarSymbol] + -> RecursiveCarrierContext + -> Either + TypedInductiveError + (CheckedRecursiveCarrierContext (InductiveGlobal global)) +prepareRecursiveCarrierTemplate resolveGlobal variables context = do + body <- + buildUnderVariables emptyEnvironment variables \environment -> do + underHole <- shiftEnvironment environment + lowerRecursiveCarrierContext + resolveGlobal underHole (CBound 0) context + checked <- + first TypedInductiveCoreError + (checkCanonicalCore + (Just . inductiveGlobalType) + -- Transparent expansion may leave beta redexes. Freeze one + -- normalized template so routing, generated laws, and kernel + -- transport all see the same first-order shape. + (betaNormalizeCanonical + (closeLambdas (length variables + 1) body))) + pure (CheckedRecursiveCarrierContext variables checked) + +prepareRecursiveCarrierMonotonicityTarget + :: CheckedRecursiveCarrierContext (InductiveGlobal global) + -> Either + TypedInductiveError + (FrozenCheckedCore (InductiveGlobal global)) +prepareRecursiveCarrierMonotonicityTarget + context@(CheckedRecursiveCarrierContext variables _template) = do + target <- + buildUnderVariables emptyEnvironment variables \environment -> do + underSets <- shiftEnvironment =<< shiftEnvironment environment + left <- + instantiateRecursiveCarrier + underSets (CBound 1) context + right <- + instantiateRecursiveCarrier + underSets (CBound 0) context + pure + (CImp + (subsetTerm (CBound 1) (CBound 0)) + (subsetTerm left right)) + freezeClosedTarget + (closeForalls (length variables + 2) target) + +instantiateRecursiveCarrier + :: InductiveEnvironment + -> CanonicalTerm (InductiveGlobal global) + -> CheckedRecursiveCarrierContext (InductiveGlobal global) + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +instantiateRecursiveCarrier environment replacement + context@(CheckedRecursiveCarrierContext variables _template) = do + arguments <- traverse (`lookupEnvironment` environment) variables + foldM instantiateLambda + (frozenCoreTerm (checkedRecursiveCarrierTemplate context)) + (arguments <> [replacement]) + where + instantiateLambda term argument = + case term of + CLam TySet body -> + pure (instantiateCanonical argument body) + _ -> + Left + (TypedInductiveUnsupportedExpression + "a checked recursive carrier context lost its set telescope") + +lowerRecursiveCarrierContext + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> InductiveEnvironment + -> CanonicalTerm (InductiveGlobal global) + -> RecursiveCarrierContext + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +lowerRecursiveCarrierContext resolveGlobal environment replacement + (RecursiveCarrierContext _location source) = + go source + where + go = \case + TermVar RecursiveCarrierHole -> + pure replacement + TermVar (RecursiveCarrierSourceVariable variable) -> + lookupEnvironment variable environment + TermSymbol _location symbol arguments -> do + lowered <- traverse go arguments + lowerApplicationTerms resolveGlobal symbol lowered + _ -> + Left + (TypedInductiveUnsupportedExpression + "a validated recursive carrier context left the supported set-term fragment") + +prepareCarrierBody + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> PreparedInductiveSource (InductiveGlobal global) + -> Either + TypedInductiveError (FrozenCheckedCore (InductiveGlobal global)) prepareCarrierBody resolveGlobal inductive = do body <- buildUnderVariables emptyEnvironment - (directInductiveParams + (preparedInductiveParams inductive) (\env -> fixedPointTerm resolveGlobal @@ -420,8 +830,8 @@ prepareCarrierBody resolveGlobal inductive = do env) let closed = closeLambdas - (length - (directInductiveParams + (length + (preparedInductiveParams inductive)) body checked <- @@ -431,14 +841,14 @@ prepareCarrierBody resolveGlobal inductive = do closed) pure checked -prepareGuardTarget +prepareDirectGuardTarget :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) -> DirectInductive -> DirectInductiveClause -> Either TypedInductiveError (FrozenCheckedCore (InductiveGlobal global)) -prepareGuardTarget +prepareDirectGuardTarget resolveGlobal inductive clause = do @@ -456,7 +866,7 @@ prepareGuardTarget inductive) conditions <- traverse - (conditionTerm + (directConditionTerm resolveGlobal environment domain) @@ -515,7 +925,7 @@ prepareFacts :: CheckedFoundation -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) -> Marker - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> NonEmpty (PreparedInductiveGuard (InductiveGlobal global)) -> Either TypedInductiveError @@ -545,7 +955,7 @@ prepareFacts (0 :| [1 ..]) (NonEmpty.zip guards - (directInductiveClauses + (preparedInductiveClauses inductive))) domainSubset <- first @@ -583,9 +993,9 @@ prepareIntroductionFact :: CheckedFoundation -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) -> Marker - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> Natural - -> (PreparedInductiveGuard (InductiveGlobal global), DirectInductiveClause) + -> (PreparedInductiveGuard (InductiveGlobal global), PreparedInductiveClause (InductiveGlobal global)) -> Either TypedInductiveError (PreparedTypedInductiveFact (InductiveGlobal global)) @@ -602,15 +1012,15 @@ prepareIntroductionFact foundation (Just . inductiveGlobalType)) emptyEnvironment - (directInductiveParams inductive - <> directClauseVariables clause) + (preparedInductiveParams inductive + <> preparedClauseVariables clause) (\context environment -> do domain <- checkedTerm context =<< lowerTerm resolveGlobal environment - (directInductiveDomain + (preparedInductiveDomain inductive) operator <- checkedTerm context @@ -646,14 +1056,14 @@ prepareIntroductionFact environment (scopedCoreTerm fixedPoint)) - (directClauseConditions + (preparedClauseConditions clause) result <- checkedTerm context =<< lowerTerm resolveGlobal environment - (directClauseResult + (preparedClauseResult clause) let conditionTerms = scopedCoreTerm <$> conditions @@ -675,18 +1085,18 @@ prepareIntroductionFact (eliminateWrittenForalls context environment - (directInductiveParams + (preparedInductiveParams inductive - <> directClauseVariables + <> preparedClauseVariables clause) guardProof) guardPremiseProofs <- sequence [ case condition of - DirectSideCondition _formula -> + PreparedSideCondition _formula -> pure premiseProof - DirectRecursiveCondition - recursiveTerm -> do + PreparedDirectRecursiveCondition + recursiveTerm _context -> do bound <- first TypedInductiveProofError @@ -713,9 +1123,32 @@ prepareIntroductionFact context implication premiseProof) + nested@PreparedNestedRecursiveCondition{} -> do + bound <- + first TypedInductiveProofError + (setLfpBoundProof + context + domain + operator) + recursiveElement <- + checkedTerm context + =<< lowerTerm + resolveGlobal + environment + (preparedRecursiveTerm + nested) + transportNestedRecursiveMembership + context + environment + nested + fixedPoint + domain + recursiveElement + bound + premiseProof | (condition, premiseProof) <- zip - (directClauseConditions + (preparedClauseConditions clause) premiseProofs ] @@ -841,14 +1274,16 @@ prepareIntroductionFact marker (clauseIndex + 1)) (if any isRecursiveCondition - (directClauseConditions clause) + (preparedClauseConditions clause) then SetLfpBound :| [SetLfpFixed] else SetLfpFixed :| []) + True proof where isRecursiveCondition = \case - DirectRecursiveCondition{} -> True - DirectSideCondition{} -> False + PreparedDirectRecursiveCondition{} -> True + PreparedNestedRecursiveCondition{} -> True + PreparedSideCondition{} -> False preparedGuardProof :: ProofContext (InductiveGlobal global) @@ -868,7 +1303,7 @@ prepareDomainSubsetFact :: CheckedFoundation -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) -> Marker - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> Either TypedInductiveError (PreparedTypedInductiveFact (InductiveGlobal global)) @@ -883,7 +1318,7 @@ prepareDomainSubsetFact foundation (Just . inductiveGlobalType)) emptyEnvironment - (directInductiveParams + (preparedInductiveParams inductive) (\context environment -> do domain <- @@ -891,7 +1326,7 @@ prepareDomainSubsetFact =<< lowerTerm resolveGlobal environment - (directInductiveDomain + (preparedInductiveDomain inductive) operator <- checkedTerm context @@ -907,13 +1342,14 @@ prepareDomainSubsetFact preparedFact (derivedMarker marker "dom_subset") (SetLfpBound :| []) + False proof prepareCasesFact :: CheckedFoundation -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) -> Marker - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> Either TypedInductiveError (PreparedTypedInductiveFact (InductiveGlobal global)) @@ -928,7 +1364,7 @@ prepareCasesFact foundation (Just . inductiveGlobalType)) emptyEnvironment - (directInductiveParams + (preparedInductiveParams inductive) (\parameterContext parameterEnvironment -> forallIntroductionTyped @@ -943,7 +1379,7 @@ prepareCasesFact =<< lowerTerm resolveGlobal environment - (directInductiveDomain + (preparedInductiveDomain inductive) operator <- checkedTerm context @@ -1058,13 +1494,14 @@ prepareCasesFact preparedFact (derivedMarker marker "cases") (SetLfpFixed :| []) + True proof prepareInductionFact :: CheckedFoundation -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) -> Marker - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> Either TypedInductiveError (PreparedTypedInductiveFact (InductiveGlobal global)) @@ -1079,7 +1516,7 @@ prepareInductionFact foundation (Just . inductiveGlobalType)) emptyEnvironment - (directInductiveParams + (preparedInductiveParams inductive) (\parameterContext parameterEnvironment -> forallIntroductionTyped @@ -1123,7 +1560,7 @@ prepareInductionFact =<< lowerTerm resolveGlobal elementEnvironment - (directInductiveDomain + (preparedInductiveDomain inductive) operator <- checkedTerm elementContext @@ -1201,6 +1638,7 @@ prepareInductionFact preparedFact (derivedMarker marker "induct") (SetLfpInduct :| []) + True proof proveUnderVariables @@ -1248,11 +1686,12 @@ checkedTerm context = preparedFact :: Marker -> NonEmpty KernelRuleTag + -> Bool -> BuiltProof (InductiveGlobal global) -> Either TypedInductiveError (PreparedTypedInductiveFact (InductiveGlobal global)) -preparedFact marker rules proof = do +preparedFact marker rules requiresMonotonicities proof = do target <- maybe (Left TypedInductiveProofRemainedOpen) @@ -1264,6 +1703,7 @@ preparedFact marker rules proof = do ( marker , target , canonicalRules rules + , requiresMonotonicities , builtProofDerivation proof )) where @@ -1407,8 +1847,8 @@ projectConjunctionList context terms proof = do introduceClauseWitnesses :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive - -> DirectInductiveClause + -> PreparedInductiveSource (InductiveGlobal global) + -> PreparedInductiveClause (InductiveGlobal global) -> ProofContext (InductiveGlobal global) -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) @@ -1427,7 +1867,7 @@ introduceClauseWitnesses result bodyProof = introduce - (directClauseVariables clause) + (preparedClauseVariables clause) where introduce [] = pure bodyProof @@ -1477,7 +1917,7 @@ introduceClauseWitnesses clauseFormulaWithBinders :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductiveClause + -> PreparedInductiveClause (InductiveGlobal global) -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) -> CanonicalTerm (InductiveGlobal global) @@ -1498,13 +1938,13 @@ clauseFormulaWithBinders resolveGlobal environment candidate) - (directClauseConditions + (preparedClauseConditions clause) clauseResult <- lowerTerm resolveGlobal environment - (directClauseResult clause) + (preparedClauseResult clause) pure (fromMaybe (CEq TySet result clauseResult) @@ -1608,7 +2048,7 @@ injectDisjunction context index alternatives proof = closureTerms :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) -> Either @@ -1621,18 +2061,18 @@ closureTerms subset = traverse closureFor (NonEmpty.toList - (directInductiveClauses + (preparedInductiveClauses inductive)) where closureFor clause = do clauseEnvironment <- extendVariables environment - (directClauseVariables clause) + (preparedClauseVariables clause) let binderCount = fromIntegral (length - (directClauseVariables + (preparedClauseVariables clause)) subset' = shiftCanonicalTerm @@ -1645,17 +2085,17 @@ closureTerms resolveGlobal clauseEnvironment subset') - (directClauseConditions + (preparedClauseConditions clause) result <- lowerTerm resolveGlobal clauseEnvironment - (directClauseResult clause) + (preparedClauseResult clause) pure (closeForalls (length - (directClauseVariables + (preparedClauseVariables clause)) (impliesIfNeeded (conjunctionList conditions) @@ -1666,7 +2106,7 @@ closureTerms proveBoundedMonotonicity :: CheckedFoundation -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> ProofContext (InductiveGlobal global) -> InductiveEnvironment -> Either @@ -1683,7 +2123,7 @@ proveBoundedMonotonicity =<< lowerTerm resolveGlobal environment - (directInductiveDomain + (preparedInductiveDomain inductive) operator <- checkedTerm context @@ -1712,7 +2152,7 @@ proveBoundedMonotonicity =<< lowerTerm resolveGlobal elementEnvironment - (directInductiveDomain + (preparedInductiveDomain inductive) predicate <- checkedTerm elementContext @@ -1787,7 +2227,7 @@ proveBoundedMonotonicity =<< lowerTerm resolveGlobal xyEnvironment - (directInductiveDomain + (preparedInductiveDomain inductive) relation <- checkedTerm xyContext @@ -1843,7 +2283,7 @@ proveBoundedMonotonicity =<< lowerTerm resolveGlobal elementEnvironment - (directInductiveDomain + (preparedInductiveDomain inductive) predicateX <- checkedTerm @@ -2021,7 +2461,7 @@ proveBoundedMonotonicity transformPredicateProof :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> ProofContext (InductiveGlobal global) -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) @@ -2067,7 +2507,7 @@ transformPredicateProof (atNatural clauseIndex (NonEmpty.toList - (directInductiveClauses + (preparedInductiveClauses inductive))) first (TypedInductivePreparationContext @@ -2141,7 +2581,7 @@ transformPredicateProof transformClauseBody :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductiveClause + -> PreparedInductiveClause (InductiveGlobal global) -> ProofContext (InductiveGlobal global) -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) @@ -2168,13 +2608,13 @@ transformClauseBody resolveGlobal environment candidateX) - (directClauseConditions + (preparedClauseConditions clause) clauseResult <- lowerTerm resolveGlobal environment - (directClauseResult clause) + (preparedClauseResult clause) let equality = CEq TySet result clauseResult bodyTermsX = @@ -2191,9 +2631,10 @@ transformClauseBody transformedConditions <- sequence [ case condition of - DirectSideCondition _formula -> + PreparedSideCondition _formula -> pure conditionProof - DirectRecursiveCondition recursiveTerm -> do + PreparedDirectRecursiveCondition + recursiveTerm _context -> do recursiveElement <- checkedTerm context =<< lowerTerm @@ -2217,9 +2658,33 @@ transformClauseBody context implication conditionProof) + nested@PreparedNestedRecursiveCondition{} -> do + recursiveElement <- + checkedTerm context + =<< lowerTerm + resolveGlobal + environment + (preparedRecursiveTerm nested) + subsetProof <- + subsetRelationHypothesis + context + candidateX + candidateY + domain + left <- checkedTerm context candidateX + right <- checkedTerm context candidateY + transportNestedRecursiveMembership + context + environment + nested + left + right + recursiveElement + subsetProof + conditionProof | (condition, conditionProof) <- zip - (directClauseConditions clause) + (preparedClauseConditions clause) conditionProofs ] equalityProof <- @@ -2270,9 +2735,163 @@ subsetRelationHypothesis rightSubsetDomain relationProof) +preparedRecursiveTerm + :: PreparedInductiveCondition global + -> Term +preparedRecursiveTerm = \case + PreparedDirectRecursiveCondition term _context -> term + PreparedNestedRecursiveCondition term _context _index _target -> term + PreparedSideCondition{} -> + impossible "a side condition has no recursive element" + +transportNestedRecursiveMembership + :: ProofContext (InductiveGlobal global) + -> InductiveEnvironment + -> PreparedInductiveCondition (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> BuiltProof (InductiveGlobal global) + -> BuiltProof (InductiveGlobal global) + -> Either + TypedInductiveError + (BuiltProof (InductiveGlobal global)) +transportNestedRecursiveMembership + context + environment + condition + left + right + element + subsetProof + membership = do + monotonicity <- + nestedRecursiveMonotonicityProof + context environment condition left right subsetProof + implication <- + first TypedInductiveProofError + (forallEliminationProof + context monotonicity element) + first TypedInductiveProofError + (implicationEliminationProof + context implication membership) + +nestedRecursiveMonotonicityProof + :: ProofContext (InductiveGlobal global) + -> InductiveEnvironment + -> PreparedInductiveCondition (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> BuiltProof (InductiveGlobal global) + -> Either + TypedInductiveError + (BuiltProof (InductiveGlobal global)) +nestedRecursiveMonotonicityProof + context + environment + (PreparedNestedRecursiveCondition + _term + (CheckedRecursiveCarrierContext variables _template) + index + target) + left + right + subsetProof = do + theorem <- + first TypedInductiveProofError + (importedProof context index target) + specialized <- + eliminateWrittenForalls + context environment variables theorem + atLeft <- + first TypedInductiveProofError + (forallEliminationProof context specialized left) + atRight <- + first TypedInductiveProofError + (forallEliminationProof context atLeft right) + first TypedInductiveProofError + (implicationEliminationProof + context atRight subsetProof) +nestedRecursiveMonotonicityProof + _context _environment _condition _left _right _subsetProof = + Left + (TypedInductiveUnsupportedExpression + "nested carrier transport requires a monotonicity import") + +proveInductionCandidateSubset + :: ProofContext (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> ScopedCheckedCore (InductiveGlobal global) + -> Either + TypedInductiveError + (BuiltProof (InductiveGlobal global)) +proveInductionCandidateSubset + context fixedPoint predicate candidate subset = + proveSubset + context candidate subset + (\elementContext element membership -> do + fixedPointAtElement <- + first TypedInductiveCoreError + (weakenScopedCore + (Just . inductiveGlobalType) + TySet + fixedPoint) + predicateAtElement <- + first TypedInductiveCoreError + (weakenScopedCore + (Just . inductiveGlobalType) + TySet + predicate) + explicitMembership <- + checkedTerm elementContext + (memberTerm + (scopedCoreTerm element) + (apply2 + (CIntrinsic Sep) + (scopedCoreTerm fixedPointAtElement) + (scopedCoreTerm predicateAtElement))) + membership' <- + first TypedInductiveProofError + (conversionProof + elementContext membership explicitMembership) + characteristic <- + separationForward + elementContext + fixedPointAtElement + predicateAtElement + element + membership' + satisfies <- + first TypedInductiveProofError + (conjunctionRightProof + elementContext + (memberTerm + (scopedCoreTerm element) + (scopedCoreTerm fixedPointAtElement)) + (CApp + (scopedCoreTerm predicateAtElement) + (scopedCoreTerm element)) + characteristic) + expected <- + first TypedInductiveCoreError + (weakenScopedCore + (Just . inductiveGlobalType) + TySet + subset) + target <- + checkedTerm elementContext + (memberTerm + (scopedCoreTerm element) + (scopedCoreTerm expected)) + first TypedInductiveProofError + (conversionProof + elementContext satisfies target)) + eliminateClauseWitnesses :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductiveClause + -> PreparedInductiveClause (InductiveGlobal global) -> ProofContext (InductiveGlobal global) -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) @@ -2310,7 +2929,7 @@ eliminateClauseWitnesses initialResult initialProof initialTarget - (directClauseVariables clause) + (preparedClauseVariables clause) where go depth context environment candidate result proof target = \case [] -> @@ -2442,7 +3061,7 @@ eliminateDisjunctionAlternatives proveInductionClosure :: CheckedFoundation -> (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> ProofContext (InductiveGlobal global) -> InductiveEnvironment -> ScopedCheckedCore (InductiveGlobal global) @@ -2521,7 +3140,7 @@ proveInductionClosure =<< lowerTerm resolveGlobal elementEnvironment - (directInductiveDomain + (preparedInductiveDomain inductive) operatorPredicate <- checkedTerm withMember @@ -2620,7 +3239,7 @@ proveInductionClosure (atNatural clauseIndex (NonEmpty.toList - (directInductiveClauses + (preparedInductiveClauses inductive))) first (TypedInductivePreparationContext @@ -2688,9 +3307,9 @@ proveInductionClosure proveInductionClause :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> Natural - -> DirectInductiveClause + -> PreparedInductiveClause (InductiveGlobal global) -> ProofContext (InductiveGlobal global) -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) @@ -2724,13 +3343,13 @@ proveInductionClause (CIntrinsic Sep) fixedPoint predicate)) - (directClauseConditions + (preparedClauseConditions clause) clauseResult <- lowerTerm resolveGlobal environment - (directClauseResult clause) + (preparedClauseResult clause) let equality = CEq TySet result clauseResult bodyTerms = @@ -2750,9 +3369,10 @@ proveInductionClause closureConditionProofs <- sequence [ case condition of - DirectSideCondition _formula -> + PreparedSideCondition _formula -> pure conditionProof - DirectRecursiveCondition recursiveTerm -> do + PreparedDirectRecursiveCondition + recursiveTerm _context -> do recursiveElement <- checkedTerm context =<< lowerTerm @@ -2794,9 +3414,41 @@ proveInductionClause context predicateMembership expected) + nested@PreparedNestedRecursiveCondition{} -> do + recursiveElement <- + checkedTerm context + =<< lowerTerm + resolveGlobal + environment + (preparedRecursiveTerm nested) + fixedPoint' <- checkedTerm context fixedPoint + predicate' <- checkedTerm context predicate + candidate <- + checkedTerm context + (apply2 + (CIntrinsic Sep) + fixedPoint + predicate) + subset' <- checkedTerm context subset + candidateSubset <- + proveInductionCandidateSubset + context + fixedPoint' + predicate' + candidate + subset' + transportNestedRecursiveMembership + context + environment + nested + candidate + subset' + recursiveElement + candidateSubset + conditionProof | (condition, conditionProof) <- zip - (directClauseConditions clause) + (preparedClauseConditions clause) conditionProofs ] closureConjunction <- @@ -2840,7 +3492,7 @@ proveInductionClause (eliminateWrittenForalls context environment - (directClauseVariables clause) + (preparedClauseVariables clause) selectedClosure) resultMembership <- case closureConditionProofs of @@ -2951,7 +3603,7 @@ transportElementMembership predicateAt :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) -> CanonicalTerm (InductiveGlobal global) @@ -2974,7 +3626,7 @@ predicateAt clauseFormulaTerms :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) -> CanonicalTerm (InductiveGlobal global) @@ -2994,7 +3646,7 @@ clauseFormulaTerms candidate result) (NonEmpty.toList - (directInductiveClauses + (preparedInductiveClauses inductive)) clauseFormulaAt @@ -3002,7 +3654,7 @@ clauseFormulaAt -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) -> CanonicalTerm (InductiveGlobal global) - -> DirectInductiveClause + -> PreparedInductiveClause (InductiveGlobal global) -> Either TypedInductiveError (CanonicalTerm (InductiveGlobal global)) @@ -3015,11 +3667,11 @@ clauseFormulaAt clauseEnvironment <- extendVariables environment - (directClauseVariables clause) + (preparedClauseVariables clause) let binderCount = fromIntegral (length - (directClauseVariables + (preparedClauseVariables clause)) candidate' = shiftCanonicalTerm binderCount 0 candidate @@ -3031,17 +3683,17 @@ clauseFormulaAt resolveGlobal clauseEnvironment candidate') - (directClauseConditions + (preparedClauseConditions clause) clauseResult <- lowerTerm resolveGlobal clauseEnvironment - (directClauseResult clause) + (preparedClauseResult clause) pure (closeExistentials (length - (directClauseVariables + (preparedClauseVariables clause)) (fromMaybe (CEq TySet result' clauseResult) @@ -3101,7 +3753,7 @@ membershipPredicate context set = do operatorPredicateAt :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) -> Either @@ -3128,7 +3780,7 @@ operatorPredicateAt separationSetAt :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) -> Either @@ -3143,7 +3795,7 @@ separationSetAt lowerTerm resolveGlobal environment - (directInductiveDomain + (preparedInductiveDomain inductive) predicate <- operatorPredicateAt @@ -3472,7 +4124,7 @@ buildUnderVariables fixedPointTerm :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> InductiveEnvironment -> Either TypedInductiveError @@ -3482,7 +4134,7 @@ fixedPointTerm resolveGlobal inductive environment = do lowerTerm resolveGlobal environment - (directInductiveDomain + (preparedInductiveDomain inductive) operator <- operatorTerm @@ -3498,7 +4150,7 @@ fixedPointTerm resolveGlobal inductive environment = do operatorTerm :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) - -> DirectInductive + -> PreparedInductiveSource (InductiveGlobal global) -> InductiveEnvironment -> Either TypedInductiveError @@ -3510,7 +4162,7 @@ operatorTerm resolveGlobal inductive parameterEnvironment = do lowerTerm resolveGlobal candidateEnvironment - (directInductiveDomain + (preparedInductiveDomain inductive) resultEnvironment <- shiftEnvironment candidateEnvironment @@ -3519,7 +4171,7 @@ operatorTerm resolveGlobal inductive parameterEnvironment = do (clausePredicateTerm resolveGlobal resultEnvironment) - (directInductiveClauses + (preparedInductiveClauses inductive) pure (CLam TySet @@ -3535,7 +4187,7 @@ operatorTerm resolveGlobal inductive parameterEnvironment = do clausePredicateTerm :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) -> InductiveEnvironment - -> DirectInductiveClause + -> PreparedInductiveClause (InductiveGlobal global) -> Either TypedInductiveError (CanonicalTerm (InductiveGlobal global)) @@ -3546,11 +4198,11 @@ clausePredicateTerm clauseEnvironment <- extendVariables resultEnvironment - (directClauseVariables clause) + (preparedClauseVariables clause) let variableCount = fromIntegral (length - (directClauseVariables + (preparedClauseVariables clause)) resultVariable = CBound variableCount @@ -3562,18 +4214,18 @@ clausePredicateTerm resolveGlobal clauseEnvironment candidate) - (directClauseConditions + (preparedClauseConditions clause) result <- lowerTerm resolveGlobal clauseEnvironment - (directClauseResult + (preparedClauseResult clause) pure (closeExistentials (length - (directClauseVariables clause)) + (preparedClauseVariables clause)) (fromMaybe (CEq TySet @@ -3586,7 +4238,7 @@ clausePredicateTerm resultVariable result])))) -conditionTerm +directConditionTerm :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) -> InductiveEnvironment -> CanonicalTerm (InductiveGlobal global) @@ -3594,19 +4246,47 @@ conditionTerm -> Either TypedInductiveError (CanonicalTerm (InductiveGlobal global)) -conditionTerm resolveGlobal environment candidate = \case +directConditionTerm resolveGlobal environment candidate = \case DirectSideCondition formula -> + lowerFormula resolveGlobal environment formula + DirectRecursiveCondition term context -> do + carrier <- + betaNormalizeCanonical + <$> lowerRecursiveCarrierContext + resolveGlobal environment candidate context + memberTerm + <$> lowerTerm resolveGlobal environment term + <*> pure carrier + +conditionTerm + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> InductiveEnvironment + -> CanonicalTerm (InductiveGlobal global) + -> PreparedInductiveCondition (InductiveGlobal global) + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +conditionTerm resolveGlobal environment candidate = \case + PreparedSideCondition formula -> lowerFormula resolveGlobal environment formula - DirectRecursiveCondition term -> + PreparedDirectRecursiveCondition term context -> do + carrier <- + instantiateRecursiveCarrier environment candidate context memberTerm <$> lowerTerm resolveGlobal environment term - <*> pure candidate + <*> pure carrier + PreparedNestedRecursiveCondition term context _index _target -> do + carrier <- + instantiateRecursiveCarrier environment candidate context + memberTerm + <$> lowerTerm resolveGlobal environment term + <*> pure carrier shiftEnvironment :: InductiveEnvironment @@ -3708,7 +4388,7 @@ lowerFormulaWith allowQuantified resolveGlobal environment = \case <*> lowerFormulaWith allowQuantified resolveGlobal environment right Atomic _location predicate arguments -> - lowerApplication + lowerPredicateApplication resolveGlobal environment (SymbolPredicate predicate) @@ -3783,6 +4463,40 @@ lowerApplication resolveGlobal environment symbol arguments = do resolveGlobal environment) arguments + lowerApplicationTerms resolveGlobal symbol arguments' + +lowerPredicateApplication + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> InductiveEnvironment + -> Symbol + -> [Expr] + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +lowerPredicateApplication resolveGlobal environment symbol arguments = do + arguments' <- + traverse + (lowerTerm + resolveGlobal + environment) + arguments + case classifyExactSymbol symbol of + ExactFixedPrimitive meaning -> + maybe + (lowerApplicationTerms resolveGlobal symbol arguments') + Right + (lowerFixedEqualityPredicate meaning arguments') + _ -> + lowerApplicationTerms resolveGlobal symbol arguments' + +lowerApplicationTerms + :: (Symbol -> Maybe (SourceGlobal (InductiveGlobal global))) + -> Symbol + -> [CanonicalTerm (InductiveGlobal global)] + -> Either + TypedInductiveError + (CanonicalTerm (InductiveGlobal global)) +lowerApplicationTerms resolveGlobal symbol arguments' = case dispatchFixedSetTerm symbol arguments' of LoweredFixedSetTerm term -> pure term |