{-# 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