module Main where

import SimpleTheoremProver

import Text.Regex (subRegex, matchRegex, mkRegex)
import Data.List (isSuffixOf)

muRules :: [Rule String]
muRules = [
    Rule   "One"   (\thm -> if (isSuffixOf "I" thm) then (thm ++ "U") else thm)
    , Rule "Two"   (\thm -> case (matchRegex (mkRegex "M(.*)") thm) of
                                Just [x] -> thm ++ x
                                _        -> thm)
    , Rule "Three" (\thm -> subRegex (mkRegex "III") thm "U")
    , Rule "Four"  (\thm -> subRegex (mkRegex "UU") thm "")
    ]

testProver = TheoremProver (map mkAxiom ["MI"]) muRules

main :: IO ()
main = print $ findProof testProver "MIUIU" 5