diff options
Diffstat (limited to 'source/Checking/Backend/Problem.hs')
| -rw-r--r-- | source/Checking/Backend/Problem.hs | 224 |
1 files changed, 150 insertions, 74 deletions
diff --git a/source/Checking/Backend/Problem.hs b/source/Checking/Backend/Problem.hs index 61a31d2..1f51eb2 100644 --- a/source/Checking/Backend/Problem.hs +++ b/source/Checking/Backend/Problem.hs @@ -38,8 +38,7 @@ module Checking.Backend.Problem , typedProblemAuxiliaryTag , typedProblemAuxiliaryProposition , typedProblemAuxiliaryCapability - , GlobalPremiseMode(..) - , LocalPremisePolicy(..) + , PremiseSelectionMode(..) , selectTypedLocalPremises , TypedProblemRoute(..) , TypedProblem @@ -806,33 +805,44 @@ typedProblemAuxiliaryCapability capability -data GlobalPremiseMode - = ImplicitFofPremises - | ExplicitGlobalPremises - | NoGlobalPremises - deriving stock (Show, Eq) - -data LocalPremisePolicy - = FirstOrderLocals - | AllLocals +-- | Source justification policy for premise selection. Higher-order routing +-- is validated separately after the complete selected problem is known. +data PremiseSelectionMode + = ImplicitPremiseSelection + | ExplicitGlobalPremiseSelection + | LocalOnlyPremiseSelection deriving stock (Show, Eq) selectTypedLocalPremises - :: LocalPremisePolicy + :: PremiseSelectionMode -> [TypedLocalPremise local origin global] -> Vector (TypedLocalPremise local origin global) -selectTypedLocalPremises localPolicy availableLocals = +selectTypedLocalPremises selection availableLocals = Vector.fromList (List.sortOn typedLocalPremiseOrdinal - (case localPolicy of - FirstOrderLocals -> + (case selection of + ImplicitPremiseSelection -> + List.filter implicitLocalPremise availableLocals + ExplicitGlobalPremiseSelection -> List.filter (isFofCapability . typedLocalPremiseCapability) availableLocals - AllLocals -> + LocalOnlyPremiseSelection -> availableLocals)) + where + implicitLocalPremise premise = + isFofCapability (typedLocalPremiseCapability premise) + || isJust + (implicitConstructionAdmission + (typedLocalPremiseProposition premise) + (typedLocalPremiseCapability premise)) + +data ImplicitHigherOrderConstruction + = ImplicitSeparation + | ImplicitFunctionalReplacement + deriving stock (Show, Eq, Ord) data TypedProblemRoute = RouteFof @@ -855,9 +865,6 @@ data TypedProblemError local global !(BackendClassificationError global) | TypedProblemExplicitHigherOrderJustificationRequired !(NonEmpty BackendFofExclusion) - | TypedProblemInvalidPolicyCombination - !GlobalPremiseMode - !LocalPremisePolicy | TypedProblemDuplicateLocalPremiseOrdinal !LocalPremiseOrdinal | TypedProblemLocalTypeMismatch @@ -873,8 +880,7 @@ planTypedProblem -> SupportedProposition local global -> [TypedLocalPremise local origin global] -> [TypedFoundationAuxiliaryInput global] - -> GlobalPremiseMode - -> LocalPremisePolicy + -> PremiseSelectionMode -> Either (TypedProblemError local global) (TypedProblem ref local origin global) @@ -884,11 +890,7 @@ planTypedProblem claim availableLocals auxiliaries - globalPolicy - localPolicy = do - validatePolicyCombination - globalPolicy - localPolicy + selection = do validateLocalPremiseOrdinals availableLocals claimCapability <- @@ -899,25 +901,21 @@ planTypedProblem claim) let selectedLocals = selectTypedLocalPremises - localPolicy + selection availableLocals let preparedAuxiliaries = zipWith prepareAuxiliary [0..] auxiliaries - case globalPolicy of - ImplicitFofPremises -> - case implicitTh0Requirement - claimCapability - (typedProblemAuxiliaryCapability - <$> preparedAuxiliaries) of - Nothing -> - pure () - Just exclusions -> - Left - (TypedProblemExplicitHigherOrderJustificationRequired - exclusions) + case selection of + ImplicitPremiseSelection -> + validateImplicitHigherOrderAdmission + claim + claimCapability + selectedFacts + selectedLocals + preparedAuxiliaries _ -> pure () let selectedFofCapabilities = @@ -956,23 +954,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 +966,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] |