module SimpleTheoremProver where
import Data.List (nubBy, find)
import Data.Set (fromList, union)
data Rule a = Rule { name :: String , function :: a -> a }
instance Show (Rule a) where
show (Rule a _) = a
data Theorem a = Theorem { axiom :: a , rulesThm :: [Rule a] , result :: a } deriving (Show)
data TheoremProver a = TheoremProver { axioms :: [Theorem a] , rulesThmProver :: [Rule a] } deriving (Show)
mkAxiom :: a -> Theorem a
mkAxiom a = Theorem a [] a
thmApplyRule :: Theorem a -> Rule a -> Theorem a
thmApplyRule theorem rule =
Theorem
(axiom theorem)
(rulesThm theorem ++ [rule])
((function rule) (result theorem))
thmApplyRules :: TheoremProver a -> [Theorem a] -> [Theorem a]
thmApplyRules prover (thm:thms) = map (thmApplyRule thm) (rulesThmProver prover) ++ (thmApplyRules prover thms)
thmApplyRules _ _ = []
mergeProofs :: Eq a => [Theorem a] -> [Theorem a] -> [Theorem a]
mergeProofs p1 p2 = nubBy (\t1 t2 -> result t1 == result t2) p1 ++ p2
findProofIter :: (Ord a, Eq a) => TheoremProver a -> a -> Int -> [Theorem a] -> Maybe (Theorem a)
findProofIter _ _ 0 _ = Nothing
findProofIter prover target depth foundProofs = case (find (\x -> target == result x) foundProofs) of
Just prf -> Just prf
Nothing ->
let theorems = thmApplyRules prover foundProofs
proofsSet = fromList (map result foundProofs)
theoremsSet = fromList (map result theorems) in
if (union proofsSet theoremsSet) == proofsSet
then Nothing
else findProofIter prover target (depth - 1) (mergeProofs foundProofs theorems)
findProof :: Ord a => TheoremProver a -> a -> Int -> Maybe (Theorem a)
findProof prover target depth = findProofIter prover target depth (axioms prover)