{- | Module : ./THF/ProverState.hs Description : Help functions for all automatic theorem provers. Copyright : (c) Rainer Grabbe License : GPLv2 or higher, see LICENSE.txt Maintainer : Christian.Maeder@dfki.de Stability : provisional Portability : needs POSIX Data structures, initialising functions for Prover state and configurations. -} module THF.ProverState where import Logic.Prover import THF.As import THF.Sign import THF.Print import Common.AS_Annotation {- ----------------------------------------------------------------------------- Todos: maybe use FreeDefMorphism in the ProverStateTHF ----------------------------------------------------------------------------- -} data ProverStateTHF = ProverStateTHF { ProverStateTHF -> [Named THFFormula] axioms :: [Named THFFormula] , ProverStateTHF -> SignTHF signature :: SignTHF , ProverStateTHF -> [FreeDefMorphism THFFormula MorphismTHF] freeDefs :: [FreeDefMorphism THFFormula MorphismTHF] } -- Creates an initial THF prover state. initialProverStateTHF :: SignTHF -> [Named THFFormula] -> [FreeDefMorphism THFFormula MorphismTHF] -> ProverStateTHF initialProverStateTHF :: SignTHF -> [Named THFFormula] -> [FreeDefMorphism THFFormula MorphismTHF] -> ProverStateTHF initialProverStateTHF sign :: SignTHF sign oSens :: [Named THFFormula] oSens freedefs :: [FreeDefMorphism THFFormula MorphismTHF] freedefs = ProverStateTHF :: [Named THFFormula] -> SignTHF -> [FreeDefMorphism THFFormula MorphismTHF] -> ProverStateTHF ProverStateTHF { axioms :: [Named THFFormula] axioms = (Named THFFormula -> Bool) -> [Named THFFormula] -> [Named THFFormula] forall a. (a -> Bool) -> [a] -> [a] filter Named THFFormula -> Bool forall s a. SenAttr s a -> Bool isAxiom [Named THFFormula] oSens , signature :: SignTHF signature = SignTHF sign , freeDefs :: [FreeDefMorphism THFFormula MorphismTHF] freeDefs = [FreeDefMorphism THFFormula MorphismTHF] freedefs } -- todo: investigate comment about negated axioms -- Insert a Named SentenceTHF into the ProverStateTHF insertSentenceTHF :: ProverStateTHF -> Named THFFormula -> ProverStateTHF insertSentenceTHF :: ProverStateTHF -> Named THFFormula -> ProverStateTHF insertSentenceTHF ps :: ProverStateTHF ps ns :: Named THFFormula ns = ProverStateTHF ps {axioms :: [Named THFFormula] axioms = Named THFFormula ns Named THFFormula -> [Named THFFormula] -> [Named THFFormula] forall a. a -> [a] -> [a] : ProverStateTHF -> [Named THFFormula] axioms ProverStateTHF ps} showProblemTHF :: ProverStateTHF -> Named THFFormula -> [String] -> IO String showProblemTHF :: ProverStateTHF -> Named THFFormula -> [String] -> IO String showProblemTHF ps :: ProverStateTHF ps goal :: Named THFFormula goal _ = String -> IO String forall (m :: * -> *) a. Monad m => a -> m a return (String -> IO String) -> String -> IO String forall a b. (a -> b) -> a -> b $ Doc -> String forall a. Show a => a -> String show (Doc -> String) -> Doc -> String forall a b. (a -> b) -> a -> b $ SignTHF -> [Named THFFormula] -> Named THFFormula -> Doc printProblemTHF (ProverStateTHF -> SignTHF signature ProverStateTHF ps) ((Named THFFormula -> Bool) -> [Named THFFormula] -> [Named THFFormula] forall a. (a -> Bool) -> [a] -> [a] filter Named THFFormula -> Bool forall s a. SenAttr s a -> Bool isAxiom (ProverStateTHF -> [Named THFFormula] axioms ProverStateTHF ps)) Named THFFormula goal -- Get all axioms possibly used in a proof. getAxioms :: ProverStateTHF -> [String] getAxioms :: ProverStateTHF -> [String] getAxioms = (Named THFFormula -> String) -> [Named THFFormula] -> [String] forall a b. (a -> b) -> [a] -> [b] map Named THFFormula -> String forall s a. SenAttr s a -> a senAttr ([Named THFFormula] -> [String]) -> (ProverStateTHF -> [Named THFFormula]) -> ProverStateTHF -> [String] forall b c a. (b -> c) -> (a -> b) -> a -> c . (Named THFFormula -> Bool) -> [Named THFFormula] -> [Named THFFormula] forall a. (a -> Bool) -> [a] -> [a] filter Named THFFormula -> Bool forall s a. SenAttr s a -> Bool isAxiom ([Named THFFormula] -> [Named THFFormula]) -> (ProverStateTHF -> [Named THFFormula]) -> ProverStateTHF -> [Named THFFormula] forall b c a. (b -> c) -> (a -> b) -> a -> c . ProverStateTHF -> [Named THFFormula] axioms -- FormulaRoles that are treated like axioms thfAxioms :: [FormulaRole] thfAxioms :: [FormulaRole] thfAxioms = [FormulaRole Axiom, FormulaRole Definition, FormulaRole Lemma, FormulaRole Theorem]