diff options
Diffstat (limited to 'source/Felix/Checking/Backend')
| -rw-r--r-- | source/Felix/Checking/Backend/Problem.hs | 1301 | ||||
| -rw-r--r-- | source/Felix/Checking/Backend/Tptp.hs | 1281 |
2 files changed, 2582 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 diff --git a/source/Felix/Checking/Backend/Tptp.hs b/source/Felix/Checking/Backend/Tptp.hs new file mode 100644 index 0000000..a5c0546 --- /dev/null +++ b/source/Felix/Checking/Backend/Tptp.hs @@ -0,0 +1,1281 @@ +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE NoImplicitPrelude #-} + +-- | Deterministic task-wide TPTP preparation for checked typed problems. +module Felix.Checking.Backend.Tptp + ( TypedFormulaOccurrence(..) + , TypedTptpNameOrigin(..) + , PreparedTypedTptpProblem + , prepareTypedTptpProblem + , preparedTypedTptpRoute + , preparedTypedTptpText + , preparedTypedTptpTextNewline + , preparedTypedTptpConjectureText + , preparedTypedTptpNameOrigins + , TypedTptpPreparationError(..) + ) where + +import Base hiding (Empty) +import Felix.Checking.Backend.Problem +import Felix.Checking.Core +import Tptp.UnsortedFirstOrder qualified as Tptp + +import Control.Monad (foldM) +import Control.Monad.State.Strict (StateT) +import Control.Monad.State.Strict qualified as State +import Control.Monad.Trans.Class (lift) +import Data.Map.Strict qualified as Map +import Data.Set qualified as Set +import Data.Text qualified as Text +import Data.Vector qualified as Vector +import Numeric.Natural (Natural) +import TextBuilder + + +data TypedFormulaOccurrence ref + = TypedGlobalPremiseOccurrence !ref + | TypedLocalPremiseOccurrence !LocalPremiseOrdinal + | TypedAuxiliaryOccurrence !Natural + | TypedConjectureOccurrence + deriving stock (Show, Eq, Ord) + +data TypedTptpNameOrigin ref local global + = TypedGlobalNameOrigin !global + | TypedLocalNameOrigin !local + | TypedIntrinsicNameOrigin !CoreIntrinsicTag + | TypedIntegerNameOrigin !Integer + | TypedBinderNameOrigin !Natural + | TypedFormulaNameOrigin !(TypedFormulaOccurrence ref) + deriving stock (Show, Eq, Ord) + +data PreparedTypedTptpProblem ref local global = + PreparedTypedTptpProblem + !TypedProblemRoute + !Text + !Text + !(Map + Text + (TypedTptpNameOrigin ref local global)) + deriving stock (Eq) + +preparedTypedTptpRoute + :: PreparedTypedTptpProblem ref local global + -> TypedProblemRoute +preparedTypedTptpRoute + (PreparedTypedTptpProblem + route + _text + _conjecture + _origins) = + route + +preparedTypedTptpText + :: PreparedTypedTptpProblem ref local global + -> Text +preparedTypedTptpText + (PreparedTypedTptpProblem + _route + problemText + _conjecture + _origins) = + problemText + +preparedTypedTptpTextNewline + :: PreparedTypedTptpProblem ref local global + -> Text +preparedTypedTptpTextNewline = + (`Text.snoc` '\n') + . preparedTypedTptpText + +preparedTypedTptpConjectureText + :: PreparedTypedTptpProblem ref local global + -> Text +preparedTypedTptpConjectureText + (PreparedTypedTptpProblem + _route + _text + conjecture + _origins) = + conjecture + +preparedTypedTptpNameOrigins + :: PreparedTypedTptpProblem ref local global + -> Map + Text + (TypedTptpNameOrigin ref local global) +preparedTypedTptpNameOrigins + (PreparedTypedTptpProblem + _route + _text + _conjecture + origins) = + origins + +data TypedTptpPreparationError local global + = InvalidGeneratedTypedTptpName !Text + | DuplicateGeneratedTypedTptpName !Text + | TypedTptpUnknownGlobal !global + | TypedTptpUnknownLocal !local + | TypedTptpUnboundIndex !Natural + | TypedTptpFofProjectionMismatch + deriving stock (Show, Eq) + + +data NameEnvironment ref local global = + NameEnvironment + !(Map global Tptp.AtomicWord) + !(Map global CoreType) + !(Map local Tptp.AtomicWord) + !(Map CoreIntrinsicTag Tptp.AtomicWord) + !(Map Integer Tptp.AtomicWord) + !(Map + Text + (TypedTptpNameOrigin ref local global)) + +data RenderState ref local global = + RenderState + !Natural + !Natural + !(Map + Text + (TypedTptpNameOrigin ref local global)) + +type Render ref local global = + StateT + (RenderState ref local global) + (Either + (TypedTptpPreparationError local global)) + +data RenderedFormula ref = RenderedFormula + !Tptp.AtomicWord + !(TypedFormulaOccurrence ref) + !TextBuilder + +data BoundTarget + = BoundFofVariable !Tptp.Variable + | BoundTh0Variable !Tptp.Variable + | AmbientConstant !Tptp.AtomicWord + +prepareTypedTptpProblem + :: (Ord local, Ord global) + => TypedProblem ref local origin global + -> Either + (TypedTptpPreparationError local global) + (PreparedTypedTptpProblem ref local global) +prepareTypedTptpProblem problem = do + names <- + allocateNames problem + let initialState = + RenderState + 0 + 0 + (nameEnvironmentOrigins names) + (rendered, finalState) <- + State.runStateT + (renderProblem names problem) + initialState + let (problemBuilder, conjectureBuilder) = + rendered + RenderState _nextBinder _nextHypothesis origins = + finalState + pure + (PreparedTypedTptpProblem + (typedProblemRoute problem) + (TextBuilder.toText problemBuilder) + (TextBuilder.toText conjectureBuilder) + origins) + +allocateNames + :: (Ord local, Ord global) + => TypedProblem ref local origin global + -> Either + (TypedTptpPreparationError local global) + (NameEnvironment ref local global) +allocateNames problem = do + globalAllocations <- + allocateCategory + "tg_g" + TypedGlobalNameOrigin + (Map.keys + (typedProblemGlobalTypes + problem)) + localAllocations <- + allocateCategory + "tg_l" + TypedLocalNameOrigin + (Map.keys + (typedProblemLocalTypes + problem)) + intrinsicAllocations <- + allocateCategory + "tg_i" + TypedIntrinsicNameOrigin + (Set.toAscList + (problemIntrinsics problem)) + integerAllocations <- + allocateCategory + "tg_n" + TypedIntegerNameOrigin + (Set.toAscList + (problemIntegers problem)) + origins <- + foldM + (\current (target, nameOrigin) -> + insertOrigin + (Tptp.atomicWordText target) + nameOrigin + current) + Map.empty + ( [ (target, nameOrigin) + | (_global, target, nameOrigin) <- + globalAllocations + ] + <> [ (target, nameOrigin) + | (_local, target, nameOrigin) <- + localAllocations + ] + <> [ (target, nameOrigin) + | (_intrinsic, target, nameOrigin) <- + intrinsicAllocations + ] + <> [ (target, nameOrigin) + | (_integer, target, nameOrigin) <- + integerAllocations + ] + ) + pure + (NameEnvironment + (Map.fromList + [ (global, target) + | (global, target, _nameOrigin) <- + globalAllocations + ]) + (typedProblemGlobalTypes problem) + (Map.fromList + [ (local, target) + | (local, target, _nameOrigin) <- + localAllocations + ]) + (Map.fromList + [ (intrinsic, target) + | (intrinsic, target, _nameOrigin) <- + intrinsicAllocations + ]) + (Map.fromList + [ (integer, target) + | (integer, target, _nameOrigin) <- + integerAllocations + ]) + origins) + where + allocateCategory prefix makeOrigin semantics = + traverse + (\(ordinal, semantic) -> do + target <- + generatedAtomicWord + (prefix + <> Text.pack + (show ordinal)) + pure + ( semantic + , target + , makeOrigin semantic + )) + (zip [0 :: Int ..] semantics) + +nameEnvironmentOrigins + :: NameEnvironment ref local global + -> Map + Text + (TypedTptpNameOrigin ref local global) +nameEnvironmentOrigins + (NameEnvironment + _globals + _globalTypes + _locals + _intrinsics + _integers + origins) = + origins + +generatedAtomicWord + :: Text + -> Either + (TypedTptpPreparationError local global) + Tptp.AtomicWord +generatedAtomicWord target = + maybe + (Left + (InvalidGeneratedTypedTptpName + target)) + Right + (Tptp.atomicWord target) + +generatedVariable + :: Text + -> Either + (TypedTptpPreparationError local global) + Tptp.Variable +generatedVariable target = + maybe + (Left + (InvalidGeneratedTypedTptpName + target)) + Right + (Tptp.variable target) + +insertOrigin + :: Text + -> TypedTptpNameOrigin ref local global + -> Map + Text + (TypedTptpNameOrigin ref local global) + -> Either + (TypedTptpPreparationError local global) + (Map + Text + (TypedTptpNameOrigin ref local global)) +insertOrigin target nameOrigin origins = + if Map.member target origins + then + Left + (DuplicateGeneratedTypedTptpName + target) + else + Right + (Map.insert + target + nameOrigin + origins) + +renderProblem + :: (Ord local, Ord global) + => NameEnvironment ref local global + -> TypedProblem ref local origin global + -> Render + ref + local + global + (TextBuilder, TextBuilder) +renderProblem names problem = do + hypotheses <- + renderHypotheses names problem + conjecture <- + renderConjecture names problem + declarations <- + case typedProblemRoute problem of + RouteFof -> + pure [] + RouteTh0 -> + renderTh0Declarations + names + problem + let formulaBuilders = + renderFormulaLine + (typedProblemRoute problem) + "axiom" + <$> hypotheses + conjectureBuilder = + renderFormulaLine + (typedProblemRoute problem) + "conjecture" + conjecture + complete = + intercalate + (char '\n') + (declarations + <> formulaBuilders + <> [conjectureBuilder]) + pure + ( complete + , conjectureBuilder + ) + +renderHypotheses + :: (Ord local, Ord global) + => NameEnvironment ref local global + -> TypedProblem ref local origin global + -> Render + ref + local + global + [RenderedFormula ref] +renderHypotheses names problem = do + globalFormulas <- + traverse + (\fact -> + renderOccurrence + names + problem + (TypedGlobalPremiseOccurrence + (typedBackendFactReference + fact)) + (weakenClosedSupportedProposition + (typedBackendFactProposition + fact))) + (Vector.toList + (typedProblemGlobalPremises + problem)) + localFormulas <- + traverse + (\premise -> + renderOccurrence + names + problem + (TypedLocalPremiseOccurrence + (typedLocalPremiseOrdinal + premise)) + (typedLocalPremiseProposition + premise)) + (Vector.toList + (typedProblemLocalPremises + problem)) + auxiliaryFormulas <- + traverse + (\auxiliary -> + renderOccurrence + names + problem + (TypedAuxiliaryOccurrence + (typedProblemAuxiliaryOrdinal + auxiliary)) + (weakenClosedSupportedProposition + (typedProblemAuxiliaryProposition + auxiliary))) + (Vector.toList + (typedProblemAuxiliaries + problem)) + pure + (globalFormulas + <> localFormulas + <> auxiliaryFormulas) + +renderConjecture + :: (Ord local, Ord global) + => NameEnvironment ref local global + -> TypedProblem ref local origin global + -> Render + ref + local + global + (RenderedFormula ref) +renderConjecture names problem = + renderOccurrence + names + problem + TypedConjectureOccurrence + (typedProblemClaim problem) + +renderOccurrence + :: (Ord local, Ord global) + => NameEnvironment ref local global + -> TypedProblem ref local origin global + -> TypedFormulaOccurrence ref + -> SupportedProposition local global + -> Render + ref + local + global + (RenderedFormula ref) +renderOccurrence names problem occurrence proposition = do + target <- + case occurrence of + TypedConjectureOccurrence -> + liftEither + (generatedAtomicWord "tg_q0") + _ -> do + ordinal <- + nextHypothesisOrdinal + liftEither + (generatedAtomicWord + ("tg_h" + <> Text.pack + (show ordinal))) + registerOrigin + (Tptp.atomicWordText target) + (TypedFormulaNameOrigin occurrence) + bounds <- + initialBounds + names + proposition + formula <- + case typedProblemRoute problem of + RouteFof -> + renderFofFormula + names + bounds + (supportedPropositionTerm + proposition) + RouteTh0 -> + renderTh0Term + names + bounds + (supportedPropositionTerm + proposition) + pure + (RenderedFormula + target + occurrence + formula) + +-- Formula and binder ordinals use separate dense namespaces. +nextHypothesisOrdinal + :: Render ref local global Natural +nextHypothesisOrdinal = do + RenderState nextBinder nextHypothesis origins <- + State.get + State.put + (RenderState + nextBinder + (nextHypothesis + 1) + origins) + pure nextHypothesis + +registerOrigin + :: Text + -> TypedTptpNameOrigin ref local global + -> Render ref local global () +registerOrigin target nameOrigin = do + RenderState nextBinder nextHypothesis origins <- + State.get + origins' <- + liftEither + (insertOrigin + target + nameOrigin + origins) + State.put + (RenderState + nextBinder + nextHypothesis + origins') + +freshBinder + :: Render ref local global Tptp.Variable +freshBinder = do + RenderState nextBinder nextHypothesis origins <- + State.get + let target = + "V" <> Text.pack (show nextBinder) + variable <- + liftEither + (generatedVariable target) + origins' <- + liftEither + (insertOrigin + target + (TypedBinderNameOrigin + nextBinder) + origins) + State.put + (RenderState + (nextBinder + 1) + nextHypothesis + origins') + pure variable + +liftEither + :: Either + (TypedTptpPreparationError local global) + value + -> Render ref local global value +liftEither = + lift + +initialBounds + :: Ord local + => NameEnvironment ref local global + -> SupportedProposition local global + -> Render ref local global [BoundTarget] +initialBounds + (NameEnvironment + _globals + _globalTypes + localNames + _intrinsics + _integers + _origins) + proposition = + traverse + (\(local, _coreType) -> + maybe + (lift + (Left + (TypedTptpUnknownLocal + local))) + (pure . AmbientConstant) + (Map.lookup + local + localNames)) + (Vector.toList + (supportedPropositionSupport + proposition)) + +renderFormulaLine + :: TypedProblemRoute + -> TextBuilder + -> RenderedFormula ref + -> TextBuilder +renderFormulaLine route role + (RenderedFormula target _occurrence formula) = + dialect + <> char '(' + <> Tptp.buildAtomicWord target + <> char ',' + <> role + <> char ',' + <> formula + <> text ")." + where + dialect = + case route of + RouteFof -> + text "fof" + RouteTh0 -> + text "thf" + + +renderFofFormula + :: (Ord global) + => NameEnvironment ref local global + -> [BoundTarget] + -> CanonicalTerm global + -> Render ref local global TextBuilder +renderFofFormula names bounds = \case + CFalsum -> + pure (text "$false") + CImp premise conclusion -> do + premise' <- + renderFofFormula names bounds premise + conclusion' <- + renderFofFormula names bounds conclusion + pure + (parenthesize + (premise' + <> text "=>" + <> conclusion')) + CEq TySet left right -> do + left' <- + renderFofTerm names bounds left + right' <- + renderFofTerm names bounds right + pure + (parenthesize + (left' + <> char '=' + <> right')) + CEq TyProp left right -> do + left' <- + renderFofFormula names bounds left + right' <- + renderFofFormula names bounds right + pure + (parenthesize + (left' + <> text "<=>" + <> right')) + CForall TySet body -> do + variable <- + freshBinder + body' <- + renderFofFormula + names + (BoundFofVariable variable + : bounds) + body + pure + (parenthesize + (text "![" + <> Tptp.buildVariable variable + <> text "]:" + <> body')) + application -> + renderFofApplication + names + bounds + TyProp + application + +renderFofTerm + :: Ord global + => NameEnvironment ref local global + -> [BoundTarget] + -> CanonicalTerm global + -> Render ref local global TextBuilder +renderFofTerm names bounds = \case + CBound index -> + renderBound index bounds + CGlobal global -> + Tptp.buildAtomicWord + <$> lookupGlobal names global + CIntrinsic intrinsic -> + Tptp.buildAtomicWord + <$> lookupIntrinsic names intrinsic + COpaqueInteger integer -> + Tptp.buildAtomicWord + <$> lookupInteger names integer + application -> + renderFofApplication + names + bounds + TySet + application + +renderFofApplication + :: Ord global + => NameEnvironment ref local global + -> [BoundTarget] + -> CoreType + -> CanonicalTerm global + -> Render ref local global TextBuilder +renderFofApplication names bounds expected application = + case applicationHead application of + (CGlobal global, arguments) -> do + coreType <- + maybe + (lift + (Left + (TypedTptpUnknownGlobal + global))) + pure + (Map.lookup + global + (nameEnvironmentGlobalTypes + names)) + renderHead + coreType + (lookupGlobal names global) + arguments + (CIntrinsic intrinsic, arguments) -> + renderHead + (coreIntrinsicType intrinsic) + (lookupIntrinsic names intrinsic) + arguments + _ -> + lift + (Left + TypedTptpFofProjectionMismatch) + where + renderHead coreType targetAction arguments = do + unlessFofApplication + expected + coreType + arguments + target <- + targetAction + arguments' <- + traverse + (renderFofTerm names bounds) + arguments + pure + (applyAtomicWord + target + arguments') + +-- Global types are retained in the problem, but names need only the allocated +-- symbols. FOF saturation was already checked by the projection witness. +nameEnvironmentGlobalTypes + :: NameEnvironment ref local global + -> Map global CoreType +nameEnvironmentGlobalTypes + (NameEnvironment + _globals + globalTypes + _locals + _intrinsics + _integers + _origins) = + globalTypes + +unlessFofApplication + :: CoreType + -> CoreType + -> [CanonicalTerm global] + -> Render ref local global () +unlessFofApplication expected coreType arguments = + case consume coreType arguments of + Just result + | result == expected -> + pure () + _ -> + lift + (Left + TypedTptpFofProjectionMismatch) + where + consume current = \case + [] -> + Just current + _argument : remaining -> + case current of + TyArrow TySet result -> + consume result remaining + _ -> + Nothing + +applyAtomicWord + :: Tptp.AtomicWord + -> [TextBuilder] + -> TextBuilder +applyAtomicWord target = \case + [] -> + Tptp.buildAtomicWord target + arguments -> + Tptp.buildAtomicWord target + <> Tptp.buildTuple arguments + +renderBound + :: Natural + -> [BoundTarget] + -> Render ref local global TextBuilder +renderBound index bounds = + case contextAt index bounds of + Nothing -> + lift + (Left + (TypedTptpUnboundIndex + index)) + Just (BoundFofVariable variable) -> + pure + (Tptp.buildVariable + variable) + Just (BoundTh0Variable variable) -> + pure + (Tptp.buildVariable + variable) + Just (AmbientConstant target) -> + pure + (Tptp.buildAtomicWord + target) + + +renderTh0Term + :: Ord global + => NameEnvironment ref local global + -> [BoundTarget] + -> CanonicalTerm global + -> Render ref local global TextBuilder +renderTh0Term names bounds = \case + CBound index -> + renderBound index bounds + CGlobal global -> + Tptp.buildAtomicWord + <$> lookupGlobal names global + CIntrinsic intrinsic -> + Tptp.buildAtomicWord + <$> lookupIntrinsic names intrinsic + COpaqueInteger integer -> + Tptp.buildAtomicWord + <$> lookupInteger names integer + CApp function argument -> do + function' <- + renderTh0Term names bounds function + argument' <- + renderTh0Term names bounds argument + pure + (parenthesize + (function' + <> char '@' + <> argument')) + CLam binderType body -> do + variable <- + freshBinder + body' <- + renderTh0Term + names + (BoundTh0Variable variable + : bounds) + body + pure + (parenthesize + (text "^ [" + <> Tptp.buildVariable variable + <> char ':' + <> renderCoreType binderType + <> text "] : " + <> body')) + CFalsum -> + pure (text "$false") + CImp premise conclusion -> do + premise' <- + renderTh0Term names bounds premise + conclusion' <- + renderTh0Term names bounds conclusion + pure + (parenthesize + (premise' + <> text "=>" + <> conclusion')) + CEq operandType left right -> do + left' <- + renderTh0Term names bounds left + right' <- + renderTh0Term names bounds right + pure + (parenthesize + (left' + <> (case operandType of + TyProp -> text "<=>" + _ -> char '=') + <> right')) + CForall binderType body -> do + variable <- + freshBinder + body' <- + renderTh0Term + names + (BoundTh0Variable variable + : bounds) + body + pure + (parenthesize + (text "! [" + <> Tptp.buildVariable variable + <> char ':' + <> renderCoreType binderType + <> text "] : " + <> body')) + +renderTh0Declarations + :: (Ord local, Ord global) + => NameEnvironment ref local global + -> TypedProblem ref local origin global + -> Render ref local global [TextBuilder] +renderTh0Declarations names problem = do + globalDeclarations <- + traverse + (\(ordinal, (global, coreType)) -> do + target <- + lookupGlobal names global + label <- + liftEither + (generatedAtomicWord + ("tg_g_type_" + <> Text.pack + (show ordinal))) + pure + (typeDeclaration + label + target + (renderCoreType coreType))) + (zip [0 :: Int ..] + (Map.toAscList + (typedProblemGlobalTypes + problem))) + localDeclarations <- + traverse + (\(ordinal, (local, coreType)) -> do + target <- + lookupLocal names local + label <- + liftEither + (generatedAtomicWord + ("tg_l_type_" + <> Text.pack + (show ordinal))) + pure + (typeDeclaration + label + target + (renderCoreType coreType))) + (zip [0 :: Int ..] + (Map.toAscList + (typedProblemLocalTypes + problem))) + intrinsicDeclarations <- + traverse + (\(ordinal, intrinsic) -> do + target <- + lookupIntrinsic names intrinsic + label <- + liftEither + (generatedAtomicWord + ("tg_i_type_" + <> Text.pack + (show ordinal))) + pure + (typeDeclaration + label + target + (renderCoreType + (coreIntrinsicType + intrinsic)))) + (zip [0 :: Int ..] + (Set.toAscList + (problemIntrinsics problem))) + integerDeclarations <- + traverse + (\(ordinal, integer) -> do + target <- + lookupInteger names integer + label <- + liftEither + (generatedAtomicWord + ("tg_n_type_" + <> Text.pack + (show ordinal))) + pure + (typeDeclaration + label + target + (renderCoreType TySet))) + (zip [0 :: Int ..] + (Set.toAscList + (problemIntegers problem))) + pure + (globalDeclarations + <> localDeclarations + <> intrinsicDeclarations + <> integerDeclarations) + +typeDeclaration + :: Tptp.AtomicWord + -> Tptp.AtomicWord + -> TextBuilder + -> TextBuilder +typeDeclaration label target coreType = + text "thf(" + <> Tptp.buildAtomicWord label + <> text ",type,(" + <> Tptp.buildAtomicWord target + <> char ':' + <> coreType + <> text "))." + +renderCoreType :: CoreType -> TextBuilder +renderCoreType = \case + TyProp -> + text "$o" + TySet -> + text "$i" + TyArrow argument result -> + parenthesize + (renderCoreType argument + <> char '>' + <> renderCoreType result) + +parenthesize :: TextBuilder -> TextBuilder +parenthesize builder = + char '(' <> builder <> char ')' + + +lookupGlobal + :: Ord global + => NameEnvironment ref local global + -> global + -> Render ref local global Tptp.AtomicWord +lookupGlobal names global = + maybe + (lift + (Left + (TypedTptpUnknownGlobal + global))) + pure + (lookupGlobalPure names global) + +lookupGlobalPure + :: Ord global + => NameEnvironment ref local global + -> global + -> Maybe Tptp.AtomicWord +lookupGlobalPure + (NameEnvironment + globals + _globalTypes + _locals + _intrinsics + _integers + _origins) = + (`Map.lookup` globals) + +lookupLocalPure + :: Ord local + => NameEnvironment ref local global + -> local + -> Maybe Tptp.AtomicWord +lookupLocalPure + (NameEnvironment + _globals + _globalTypes + locals + _intrinsics + _integers + _origins) = + (`Map.lookup` locals) + +lookupLocal + :: Ord local + => NameEnvironment ref local global + -> local + -> Render ref local global Tptp.AtomicWord +lookupLocal names local = + maybe + (lift + (Left + (TypedTptpUnknownLocal + local))) + pure + (lookupLocalPure names local) + +lookupIntrinsic + :: NameEnvironment ref local global + -> CoreIntrinsicTag + -> Render ref local global Tptp.AtomicWord +lookupIntrinsic names intrinsic = + maybe + (lift + (Left + TypedTptpFofProjectionMismatch)) + pure + (lookupIntrinsicPure names intrinsic) + +lookupIntrinsicPure + :: NameEnvironment ref local global + -> CoreIntrinsicTag + -> Maybe Tptp.AtomicWord +lookupIntrinsicPure + (NameEnvironment + _globals + _globalTypes + _locals + intrinsics + _integers + _origins) = + (`Map.lookup` intrinsics) + +lookupInteger + :: NameEnvironment ref local global + -> Integer + -> Render ref local global Tptp.AtomicWord +lookupInteger names integer = + maybe + (lift + (Left + TypedTptpFofProjectionMismatch)) + pure + (lookupIntegerPure names integer) + +lookupIntegerPure + :: NameEnvironment ref local global + -> Integer + -> Maybe Tptp.AtomicWord +lookupIntegerPure + (NameEnvironment + _globals + _globalTypes + _locals + _intrinsics + integers + _origins) = + (`Map.lookup` integers) + +problemIntrinsics + :: TypedProblem ref local origin global + -> Set CoreIntrinsicTag +problemIntrinsics = + foldMap canonicalIntrinsics + . problemTerms + +problemIntegers + :: TypedProblem ref local origin global + -> Set Integer +problemIntegers = + foldMap canonicalIntegers + . problemTerms + +problemTerms + :: TypedProblem ref local origin global + -> [CanonicalTerm global] +problemTerms problem = + supportedPropositionTerm + (typedProblemClaim problem) + : (supportedPropositionTerm + . typedBackendFactProposition + <$> Vector.toList + (typedProblemGlobalPremises + problem)) + <> (supportedPropositionTerm + . typedLocalPremiseProposition + <$> Vector.toList + (typedProblemLocalPremises + problem)) + <> (supportedPropositionTerm + . typedProblemAuxiliaryProposition + <$> Vector.toList + (typedProblemAuxiliaries + problem)) + +canonicalIntrinsics + :: CanonicalTerm global + -> Set CoreIntrinsicTag +canonicalIntrinsics = \case + CBound{} -> + mempty + CGlobal{} -> + mempty + CIntrinsic intrinsic -> + Set.singleton intrinsic + COpaqueInteger{} -> + mempty + CApp function argument -> + canonicalIntrinsics function + <> canonicalIntrinsics argument + CLam _binderType body -> + canonicalIntrinsics body + CFalsum -> + mempty + CImp premise conclusion -> + canonicalIntrinsics premise + <> canonicalIntrinsics conclusion + CEq _operandType left right -> + canonicalIntrinsics left + <> canonicalIntrinsics right + CForall _binderType body -> + canonicalIntrinsics body + +canonicalIntegers + :: CanonicalTerm global + -> Set Integer +canonicalIntegers = \case + CBound{} -> + mempty + CGlobal{} -> + mempty + CIntrinsic{} -> + mempty + COpaqueInteger integer -> + Set.singleton integer + CApp function argument -> + canonicalIntegers function + <> canonicalIntegers argument + CLam _binderType body -> + canonicalIntegers body + CFalsum -> + mempty + CImp premise conclusion -> + canonicalIntegers premise + <> canonicalIntegers conclusion + CEq _operandType left right -> + canonicalIntegers left + <> canonicalIntegers right + CForall _binderType body -> + canonicalIntegers body + +applicationHead + :: CanonicalTerm global + -> (CanonicalTerm global, [CanonicalTerm global]) +applicationHead = + go [] + where + go arguments = \case + CApp function argument -> + go (argument : arguments) function + headTerm -> + (headTerm, arguments) + +contextAt :: Natural -> [value] -> Maybe value +contextAt _index [] = + Nothing +contextAt 0 (value : _remaining) = + Just value +contextAt index (_value : remaining) = + contextAt (index - 1) remaining |