content: module LaTeX where
  -- pretty-printer generated by the BNF converter + tweaked
  import qualified System.IO           as Sys ( stdin, hGetContents )
  import qualified System.Environment  as Sys ( getArgs, getProgName )
  import qualified System.Exit         as Sys ( exitFailure, exitSuccess )
  
  import qualified Eprover.Par   as P
  import qualified Eprover.Print as P
  import qualified Eprover.Lex   as L
  import qualified Eprover.ErrM  as E
  import Eprover.Abs
  import Data.Char
  
  -- the top-level printing method
  printTree :: Print a => a -> String
  printTree = render . prt 0
  
  type Doc = [ShowS] -> [ShowS]
  
  doc :: ShowS -> Doc
  doc = (:)
  
  render :: Doc -> String
  render d = rend 0 (map ($ "") $ d []) "" where
    rend i ss = case ss of
      "["      :ts -> showChar '[' . rend i ts
      "("      :ts -> showChar '(' . rend i ts
      "{"      :ts -> showChar '{' . new (i+1) . rend (i+1) ts
      "}" : ";":ts -> new (i-1) . space "}" . showChar ';' . new (i-1) . rend (i-1) ts
      "}"      :ts -> new (i-1) . showChar '}' . new (i-1) . rend (i-1) ts
      ";"      :ts -> showChar ';' . new i . rend i ts
      t  : "," :ts -> showString t . space "," . rend i ts
      t  : ")" :ts -> showString t . showChar ')' . rend i ts
      t  : "]" :ts -> showString t . showChar ']' . rend i ts
      t        :ts -> space t . rend i ts
      _            -> id
    new i   = id             -- spacing handled by LaTeX
    space t = showString t   -- spacing handled by LaTeX
  --  new i   = showChar '\n' . replicateS (2*i) (showChar ' ') . dropWhile isSpace
  --  space t = showString t . (\s -> if null s then "" else (' ':s))
  
  parenth :: Doc -> Doc
  parenth ss = doc (showChar '(') . ss . doc (showChar ')')
  
  concatS :: [ShowS] -> ShowS
  concatS = foldr (.) id
  
  concatD :: [Doc] -> Doc
  concatD = foldr (.) id
  
  replicateS :: Int -> ShowS -> ShowS
  replicateS n f = concatS (replicate n f)
  
  -- the printer class does the job
  class Print a where
    prt :: Int -> a -> Doc
    prtList :: Int -> [a] -> Doc
    prtList i = concatD . map (prt i)
  
  instance Print a => Print [a] where
    prt = prtList
  
  instance Print Char where
    prt _ s = doc (showChar '\'' . mkEsc '\'' s . showChar '\'')
    prtList _ s = doc (showChar '"' . concatS (map (mkEsc '"') s) . showChar '"')
  
  mkEsc :: Char -> Char -> ShowS
  mkEsc q s = case s of
    _ | s == q -> showChar '\\' . showChar s
    '\\'-> showString "\\\\"
    '\n' -> showString "\\n"
    '\t' -> showString "\\t"
    _ -> showChar s
  
  prPrec :: Int -> Int -> Doc -> Doc
  prPrec i j = if j<i then parenth else id
  
  
  instance Print Integer where
    prt _ x = doc (shows x)
  
  
  instance Print Double where
    prt _ x = doc (shows x)
  
  instance Print LitString where
    prt _ (LitString i) = doc (showString i)
  
  
  instance Print UIdent where
    prt _ (UIdent i) = docS ("\\Tvar{"++i++"}")
  
  instance Print LIdent where
    prt _ (LIdent i) = doc (showString i)
  
  
  instance Print Wild where
    prt _ (Wild i) = doc (showString ('\\':i))
  
  instance Print Database where
    prt i e = case e of
      Db clauses -> prPrec i 0 (concatD [beginSemantics, prt 0 clauses, endSemantics])
  
  docS :: String -> Doc
  docS = doc . showString
  
  beginSemantics, endSemantics :: Doc
  beginSemantics = docS "" -- "\\[\n\\begin{array}{r@{}c@{}llllll}\n"
  endSemantics   = docS "" -- "\\end{array}\n\\]"
  
  beginFact, endFact :: Doc
  beginFact = docS "\\Pfact{"
  endFact   = docS "}"
  
  beginRule, midRule, endRule :: Doc
  beginRule = docS "\\Prule{"
  midRule   = docS "}{"
  endRule   = docS "}"
  
  beginGroup a = concatD [docS "\\newcommand{\\", docS a, docS "}{%"]
  endGroup   a = docS "}"
  
  instance Print Clause where
    prt i e = case e of
      Fact (TPred (Complex (Atm (LIdent "begingroup")) [VarT (V (UIdent a))])) -> prPrec i 0 (beginGroup a)
      Fact (TPred (Complex (Atm (LIdent "endgroup"))   [VarT (V (UIdent a))])) -> prPrec i 0 (endGroup a)
      Fact predicate -> prPrec i 0 (concatD [beginFact, prt 0 predicate, endFact])
      Rule predicate predicates ->
        prPrec i 0 (concatD [beginRule,
                             prt 0 predicate,
                             midRule,
                             prt 0 predicates,
                             endRule])
      Directive predicates -> prPrec i 0 (concatD [doc (showString ":-"), prt 0 predicates])
    prtList _ [] = (concatD [])
    prtList _ (x:xs) = (concatD [prt 0 x, doc (showString "\n"), prt 0 xs])
    -- TODO: perhaps generate a macro for the "cons" in the list of clauses
  
  instance Print Predicate where
    prt i e = case e of
      NPred term -> prPrec i 0 (concatD [doc (showString "\\Pnegate{"), prt 0 term, doc (showString "}")])
      TPred term -> prPrec i 0 (concatD [prt 0 term])
    prtList _ [x] = (concatD [prt 0 x])
    prtList _ (x:xs) = (concatD [prt 0 x, doc (showString "\\Pcomma"), prt 0 xs])
  
  instance Print Term where
    prt i e = case e of
      Complex atom terms ->
        prPrec i 0 (concatD [ docS "\\T"
                            , prt 0 atom
                            , docS "{"
                            , prt 0 terms
                            , docS "}"
                            ])
      TAtom   atom  -> prPrec i 0 (concatD [docS "\\T", prt 0 atom])
      VarT    var   -> prPrec i 0 (concatD [prt 0 var])
      TInt    n     -> prPrec i 0 (concatD [prt 0 n])
      TParen  term  -> prPrec i 0 (concatD [doc (showString "("), prt 0 term, doc (showString ")")])
    prtList _ [x]     = concatD [prt 0 x]
    prtList _ (x:xs)  = concatD [prt 0 x, doc (showString "}{"), prt 0 xs]
  instance Print Atom where
    prt i e = case e of
      Atm (LIdent s) | elem '_' s -> prPrec i 0 (concatD [prt 0 (LIdent (filter ('_'/=) s))])
                     | otherwise  -> prPrec i 0 (concatD [prt 0 (LIdent s)])
  
  instance Print Var where
    prt i e = case e of
      V uident  -> prPrec i 0 (concatD [prt 0 uident])
      A wild    -> prPrec i 0 (concatD [prt 0 wild])
  
  ----------------------------------------------------------------
  type ParseFun a = [L.Token] -> E.Err a
  type Verbosity = Int
  
  run :: (Print a, Show a) => Verbosity -> ParseFun a -> String -> IO ()
  run v p s = let ts = P.myLexer s in case p ts of
             E.Bad s    -> do putStrLn "\nParse              Failed...\n"
                              putStrLnV v "Tokens:"
                              putStrLnV v $ show ts
                              putStrLn s
                              Sys.exitFailure
             E.Ok  tree -> do putStrLnV v "\nParse Successful!"
                              putStrLn (printTree tree)
                              Sys.exitSuccess
  
  putStrLnV :: Verbosity -> String -> IO ()
  putStrLnV v s = if v > 1 then putStrLn s else return ()
  
  runFile :: (Print a, Show a) => Verbosity -> ParseFun a -> FilePath -> IO ()
  runFile v p f = putStrLnV v f >>
                  readFile f >>= run v p
  
  usage :: IO ()
  usage = do
    putStrLn $ unlines
      [ "usage: Call with one of the following argument combinations:"
      , "  --help          Display this help message."
      , "  (no arguments)  Parse stdin verbosely."
      , "  (files)         Parse content of files verbosely."
      , "  -s (files)      Silent mode (default). Parse content of files silently."
      , "  -v (files)      Verbose mode."
      ]
    Sys.exitFailure
  
  main :: IO ()
  main = do
    args <- Sys.getArgs
    case args of
      ["--help"]  -> usage
      []          -> Sys.hGetContents Sys.stdin >>= run 2 P.pDatabase
      "-s":fs     -> mapM_ (runFile 0 P.pDatabase) fs
      "-v":fs     -> mapM_ (runFile 2 P.pDatabase) fs
      fs          -> mapM_ (runFile 0 P.pDatabase) fs
  
  -- main = putStrLn (printTree sem)
  