-- All the parser, command processor, and pretty printing code that
-- was removed from the library.

{-------------------------------------------------------------------}
{-- A monadic combinator parser for sentences in first-order logic -}
{-------------------------------------------------------------------}

{-
parseFOL :: String -> Maybe Sentence
parseFOL s =
    case (papply sentence s) of
      [] -> Nothing
      xs -> case ((snd . head) xs) of
	      [] -> Just ((fst . head) xs)
	      _ -> Nothing

-- Sentence parsers

sentence :: Parser Sentence
sentence = sQuant +++ sConn +++ sNot +++ sAtomic

sAtomic :: Parser Sentence
sAtomic = sEqual +++ sPred +++ sBracket

sBracket :: Parser Sentence
sBracket = bracket (symbol "(") sentence (symbol ")")

sPred :: Parser Sentence
sPred = do p <- predicate
	   ts <- bracket (symbol "(") terms (symbol ")") +++ (return [])
	   return (Predicate p ts)

sEqual :: Parser Sentence
sEqual = do t1 <- term
	    symbol "="
	    t2 <- term
	    return (Equal t1 t2)

sConn :: Parser Sentence
sConn = let
	  s1 = sAtomic +++ sNot
	  s2 = sAnd +++ s1
	  s3 = sOr +++ s2
	  s4 = sImply +++ s3
	  sAnd = s1 `chainl1` cAnd
	  sOr = s2 `chainl1` cOr
	  sImply = s3 `chainl1` cImply
	  sEquiv = s4 `chainl1` cEquiv
	in
	  sEquiv +++ sImply +++ sOr +++ sAnd

cImply :: Parser (Sentence -> Sentence -> Sentence)
cImply = do symbol "=>"
	    return (\s1 -> \s2 -> Connective s1 Imply s2)

cEquiv :: Parser (Sentence -> Sentence -> Sentence)
cEquiv = do symbol "<=>"
	    return (\s1 -> \s2 -> Connective s1 Equiv s2)

cAnd :: Parser (Sentence -> Sentence -> Sentence)
cAnd = do symbol "AND" +++ symbol "And" +++ symbol "and"
	  return (\s1 -> \s2 -> Connective s1 And s2)

cOr :: Parser (Sentence -> Sentence -> Sentence)
cOr = do symbol "OR" +++ symbol "Or" +++ symbol "or"
	 return (\s1 -> \s2 -> Connective s1 Or s2)

sQuant :: Parser Sentence
sQuant = do q <- quantifier
	    vs <- variables
	    s <- sentence
	    return (Quantifier q vs s)

sNot :: Parser Sentence
sNot = do symbol "NOT" +++ symbol "Not" +++ symbol "not"
	  s <- sAtomic
	  return (Not s)

-- Term parsers

term :: Parser Term
term = tFunc +++ tConst +++ tVar

terms :: Parser [Term]
terms = (token term) `sepby1` char ','

tFunc :: Parser Term
tFunc = do f <- function
	   ts <- bracket (symbol "(") terms (symbol ")")
	   return (Function f ts)

tConst :: Parser Term
tConst = do c <- constant
	    return (Constant c)

tVar :: Parser Term
tVar = do v <- variable
	  return (Variable v)

-- Connective parser

connective :: Parser Connective
connective = do s <- symbol "=>" +++ symbol "<=>" +++
		     symbol "AND" +++ symbol "And" +++ symbol "and" +++
		     symbol "OR" +++ symbol "Or" +++ symbol "or"
		case s of
		  "=>"  -> return Imply
		  "<=>" -> return Equiv
		  "AND" -> return And
		  "And" -> return And
		  "and" -> return And
		  "OR"  -> return Or
		  "Or"  -> return Or
		  "or"  -> return Or
		  _     -> mzero

-- Quatifier parser

quantifier :: Parser Quantifier
quantifier = do s <- symbol "FORALL" +++ symbol "ForAll" +++ symbol "forall" +++
		     symbol "EXISTS" +++ symbol "Exists" +++ symbol "exists"
		case s of
		  "FORALL" -> return ForAll
		  "ForAll" -> return ForAll
		  "forall" -> return ForAll
		  "EXISTS" -> return Exists
		  "Exists" -> return Exists
		  "exists" -> return Exists
		  _        -> mzero

-- Lexers

keywords :: [String]
keywords = [ "TRUE", "True", "true",
	     "FALSE", "False", "false",
	     "NOT", "Not", "not",
	     "AND", "And", "and",
	     "OR", "Or", "or",
	     "FORALL", "ForAll", "forall",
	     "EXISTS", "Exists", "exists" ]

variable :: Parser String
variable = identifier keywords

variables :: Parser [String]
variables = (token variable) `sepby1` char ','

constant, predicate, function :: Parser String
constant = capitalized
predicate = capitalized
function = capitalized

capitalized :: Parser String
capitalized = token (do x <- upper
		        xs <- many alphanum
		        (if not (elem (x:xs) keywords) then
		           return (x:xs)
		         else
                           mzero))

-}

{-
{- This is very ugly -}
loadKB :: String -> ProverT String
loadKB f = do unloadKB f
	      --fin <- readFile f
	      let fin = myReadFile f
	      (_, _, m) <- get
	      let idx = (case m of
			   [] -> 1
			   _  -> snd (last m) + 1)
	      (n, msg) <- loadKB' (lines fin) idx
	      let newmod = (if n > 0 then
			      [(f, idx)]
			    else
			      [])
              modify (\(kbS', c', m') -> (kbS', c', m' ++ newmod))
	      return (if n > 0 then
		        "Loaded " ++ show n ++ " entries from " ++ f ++
			":\n" ++ msg
		      else
		        "\nNo entries loaded from " ++ f)

loadKB' :: [String] -> Int -> ProverT (Int, String)
loadKB' [] _ = return (0, "")
loadKB' (x:xs) i =
    let
      sentence = parseFOL x
    in
      do (case sentence of
	  Just sentence' -> do tellKB sentence'
	                       (n', msg') <- loadKB' xs i
	                       return (1 + n', show sentence' ++ "\n" ++ msg')
	  Nothing -> do (n', msg') <- loadKB' xs i
			return (n', "parse error: " ++ x ++ "\n" ++ msg'))

unloadKB :: String -> ProverT String
unloadKB f =
    do (_, _, m) <- get
       (case lookup f m of 
	  Nothing -> return ("Module " ++ f ++ " is not loaded!")
	  Just idx -> do modify (\(kbS', c', m') ->
		                       (filter (\(inf, mi) -> mi /= idx) kbS',
	                                c',
	                                filter (\(mn, mi) -> mi /= idx) m'))
			 return ("Module " ++ f ++ " unloaded"))
-}

{-
helpMessage :: String
helpMessage =
    "|==================================================================|\n" ++
    "|                  H        E        L        P                    |\n" ++
    "|==================================================================|\n" ++
    "| Writing sentences in First-Order-Logic:                          |\n" ++
    "|   1) The keywords are: NOT, AND, OR, =>, <=>, =, ForAll, Exists  |\n" ++
    "|   2) Variables must begin with a lower case letter.              |\n" ++
    "|   3) Predicates, functions, constants, must begin with an upper  |\n" ++
    "|      case letter.                                                |\n" ++
    "|   4) Predicates and functions are followed by parentheses ().    |\n" ++
    "|__________________________________________________________________|\n" ++
    "|                                                                  |\n" ++
    "| The valid commands are:                                          |\n" ++
    "|   Tell <sentence>  - Inserts a sentence into the KB.             |\n" ++
    "|   Ask <sentence>   - Proves a sentence (True, False).            |\n" ++
    "|   Delete [index]   - Deletes an entry from the KB.               |\n" ++
    "|   Load <file>      - Loads a file as a module into the KB.       |\n" ++
    "|   Unload <file>    - Unloads a previously loaded module.         |\n" ++
    "|   Reset            - Resets the KB to empty.                     |\n" ++
    "|   Show             - Displays the contents of the KB             |\n" ++
    "|   Quit             - Quits this program.                         |\n" ++
    "|   Help             - Displays this message.                      |\n" ++
    "|==================================================================|\n"

-- Command parser

parseCmd :: String -> Cmd
parseCmd s = case (papply cmd s) of
	        [] -> ErrorCmd
	        xs -> case ((snd . head) xs) of
			     [] -> ((fst . head) xs)
			     _ -> ErrorCmd

cmd :: Parser Cmd
cmd = ctell +++ cask +++ cdelete +++ cload +++ cunload +++
      creset +++ cshow +++ cquit +++ chelp +++ cdebug

ctell :: Parser Cmd
ctell = do symbol "TELL" +++ symbol "Tell" +++ symbol "tell"
	   s <- everything
	   return (TellCmd s)

cask :: Parser Cmd
cask = do symbol "ASK" +++ symbol "Ask" +++ symbol "ask"
	  s <- everything
	  return (AskCmd s)

cdelete :: Parser Cmd
cdelete = do symbol "DELETE" +++ symbol "Delete" +++ symbol "delete"
	     i <- nat
	     return (DeleteCmd i)

cload :: Parser Cmd
cload = do symbol "LOAD" +++ symbol "Load" +++ symbol "load"
	   file <- fname
	   return (LoadCmd file)

cunload :: Parser Cmd
cunload = do symbol "UNLOAD" +++ symbol "Unload" +++ symbol "unload"
	     file <- fname
	     return (UnloadCmd file)

creset :: Parser Cmd
creset = do symbol "RESET" +++ symbol "Reset" +++ symbol "reset"
	    return (ResetCmd)

cshow :: Parser Cmd
cshow = do symbol "SHOW" +++ symbol "Show" +++ symbol "show"
	   return (ShowCmd)

cquit :: Parser Cmd
cquit = do symbol "QUIT"  +++ symbol "Quit" +++ symbol "quit"
	   return (QuitCmd)

chelp :: Parser Cmd
chelp = do symbol "HELP"  +++ symbol "Help" +++ symbol "help"
	   return (HelpCmd)

cdebug :: Parser Cmd
cdebug = do symbol "DEBUG"  +++ symbol "Debug" +++ symbol "debug"
	    s <- everything
	    return (DebugCmd s)

everything :: Parser String
everything = token (do s <- many item
		       return s)

fname :: Parser String
fname = token (do s <- many (sat isAlphaNum +++ char '.')
	          return s)
-}

{-
From Prover.hs:

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
-}

{---------------------}
{-- Pretty Printing --}
{---------------------}

{-
flattenListString :: String -> String
flattenListString s = filter (\c -> c /= '[' && c /= ']' && c /= '\"') s

instance (Show v, Show p, Show f) => Show (Sentence v p f) where
    show (Connective s1 c s2) = "(" ++ show s1 ++ show c ++ show s2 ++ ")"
    show (Quantifier q [] s) = show q ++ " " ++ show s
    show (Quantifier q vs s) = show q ++ " " ++ (flattenListString (show vs)) ++
			       " " ++ show s
    show (Not s) = "NOT " ++ "(" ++ show s ++ ")"
    show (Predicate p []) = show p
    show (Predicate p ts) = show p ++ "(" ++ (flattenListString (show ts)) ++ ")"
    show (Equal t1 t2) = show t1 ++ "=" ++ show t2

instance (Show v, Show f) => Show (Term v f) where
    show (Function f ts) = show f ++ "(" ++ (flattenListString (show ts)) ++ ")"
    show (Constant c) = show c
    show (Variable v) = show v
    show (SkolemFunction i ts) = "SKOLEM_FUNCTION_" ++ show i ++ "(" ++
				 (flattenListString (show ts)) ++ ")"
    show (SkolemConstant i) = "SKOLEM_CONSTANT_" ++ show i

instance Show Connective where
    show (Imply) = " => "
    show (Equiv) = " <=> "
    show (And)   = " AND "
    show (Or)    = " OR "

instance Show Quantifier where
    show (ForAll) = "ForAll"
    show (Exists) = "Exists"

{--------------------}
{-- Pretty Printing -}
{--------------------}

connectNormalSentence :: (Show v, Show p, Show f) => String -> [NormalSentence v p f] -> String
connectNormalSentence s [] = case s of
			       " AND " -> "True"
			       " OR "  -> "False"
                               _ -> error ("unknown connective: " ++ show s)
connectNormalSentence _s (x:[]) = show x
connectNormalSentence s (x:xs) = show x ++ s ++ connectNormalSentence s xs

instance (Show v, Show p, Show f) => Show (ConjunctiveNormalForm v p f) where
    show (CNF xs) = connectNormalSentence "\n" xs

instance (Show v, Show p, Show f) => Show (ImplicativeNormalForm v p f) where
    show (INF ls rs) = connectNormalSentence " AND " ls ++ " => " ++
		       connectNormalSentence " OR " rs

instance (Show v, Show p, Show f) => Show (NormalSentence v p f) where
    show (NFNot s) = "NOT " ++ "(" ++ show s ++ ")"
    show (NFPredicate p []) = show p
    show (NFPredicate p ts) = show p ++ "(" ++ (flattenListString (show ts)) ++ ")"
    show (NFEqual t1 t2) = show t1 ++ "=" ++ show t2

--reportSetOfSupport :: SetOfSupport v p f -> String
--reportSetOfSupport [] = ""
--reportSetOfSupport ((inf, _theta):xs) = show inf ++ ('\n':reportSetOfSupport xs)
-}