diff options
Diffstat (limited to 'source/Checking/Backend')
| -rw-r--r-- | source/Checking/Backend/Problem.hs | 211 |
1 files changed, 144 insertions, 67 deletions
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] |