content: {- |
  Module      :  ./CMDL/ParseProofScript.hs
  Description :  parse a heterogeneous proof script
  Copyright   :  (c) Christian Maeder, DFKI GmbH 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  -}
  
  
  module CMDL.ParseProofScript where
  
  import Interfaces.Command
  
  import CMDL.DataTypes
  import CMDL.Commands
  
  import Text.ParserCombinators.Parsec
  import Text.ParserCombinators.Parsec.Pos (initialPos)
  
  import Data.Char
  
  import qualified Control.Monad.Fail as Fail
  
  data WhiteWord = WhiteWord
    { leading :: String -- ^ leading white space
    , word :: String }
  
  data LitCommand = LitCommand
    { commandWW :: WhiteWord
    , argumentWW :: Maybe WhiteWord
    , trailing :: String -- ^ trailing white space
    , command :: CmdlCmdDescription }
  
  parseLine :: [CmdlCmdDescription] -> FilePath -> Int -> Parser LitCommand
  parseLine cl fp i = do
    setPosition $ setSourceLine (initialPos fp) i
    s1 <- many space
    (eof >> return LitCommand
        { commandWW = WhiteWord "" ""
        , argumentWW = Nothing
        , trailing = s1
        , command = cmdlIgnoreFunc "" }) <|> do
      (cs, cm) <- choice (map (\ (c, sl) -> do
        s <- try $ parseCommand sl
        return (s, c)) $ (proveAll, ["prove-all"])
          : map (\ c -> (c, words $ cmdNameStr $ cmdDescription c)) cl)
        <|> do
          h <- char '#'
          r <- many anyChar
          return (h : r, cmdlIgnoreFunc r)
      s2 <- many space
      (eof >> return LitCommand
          { commandWW = WhiteWord s1 cs
          , argumentWW = Nothing
          , trailing = s2
          , command = cm }) <|> do
        (arg, s3) <- parseArgument
        return LitCommand
          { commandWW = WhiteWord s1 cs
          , argumentWW = Just $ WhiteWord s2 arg
          , trailing = s3
          , command = cm
              { cmdDescription = setInputStr arg $ cmdDescription cm } }
  
  parseArgument :: Parser (String, String)
  parseArgument = do
    arg <- many1 (satisfy $ not . isSpace)
    sp <- many space
    (eof >> return (arg, sp)) <|> do
      (rargs, s) <- parseArgument
      return (arg ++ sp ++ rargs, s)
  
  parseCommand :: [String] -> Parser String
  parseCommand cmd = case cmd of
     [] -> Fail.fail ""
     [c] -> string c
     c : r -> do
       string c
       s <- many1 space
       t <- parseCommand r
       return $ c ++ s ++ t
  
  parseSingleLine :: FilePath -> Int -> String -> Either String LitCommand
  parseSingleLine fp i str =
    case parse (parseLine getCommands fp i) fp str of
      Left e -> Left $ show e
      Right r -> Right r
  