{- Prover.hs -}
{- Charles Chiou -}
{-# OPTIONS -Wall -Werror #-}

module Chiou.Prover 
    ( tellCmd
    , askCmd
    , unloadCmd
    , resetCmd
    , showCmd
    , debugCmd
    , deleteCmd
    ) where

import Chiou.FirstOrderLogic (Sentence)
import Chiou.NormalForm (ImplicativeNormalForm, showINFDerivation)
import Chiou.KnowledgeBase (ProverT, tellKB, deleteKB, unloadKB, emptyKB, showKB)
import Chiou.Resolution (askKB, SetOfSupport)
import Control.Monad.Trans (MonadIO, liftIO)
import Data.List (intercalate)
import Data.String (IsString(..))

tellCmd :: (Monad m, Eq v, Eq p, Eq f, IsString p, Enum f) => Sentence v p f -> ProverT v p f m [ImplicativeNormalForm v p f]
tellCmd = tellKB


askCmd :: (MonadIO m, Eq v, Eq p, Eq f, IsString p, Show v, Show p, Show f) =>
          Sentence v p f -> ProverT v p f m (Bool, SetOfSupport v p f)
askCmd sentence = 
    liftIO (putStrLn ("askCmd " ++ show sentence)) >>
    askKB sentence >>= \ result ->
    liftIO (putStrLn (format result)) >>
    return result
    where format (flag, proof) = "(" ++ show flag ++
                                 ",\n   [" ++ intercalate "\n    " (map show proof) ++ "])"

deleteCmd :: Monad m => Int -> ProverT v p f m String
deleteCmd i = deleteKB i

unloadCmd :: Monad m => ProverT v p f m ()
unloadCmd = unloadKB

resetCmd :: Monad m => ProverT v p f m ()
resetCmd = emptyKB

showCmd :: (MonadIO m, Show v, Show p, Show f) => ProverT v p f m ()
showCmd = showKB >>= liftIO . putStrLn

debugCmd :: (Eq v, IsString p, Show v, Show p, Show f) => Sentence v p f -> String
debugCmd sentence = showINFDerivation sentence