content: {- |
  Module      :  ./PGIP/ParseProofScript.hs
  Description :  parse a heterogeneous proof script and return it as pgip-xml
  Copyright   :  (c) Christian Maeder, DFKI GmbH 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  -}
  
  module Main where
  
  import Interfaces.Command
  
  import CMDL.ParseProofScript
  import CMDL.DataTypes
  
  import PGIP.XMLstate
  
  import Common.Utils
  
  import Text.XML.Light as XML
  
  import Data.Either
  import Data.List
  
  import System.Environment
  
  parseContent :: FilePath -> String -> Either String [LitCommand]
  parseContent fp str = let
    l = number $ lines str
    (es, rs) = partitionEithers $ map
      (\ (s, i) -> parseSingleLine fp i s) l
    in if null es then Right rs else
       Left $ unlines es
  
  whiteSpaceElems :: String -> [Element]
  whiteSpaceElems str = if null str then [] else [unode "whitespace" str]
  
  litString :: LitCommand -> String
  litString c = word (commandWW c)
    ++ maybe "" (\ a -> leading a ++ word a) (argumentWW c)
  
  closeTheory :: Bool -> [Element]
  closeTheory isOpen = [unode "closetheory" () | isOpen]
  
  xmlLitCmds :: String -> Bool -> [LitCommand] -> [Element]
  xmlLitCmds trailer isOpen ls = case ls of
    [] -> closeTheory isOpen ++ whiteSpaceElems trailer
    h : r ->
      let wsp = trailer ++ leading (commandWW h)
          wspes = whiteSpaceElems wsp
      in case cmdDescription $ command h of
      SelectCmd LibFile _ ->
        wspes ++ closeTheory isOpen ++
        [unode "opentheory" $ litString h]
        ++ xmlLitCmds (trailing h ++ "\n") True r
      GroupCmd _ -> xmlLitCmds (wsp ++ "\n") isOpen r
      CommentCmd _ -> xmlLitCmds (wsp ++ litString h ++ "\n") isOpen r
      _ -> wspes ++ [unode "proofstep" $ litString h]
           ++ xmlLitCmds (trailing h ++ "\n") isOpen r
  
  parseHPF :: Bool -> FilePath -> IO ()
  parseHPF normal fp = do
    str <- readFile fp
    putStrLn $ case parseContent fp str of
      Left err -> showElement $ genErrorResponse True err
      Right rs -> (if normal then showElement . genNormalResponse "" else
                       intercalate "\n" . map (showElement . unode "pgip"))
        $ xmlLitCmds "" False rs
  
  -- with an argument "-" the output can be standard input for hets -I -x
  main :: IO ()
  main = do
    args <- getArgs
    let (opts, files) = partition (isPrefixOf "-") args
    mapM_ (parseHPF $ null opts) files
  