{- |
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
  { WhiteWord -> String
leading :: String -- ^ leading white space
  , WhiteWord -> String
word :: String }

data LitCommand = LitCommand
  { LitCommand -> WhiteWord
commandWW :: WhiteWord
  , LitCommand -> Maybe WhiteWord
argumentWW :: Maybe WhiteWord
  , LitCommand -> String
trailing :: String -- ^ trailing white space
  , LitCommand -> CmdlCmdDescription
command :: CmdlCmdDescription }

parseLine :: [CmdlCmdDescription] -> FilePath -> Int -> Parser LitCommand
parseLine :: [CmdlCmdDescription] -> String -> Int -> Parser LitCommand
parseLine cl :: [CmdlCmdDescription]
cl fp :: String
fp i :: Int
i = do
  SourcePos -> ParsecT String () Identity ()
forall (m :: * -> *) s u. Monad m => SourcePos -> ParsecT s u m ()
setPosition (SourcePos -> ParsecT String () Identity ())
-> SourcePos -> ParsecT String () Identity ()
forall a b. (a -> b) -> a -> b
$ SourcePos -> Int -> SourcePos
setSourceLine (String -> SourcePos
initialPos String
fp) Int
i
  String
s1 <- ParsecT String () Identity Char
-> ParsecT String () Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space
  (ParsecT String () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof ParsecT String () Identity ()
-> Parser LitCommand -> Parser LitCommand
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LitCommand -> Parser LitCommand
forall (m :: * -> *) a. Monad m => a -> m a
return LitCommand :: WhiteWord
-> Maybe WhiteWord -> String -> CmdlCmdDescription -> LitCommand
LitCommand
      { commandWW :: WhiteWord
commandWW = String -> String -> WhiteWord
WhiteWord "" ""
      , argumentWW :: Maybe WhiteWord
argumentWW = Maybe WhiteWord
forall a. Maybe a
Nothing
      , trailing :: String
trailing = String
s1
      , command :: CmdlCmdDescription
command = String -> CmdlCmdDescription
cmdlIgnoreFunc "" }) Parser LitCommand -> Parser LitCommand -> Parser LitCommand
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (cs :: String
cs, cm :: CmdlCmdDescription
cm) <- [ParsecT String () Identity (String, CmdlCmdDescription)]
-> ParsecT String () Identity (String, CmdlCmdDescription)
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice (((CmdlCmdDescription, [String])
 -> ParsecT String () Identity (String, CmdlCmdDescription))
-> [(CmdlCmdDescription, [String])]
-> [ParsecT String () Identity (String, CmdlCmdDescription)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (c :: CmdlCmdDescription
c, sl :: [String]
sl) -> do
      String
s <- ParsecT String () Identity String
-> ParsecT String () Identity String
forall tok st a. GenParser tok st a -> GenParser tok st a
try (ParsecT String () Identity String
 -> ParsecT String () Identity String)
-> ParsecT String () Identity String
-> ParsecT String () Identity String
forall a b. (a -> b) -> a -> b
$ [String] -> ParsecT String () Identity String
parseCommand [String]
sl
      (String, CmdlCmdDescription)
-> ParsecT String () Identity (String, CmdlCmdDescription)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
s, CmdlCmdDescription
c)) ([(CmdlCmdDescription, [String])]
 -> [ParsecT String () Identity (String, CmdlCmdDescription)])
-> [(CmdlCmdDescription, [String])]
-> [ParsecT String () Identity (String, CmdlCmdDescription)]
forall a b. (a -> b) -> a -> b
$ (CmdlCmdDescription
proveAll, ["prove-all"])
        (CmdlCmdDescription, [String])
-> [(CmdlCmdDescription, [String])]
-> [(CmdlCmdDescription, [String])]
forall a. a -> [a] -> [a]
: (CmdlCmdDescription -> (CmdlCmdDescription, [String]))
-> [CmdlCmdDescription] -> [(CmdlCmdDescription, [String])]
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: CmdlCmdDescription
c -> (CmdlCmdDescription
c, String -> [String]
words (String -> [String]) -> String -> [String]
forall a b. (a -> b) -> a -> b
$ Command -> String
cmdNameStr (Command -> String) -> Command -> String
forall a b. (a -> b) -> a -> b
$ CmdlCmdDescription -> Command
cmdDescription CmdlCmdDescription
c)) [CmdlCmdDescription]
cl)
      ParsecT String () Identity (String, CmdlCmdDescription)
-> ParsecT String () Identity (String, CmdlCmdDescription)
-> ParsecT String () Identity (String, CmdlCmdDescription)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
        Char
h <- Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '#'
        String
r <- ParsecT String () Identity Char
-> ParsecT String () Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar
        (String, CmdlCmdDescription)
-> ParsecT String () Identity (String, CmdlCmdDescription)
forall (m :: * -> *) a. Monad m => a -> m a
return (Char
h Char -> String -> String
forall a. a -> [a] -> [a]
: String
r, String -> CmdlCmdDescription
cmdlIgnoreFunc String
r)
    String
s2 <- ParsecT String () Identity Char
-> ParsecT String () Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space
    (ParsecT String () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof ParsecT String () Identity ()
-> Parser LitCommand -> Parser LitCommand
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> LitCommand -> Parser LitCommand
forall (m :: * -> *) a. Monad m => a -> m a
return LitCommand :: WhiteWord
-> Maybe WhiteWord -> String -> CmdlCmdDescription -> LitCommand
LitCommand
        { commandWW :: WhiteWord
commandWW = String -> String -> WhiteWord
WhiteWord String
s1 String
cs
        , argumentWW :: Maybe WhiteWord
argumentWW = Maybe WhiteWord
forall a. Maybe a
Nothing
        , trailing :: String
trailing = String
s2
        , command :: CmdlCmdDescription
command = CmdlCmdDescription
cm }) Parser LitCommand -> Parser LitCommand -> Parser LitCommand
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
      (arg :: String
arg, s3 :: String
s3) <- Parser (String, String)
parseArgument
      LitCommand -> Parser LitCommand
forall (m :: * -> *) a. Monad m => a -> m a
return LitCommand :: WhiteWord
-> Maybe WhiteWord -> String -> CmdlCmdDescription -> LitCommand
LitCommand
        { commandWW :: WhiteWord
commandWW = String -> String -> WhiteWord
WhiteWord String
s1 String
cs
        , argumentWW :: Maybe WhiteWord
argumentWW = WhiteWord -> Maybe WhiteWord
forall a. a -> Maybe a
Just (WhiteWord -> Maybe WhiteWord) -> WhiteWord -> Maybe WhiteWord
forall a b. (a -> b) -> a -> b
$ String -> String -> WhiteWord
WhiteWord String
s2 String
arg
        , trailing :: String
trailing = String
s3
        , command :: CmdlCmdDescription
command = CmdlCmdDescription
cm
            { cmdDescription :: Command
cmdDescription = String -> Command -> Command
setInputStr String
arg (Command -> Command) -> Command -> Command
forall a b. (a -> b) -> a -> b
$ CmdlCmdDescription -> Command
cmdDescription CmdlCmdDescription
cm } }

parseArgument :: Parser (String, String)
parseArgument :: Parser (String, String)
parseArgument = do
  String
arg <- ParsecT String () Identity Char
-> ParsecT String () Identity String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ((Char -> Bool) -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
(Char -> Bool) -> ParsecT s u m Char
satisfy ((Char -> Bool) -> ParsecT String () Identity Char)
-> (Char -> Bool) -> ParsecT String () Identity Char
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> (Char -> Bool) -> Char -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> Bool
isSpace)
  String
sp <- ParsecT String () Identity Char
-> ParsecT String () Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space
  (ParsecT String () Identity ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof ParsecT String () Identity ()
-> Parser (String, String) -> Parser (String, String)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (String, String) -> Parser (String, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
arg, String
sp)) Parser (String, String)
-> Parser (String, String) -> Parser (String, String)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> do
    (rargs :: String
rargs, s :: String
s) <- Parser (String, String)
parseArgument
    (String, String) -> Parser (String, String)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
arg String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
sp String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
rargs, String
s)

parseCommand :: [String] -> Parser String
parseCommand :: [String] -> ParsecT String () Identity String
parseCommand cmd :: [String]
cmd = case [String]
cmd of
   [] -> String -> ParsecT String () Identity String
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ""
   [c :: String
c] -> String -> ParsecT String () Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
c
   c :: String
c : r :: [String]
r -> do
     String -> ParsecT String () Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string String
c
     String
s <- ParsecT String () Identity Char
-> ParsecT String () Identity String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space
     String
t <- [String] -> ParsecT String () Identity String
parseCommand [String]
r
     String -> ParsecT String () Identity String
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> ParsecT String () Identity String)
-> String -> ParsecT String () Identity String
forall a b. (a -> b) -> a -> b
$ String
c String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
t

parseSingleLine :: FilePath -> Int -> String -> Either String LitCommand
parseSingleLine :: String -> Int -> String -> Either String LitCommand
parseSingleLine fp :: String
fp i :: Int
i str :: String
str =
  case Parser LitCommand
-> String -> String -> Either ParseError LitCommand
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse ([CmdlCmdDescription] -> String -> Int -> Parser LitCommand
parseLine [CmdlCmdDescription]
getCommands String
fp Int
i) String
fp String
str of
    Left e :: ParseError
e -> String -> Either String LitCommand
forall a b. a -> Either a b
Left (String -> Either String LitCommand)
-> String -> Either String LitCommand
forall a b. (a -> b) -> a -> b
$ ParseError -> String
forall a. Show a => a -> String
show ParseError
e
    Right r :: LitCommand
r -> LitCommand -> Either String LitCommand
forall a b. b -> Either a b
Right LitCommand
r