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