diff options
Diffstat (limited to 'source/Encoding.hs')
| -rw-r--r-- | source/Encoding.hs | 588 |
1 files changed, 0 insertions, 588 deletions
diff --git a/source/Encoding.hs b/source/Encoding.hs deleted file mode 100644 index fd988de..0000000 --- a/source/Encoding.hs +++ /dev/null @@ -1,588 +0,0 @@ -module Encoding - ( PreparedTptpTask - , prepareTptpTask - , prepareTrainingTptpTask - , preparedTptpSyntax - , preparedTptpText - , preparedTptpTextNewline - , preparedTptpConjectureText - , preparedTptpNameOrigins - , encodeTask - , encodeTaskText - , writeTask - , contractionTask - ) where - - -import Base -import Syntax.Internal -import Tptp.UnsortedFirstOrder qualified as Tptp - -import Bound -import Control.Monad.State.Strict qualified as State -import Data.List qualified as List -import Data.Map.Strict qualified as Map -import Data.Set qualified as Set -import Data.Text qualified as Text -import Data.Text.IO qualified as TextIO -import TextBuilder - - --- | The structural semantic keys available before nominal identities land. -data LegacyTaskKey - = LegacyObjectSymbolKey !Symbol - | LegacyFreeConstantKey !VarSymbol - | LegacyStructureSymbolKey !StructSymbol - deriving (Show, Eq, Ord) - -newtype EncodingEnv = EncodingEnv - { legacyTargetNames :: Map LegacyTaskKey Tptp.AtomicWord - } - -data FormulaOccurrenceKey - = ConjectureFormulaOccurrence - | HypothesisFormulaOccurrence !Tptp.Role !Int - deriving (Show, Eq, Ord) - -data TptpNameOrigin - = LegacyTaskNameOrigin !LegacyTaskKey - | BinderPositionOrigin !Int - | FormulaOccurrenceOrigin !FormulaOccurrenceKey - deriving (Show, Eq, Ord) - -data PreparedTptpTask = PreparedTptpTask - { preparedTptpSyntax :: !Tptp.Task - , preparedTptpText :: !Text - , preparedTptpConjectureText :: !Text - , _preparedTptpNameTable :: !EncodingEnv - , preparedTptpReverseNames :: !(Map Text TptpNameOrigin) - } - -preparedTptpTextNewline :: PreparedTptpTask -> Text -preparedTptpTextNewline = - (`Text.snoc` '\n') . preparedTptpText - --- | Target name to location-free semantic meaning. -preparedTptpNameOrigins :: PreparedTptpTask -> Map Text Text -preparedTptpNameOrigins = - Map.map (Text.pack . show) . preparedTptpReverseNames - -data SelectedFormula = SelectedFormula - { selectedFormulaRole :: !Tptp.Role - , selectedFormulaBody :: !Formula - } - -prepareTptpTask :: Task -> PreparedTptpTask -prepareTptpTask task = - prepareSelectedTptpTask - (SelectedFormula Tptp.Conjecture (taskConjecture task)) - [ SelectedFormula - Tptp.Axiom - (contraction (hypothesisFormula hypothesis)) - | hypothesis <- taskHypotheses task - ] - -prepareTrainingTptpTask - :: Formula - -> [Hypothesis] - -> [Hypothesis] - -> PreparedTptpTask -prepareTrainingTptpTask conjecture usefuls redundants = - prepareSelectedTptpTask - (SelectedFormula Tptp.Conjecture conjecture) - ( trainingFormulas Tptp.AxiomUseful usefuls - <> trainingFormulas Tptp.AxiomRedundant redundants - ) - where - trainingFormulas role hypotheses = - [ SelectedFormula role (contraction (hypothesisFormula hypothesis)) - | hypothesis <- hypotheses - ] - -prepareSelectedTptpTask - :: SelectedFormula - -> [SelectedFormula] - -> PreparedTptpTask -prepareSelectedTptpTask conjecture hypotheses = - let allFormulas = conjecture : hypotheses - (encodingEnv, semanticReverseNames) = - allocateLegacyNames - (Set.unions - (legacyFormulaKeys . selectedFormulaBody <$> allFormulas)) - orderedHypotheses = - -- Hypothesis list order is not semantic. Equal lowered records stay - -- duplicated. - List.sortOn - (\selected -> - ( selectedFormulaRole selected - , canonicalFormulaText encodingEnv selected - )) - hypotheses - initialEncodingState = - EncodingState - { nextBinderPosition = 0 - , encodingReverseNames = semanticReverseNames - } - ((encodedConjecture, encodedHypotheses), finalEncodingState) = - State.runState - (do - conjectureFormula <- - encodeSelectedFormula - encodingEnv - (generatedAtomicWord "zf_q" 0) - ConjectureFormulaOccurrence - conjecture - hypothesisFormulas <- - for - (zip [0..] orderedHypotheses) - \(ordinal, selected) -> - encodeSelectedFormula - encodingEnv - (generatedAtomicWord "zf_h" ordinal) - (HypothesisFormulaOccurrence - (selectedFormulaRole selected) - ordinal) - selected - pure (conjectureFormula, hypothesisFormulas)) - initialEncodingState - syntax = Tptp.Task (encodedConjecture : encodedHypotheses) - in - PreparedTptpTask - { preparedTptpSyntax = syntax - , preparedTptpText = Tptp.toText syntax - , preparedTptpConjectureText = - Tptp.toText (Tptp.Task [encodedConjecture]) - , _preparedTptpNameTable = encodingEnv - , preparedTptpReverseNames = - encodingReverseNames finalEncodingState - } - -encodeTask :: Task -> Tptp.Task -encodeTask = preparedTptpSyntax . prepareTptpTask - -encodeTaskText :: Task -> Text -encodeTaskText = preparedTptpText . prepareTptpTask - -writeTask :: Handle -> Task -> IO () -writeTask handle = - TextIO.hPutStr handle . preparedTptpTextNewline . prepareTptpTask - --- | Boolean contraction of a task. -contractionTask :: Task -> Task -contractionTask task = task - { taskConjecture = contraction (taskConjecture task) - } - -allocateLegacyNames - :: Set LegacyTaskKey - -> (EncodingEnv, Map Text TptpNameOrigin) -allocateLegacyNames keys = - let orderedKeys = Set.toAscList keys - objectKeys = - [ key - | key@LegacyObjectSymbolKey{} <- orderedKeys - ] - freeConstantKeys = - [ key - | key@LegacyFreeConstantKey{} <- orderedKeys - ] - structureKeys = - [ key - | key@LegacyStructureSymbolKey{} <- orderedKeys - ] - allocations = - allocateCategory "zf_u" objectKeys - <> allocateCategory "zf_f" freeConstantKeys - <> allocateCategory "zf_s" structureKeys - targetNames = - Map.fromList - [ (key, target) - | (key, target) <- allocations - ] - reverseNames = - foldl' - (\reverseNames' (key, target) -> - insertReverseName - (Tptp.atomicWordText target) - (LegacyTaskNameOrigin key) - reverseNames') - mempty - allocations - in - (EncodingEnv targetNames, reverseNames) - where - allocateCategory prefix = - zipWith - (\ordinal key -> - (key, generatedAtomicWord prefix ordinal)) - [0..] - -legacyFormulaKeys :: Formula -> Set LegacyTaskKey -legacyFormulaKeys formula = - Set.fromList - (LegacyFreeConstantKey <$> toList formula) - <> Set.map - LegacyObjectSymbolKey - (Set.filter requiresAllocatedName (mentionedSymbols formula)) - <> Set.map - LegacyStructureSymbolKey - (mentionedStructureSymbols formula) - -requiresAllocatedName :: Symbol -> Bool -requiresAllocatedName = \case - SymbolPredicate (PredicateRelation relation) -> - relation /= EqSymbol && relation /= NeqSymbol - _ -> - True - -mentionedStructureSymbols :: ExprOf a -> Set StructSymbol -mentionedStructureSymbols = \case - TermVar{} -> - mempty - TermSymbol _loc _symbol args -> - Set.unions (mentionedStructureSymbols <$> args) - TermSymbolStruct symbol maybeArgument -> - Set.insert symbol (foldMap mentionedStructureSymbols maybeArgument) - Apply expression arguments -> - mentionedStructureSymbols expression - <> Set.unions - (mentionedStructureSymbols <$> toList arguments) - TermSep _variable bound scope -> - mentionedStructureSymbols bound - <> mentionedStructureSymbols (fromScope scope) - ReplacePred _rangeVariable _domainVariable bound scope -> - mentionedStructureSymbols bound - <> mentionedStructureSymbols (fromScope scope) - ReplaceFun bounds lhs condition -> - Set.unions - (mentionedStructureSymbols . snd <$> toList bounds) - <> mentionedStructureSymbols (fromScope lhs) - <> mentionedStructureSymbols (fromScope condition) - Connected _connective left right -> - mentionedStructureSymbols left <> mentionedStructureSymbols right - Lambda scope -> - mentionedStructureSymbols (fromScope scope) - Quantified _quantifier scope -> - mentionedStructureSymbols (fromScope scope) - PropositionalConstant{} -> - mempty - Not _loc expression -> - mentionedStructureSymbols expression - -canonicalFormulaText :: EncodingEnv -> SelectedFormula -> Text -canonicalFormulaText encodingEnv selected = - TextBuilder.toText - (State.evalState - (encodeExpr encodingEnv (selectedFormulaBody selected)) - EncodingState - { nextBinderPosition = 0 - , encodingReverseNames = mempty - }) - -data EncodingState = EncodingState - { nextBinderPosition :: !Int - , encodingReverseNames :: !(Map Text TptpNameOrigin) - } - -type Encode = State.State EncodingState - -encodeSelectedFormula - :: EncodingEnv - -> Tptp.AtomicWord - -> FormulaOccurrenceKey - -> SelectedFormula - -> Encode Tptp.FofFormula -encodeSelectedFormula encodingEnv targetName occurrence selected = do - registerReverseName - (Tptp.atomicWordText targetName) - (FormulaOccurrenceOrigin occurrence) - body <- encodeExpr encodingEnv (selectedFormulaBody selected) - pure - (Tptp.FofFormula - (Tptp.NameAtomicWord targetName) - (selectedFormulaRole selected) - body) - -encodeExpr :: EncodingEnv -> Expr -> Encode TextBuilder -encodeExpr encodingEnv = - buildExpr . fmap (encodeFreeVar encodingEnv) - where - -- Source tasks reach encoding only after checker canonicalization. - buildExpr :: ExprOf EncodedVar -> Encode TextBuilder - buildExpr = \case - Equals _pos left right -> do - left' <- buildExpr left - right' <- buildExpr right - pure (left' <> char '=' <> right') - NotEquals _pos left right -> do - left' <- buildExpr left - right' <- buildExpr right - pure (left' <> text "!=" <> right') - Atomic _pos predicate arguments -> do - arguments' <- traverse buildExpr arguments - pure - (buildApply - (encodePredicate encodingEnv predicate) - arguments') - PropositionalConstant IsBottom -> - pure (text "$false") - PropositionalConstant IsTop -> - pure (text "$true") - Not _pos formula -> do - formula' <- buildUnitary formula - pure (char '~' <> formula') - Connected Conjunction left right -> do - left' <- buildAnd left - right' <- buildAnd right - pure (left' <> char '&' <> right') - Connected Disjunction left right -> do - left' <- buildOr left - right' <- buildOr right - pure (left' <> char '|' <> right') - Connected Implication left right -> do - left' <- buildUnitary left - right' <- buildUnitary right - pure (left' <> text "=>" <> right') - Connected Equivalence left right -> do - left' <- buildUnitary left - right' <- buildUnitary right - pure (left' <> text "<=>" <> right') - Connected NegatedDisjunction left right -> do - formula' <- - buildUnitary (Connected Disjunction left right) - pure (char '~' <> formula') - Connected ExclusiveOr left right -> do - formula' <- - buildUnitary (Connected Equivalence left right) - pure (char '~' <> formula') - Quantified quantifier scope -> - buildQuantified buildExpr buildUnitary quantifier scope - TermVar variable -> - pure (buildTermVar variable) - Apply expression arguments -> case expression of - TermVar (FreeConst targetName) -> do - arguments' <- traverse buildExpr (toList arguments) - pure (buildApply targetName arguments') - _ -> - error - ("encodeExpr: complex term as head of application: " - <> show expression) - TermSymbol _pos symbol arguments -> do - arguments' <- traverse buildExpr arguments - pure - (buildApply - (encodeSymbol encodingEnv symbol) - arguments') - expression@ReplaceFun{} -> - error - ("Precondition failed in encodeTerm, cannot encode terms with comprehensions directly: " - <> show expression) - expression@ReplacePred{} -> - error - ("Precondition failed in encodeTerm, cannot encode terms with comprehensions directly: " - <> show expression) - expression@TermSep{} -> - error - ("Precondition failed in encodeTerm, cannot encode terms with comprehensions directly: " - <> show expression) - TermSymbolStruct symbol maybeArgument -> case maybeArgument of - Just argument -> do - argument' <- buildExpr argument - pure - (buildApply - (lookupLegacyName - encodingEnv - (LegacyStructureSymbolKey symbol)) - [argument']) - Nothing -> - error - ("encodeExpr (precondition failed): unannotated struct symbol " - <> show symbol) - _ -> - error "encodeExpr: missing case" - - buildTermVar :: EncodedVar -> TextBuilder - buildTermVar = \case - BoundVar variable -> - Tptp.buildVariable variable - FreeConst targetName -> - Tptp.buildAtomicWord targetName - - buildApply :: Tptp.AtomicWord -> [TextBuilder] -> TextBuilder - buildApply function arguments = case arguments of - [] -> - Tptp.buildAtomicWord function - _ -> - Tptp.buildAtomicWord function <> Tptp.buildTuple arguments - - isAtom :: ExprOf EncodedVar -> Bool - isAtom = \case - TermVar{} -> True - TermSymbol{} -> True - TermSymbolStruct{} -> True - Apply{} -> True - PropositionalConstant{} -> True - Equals{} -> True - NotEquals{} -> True - _ -> False - - buildQuantified - :: (ExprOf EncodedVar -> Encode TextBuilder) - -> (ExprOf EncodedVar -> Encode TextBuilder) - -> Quantifier - -> Scope VarSymbol ExprOf EncodedVar - -> Encode TextBuilder - buildQuantified renderEmpty renderBody quantifier scope = do - let boundKeys = currentScopeBindings scope - targetVariables <- traverse (const allocateBinderVariable) boundKeys - let binderNames = Map.fromList (zip boundKeys targetVariables) - instantiateBinder key = - TermVar - (BoundVar - (Map.lookup key binderNames - ?? impossible - ("encodeExpr: missing binder position for " - <> show key))) - body = instantiate instantiateBinder scope - case targetVariables of - [] -> - renderEmpty body - _ -> do - body' <- renderBody body - pure - ( buildQuantifier quantifier - <> Tptp.buildList - (Tptp.buildVariable <$> targetVariables) - <> char ':' - <> body' - ) - - buildQuantifier :: Quantifier -> TextBuilder - buildQuantifier = \case - Universally -> - text "!" - Existentially -> - text "?" - - buildUnitary :: ExprOf EncodedVar -> Encode TextBuilder - buildUnitary = \case - atom | isAtom atom -> - buildExpr atom - Quantified quantifier scope -> - buildQuantified buildUnitary buildUnitary quantifier scope - Not _ formula -> do - formula' <- buildUnitary formula - pure (char '~' <> formula') - formula -> do - formula' <- buildExpr formula - pure (char '(' <> formula' <> char ')') - - buildAnd :: ExprOf EncodedVar -> Encode TextBuilder - buildAnd = \case - Connected Conjunction left right -> do - left' <- buildAnd left - right' <- buildAnd right - pure (left' <> char '&' <> right') - formula -> - buildUnitary formula - - buildOr :: ExprOf EncodedVar -> Encode TextBuilder - buildOr = \case - Connected Disjunction left right -> do - left' <- buildOr left - right' <- buildUnitary right - pure (left' <> char '|' <> right') - formula -> - buildUnitary formula - -currentScopeBindings - :: Scope VarSymbol ExprOf a - -> [VarSymbol] -currentScopeBindings scope = - nubOrd - [ binder - | B binder <- toList (fromScope scope) - ] - -data EncodedVar - = BoundVar Tptp.Variable - | FreeConst Tptp.AtomicWord - deriving (Show, Eq, Ord) - -encodeFreeVar :: EncodingEnv -> VarSymbol -> EncodedVar -encodeFreeVar encodingEnv variable = - FreeConst - (lookupLegacyName - encodingEnv - (LegacyFreeConstantKey variable)) - -encodeSymbol :: EncodingEnv -> Symbol -> Tptp.AtomicWord -encodeSymbol encodingEnv symbol = - lookupLegacyName encodingEnv (LegacyObjectSymbolKey symbol) - -encodePredicate :: EncodingEnv -> Predicate -> Tptp.AtomicWord -encodePredicate encodingEnv predicate = - encodeSymbol encodingEnv (SymbolPredicate predicate) - -lookupLegacyName :: EncodingEnv -> LegacyTaskKey -> Tptp.AtomicWord -lookupLegacyName encodingEnv key = - Map.lookup key (legacyTargetNames encodingEnv) - ?? impossible - ("Encoding lookup missed inventoried key " <> show key) - -allocateBinderVariable :: Encode Tptp.Variable -allocateBinderVariable = do - position <- State.gets nextBinderPosition - let targetVariable = generatedVariable "V" position - State.modify' \state -> - state{nextBinderPosition = position + 1} - registerReverseName - (Tptp.variableText targetVariable) - (BinderPositionOrigin position) - pure targetVariable - -registerReverseName :: Text -> TptpNameOrigin -> Encode () -registerReverseName target origin = - State.modify' \state -> - state - { encodingReverseNames = - insertReverseName - target - origin - (encodingReverseNames state) - } - -insertReverseName - :: Text - -> TptpNameOrigin - -> Map Text TptpNameOrigin - -> Map Text TptpNameOrigin -insertReverseName target origin reverseNames = - case Map.lookup target reverseNames of - Nothing -> - Map.insert target origin reverseNames - Just existing -> - impossible - ( "TPTP target name " - <> show target - <> " was allocated for both " - <> show existing - <> " and " - <> show origin - ) - -generatedAtomicWord :: Text -> Int -> Tptp.AtomicWord -generatedAtomicWord prefix ordinal = - let target = prefix <> Text.pack (show ordinal) - in - Tptp.atomicWord target - ?? impossible - ("generated invalid TPTP atomic word " <> show target) - -generatedVariable :: Text -> Int -> Tptp.Variable -generatedVariable prefix ordinal = - let target = prefix <> Text.pack (show ordinal) - in - Tptp.variable target - ?? impossible - ("generated invalid TPTP variable " <> show target) |