diff options
Diffstat (limited to 'source/Felix/Checking/Backend/Problem.hs')
| -rw-r--r-- | source/Felix/Checking/Backend/Problem.hs | 1301 |
1 files changed, 1301 insertions, 0 deletions
diff --git a/source/Felix/Checking/Backend/Problem.hs b/source/Felix/Checking/Backend/Problem.hs new file mode 100644 index 0000000..0390020 --- /dev/null +++ b/source/Felix/Checking/Backend/Problem.hs @@ -0,0 +1,1301 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Complete-problem FOF/TH0 classification and construction. +module Felix.Checking.Backend.Problem + ( SupportedProposition + , supportedProposition + , projectSupportedProposition + , supportedPropositionSupport + , supportedPropositionTerm + , weakenClosedSupportedProposition + , SupportedPropositionError(..) + , SupportedPropositionProjectionError(..) + , CheckedFofProjection + , checkedFofProjectionProposition + , FofCapability(..) + , BackendFofExclusion(..) + , BackendClassificationError(..) + , classifySupportedProposition + , TypedBackendFact + , typedBackendFact + , typedBackendFactReference + , typedBackendFactProposition + , typedBackendFactCapability + , LocalPremiseOrdinal + , localPremiseOrdinal + , localPremiseOrdinalValue + , TypedLocalPremise + , typedLocalPremise + , typedLocalPremiseOrdinal + , typedLocalPremiseOrigin + , typedLocalPremiseProposition + , typedLocalPremiseCapability + , TypedFoundationAuxiliaryInput + , typedFoundationAuxiliaryInput + , TypedProblemAuxiliary + , typedProblemAuxiliaryOrdinal + , typedProblemAuxiliaryTag + , typedProblemAuxiliaryProposition + , typedProblemAuxiliaryCapability + , LocalPremisePolicy(..) + , HigherOrderJustificationPolicy(..) + , selectTypedLocalPremises + , TypedProblemRoute(..) + , TypedProblem + , planTypedProblem + , typedProblemRoute + , typedProblemClaim + , typedProblemGlobalPremises + , typedProblemLocalPremises + , typedProblemAuxiliaries + , typedProblemGlobalTypes + , typedProblemLocalTypes + , TypedProblemError(..) + ) where + +import Base +import Felix.Checking.Core +import Felix.Checking.Foundation + +import Control.Monad (foldM, unless) +import Data.Bifunctor (first) +import Data.List qualified as List +import Data.Map.Strict qualified as Map +import Data.Set qualified as Set +import Data.Vector (Vector) +import Data.Vector qualified as Vector +import Numeric.Natural (Natural) + + +-- | A proposition under its exact nearest-first ambient-local support. +data SupportedProposition local global = + SupportedProposition + !(Vector (local, CoreType)) + !(ScopedCheckedCore global) + deriving stock (Eq) + +data SupportedPropositionError local + = SupportedPropositionIsNotProposition !CoreType + | SupportedPropositionContextMismatch + ![CoreType] + ![CoreType] + | DuplicateSupportedLocal !local + | UnusedSupportedLocal !local + deriving stock (Show, Eq) + +data SupportedPropositionProjectionError local + = SupportedProjectionContextMismatch + ![CoreType] + ![CoreType] + | SupportedProjectionDuplicateLocal !local + | SupportedProjectionIndexMissing !Natural + | SupportedProjectionCoreCheckFailed !CoreCheckError + | SupportedProjectionValidationFailed + !(SupportedPropositionError local) + deriving stock (Show, Eq) + +supportedProposition + :: Ord local + => Vector (local, CoreType) + -> ScopedCheckedCore global + -> Either + (SupportedPropositionError local) + (SupportedProposition local global) +supportedProposition support statement = do + unless + (scopedCoreType statement == TyProp) + (Left + (SupportedPropositionIsNotProposition + (scopedCoreType statement))) + let expectedContext = + snd <$> Vector.toList support + actualContext = + scopedCoreContext statement + unless + (actualContext == expectedContext) + (Left + (SupportedPropositionContextMismatch + expectedContext + actualContext)) + void + (foldM + (\seen (local, _coreType) -> + if local `Set.member` seen + then + Left + (DuplicateSupportedLocal local) + else + Right (Set.insert local seen)) + Set.empty + support) + case + List.find + (\(ordinal, _entry) -> + fromIntegral ordinal + `Set.notMember` + ambientIndices + (scopedCoreTerm statement)) + (Vector.toList + (Vector.indexed support)) of + Just (_ordinal, (local, _coreType)) -> + Left (UnusedSupportedLocal local) + Nothing -> + pure () + pure + (SupportedProposition + support + statement) + +-- | Retain exactly the ambient locals used by a checked proposition and +-- remap its indices to that dense nearest-first support. +projectSupportedProposition + :: Ord local + => (global -> Maybe CoreType) + -> Vector (local, CoreType) + -> ScopedCheckedCore global + -> Either + (SupportedPropositionProjectionError local) + (SupportedProposition local global) +projectSupportedProposition globalType available statement = do + let expectedContext = snd <$> Vector.toList available + actualContext = scopedCoreContext statement + unless (expectedContext == actualContext) + (Left + (SupportedProjectionContextMismatch + expectedContext + actualContext)) + void + (foldM + (\seen (local, _coreType) -> + if local `Set.member` seen + then Left (SupportedProjectionDuplicateLocal local) + else Right (Set.insert local seen)) + Set.empty + available) + let used = + Set.toAscList + (ambientIndices + (scopedCoreTerm statement)) + selected <- traverse (lookupNatural available) used + let remapping = + Map.fromAscList + (zip used [0 ..]) + remapped <- remapAmbientIndices remapping 0 + (scopedCoreTerm statement) + checked <- + first SupportedProjectionCoreCheckFailed + (checkScopedCanonicalCore + globalType + (snd <$> selected) + remapped) + first SupportedProjectionValidationFailed + (supportedProposition + (Vector.fromList selected) + checked) + where + lookupNatural values index = + maybe + (Left (SupportedProjectionIndexMissing index)) + Right + (go index (Vector.toList values)) + + go _index [] = + Nothing + go 0 (value : _rest) = + Just value + go index (_value : rest) = + go (index - 1) rest + + remapAmbientIndices remapping depth = \case + CBound index + | index < depth -> + Right (CBound index) + | otherwise -> + maybe + (Left + (SupportedProjectionIndexMissing + (index - depth))) + (Right . CBound . (+ depth)) + (Map.lookup (index - depth) remapping) + CGlobal global -> + Right (CGlobal global) + CIntrinsic intrinsic -> + Right (CIntrinsic intrinsic) + COpaqueInteger integer -> + Right (COpaqueInteger integer) + CApp function argument -> + CApp + <$> remapAmbientIndices remapping depth function + <*> remapAmbientIndices remapping depth argument + CLam binderType body -> + CLam binderType + <$> remapAmbientIndices remapping (depth + 1) body + CFalsum -> + Right CFalsum + CImp premise conclusion -> + CImp + <$> remapAmbientIndices remapping depth premise + <*> remapAmbientIndices remapping depth conclusion + CEq operandType left right -> + CEq operandType + <$> remapAmbientIndices remapping depth left + <*> remapAmbientIndices remapping depth right + CForall binderType body -> + CForall binderType + <$> remapAmbientIndices remapping (depth + 1) body + +ambientIndices + :: CanonicalTerm global + -> Set Natural +ambientIndices = + go 0 + where + go depth = \case + CBound index + | index < depth -> + mempty + | otherwise -> + Set.singleton (index - depth) + CGlobal{} -> + mempty + CIntrinsic{} -> + mempty + COpaqueInteger{} -> + mempty + CApp function argument -> + go depth function <> go depth argument + CLam _binderType body -> + go (depth + 1) body + CFalsum -> + mempty + CImp premise conclusion -> + go depth premise <> go depth conclusion + CEq _operandType left right -> + go depth left <> go depth right + CForall _binderType body -> + go (depth + 1) body + +supportedPropositionSupport + :: SupportedProposition local global + -> Vector (local, CoreType) +supportedPropositionSupport + (SupportedProposition support _statement) = + support + +supportedPropositionTerm + :: SupportedProposition local global + -> CanonicalTerm global +supportedPropositionTerm + (SupportedProposition _support statement) = + scopedCoreTerm statement + +weakenClosedSupportedProposition + :: SupportedProposition Void global + -> SupportedProposition local global +weakenClosedSupportedProposition + (SupportedProposition support statement) = + SupportedProposition + (fmap + (\(local, coreType) -> + (absurd local, coreType)) + support) + statement + + +newtype CheckedFofProjection local global = + CheckedFofProjection + (SupportedProposition local global) + deriving stock (Eq) + +checkedFofProjectionProposition + :: CheckedFofProjection local global + -> SupportedProposition local global +checkedFofProjectionProposition + (CheckedFofProjection proposition) = + proposition + +data FofCapability projection + = FofProjectable !projection + | RequiresTh0 !(NonEmpty BackendFofExclusion) + deriving stock (Eq) + +data BackendFofExclusion + = StructuralFofExclusion !FofExclusion + | HigherOrderGlobalType !CoreType + | HigherOrderAmbientLocal !CoreType + deriving stock (Show, Eq, Ord) + +data BackendClassificationError global + = UnknownBackendGlobal !global + | BackendFofProjectionInvariantFailed + deriving stock (Show, Eq) + +classifySupportedProposition + :: Ord global + => (global -> Maybe CoreType) + -> SupportedProposition local global + -> Either + (BackendClassificationError global) + (FofCapability + (CheckedFofProjection local global)) +classifySupportedProposition globalType proposition = do + globalExclusions <- + foldM + collectGlobal + Set.empty + (Set.toAscList + (canonicalGlobals + (supportedPropositionTerm proposition))) + let structuralExclusions = + case classifyScopedStructure proposition of + FoundationFofProjectable -> + Set.empty + FoundationRequiresTh0 structural -> + Set.fromList + (StructuralFofExclusion + <$> toList structural) + localExclusions = + Set.fromList + [ HigherOrderAmbientLocal coreType + | (_local, coreType) <- + Vector.toList + (supportedPropositionSupport + proposition) + , coreType /= TySet + ] + exclusions = + structuralExclusions + <> globalExclusions + <> localExclusions + case Set.toAscList exclusions of + [] -> + if isFirstOrderProposition + globalType + proposition + then + Right + (FofProjectable + (CheckedFofProjection + proposition)) + else + Left BackendFofProjectionInvariantFailed + firstExclusion : remainingExclusions -> + Right + (RequiresTh0 + (firstExclusion + :| remainingExclusions)) + where + collectGlobal exclusions global = + case globalType global of + Nothing -> + Left (UnknownBackendGlobal global) + Just coreType -> + Right + (if isFirstOrderGlobalType coreType + then exclusions + else + Set.insert + (HigherOrderGlobalType + coreType) + exclusions) + +classifyScopedStructure + :: SupportedProposition local global + -> FoundationBackendClass +classifyScopedStructure = + classifyCanonicalFofStructure + . supportedPropositionTerm + +isFirstOrderGlobalType :: CoreType -> Bool +isFirstOrderGlobalType = + go + where + go = \case + TySet -> + True + TyProp -> + True + TyArrow TySet result -> + go result + TyArrow _argument _result -> + False + +-- The structural and type exclusions make this projection total. This final +-- walk catches an accidentally unsaturated first-order head. +isFirstOrderProposition + :: (global -> Maybe CoreType) + -> SupportedProposition local global + -> Bool +isFirstOrderProposition globalType proposition = + isFormula initialContext + (supportedPropositionTerm proposition) + where + initialContext = + snd + <$> Vector.toList + (supportedPropositionSupport + proposition) + + isFormula context = \case + CFalsum -> + True + CImp premise conclusion -> + isFormula context premise + && isFormula context conclusion + CEq TySet left right -> + isTerm context left + && isTerm context right + CEq TyProp left right -> + isFormula context left + && isFormula context right + CForall TySet body -> + isFormula (TySet : context) body + application -> + case applicationHead application of + (CGlobal global, arguments) -> + maybe + False + (\coreType -> + applicationResult + coreType + arguments + == Just TyProp + && all + (isTerm context) + arguments) + (globalType global) + (CIntrinsic intrinsic, arguments) -> + applicationResult + (coreIntrinsicType intrinsic) + arguments + == Just TyProp + && all + (isTerm context) + arguments + _ -> + False + + isTerm context = \case + CBound index -> + contextAt index context + == Just TySet + CGlobal global -> + globalType global == Just TySet + CIntrinsic intrinsic -> + coreIntrinsicType intrinsic == TySet + COpaqueInteger{} -> + True + application -> + case applicationHead application of + (CGlobal global, arguments) -> + maybe + False + (\coreType -> + applicationResult + coreType + arguments + == Just TySet + && all + (isTerm context) + arguments) + (globalType global) + (CIntrinsic intrinsic, arguments) -> + applicationResult + (coreIntrinsicType intrinsic) + arguments + == Just TySet + && all + (isTerm context) + arguments + _ -> + False + +applicationHead + :: CanonicalTerm global + -> (CanonicalTerm global, [CanonicalTerm global]) +applicationHead = + go [] + where + go arguments = \case + CApp function argument -> + go (argument : arguments) function + headTerm -> + (headTerm, arguments) + +applicationResult + :: CoreType + -> [CanonicalTerm global] + -> Maybe CoreType +applicationResult = + foldM + (\coreType _argument -> + case coreType of + TyArrow TySet result -> + Just result + _ -> + Nothing) + +contextAt :: Natural -> [value] -> Maybe value +contextAt _index [] = + Nothing +contextAt 0 (value : _remaining) = + Just value +contextAt index (_value : remaining) = + contextAt (index - 1) remaining + +canonicalGlobals + :: Ord global + => CanonicalTerm global + -> Set global +canonicalGlobals = \case + CBound{} -> + mempty + CGlobal global -> + Set.singleton global + CIntrinsic{} -> + mempty + COpaqueInteger{} -> + mempty + CApp function argument -> + canonicalGlobals function + <> canonicalGlobals argument + CLam _binderType body -> + canonicalGlobals body + CFalsum -> + mempty + CImp premise conclusion -> + canonicalGlobals premise + <> canonicalGlobals conclusion + CEq _operandType left right -> + canonicalGlobals left + <> canonicalGlobals right + CForall _binderType body -> + canonicalGlobals body + + +data TypedBackendFact ref global = + TypedBackendFact + !ref + !(SupportedProposition Void global) + !(FofCapability + (CheckedFofProjection Void global)) + deriving stock (Eq) + +typedBackendFact + :: ref + -> SupportedProposition Void global + -> FofCapability + (CheckedFofProjection Void global) + -> TypedBackendFact ref global +typedBackendFact = + TypedBackendFact + +typedBackendFactReference + :: TypedBackendFact ref global + -> ref +typedBackendFactReference + (TypedBackendFact + reference + _proposition + _capability) = + reference + +typedBackendFactProposition + :: TypedBackendFact ref global + -> SupportedProposition Void global +typedBackendFactProposition + (TypedBackendFact + _reference + proposition + _capability) = + proposition + +typedBackendFactCapability + :: TypedBackendFact ref global + -> FofCapability + (CheckedFofProjection Void global) +typedBackendFactCapability + (TypedBackendFact + _reference + _proposition + capability) = + capability + + +newtype LocalPremiseOrdinal = + LocalPremiseOrdinal Natural + deriving stock (Show, Eq, Ord) + +localPremiseOrdinal :: Natural -> LocalPremiseOrdinal +localPremiseOrdinal = + LocalPremiseOrdinal + +localPremiseOrdinalValue + :: LocalPremiseOrdinal + -> Natural +localPremiseOrdinalValue + (LocalPremiseOrdinal ordinal) = + ordinal + +data TypedLocalPremise local origin global = + TypedLocalPremise + !LocalPremiseOrdinal + !origin + !(SupportedProposition local global) + !(FofCapability + (CheckedFofProjection local global)) + deriving stock (Eq) + +typedLocalPremise + :: Ord global + => (global -> Maybe CoreType) + -> LocalPremiseOrdinal + -> origin + -> SupportedProposition local global + -> Either + (BackendClassificationError global) + (TypedLocalPremise local origin global) +typedLocalPremise globalType ordinal premiseOrigin proposition = + TypedLocalPremise + ordinal + premiseOrigin + proposition + <$> classifySupportedProposition + globalType + proposition + +typedLocalPremiseOrdinal + :: TypedLocalPremise local origin global + -> LocalPremiseOrdinal +typedLocalPremiseOrdinal + (TypedLocalPremise + ordinal + _origin + _proposition + _capability) = + ordinal + +typedLocalPremiseOrigin + :: TypedLocalPremise local origin global + -> origin +typedLocalPremiseOrigin + (TypedLocalPremise + _ordinal + premiseOrigin + _proposition + _capability) = + premiseOrigin + +typedLocalPremiseProposition + :: TypedLocalPremise local origin global + -> SupportedProposition local global +typedLocalPremiseProposition + (TypedLocalPremise + _ordinal + _origin + proposition + _capability) = + proposition + +typedLocalPremiseCapability + :: TypedLocalPremise local origin global + -> FofCapability + (CheckedFofProjection local global) +typedLocalPremiseCapability + (TypedLocalPremise + _ordinal + _origin + _proposition + capability) = + capability + + +data TypedFoundationAuxiliaryInput global = + TypedFoundationAuxiliaryInput + !FoundationAxiomTag + !(SupportedProposition Void global) + !(FofCapability + (CheckedFofProjection Void global)) + +typedFoundationAuxiliaryInput + :: CheckedFoundation + -> FoundationAxiomTag + -> TypedFoundationAuxiliaryInput global +typedFoundationAuxiliaryInput foundation tag = + TypedFoundationAuxiliaryInput + tag + proposition + capability + where + proposition = + SupportedProposition + Vector.empty + (embedClosedCore + [] + (mapFrozenGlobals + absurd + (foundationAxiomFrozen + foundation + tag))) + capability = + case foundationAxiomBackendClass + foundation + tag of + FoundationFofProjectable -> + FofProjectable + (CheckedFofProjection + proposition) + FoundationRequiresTh0 exclusions -> + RequiresTh0 + (StructuralFofExclusion + <$> exclusions) + +data TypedProblemAuxiliary global = + TypedProblemAuxiliary + !Natural + !FoundationAxiomTag + !(SupportedProposition Void global) + !(FofCapability + (CheckedFofProjection Void global)) + deriving stock (Eq) + +typedProblemAuxiliaryOrdinal + :: TypedProblemAuxiliary global + -> Natural +typedProblemAuxiliaryOrdinal + (TypedProblemAuxiliary + ordinal + _tag + _proposition + _capability) = + ordinal + +typedProblemAuxiliaryTag + :: TypedProblemAuxiliary global + -> FoundationAxiomTag +typedProblemAuxiliaryTag + (TypedProblemAuxiliary + _ordinal + tag + _proposition + _capability) = + tag + +typedProblemAuxiliaryProposition + :: TypedProblemAuxiliary global + -> SupportedProposition Void global +typedProblemAuxiliaryProposition + (TypedProblemAuxiliary + _ordinal + _tag + proposition + _capability) = + proposition + +typedProblemAuxiliaryCapability + :: TypedProblemAuxiliary global + -> FofCapability + (CheckedFofProjection Void global) +typedProblemAuxiliaryCapability + (TypedProblemAuxiliary + _ordinal + _tag + _proposition + capability) = + capability + + +-- | Source justification policy for premise selection. Higher-order routing +-- is validated separately after the complete selected problem is known. +data LocalPremisePolicy + = FirstOrderLocals + | 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 selection availableLocals = + Vector.fromList + (List.sortOn + typedLocalPremiseOrdinal + (case selection of + FirstOrderLocals -> + List.filter + (isFofCapability + . typedLocalPremiseCapability) + availableLocals + CompleteLocals -> + availableLocals)) + +data ImplicitHigherOrderConstruction + = ImplicitSeparation + | ImplicitFunctionalReplacement + deriving stock (Show, Eq, Ord) + +data TypedProblemRoute + = RouteFof + | RouteTh0 + deriving stock (Show, Eq) + +data TypedProblem ref local origin global = + TypedProblem + !TypedProblemRoute + !(SupportedProposition local global) + !(Vector (TypedBackendFact ref global)) + !(Vector (TypedLocalPremise local origin global)) + !(Vector (TypedProblemAuxiliary global)) + !(Map global CoreType) + !(Map local CoreType) + deriving stock (Eq) + +data TypedProblemError local global + = TypedProblemClaimClassificationFailed + !(BackendClassificationError global) + | TypedProblemExplicitHigherOrderJustificationRequired + !(NonEmpty BackendFofExclusion) + | TypedProblemDuplicateLocalPremiseOrdinal + !LocalPremiseOrdinal + | TypedProblemLocalTypeMismatch + !local + !CoreType + !CoreType + deriving stock (Show, Eq) + +planTypedProblem + :: (Ord local, Ord global) + => (global -> Maybe CoreType) + -> Vector (TypedBackendFact ref global) + -> SupportedProposition local global + -> [TypedLocalPremise local origin global] + -> [TypedFoundationAuxiliaryInput global] + -> LocalPremisePolicy + -> HigherOrderJustificationPolicy + -> Either + (TypedProblemError local global) + (TypedProblem ref local origin global) +planTypedProblem + globalType + selectedFacts + claim + availableLocals + auxiliaries + localPolicy + higherOrderPolicy = do + validateLocalPremiseOrdinals + availableLocals + claimCapability <- + first + TypedProblemClaimClassificationFailed + (classifySupportedProposition + globalType + claim) + let selectedLocals = + selectTypedLocalPremises + localPolicy + availableLocals + let preparedAuxiliaries = + zipWith + prepareAuxiliary + [0..] + auxiliaries + case higherOrderPolicy of + ImplicitConstructionJustification -> + validateImplicitHigherOrderAdmission + claim + claimCapability + selectedFacts + selectedLocals + preparedAuxiliaries + ExplicitHigherOrderJustification -> + pure () + let selectedFofCapabilities = + isFofCapability claimCapability + : (isFofCapability + . typedBackendFactCapability + <$> Vector.toList selectedFacts) + <> (isFofCapability + . typedLocalPremiseCapability + <$> Vector.toList selectedLocals) + <> (isFofCapability + . typedProblemAuxiliaryCapability + <$> preparedAuxiliaries) + route = + if and selectedFofCapabilities + then RouteFof + else RouteTh0 + globalTypes <- + collectProblemGlobals + globalType + claim + selectedFacts + selectedLocals + preparedAuxiliaries + localTypes <- + collectProblemLocals + claim + selectedLocals + pure + (TypedProblem + route + claim + selectedFacts + selectedLocals + (Vector.fromList preparedAuxiliaries) + globalTypes + localTypes) + where + prepareAuxiliary + ordinal + (TypedFoundationAuxiliaryInput + tag + proposition + capability) = + TypedProblemAuxiliary + ordinal + tag + proposition + capability + +-- | 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 + _ -> + False + +validateLocalPremiseOrdinals + :: [TypedLocalPremise local origin global] + -> Either + (TypedProblemError local global) + () +validateLocalPremiseOrdinals = + void + . foldM + (\seen premise -> + let ordinal = + typedLocalPremiseOrdinal premise + in + if ordinal `Set.member` seen + then + Left + (TypedProblemDuplicateLocalPremiseOrdinal + ordinal) + else + Right + (Set.insert + ordinal + seen)) + Set.empty + +isFofCapability :: FofCapability projection -> Bool +isFofCapability = \case + FofProjectable{} -> + True + RequiresTh0{} -> + False + +collectProblemGlobals + :: Ord global + => (global -> Maybe CoreType) + -> SupportedProposition local global + -> Vector (TypedBackendFact ref global) + -> Vector (TypedLocalPremise local origin global) + -> [TypedProblemAuxiliary global] + -> Either + (TypedProblemError local global) + (Map global CoreType) +collectProblemGlobals + globalType + claim + facts + locals + auxiliaries = + Map.fromAscList + <$> traverse + resolveGlobal + (Set.toAscList globals) + where + globals = + canonicalGlobals + (supportedPropositionTerm claim) + <> foldMap + (canonicalGlobals + . supportedPropositionTerm + . typedBackendFactProposition) + facts + <> foldMap + (canonicalGlobals + . supportedPropositionTerm + . typedLocalPremiseProposition) + locals + <> foldMap + (canonicalGlobals + . supportedPropositionTerm + . typedProblemAuxiliaryProposition) + auxiliaries + + resolveGlobal global = + case globalType global of + Nothing -> + Left + (TypedProblemClaimClassificationFailed + (UnknownBackendGlobal global)) + Just coreType -> + Right (global, coreType) + +collectProblemLocals + :: Ord local + => SupportedProposition local global + -> Vector (TypedLocalPremise local origin global) + -> Either + (TypedProblemError local global) + (Map local CoreType) +collectProblemLocals claim locals = + foldM + insertSupport + Map.empty + supports + where + supports = + Vector.toList + (supportedPropositionSupport claim) + <> concatMap + (Vector.toList + . supportedPropositionSupport + . typedLocalPremiseProposition) + (Vector.toList locals) + + insertSupport current (local, coreType) = + case Map.lookup local current of + Nothing -> + Right + (Map.insert + local + coreType + current) + Just previousType + | previousType == coreType -> + Right current + | otherwise -> + Left + (TypedProblemLocalTypeMismatch + local + previousType + coreType) + +typedProblemRoute + :: TypedProblem ref local origin global + -> TypedProblemRoute +typedProblemRoute + (TypedProblem + route + _claim + _facts + _locals + _auxiliaries + _globals + _localTypes) = + route + +typedProblemClaim + :: TypedProblem ref local origin global + -> SupportedProposition local global +typedProblemClaim + (TypedProblem + _route + claim + _facts + _locals + _auxiliaries + _globals + _localTypes) = + claim + +typedProblemGlobalPremises + :: TypedProblem ref local origin global + -> Vector (TypedBackendFact ref global) +typedProblemGlobalPremises + (TypedProblem + _route + _claim + facts + _locals + _auxiliaries + _globals + _localTypes) = + facts + +typedProblemLocalPremises + :: TypedProblem ref local origin global + -> Vector (TypedLocalPremise local origin global) +typedProblemLocalPremises + (TypedProblem + _route + _claim + _facts + locals + _auxiliaries + _globals + _localTypes) = + locals + +typedProblemAuxiliaries + :: TypedProblem ref local origin global + -> Vector (TypedProblemAuxiliary global) +typedProblemAuxiliaries + (TypedProblem + _route + _claim + _facts + _locals + auxiliaries + _globals + _localTypes) = + auxiliaries + +typedProblemGlobalTypes + :: TypedProblem ref local origin global + -> Map global CoreType +typedProblemGlobalTypes + (TypedProblem + _route + _claim + _facts + _locals + _auxiliaries + globals + _localTypes) = + globals + +typedProblemLocalTypes + :: TypedProblem ref local origin global + -> Map local CoreType +typedProblemLocalTypes + (TypedProblem + _route + _claim + _facts + _locals + _auxiliaries + _globals + localTypes) = + localTypes |